The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 01 Aug 2011 20:16:39 -0700,
S3 
<scubed2 AT gmail.com>
 a écrit :

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

Ok, lot of people already replied to you.
I would like to just add some other piece of advice (which won't solve
your ploblem, as opposed to the other replies, but may be useful none
the less).

In inductive definitions, you have two kind of parameters; as I don't
know their names, I will call them "dependents" and "non dependents";
then dependents are right of the colon; the non dependents are left.

For example this is the definition of equality:

Inductive eq {A: Type} (a: A): forall (b: A), Prop :=
| eq_refl: eq a a.

What I call "non dependent" is 'A' and 'a'
 (so my terminology, is not that good, since 'a' depends on 'A')
and 'b' is "dependent"
 (of course I should have written 'A->Prop'
  instead of 'forall (b: A), Prop', but that way I have a name)

So if you have an inductive type, you always can write it with
"dependent" parameters only, but not with "non-dependent" parameters
only.

For instance, that would lead to:

Inductive eq: forall {A: Type} (a: A) (b: A), Prop :=
| eq_refl: forall A a, eq a a.

But the good practice, is to put the most parameters as "non-dependent"
as you can.

Same thing applies to your inductive:

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

Your second parameter is unchanged between calls, so it should be
"non-dependent", thus leading to the conventionnal naming (but it is
some coincidence, not the reason why we use this order)

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

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

I will try to make an exemple for that.