(* Logique du premier ordre *) (** Tactiques : pour forall : introduction : intro, intros. elimination : apply, eapply, specialize. (H x ...) pour exists exists, destruct. pour = reflexivity, rewrite H [in HØ] rewrite <- H [in H0] *) (* tactique maison pour eliminer un forall *) Ltac forall_e H t := (generalize (H t); intro). (* Exemple *) Example E0 : ~(forall x:nat, x <> x). Proof. intro H. forall_e H 32. apply H0. trivial. (* reflexivity. *) Qed. Section Syllogismes. Variable Etre: Type. Variables humain mortel animal : Etre -> Prop. Variable Socrate : Etre. Variable Rhino : Etre. Hypothesis HM : forall x, humain x -> mortel x. Hypothesis HSocrate : humain Socrate. Hypothesis Etre_disj : forall x:Etre, humain x \/ animal x. Hypothesis Hrhino : ~ humain Rhino. Lemma Syllogisme : mortel Socrate. Proof. apply HM. (* elimination du forall et modus-ponens *) assumption. Qed. Lemma contraposee : forall x, ~ mortel x -> ~ humain x. Proof. intros x Hx H. apply Hx. apply HM; trivial. Qed. Lemma Lm: exists x, mortel x. Proof. exists Socrate. (* introduction de l'existentiel *) apply Syllogisme. Qed. Lemma La: exists x, animal x. Proof. exists Rhino. destruct (Etre_disj Rhino). contradiction. trivial. Qed. Lemma L : ~(exists x:Etre, ~ humain x /\ ~ animal x). Proof. intro H. destruct H as [e He]. (* elimination de l'existentiel *) destruct He. destruct (Etre_disj e). (* elimination du forall, puis du ou *) contradiction. contradiction. Qed. End Syllogismes. Section Egalite. Variable A : Type. Variable f : A -> A. Lemma E1 : forall x:A, exists y: A, x=y. Proof. intros x. exists x. reflexivity. (* trivial *) Qed. Lemma E2 : forall x y z: A, x = y -> y = z -> x = z. Proof. intros x y z H H0. rewrite H. assumption. Qed. (* x <> y est une abréviation de ~ (x = y) *) Lemma diff_eq : forall x y z:A, x <> y -> y = z -> x <> z. Proof. intros. rewrite H0 in H. assumption. Qed. Lemma L3 : forall x y z: A , x = y -> x <> z -> z <> y. Proof. intros. intro. rewrite H1 in H0. apply H0; trivial. Qed. Lemma L4 : forall x y:A, f x <> f y -> x <> y. Proof. intros. intro H0. rewrite <- H0 in H. apply H. trivial. Qed. End Egalite. (* Exercice 3 de la feuille de TD N° 3 *) Section Exercices_3_et_5. Variable A B: Type. Variables P Q : A -> Prop. Variable R : A -> B -> Prop. Variable X : Prop. Lemma Question1 : (forall x:A, P x /\ Q x) <-> (forall x:A, P x) /\ (forall x:A, Q x). Proof. split; intro H. - split. + intro x. destruct (H x). assumption. + intro x; destruct (H x); trivial. - intro x; split. + destruct H. auto. (* apply H. *) + destruct H;auto. Qed. Lemma Question2 : (forall x, P x) \/ (forall x, Q x) -> forall x, P x \/ Q x. Proof. intro H; destruct H. - intro x; left;auto. - intro x; right;auto. Qed. Lemma Question4 : (exists x:A, P x /\ Q x) -> (exists x:A, P x) /\ (exists x:A, Q x). Proof. firstorder. (* a faire a la main ! *) Qed. Lemma Question6 : (exists x:A, P x \/ Q x) <-> (exists x:A, P x) \/ (exists x:A, Q x). Proof. firstorder. Qed. Section Question7. Hypothesis H : forall x, P x -> Q x. Hypothesis H0 : exists x, P x. Lemma L7 : exists x, Q x. Proof. firstorder. (* a faire a la main ! *) Qed. End Question7. Lemma Question8 : forall x, P x -> exists y, P y. Proof. firstorder. (* a faire a la main ! *) Qed. Lemma Question10 : ~(exists x, P x) <-> forall x, ~ P x. Proof. firstorder. (* a faire a la main ! *) Qed. Lemma Question11 : ((exists x, P x) -> X) <-> forall x, P x -> X. Proof. firstorder. (* a faire a la main ! *) Qed. Lemma Question12 : (exists x:A, forall y:B, R x y) -> (forall y:B, exists x:A, R x y). Proof. firstorder. (* a faire a la main ! *) Qed. (* Sur l egalite *) Lemma eq_sym : forall x y:A, x = y -> y = x. Proof. intros x y H. rewrite H. reflexivity. Qed. Lemma eq_trans : forall x y z:A, x = y -> y = z -> x = z. Proof. intros. rewrite H. assumption. Qed. (* De l'exercice 5 *) Definition A_est_vide := forall x:A, x <> x. Lemma exercice5_1 : A_est_vide -> forall x:A, P x. Proof. unfold A_est_vide; firstorder. Qed. Lemma exercice_5_3 : (forall x y:A, x <> y) -> A_est_vide. Proof. unfold A_est_vide; firstorder. Qed. Section classic. Hypothesis exm : forall X : Prop, X \/ ~X. Ltac add_exm P := let hname := fresh "exm" in assert(hname := exm P). (* ne pas essayer de comprendre : applique le raisonnement par l'absurde classique Transforme un but "Gamma |- P " en "Gamma, ~P |- False" *) Ltac absurdK := match goal with |- ?X => let hname := fresh "exm" in assert(hname := exm X); destruct hname;[assumption| elimtype False] end. Lemma Question9 : ~ (forall x, P x) <-> exists x, ~ P x. Proof. split. - intro H. absurdK. apply H. admit. (* remplacer le admit *) - firstorder. Admitted. (* finir la preuve *) Section Exercice_5_2. Hypothesis H : ~ A_est_vide. Hypothesis H0 : forall x:A, P x. Lemma L_5_2 : exists x:A, P x. (* difficile *) Proof. unfold A_est_vide in H. assert (exists x:A, x = x). { absurdK. firstorder. } firstorder. Qed. End Exercice_5_2. Section drinkers_problem. (* Exercice 4 *) Variable people : Type. Variable patron : people. Variable boit : people -> Prop. Theorem buveurs : exists p:people, boit p -> forall q, boit q. Proof. add_exm (forall q, boit q). destruct exm0. - exists patron;auto. - assert (exists x:people, ~ boit x). { admit. } firstorder. Admitted. End drinkers_problem. End classic. End Exercices_3_et_5.