The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Something very simple:

Fixpoint my_plus (x y : nat) : nat :=
  match x with
  | O => y
  | S x => my_plus x (S y)
  end.

Now, if you want to prove "∀ x, my_plus x O = x", when performing induction on x, you will be in the following situation:

"IHx : my_plus x O = x ⊢ my_plus x (S O) = S x", and you will get stuck.

Thus you will need for instance to first "intros x; change (my_plus x O = O + x).". Then you "generalize O.", and you can "induction x.".
There, your situation will be more general, and you can prove it:
"IHx : ∀ y, my_plus x y = y+x ⊢ my_plus x (S y) = y+S x", which can then be turned into "S y+x = y+S x" by rewriting IHx.

I really did not mean more.

2014-06-11 7:42 GMT+02:00 Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>:

Hi Cedric,

> When you perform some induction, you sometimes need to generalize your goal.

This is interesting. Could you state a simple (if possible, "simplest") example goal where this happens?

Thanks!
Best regards,

Bruno

--
.../Sedrikov\...