6/12/2010

Après présentation du sujet du projet…

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

Avec ça, prouvons que

Lemma toto : forall n:nat, le n 1 -> n=1 \/ n=0.
Proof.
intros.
(*
n:nat
H: le n 1
*)

On sait le n 1, donc, de deux choses l'une :

• soit n=1 (par règle le_n)
• ou alors on a utilisé ”“le_S avec m=0 et un certain n' tel que n'≤0. Pour déduire n'≤0 la seule règle qui a pu être utilisée est le_n'' donc n'=0. Pour employer ce raisonnement en Coq, on ferait

inversion H.
left.
reflexivity.
inversion H1.
right.
reflexivity.