The Coq mailing list

["Eric Jaeger" <eric.jaeger.paris AT noos.fr>]

Hi,

 

Just a simple question about the encoding of le. The standard definition is:

 

Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m.

 

An alternative definition would be:

 

Inductive le' :nat->nat -> Prop := le'_0 : forall n : nat, le' 0 n | le'_S : forall (m n : nat), le' n m -> le' (S n) (S m).

 

Putting aside the question of parameter n, the le' approach would have my preference for a question of efficiency. Indeed, considering a computation associated to these definitions, the algorithm would be:

- le n m: decrements m until it is equal to n

- le' n m: decrements m and n until n is equal to 0

Both may appear equivalent (considering all possible case for n and m), but how do we know that "m is equal to n" in the first case? This, again, requires decrementing both m and n until 0 is reached. So, in any case, the computation associated to the definition of le requires m iterations, while for le' it would be something like min(m,n).

 

Just by pure curiosity, is there anything wrong in this analysis?

 

    Best Regards, Eric