Case of two ‘fix’es

Using Coq
1

What is the principal difference between the two goals that make the second harder? (And what is the preferred way to solve it?)

Goal forall q,
      (fix go a := match a with S a' => go a' | _ => 0     end)
        q
 =
 fst ((fix go a := match a with S a' => go a' | _ => (0,0) end)
        q).
Proof.
  now induction 0.
Qed.

Goal forall q,
       (fix go a r := match a with S a' => go a' (S r) | _ => 0 end)
       q 0
 =
  fst ((fix go a r := match a with S a' => go a' (S r) | _ => (0,0) end)
       q 0).
Proof.
  induction 0.
  - easy.
  - give_up.
Abort.
1 Like
2

Hello,

In the second case, you need to generalize your lemma for the induction hypothesis to be strong enough.
If you look at your goal in the inductive case, naming your fix F, you can see that your goal talks about F q 1, while your induction hypothesis is your lemma instantiated at q, i.e. talks about F q 0.

The approach is hence to generalize the lemma so that the equation is stated for any value of the second argument:

Goal forall q a,
       (fix go a r := match a with S a' => go a' (S r) | _ => 0 end)
       q a
 =
  fst ((fix go a r := match a with S a' => go a' (S r) | _ => (0,0) end)
       q a).

Hence your induction hypothesis is quantified over all a, allowing you to instantiate it in particular at S a.

Hope it helps,
Yannick

3 Likes