The Coq mailing list

[Kwanghoon Choi <kwanghoon.choi AT yonsei.ac.kr>]

Hi,

I am wondering what is a difference between

 1) induction n m

     and

 2) induction n

     induction m  ?

It is acceptable to me that some of the proof structure can be changed when I choose different options of the induction tactic, like 1) and 2). 

I thought that either way I could easily prove the same lemmas. But when I choose to use 2), I still don't know how I prove the lemmas that I have proved easily when I choose to use 1). 

One reason for the difference may come from the fact that I am a novice user for Coq. But, if there is any more interesting reason, could anybody explain the difference between 1) and 2)? 

Best regards,

Kwanghoon Choi

=====

Require Import Omega.

Inductive setZ : Set := zero : setZ | pos : nat -> setZ | neg : nat -> setZ.

Inductive Diff : nat -> nat -> setZ -> Prop :=

| Diff_eq : forall n:nat, Diff n n zero

| Diff_pos : forall n p:nat, Diff (S (p+n)) p (pos n)

| Diff_neg : forall n p:nat, Diff p (S (p+n)) (neg n).

Fixpoint diff n m :=

  match n, m with

  | O, O => zero

  | O, (S p) => neg p

  | (S p), O => pos p

  | (S p), (S q) => diff p q

  end.

Lemma Diff_k : forall n m k, forall z, Diff m n z -> Diff (k+m) (k+n) z.

Proof.

  intros.

  induction k.

  simpl.

  exact H.

  destruct z.

  inversion IHk.

  assert (S k + m = S k + n).

  omega.

  rewrite H1.

  apply Diff_eq.

  inversion IHk.

  simpl.

  rewrite <- H0.

  rewrite <- H1.

  rewrite <- H3.

  assert (S (p + n1) = S p + n1).

  omega.

  rewrite H2.

  apply Diff_pos.

  inversion IHk.

  assert (S k + n = S (S k + m + n0)).

  omega.

  rewrite H1.

  apply Diff_neg.

Qed.

Lemma diff_k : forall n m k, forall z, diff m n=z -> diff (k+m) (k+n)=z.

Proof.

  intros.

  induction k.

  simpl.

  exact H.

  simpl.

  exact IHk.

Qed.  

                                                       

Lemma Diff_equiv_diff:

  forall n m:nat, Diff n m (diff n m).

Proof.

  induction n,m.    (*  <====   See here. *)

  simpl.

  apply Diff_eq.

  simpl.

  assert (m=0+m).

  auto.

  rewrite H at 1.

  apply Diff_neg.

  simpl.

  assert (n=0+n).

  auto.

  rewrite H at 1.

  apply Diff_pos.

  assert (S n=1+n).

  omega.

  assert (S m=1+m).

  omega.

  rewrite H.

  rewrite H0.

  apply Diff_k.

  assert (diff (1+n) (1+m) = diff n m).

  apply diff_k.

  reflexivity.

  rewrite H1.

  apply IHn.

Qed.