(* La fonction pred est déjà définie *) Print pred. (* On définit null comme dans l'énoncé *) Definition null (n : nat) := match n with O => True | S _ => False end. Lemma Sinj : forall x y : nat, S x = S y -> x = y. Proof. intros x y hxy. (* on remplace x = y par un but convertible, ie égal modulo le calcul*) change (pred (S x) = pred (S y)). rewrite hxy; reflexivity. Qed. (* On définit null et sa spec comme dans l'énoncé *) Definition Even (n : nat) := exists p : nat, n = 2 * p. (* On charge d'abord une bibliothèque sur les booléens *) Require Import Bool. Fixpoint even (n : nat) : bool := match n with | O => true | S p => negb (even p) (* Nécessite un "Require Import Bool." *) end. (* pour accéder à la constante "negb". *) (* Test des valeurs de even : *) Eval compute in (even 3). Eval compute in (even 78). (* La partie facile : Even -> even *) Lemma Even_even : forall x, Even x -> even x = true. Proof. unfold Even; intros n h. destruct h as [x hx]; rewrite hx; clear hx n. elim x. reflexivity. clear x; intros x; simpl. rewrite <- plus_n_O. rewrite <- plus_n_Sm; simpl. intro h; rewrite h; simpl. reflexivity. Qed. (* Pour even <- Even on prouve un schéma de récurrence bien adapté *) Lemma nat_ind2 : forall P : nat -> Prop, P 0 -> P 1 -> (forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n. Proof. intros P P0 P1 hP n. assert (hn : P n /\ P (S n)). induction n. split; assumption. destruct IHn as [Pn Psn]. split; try assumption. apply hP; assumption. destruct hn; assumption. Qed. Lemma Eveneven : forall n, even n = true -> Even n. Proof. intros n; induction n using nat_ind2. intro h; unfold Even; exists 0; reflexivity. simpl; intro h; discriminate. simpl. (* On cherche un lemme qui dit que negb est involutive*) SearchAbout negb. rewrite negb_involutive; intro h. assert (hE : Even n) by (apply IHn; assumption). destruct hE as [y hy]. unfold Even. rewrite hy. exists (S y). simpl. rewrite <- plus_n_Sm. reflexivity. Qed. Parameter T : Set. Definition EQ (x y : T) := forall P : T -> Prop, P x -> P y. Lemma EQ_refl : forall x, EQ x x. Proof. unfold EQ; intros x P Px. assumption. Qed. Lemma EQ_trans : forall x y z, EQ x y -> EQ y z -> EQ x z. Proof. unfold EQ; intros x y z Exy Eyz P Px. apply Eyz; apply Exy. assumption. Qed. (* Une preuve imprédicative, pourquoi ? *) Lemma EQ_sym : forall x y, EQ x y -> EQ y x. Proof. intros x y; unfold EQ; intro Exy. apply Exy. intros P Px; assumption. Qed. (* Une preuve prédicative *) Lemma EQ_sym_pred : forall x y, EQ x y -> EQ y x. Proof. intros x y; unfold EQ; intros Exy P. apply Exy. intros Px; assumption. Qed. Lemma EQ_eq_equiv : forall x y, EQ x y <-> eq x y. Proof. intros x y; unfold EQ; split. intro h; apply h; reflexivity. intro h; rewrite h; intros; assumption. Qed. (* Définition de la conjonction *) Definition ET (A B : Prop) := forall X : Prop, (A -> B -> X) -> X. (* Règles d'introduction et d'élimination: *) Lemma ET_intro : forall A B : Prop, A -> B -> ET A B. Proof. unfold ET in |- *; intros. apply H1; assumption. Qed. Lemma ET_elim1 : forall A B : Prop, ET A B -> A. Proof. unfold ET in |- *; intros. apply H; intros; assumption. Qed. Lemma ET_elim2 : forall A B : Prop, ET A B -> B. Proof. unfold ET in |- *; intros. apply H; intros; assumption. Qed. (* Equivalence avec le ou logique de Coq *) Lemma ET_and_equiv : forall A B : Prop, ET A B <-> A /\ B. Proof. intros A B; split. intros hET; split; [apply (ET_elim1 A B) | apply (ET_elim2 A B)]; assumption. intro hand; destruct hand as [a b]. apply ET_intro; assumption. Qed. (* Définition de la disjonction *) Definition OU (A B : Prop) := forall X : Prop, (A -> X) -> (B -> X) -> X. (* Introduction et élimination *) Lemma OU_intro1 : forall A B : Prop, A -> OU A B. Proof. unfold OU in |- *; intros. apply H0; assumption. Qed. Lemma OU_intro2 : forall A B : Prop, B -> OU A B. Proof. unfold OU in |- *; intros. apply H1; assumption. Qed. Lemma OU_elim : forall A B C : Prop, (A -> C) -> (B -> C) -> OU A B -> C. Proof. unfold OU in |- *; intros. apply H1; assumption. Qed. (* Équivalence avec le ou logique de Coq *) Lemma OU_or_equiv : forall A B : Prop, OU A B <-> A \/ B. Proof. split; intros. apply OU_elim with A B. intro; left; assumption. intro; right; assumption. assumption. destruct H; [ apply OU_intro1 | apply OU_intro2 ]; assumption. Qed. (* Un codage de bottom *) Definition BOT := forall X : Prop, X. Lemma BOT_elim : forall A : Prop, BOT -> A. Proof. unfold BOT in |- *; intros; apply H. Qed. Lemma BOT_False_equiv : BOT <-> False. Proof. split; intro; [ apply H | destruct H ]. Qed. (* Un codage de top *) Definition TOP := forall X : Prop, X -> X. Lemma TOP_intro : TOP. Proof. unfold TOP in |- *; intros; assumption. Qed. Lemma TOP_True_equiv : TOP <-> True. Proof. split; intro; [ split | exact TOP_intro ]. Qed. (* Définition du quantificateur existentiel *) Definition EX (P : T -> Prop) := forall X : Prop, (forall x : T, P x -> X) -> X. (* Introduction et élimination *) Lemma EX_intro : forall P : T -> Prop, forall x : T, P x -> EX P. Proof. unfold EX in |- *; intros. apply H0 with x; assumption. Qed. Lemma EX_elim : forall P : T -> Prop, forall A : Prop, (forall x : T, P x -> A) -> EX P -> A. Proof. intros; apply H0; assumption. Qed. (* Équivalence de "EX" et "exists" *) Lemma EX_equiv : forall P : T -> Prop, EX P <-> exists x : T, P x. Proof. split; intros. apply H; intros; exists x; assumption. destruct H as (x, H); apply EX_intro with x; assumption. Qed. (* Parameter T : Set. déja donné plus haut *) Parameter (o : T). Parameter (s : T -> T). Definition N (x : T) := forall P : T -> Prop, P o -> (forall y, P y -> P (s y)) -> P x. Lemma No : N o. Proof. unfold N. intros P Po h. assumption. Qed. Lemma Ns : forall x : T, N x -> N (s x). Proof. intros x; unfold N; intros h P Po hP. apply hP; apply h; assumption. Qed. Lemma N_rec : forall A : T -> Prop, A o -> (forall x, N x -> A x -> A (s x)) -> forall x, N x -> A x. Proof. intros A Ao hA x Nx. assert (h : N x /\ A x). apply Nx. split; [exact No | assumption]. intros y h; destruct h as [Ny Ay]; split. apply Ns; assumption. apply hA; assumption. destruct h; assumption. Qed.