The Coq mailing list

[S3 <scubed2 AT gmail.com>]

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

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

Thanks.  That's neat.  I didn't realize you can use
left and right on things other than \/.  That makes
for a very short proof.

Yes, the proof that divides m 0 -> m = 0 is very simple
when you specifically exclude dividing by 0
from divides_n.

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

Theorem divides_eq_0 n: divides 0 n -> n = 0.
  intros.
  induction H.
    tauto.

  rewrite IHdivides.
  tauto.
Qed.

> the reason, is that if you want to do some induction/inversion, a new
> variable has to be introduced, and you must have a way to link it to
> its previous value (which in this case would be itself!).

Putting m above makes that proof very simple.
I guess this is more akin to when you have
a type constructor, like vector<int> that it's
important and relevant to know the <int> part.
So, in your example, you always know that you
are talking about the same denominator.

The critical difference is that it knows the later m
equals the original m, instead of just the previous m.
(Since otherwise, it could have moved sideways at some
point for all it knows, so it would only know 1 step.)

> Ok, it is not a good one, and I probably could have make it shorter,
> but it illustrates what I meant in my previous mail.

Thank you for the full example too.
I think I understand now.

To illustrate that it enforces the constraint:
Inductive constant3 (a: nat): list nat -> Prop :=
| Cnil3: constant3 a nil
| Ccons3: forall l, constant3 a l -> constant3 (S a) (a::l).

Error: Last occurrence of "constant3" must have "a" as 1st argument in
 "forall l : list nat, constant3 a l -> constant3 (S a) (a :: l)".

Thank you for all of the thoughtful replies!

- -- 
*********************.************************************..|
**..*.*...*..**....**....*....**....***.**...*..***.......*.|
*..**.**...**.***...*...*..*.**..****...*...*.*.....**..*...|
.*..*..*.*..*.....******...*.*..*.*.**...*.**.*..*..***..*..|
...*.*..*..***..*.*****...*...*....****.....***.*...**..**..|
..*.....**..***.*.........*.*...*..**..**game*.....*........|
*....*..**..*.*.*.*..*.**.*..*..*..**..**of**......**.***...|
*.**.*..**..*.*.**.**..**.**.****..***life.**.****..*.****..|
**********************************************************..|
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Gentoo - http://enigmail.mozdev.org/

iEYEARECAAYFAk445PoACgkQxzVgPqtIcfuLnQCeKiGK8z9LsaLrCVBxe0eg8CDM
MjEAn3saucgPwnEZUziapozjz2JeVZVl
=4ftV
-----END PGP SIGNATURE-----