# Case of two ‘fix’es

**URL:** <https://discourse.rocq-prover.org/t/case-of-two-fix-es/436>\
**Category:** Using Rocq\
**Created:** [September 19, 2019, 5:01pm UTC](https://discourse.rocq-prover.org/t/case-of-two-fix-es/436 "2019-09-19T17:01:37Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![lelf](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lelf/32/179_2.png) [@lelf](https://discourse.rocq-prover.org/u/lelf)\
**Post date:** [September 19, 2019, 5:01pm UTC](https://discourse.rocq-prover.org/t/case-of-two-fix-es/436/1 "2019-09-19T17:01:37Z")

</div>

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

```coq
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.

```

---

<div class="post-metadata">

**Author:** ![Yannick](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yannick/32/321_2.png) [@Yannick](https://discourse.rocq-prover.org/u/Yannick)\
**Post date:** [September 19, 2019, 5:23pm UTC](https://discourse.rocq-prover.org/t/case-of-two-fix-es/436/2 "2019-09-19T17:23:10Z")

</div>

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:

```auto
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