The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

Hi Michael,

I guess induction with eqn would probably only make sense if it "reverted" after "remembering" like in Cedric's examples. But maybe that's not as common as "remembering" after induction like Georges is suggesting.

Require Import Setoid.

Axiom int_pos : Set. Notation "Z+" := int_pos.

Axiom int : Set. Notation "'Z'" := int.

Axiom add : Z+ -> Z+ -> Z+. Infix "+" := add.

Axiom subtr : Z+ -> Z+ -> Z. Infix "-" := subtr.

Axiom less : Z+ -> Z+ -> Prop. Infix "<" := less.

Axiom zer : Z. Notation "0" := zer.

Axiom neg : Z+ -> Z. Notation "- i1" := (neg i1).

Axiom pos : Z+ -> Z. Notation "+ i1" := (pos i1) (at level 35, right associativity).

Axiom A1 : forall i1 i2, 0 = i1 - i2 <-> i2 = i1.

Axiom A2 : forall i1 i2 i3, - i3 = i1 - i2 <-> i1 + i3 = i2.

Axiom A3 : forall i1 i2 i3, + i3 = i1 - i2 <-> i3 + i2 = i1.

Axiom A4 : forall i1 i2, i1 < i1 + i2.

Axiom A5 : forall i1 i2, i2 < i1 + i2.

Hint Rewrite A1 A2 A3 : Hints.

Hint Resolve A4 A5 : Hints.

Axiom pos_int_rect : forall p1,

  (forall i1, (forall i2, i2 < i1 -> p1 i2) -> p1 i1) ->

  forall i1, p1 i1.

Axiom int_rect : forall p1,

  p1 0 ->

  (forall i1, p1 (- i1)) ->

  (forall i1, p1 (+ i1)) ->

  forall i1, p1 i1.

Goal forall p1,

  (forall i1, p1 i1 i1) ->

  (forall i1 i2, p1 i1 i2 -> p1 i1 (i1 + i2)) ->

  (forall i1 i2, p1 i1 i2 -> p1 (i1 + i2) i2) ->

  forall i1 i2, p1 i1 i2.

Proof.

intros ? h1 h2 h3 ? ?.

remember (i1 + i2) as i3 eqn:h4.

revert i1 i2 h4.

induction i3 using pos_int_rect.

intros.

remember (subtr i1 i2) as i4.

induction i4 using int_rect.

autorewrite with Hints in *. subst. eauto with Hints.

autorewrite with Hints in *. subst. eauto with Hints.

autorewrite with Hints in *. subst. eauto with Hints.

Defined.

On Thu, Oct 24, 2013 at 2:56 PM, Cedric Auger <sedrikov AT gmail.com> wrote:

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\...