The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  In general, it's better to give non ambiguous inductive definitions.
In the attached file, I can build proofs of "divide 0 0" that use the
second constructor instead of the first one (lemma L1).

 With the definitions divide' and divides'' (this one much better than
the first one), I can prove your  simple lemma quite easily.
The last definition (divides'') makes the inversion tactic very easy to
apply.

Pierre



> Start with a simple definition for divides evenly:
> (Note: I know the arguments are usually written
> the other way around.  I arbitrarily decided to write
> it in normal division operator order.)
>
> Inductive divides: nat -> nat -> Prop :=
>   | divides_0 n: divides 0 n
>   | divides_n n m: divides n m -> divides (n + m) m
> .
>
> So, with this definition,
> divides 0 0.
> forall n, divides n 1.
> forall n m, divides (n*m) n.
> Those can all be easily and directly proven.
>
> But, how would I prove that:
> forall n, divides (S n) 0 -> False.
> Normally, I would just use inversion,
> but in this case, the predecessor is itself,
> forming a cycle.  What technique can you use
> when you form a cycle?
> Or should inductive definitions be
> given in such a way as to avoid cycles to begin with?
>
> - --
> *********************.************************************..|
> **..*.*...*..**....**....*....**....***.**...*..***.......*.|
> *..**.**...**.***...*...*..*.**..****...*...*.*.....**..*...|
> .*..*..*.*..*.....******...*.*..*.*.**...*.**.*..*..***..*..|
> ...*.*..*..***..*.*****...*...*....****.....***.*...**..**..|
> ..*.....**..***.*.........*.*...*..**..**game*.....*........|
> *....*..**..*.*.*.*..*.**.*..*..*..**..**of**......**.***...|
> *.**.*..**..*.*.**.**..**.**.****..***life.**.****..*.****..|
> **********************************************************..|
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v2.0.17 (GNU/Linux)
> Comment: Using GnuPG with Gentoo - http://enigmail.mozdev.org/
>
> iEYEARECAAYFAk43bBYACgkQxzVgPqtIcft3nQCfS2xHWVcodJ8v7unQ9gui1BzP
> Au8An0dxUJZ+M/Fuz7ihxK3Pcr9r7OYv
> =ZrqD
> -----END PGP SIGNATURE-----


Inductive divides: nat -> nat -> Prop :=
  | divides_0 n: divides 0 n
  | divides_n n m:  divides n m -> divides (n + m) m
.


Lemma L1: divides 0 0.
change (divides (0+0) 0).
right.
change (divides (0+0) 0).
right.
left.
Qed.

Lemma L0 : divides 0 0.
left.
Qed.


Inductive divides': nat -> nat -> Prop :=
  | divides_0' n: divides' 0 n
  | divides_n' n m:  0<m -> divides' n m -> divides' (n + m) m.



Lemma L2: forall m, divides' m 0 -> m =0.
induction m.
trivial.
inversion 1.
inversion H1.
Qed.


Inductive divides'': nat -> nat -> Prop :=
  | divides_0'' n: divides'' 0 n
  | divides_n'' n m:   divides'' n (S m) -> divides'' (S (n + m)) (S  m).



Lemma L3: forall m, divides'' m 0 -> m =0.

inversion 1.
trivial.
Qed.