(*** Le produit dépendant, etc *) (** Chap 4 du Coq'Art *) Check or. Check or_introl. Require Import Arith ZArith List. Check nat. Check 0%nat. Check S. Check plus. Check Zplus. Check list. Check list Z. Check list Prop. (** Predicats *) Check le. Check le 4 8. (* 4 <= 8 : Prop *) Definition positive (n:nat) := 1 <= n. Check positive. Check le_n. Check le_n 33. Check le_S. Check le_trans. Check le_S 5 5. Check le_S _ _ (le_n 5). Lemma le_n_Sn : forall n:nat, n <= S n. Proof. intro n. - apply le_S. apply le_n. Qed. Print le_n_Sn. Lemma le_plus2 : forall n, n <= S (S n). Proof. intro n; apply le_trans with (S n);apply le_n_Sn. Qed. Lemma le_plus2' : forall n, n <= S (S n). Proof. intro n; apply (le_trans _ (S n) _);apply le_n_Sn. Qed. Lemma le_plus2'' : forall n, n <= S (S n). Proof. intro n; eapply le_trans ;apply le_n_Sn. Qed. Lemma forall_imp (A:Type) : forall(P Q : A -> Prop), (forall x, P x -> Q x) -> (forall y, P y) -> (forall z, Q z). Proof. intros P Q H H0 z. apply H. apply H0. Qed. Print forall_imp. Lemma forall_imp' (A:Type) : forall(P Q : A -> Prop), (forall x, P x -> Q x) -> (forall y, P y) -> (forall z, Q z). Proof. auto. Qed. (** Egalite *) Lemma eq36 : 9 * 4 = 6 * 6. Proof. reflexivity. (* trivial *) Qed. Check eq_ind. (* eq_ind : forall (A : Type) (x : A) (P : A -> Prop), P x -> forall y : A, x = y -> P y *) Lemma eq_sym (A:Type) : forall x y:A, x = y -> y = x. Proof. intros x y Hxy. (* destruct Hxy . *) rewrite <- Hxy. reflexivity. Qed. Lemma eq_trans (A:Type) : forall x y z: A, x = y -> y = z -> x = z. Proof. intros x y z H0 H1. (* rewrite H1 in H0; assumption. *) rewrite H0; assumption. Qed. Section Example. Variable A : Type. Variable f : A -> A -> A. Infix "*" := f. Hypothesis f_assoc : forall x y z:A, x * (y * z) = (x * y) * z. Hypothesis f_com: forall x y:A, x * y = y * x . Hypothesis f_idem : forall a:A, a * a = a. Lemma f1 : forall a : A, a * (a * a) * a = (a * a) * (a * a). Proof. intro a. repeat rewrite f_assoc. reflexivity. Qed. Lemma f_com2 : forall a b c :A, a * (b * c) = b * (a * c). Proof. intros a b c; repeat rewrite f_assoc. now rewrite (f_com a b). Qed. Lemma f_idem2 : forall a b:A, a * (a * b) = a * b. Proof. intros a b; rewrite f_assoc. now rewrite f_idem. Qed. Ltac normalize a b := repeat (rewrite f_idem || rewrite (f_com a b) || rewrite <- f_assoc || rewrite f_idem2 || rewrite (f_com2 a b) ). Lemma f2 : forall a b : A, a * b * a * b * a = a * b. Proof. intros a b; normalize a b. reflexivity. Qed. End Example. Lemma sqrt_16 : exists n:nat, n * n = 16. Proof. exists 4. reflexivity. Qed. Print lt. Lemma nat_unbounded : forall n:nat, exists p, n < p. Proof. intro n; exists (S n). apply le_n. Qed. Check ex_ind. (* ex_ind : forall (A : Type) (P : A -> Prop) (P0 : Prop), (forall x : A, P x -> P0) -> (exists x, P x) -> P0 *) Section Exemples_ex. Variables (A:Type)(P Q : A -> Prop). Lemma ex_or : (exists x : A, P x \/ Q x) <-> (exists x : A, P x) \/ (exists x : A, Q x). Proof. split; intro H. - destruct H as [a H1]. destruct H1 as [H2 | H2]. left;now exists a. right; now exists a. - destruct H as [H0 | H0]. destruct H0 as [a Ha];exists a; now left. destruct H0 as [a Ha];exists a; now right. Qed. Lemma not_exists : ~ (exists x:A, P x) -> forall x, ~ P x. Proof. intros H x Hx. destruct H; now exists x. Qed. Definition EXM := forall P:Prop, P \/ ~P. Lemma classic_not_forall : EXM -> ~ (forall x, ~ P x) -> exists x, P x. Proof. intros exm H. destruct (exm (exists x : A, P x)); [assumption |]. - (* A : Type P, Q : A -> Prop R : A -> A -> Prop exm : EXM H : ~ (forall x : A, ~ P x) H0 : ~ (exists x : A, P x) ============================ exists x : A, P x *) destruct H;intros x Hx. (* A : Type P, Q : A -> Prop R : A -> A -> Prop exm : EXM H0 : ~ (exists x : A, P x) x : A Hx : P x ============================ False *) apply H0; now exists x. Qed. End Exemples_ex. Check not_exists. (* not_exists : forall (A : Type)(P : A -> Prop), ~ (exists x : A, P x) -> forall x : A, ~ P x *) Lemma classic_not_forall_R : (forall (A:Type) (P: A -> Prop), (~(forall x:A, ~ P x) -> exists x:A, P x)) -> EXM. Proof. intros H Q. destruct (H nat (fun n:nat => Q \/ ~Q)). - clear H. intro H0. absurd (~Q); auto. + intro q'; destruct (H0 0); now right. + intro q; destruct (H0 42). now left. - assumption. Qed. Definition injective {A B : Type}(f: A -> B) := forall x y:A, f x = f y -> x = y. Definition surjective {A B : Type}(f: A -> B) := forall y:B, exists x, f x = y . Lemma injective_contrap : forall (A B : Type) (f : A -> B), injective f -> forall x y, x <> y -> f x <> f y. Proof. intros A B f Hf x y H. intro eq; destruct H; now apply Hf. Qed. (** Ensembles *) Definition Ensemble (A: Type) := A -> Prop. Definition mem {A:Type} a (X : Ensemble A) := X a. Definition union {A: Type} (X Y : Ensemble A) := fun a => X a \/ Y a. Definition incl {A: Type} (X Y : Ensemble A) := forall a, mem a X -> mem a Y. Definition same_set {A: Type} (X Y : Ensemble A) := incl X Y /\ incl Y X. Definition compl {A:Type} (X : Ensemble A) := fun x:A => ~ mem x X. Definition empty_set {A:Type} := fun x:A => False. Lemma L1 {A: Type} : forall X: Ensemble A, incl X (compl X) -> same_set X empty_set. Proof. intros X H; split. - intros a Ha; now destruct (H a Ha). - intros a Ha; destruct Ha. Qed.