The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Of course not, else, that would be pretty useless.

You simply have to think of the right generalization of what you want to prove.

Imagine you want to prove "∀ x y. x=y∨x≠y".

Start with "intros x y. induction y." (forget about the equation, it is of no interest)

Now, you have two goals:

"x=0∨x≠0"

and

"x=y∨x≠y ⇒ x=y+1∨x≠y+1"

First goal is almost trivial, but second goal is not that easy.
The case "x=y" is okay (you will have to prove x≠y+1), but "x≠y" it pretty useless to tell whether x=y+1 or x≠y+1.

Now, rollback, and start with "intros x y. revert x. induction y."

Now, you have two goals:

"∀ x. x=0∨x≠0"

and

"(∀ x₀. x₀=y∨x₀≠y) ⇒ ∀ x. x=y+1∨x≠y+1"

First case is still easy, but now second case seems a lot easier than before, since now you will be able to chose the 'x₀' in "∀ x₀. x₀=y∨x₀≠y".
So you can "destruct x as [|x′]." and the second created branch "x′+1=y+1∨x′+1≠y+1", use a proof of "x′=y∨x′≠y"

Your original problem seems related to it. With the right generalization before calling the induction tactic, you should not meet the contradiction you found.

2013/10/24 Soegtrop, Michael <michael.soegtrop AT intel.com>

Dear Rui,

 

but doesn’t this always lead to the situation that in the induction step cases, the pre-condition added to the induction hypothesis contradicts the case hypothesis (as below n=p contradicts n=S p)?

 

Best regards,

 

Michael

--
.../Sedrikov\...