(************************************************* Note : ceci est une illustration de notions vues en cours. En Coq les entiers naturels, l'addition et la multiplications sont traitées sans axiomes et d'une maniere beaucoup plus efficace, ainsi que les inégalités <= et < De même, ce fichier utilise volontairement des tactiques "de base". Il peut sans nul doute être beaucoup plus concis. *******************************************************) Parameter Nat : Set. Parameter zero : Nat. Parameter S : Nat -> Nat. Parameter plus : Nat -> Nat -> Nat. Notation "n + p" := (plus n p). Definition Leq n p := exists q:Nat, n + q = p. (* Axiomes (sont des théorèmes dans la bibliotheque standard de Coq) *) Axiom zero_not_S : forall n:Nat, S n <> zero. Axiom S_injective : forall n p, S n = S p -> n = p. Axiom zero_plus_n : forall n:Nat, zero + n = n. Axiom S_plus_n : forall n p:Nat, S n + p = S (n + p). (* axiome de recurrence *) Axiom Nat_ind : forall (P:Nat->Prop), P zero -> (forall p:Nat, P p -> P (S p)) -> forall n:Nat, P n. Hint Resolve zero_not_S S_injective zero_plus_n S_plus_n. (* Une definition impredicative *) Definition Le n p := forall (P:Nat->Prop), P n -> (forall p:Nat, P p -> P (S p))-> P p. Notation "n <= p" := (Le n p). Definition Lt n p := S n <= p. Notation "n < p" := (Lt n p). (* Exemples et théorèmes *) Lemma Leq_zero_n : forall n:Nat, Leq zero n. Proof. intro n;exists n. rewrite zero_plus_n. trivial. Qed. Lemma zero_or_S : forall n:Nat, n=zero \/ exists p:Nat, n = S p. Proof. intro n; elim n using Nat_ind. (* Remarque : la ligne prcécédente peut être remplacée par induction n using Nat_ind. ou par : intro n;pattern n;apply Nat_ind. *) auto. intros p H;right;exists p;auto. Qed. Lemma n_plus_zero : forall n:Nat, n + zero =n. Proof. intro n; elim n using Nat_ind. auto. intros p Hp;rewrite S_plus_n. rewrite Hp;trivial. Qed. (* La commande suivante permet d'utiliser les égalités ci-dessous avec la commande "autorewrite with peano" Attention aux bouclages !!!!!!! *) Hint Rewrite n_plus_zero zero_plus_n S_plus_n: peano. Lemma n_plus_S : forall n p:Nat, n+ S p = S(n+p). Proof. intro n; elim n using Nat_ind. intro p. autorewrite with peano;trivial. intros p Hrec q. (* rewrite S_plus_n. rewrite Hrec. rewrite S_plus_n. *) autorewrite with peano. rewrite Hrec. trivial. Qed. Hint Rewrite n_plus_S :peano. (* Note, La preuve ci-dessous est beaucoup plus simple en utilisant les mécanismes de Coq pour la récurrence et la récursivite *) Hint Resolve n_plus_S n_plus_zero. Theorem plus_comm : forall n p:Nat, n+ p = p+ n. Proof. intro n; elim n using Nat_ind. intro; autorewrite with peano;trivial. intros p Hrec_p q. transitivity (S (p + q));auto. rewrite Hrec_p. auto. Qed. Lemma Le_refl : forall n, n <= n. Proof. unfold Le;auto. Qed. Lemma Le_S : forall n, n <= S n. Proof. unfold Le;auto. Qed. Lemma Le_trans : forall n p q: Nat, n<= p -> p <= q -> n <= q. Proof. intros n p q Hnp Hpq. unfold Le;intros P H H0. apply Hpq;trivial. apply Hnp;trivial. Qed. Lemma Le_zero_n : forall n:Nat, zero <= n. Proof. intro n; elim n using Nat_ind. apply Le_refl. intros p Hp. apply Le_trans with p. auto. apply Le_S. Qed. Lemma Le_inv : forall n p, n <=p -> n = p \/ exists q:Nat, p = S q /\ n <= q. Proof. intros n p H;pattern p;apply H. left;trivial. intros q Hq . case Hq. right. exists q;split;auto. subst q;apply Le_refl. intro H0;case H0;intros r Hr;elim Hr;intros H1 H2. right;exists q;split;auto. subst q. apply Le_trans with r;auto. apply Le_S. Qed. Lemma Le_cases : forall n p, n <= p -> n < p \/ n = p. Proof. intros n p H; pattern p. apply H. right;auto. intros q Hq. elim Hq;intro H0. left;unfold Lt. apply Le_trans with q. trivial. unfold Le;auto. left;rewrite H0;unfold Lt;apply Le_refl. Qed. Lemma Lt_Le : forall n p, n < p -> n <= p. Proof. intros n p H. apply Le_trans with (S n). apply Le_S. exact H. Qed. Lemma Le_S_S : forall n p, n <= p -> S n <= S p. Proof. intros n p H;elim (Le_cases _ _ H). unfold Lt. intro H0;apply Le_trans with p;auto. apply Le_S. intro e;subst p. apply Le_refl. Qed. Lemma Le_n_S_p : forall n p, n <= S p -> n = S p \/ n <= p. Proof. intros n p H; elim (Le_inv _ _ H). auto. intros (q, (H1,H2)). right. assert (p = q). apply S_injective. auto. subst q;auto. Qed. Lemma Le_S_SR : forall n p, S n <= S p -> n <= p. Proof. intros n p H;elim (Le_n_S_p _ _ H). intro;assert (n=p). apply S_injective. auto. subst n;apply Le_refl. intro;apply Le_trans with (S n);auto. apply Le_S. Qed. Lemma Le_n_zero : forall n, n <= zero -> n = zero. Proof. intros n Hn. elim (Le_inv _ _ Hn). trivial. intros H;elim H;intros q Hq;elim Hq;intros. elim (zero_not_S q). auto. Qed. Lemma not_lt_S_n_n : forall n, ~ (S n < n). Proof. intro n ; elim n using Nat_ind. intro H. elim (Le_inv _ _ H). intro. elim (zero_not_S (S zero));auto. intros (q,(H1,H2)). elim (zero_not_S q);auto. intros p H H'. elim H. unfold Lt. apply Le_S_SR. auto. Qed. Lemma Le_antisym : forall n p, n <= p -> p <= n -> n = p. Proof. intro n; elim n using Nat_ind. intros p Hp Hp'. symmetry;apply Le_n_zero. auto. intros. elim (Le_cases _ _ H0);elim (Le_cases _ _ H1);auto. unfold Lt;intros. elim (not_lt_S_n_n (S p)). unfold Lt. apply Le_S_S. apply Le_trans with p0;auto. apply Le_S_SR. trivial. Qed. (* Exercice : Prouver les deux lemmes suivants *) Lemma Le_plus : forall n p, n <= n + p. Proof. Admitted. Lemma Le_plus_inv : forall n p, n <= p -> exists q:Nat, n+q = p. Proof. Admitted. Theorem Le_Leq : forall n p, n <= p -> Leq n p. Proof. intros n p H; unfold Leq;apply Le_plus_inv. trivial. Qed. Theorem Leq_Le : forall n p, Leq n p -> n <= p. Proof. intros n p H. elim H;intros q Hq. rewrite <- Hq;apply Le_plus. Qed.