(* Mini projet pour la premiere partie du cours de Logique: Regle du jeu : Le fichier qui suit contient un certain nombre d'Admitted. Il s'agit de remplacer ces Admitted par des preuves completes. Note : Certaines preuves sont plus faciles que d'autres ; un petit nombre requiert de la reflexion. *) (* Exercices sur la logique du second ordre *) Theorem triple_neg : forall P:Prop, ~ ~ ~ P -> ~ P. Proof. Admitted. Theorem ex_eq : forall (A:Set) (a b:A), (exists m:A, a = m /\ m=b) -> a = b. Proof. Admitted. Theorem thm_42 : forall (A:Set) (a:A), (forall b:A, ~ a=b) -> 1=42. Proof. intros A a H. (* A tout moment on peut introduire un lemme d'enonce E dans une preuve par la commande "assert E". Si le but courant est G, deux buts sont crees a) prouver E b) montrer que E sert a prouver G *) assert (a <> a). Admitted. (* Exercice sur le tiers exclu *) Section Klas1. Hypothesis tiers_exclu : forall P : Prop, P \/ ~ P. Lemma L1 : forall P Q R: Prop, ((P -> Q) -> R) -> ((Q -> P) -> R) -> R. Proof. intros P Q R H H0. destruct (tiers_exclu P). Admitted. Lemma L2 : forall P Q:Prop, (P -> Q) \/ (Q -> P). Proof. Admitted. End Klas1. Section Klas2. Hypothesis Hyp1 : forall P Q R: Prop, ((P -> Q) -> R) -> ((Q -> P) -> R) -> R. Lemma presque_le_tiers_exclu : forall P:Prop, ~P \/ ~~P. Proof. intros; apply Hyp1 with P (not P). Admitted. End Klas2. Section Klas3. Hypothesis Hyp2 : forall P Q: Prop, (P -> Q) \/ (Q -> P). Lemma encore_presque_le_tiers_exclu : forall P:Prop, ~P \/ ~~P. Proof. intros. destruct (Hyp2 P (not P)). Admitted. End Klas3. (* Etude d'une axiomatique de l'arithmetique *) (************************************************* 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 inegalites <= et < De meme, ce fichier utilise volontairement des tactiques "de base". Il peut sans nul doute etre beaucoup plus concis. *******************************************************) Parameter Nat : Set. Parameter zero : Nat. Parameter S : Nat -> Nat. Parameter plus : Nat -> Nat -> Nat. Parameter mult : Nat -> Nat -> Nat. Notation "n + p" := (plus n p). Notation "n * p" := (mult n p). (* Axiomes (sont des theoremes 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). Axiom zero_mult_n : forall n:Nat, zero * n = zero. Axiom S_mult_n : forall n p: Nat, (S n) * p = p + (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. Lemma fib_ind : forall (P:Nat->Prop), P zero -> P (S zero) -> (forall p : Nat, P p -> P (S (S p))) -> forall n : Nat, P n. Proof. intros P H0 H1 H n. assert (P n /\ P (S n)). induction n using Nat_ind. auto. destruct IHn;auto. destruct H2. auto. Qed. Lemma zero_or_S : forall n:Nat, n=zero \/ exists p:Nat, n = S p. Proof. intro n; induction n using Nat_ind. auto. right;exists n;auto. Qed. (* Le predicat "inferieur ou egal" est axiomatise, a la difference du cours et de la bibliiotheque standard de Coq (où il est defini) *) Parameter Le : Nat -> Nat -> Prop. Notation "n <= p" := (Le n p). Axiom Le_n : forall n:Nat, n<=n. Axiom Le_S : forall n p:Nat, n <= p -> n <= S p. (* Permet aux tactiques "auto" et "auto" d'utiliser ces axiomes *) Hint Resolve Le_n Le_S. (* Pour prouver que n <= q -> P q il suffit de prouver P n et que si n <= p et P p, alors P(S p) *) Axiom Le_ind : forall n:Nat, forall P:Nat -> Prop, P n -> (forall p : Nat, n <= p -> P p -> P (S p)) -> forall q:Nat, n<= q -> P q. (* Cette preuve utilise Le_ind *) Lemma Le_Sn_p : forall n p, S n <= p -> n <= p. Proof. intros n p H. induction H using Le_ind. auto. auto. Qed. (* on place Ce resultat dans la base de theoremes pour auto *) Hint Resolve Le_Sn_p. Theorem Le_trans : forall n p q:Nat, n <= p -> p <= q -> n <= q. Proof. intros n p q H;induction H using Le_ind;auto. Qed. Lemma Le_inv : forall n p : Nat, n <= p -> n= p \/ exists q:Nat, p = S q /\ n <= q. Proof. intros n p H;induction H using Le_ind. auto. destruct IHLe. right;exists p;auto. destruct H0. destruct H0. right;exists (S x). split. rewrite H0;trivial. auto. Qed. Lemma Le_n_zero : forall n:Nat, n<=zero -> n=zero. Proof. intros n H. (* 1 subgoal n : Nat H : n <= zero ============================ n = zero Ici, on veut appliquer Le_inv Cette fonction prend trois arguments : un entier n un entier p une preuve H : n<= p Si on veut faire une preuve par cas, il suffit d'utiliser destruct sur le terme (Le_inv n zero H) dont le type est n= zero \/ exists q:Nat, zero = S q /\ n <= q. *) destruct (Le_inv n zero H). auto. destruct H0. destruct H0. destruct (zero_not_S x). rewrite H0;auto. Qed. Lemma not_le_Sn_zero : forall n:Nat, ~ (S n <= zero). Proof. intros n H. generalize (Le_n_zero _ H). intro H0;destruct (zero_not_S _ H0). Qed. Lemma Le_n_Sn : forall n, n <= S n. Proof. Admitted. Lemma Le_zero_n : forall n:Nat, zero <= n. Proof. Admitted. Hint Resolve Le_zero_n. Definition Lt n p := S n <= p. Notation "n < p" := (Lt n p). (* A tout moment, on peut transformer un but contenant (a < b) par "unfold lt" (qui le remplace par ((S a) <= b) On peut faire ce remplacement dans une hypothese H avec "unfold lt in H" *) Lemma Lt_trans : forall n p q:Nat, n < p -> p < q -> n < q. Proof. unfold Lt;auto. intros. apply Le_trans with p;auto. Qed. Lemma Le_cases : forall n p, n <= p -> n < p \/ n = p. Proof. Admitted. Lemma Lt_Le : forall n p, n < p -> n <= p. Proof. Admitted. Lemma Le_S_S : forall n p, n <= p -> S n <= S p. Proof. Admitted. Lemma Le_n_S_p : forall n p, n <= S p -> n = S p \/ n <= p. Proof. Admitted. Lemma Le_S_SR : forall n p, S n <= S p -> n <= p. Proof. Admitted. Lemma not_le_Sn_n : forall n:Nat,~ S n <= n. Proof. Admitted. Lemma Lt_irreflexive : forall n, ~ n < n. Proof. Admitted. Lemma not_lt_S_n_n : forall n, ~ (S n < n). Proof. Admitted. Lemma Le_antisym : forall n p, n <= p -> p <= n -> n = p. Proof. Admitted. (* Proprietes de l'addition *) Lemma n_plus_zero : forall n:Nat, n + zero =n. Proof. intro n; induction n using Nat_ind. auto. rewrite S_plus_n. rewrite IHn;trivial. Qed. (* La commande suivante permet d'utiliser les egalites ci-dessous avec la commande "autorewrite with peano" Attention aux bouclages eventuels !!!!!!! *) 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; induction n using Nat_ind. intro p. autorewrite with peano;trivial. intros p. autorewrite with peano. rewrite IHn; trivial. Qed. Hint Rewrite n_plus_S :peano. Hint Resolve n_plus_S n_plus_zero. Theorem plus_comm : forall n p:Nat, n + p = p + n. Proof. intro n; induction n using Nat_ind. intro p; autorewrite with peano;trivial. intros q. transitivity (S (n + q));auto. rewrite IHn. auto. Qed. (* Induction complete *) Lemma complete_induction : forall P : Nat -> Prop, (forall n : Nat, (forall p:Nat, p < n -> P p) -> P n) -> forall n:Nat, P n. Proof. intros P H n. assert (forall p:Nat, p <= n -> P p). induction n using Nat_ind. intros p H0;apply H. intros q H1. assert (q < zero). unfold Lt; apply Le_trans with p;auto. (* P : Nat -> Prop H : forall n : Nat, (forall p : Nat, p < n -> P p) -> P n p : Nat H0 : p <= zero q : Nat H1 : q < p H2 : q < zero ============================ P q *) generalize (Le_n_zero (S q) H2). (* 3 subgoals P : Nat -> Prop H : forall n : Nat, (forall p : Nat, p < n -> P p) -> P n p : Nat H0 : p <= zero q : Nat H1 : q < p H2 : q < zero ============================ S q = zero -> P q *) intro H3. destruct (zero_not_S _ H3). intros;apply H. intros. assert (p0 < S n). unfold Lt;apply Le_trans with p;auto. apply IHn. apply Le_S_SR. eauto. apply H0. auto. Qed. Hint Rewrite zero_mult_n S_mult_n : peano. Theorem plus_assoc : forall n p q:Nat, (n+p)+q = n+(p+q). Proof. intro n. induction n using Nat_ind. intros;autorewrite with peano. trivial. intros. autorewrite with peano. rewrite IHn;auto. Qed. Hint Rewrite plus_assoc :peano. Lemma plus_zero : forall n p:Nat, n+p=zero -> n=zero /\ p=zero. Proof. intro n; induction n using Nat_ind. auto. intros. autorewrite with peano in H. split;auto. intros p H. autorewrite with peano in H. destruct (zero_not_S (n + p)). assumption. Qed. (* Proprietes de la multiplication *) Theorem mult_n_zero : forall n:Nat, n* zero = zero. Proof. intro n; induction n using Nat_ind ; intros; autorewrite with peano ; trivial. Qed. Hint Rewrite mult_n_zero : peano. Theorem mult_n_Sp : forall n p:Nat, n * (S p) = n + (n * p). Proof. intro n; induction n using Nat_ind. intros;autorewrite with peano. trivial. intros;autorewrite with peano. rewrite IHn. (* ici, autorewrite ne permet pas d'automatiser la fin de la preuve *) rewrite <- plus_assoc. rewrite <- plus_assoc. (* On veut utiliser la commutativite de l'addition pour remplacer p + n par n + p Pour specifier a rewrite ces arguments, on les donne comme arguments de plus_comm *) rewrite (plus_comm n p). trivial. Qed. Hint Rewrite mult_n_Sp:peano. Lemma mult_comm: forall n p:Nat, n*p = p*n. Proof. Admitted. Lemma one_mult_n : forall n, (S zero)*n = n. Proof. Admitted. (* A faire *) Lemma n_mult_one : forall n, n*(S zero) = n. Admitted. Lemma mult_zero : forall n p:Nat, n*p=zero -> n=zero \/ p=zero. Proof. Admitted. (* Relation entre <= et l'addition *) Lemma Le_plus : forall n p:Nat, Le n p -> exists q:Nat, p = n+q. Proof. Admitted. Theorem plus_le : forall n p, n <= n + p. Proof. Admitted. (* Predicats decidables *) Definition decidable (P:Nat -> Prop) := forall n, P n \/ ~ P n. Theorem zero_dec : decidable (fun n:Nat => n=zero). Proof. intro n. destruct (zero_or_S n). auto. destruct H. right;rewrite H. intro H0. destruct (zero_not_S x);auto. Qed. Theorem le_dec : forall n:Nat, decidable (fun p:Nat => n <= p). Proof. Admitted. Theorem decidable_negation : forall P:Nat->Prop, decidable P -> decidable (fun n : Nat => ~ (P n)). Proof. Admitted. Theorem decidable_or : forall P Q:Nat->Prop, decidable P -> decidable Q -> decidable (fun n : Nat => P n \/ Q n). Proof. Admitted. (* Si un predicat P est decidable, alors le predicat qui a n associe "il existe p <= n tel que P p" est aussi decidable *) Theorem bounded_ex_dec : forall P:Nat->Prop, decidable P -> decidable (fun n:Nat => exists p:Nat, p <= n /\ P p). Proof. Admitted. (* Si un predicat P est decidable, alors le predicat qui a n associe "pour tout p<= n, P p" est aussi decidable *) Theorem bounded_all_dec : forall P:Nat->Prop, decidable P -> decidable (fun n:Nat => forall p:Nat, p<= n -> P p). Admitted. (* A partir de cette limite les declarations et axiomes peuvent entrainer des incoherences *) (* Ensembles d'entiers *) Definition Nats := Nat -> Prop. Definition In (n:Nat)(X: Nats) := X n. Definition Empty: Nats := fun n:Nat => False. (* Borne inferieur d'une partie de N *) Parameter Inf : Nats -> Nat. (* Inf X est un minorant de X *) Axiom Inf_1: forall (X : Nats) (n:Nat), In n X -> Inf X <= n. (* inf X est le plus grand des minorants de X *) Axiom Inf_2 : forall (X : Nats)(p:Nat), (forall n:Nat, In n X -> p <= n) -> p <= Inf X. (* Les axiomes ci-dessus entraînent une incoherence : Astuce : utiliser le terme (Inf Empty) *) Lemma paradox : False. Admitted.