The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

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