(* quelques tautologies en logique du premier ordre *) (* Domaine de raisonnement *) Parameter D : Set. (* predicats unaires *) Parameters P Q : D -> Prop. (* predicats binaires *) Parameters R S : D -> D -> Prop. (* note : on aurait aussi pu déclarer d : D. et prouver D_not_empty, mais bon *) Axiom D_not_empty : exists d: D, True. Theorem diff_sym : forall x y: D, ~ x = y -> ~ y = x. Proof. Admitted. Theorem not_exists_forall : ~ (exists x, P x) -> forall y, ~ P y. Proof. Admitted. Theorem no_P : (forall x:D, ~ P x) -> forall y : D, P y -> Q y. Proof. Admitted. Theorem exist_all_perm : (exists x, forall y, R x y) -> forall y, exists x, R x y. Proof. Admitted. Theorem un_seul_habitant : (exists x:D, forall y:D, x = y) -> forall x : D, forall y:D, x = y. Proof. intros H x y; elim H. intros x0 H0. (* premiere solution *) rewrite <- (H0 y). rewrite (H0 x). trivial. (* autre solution *) Restart. intros H x y. elim H;intros x0 H0. replace x with x0. auto. auto. (* autre solution *) Restart. intros H x y. elim H;intros x0 H0. transitivity x0;auto. Qed. (* Le theorème suivant est une application de l'axiome D_not_empty *) (* Sans cet axiome, ce lemmen n'est pas prouvable *) Lemma forall_2_exists : (forall x:D, P x) -> (exists x:D, P x). Proof. intro H. (* la séquence suivante permet d'introduire une variable de type D *) elim D_not_empty;intros x Hx. Admitted. Section absurdite. Hypothesis ex_diff : exists x:D, x <> x. Lemma no_diff : False. Proof. Admitted. End absurdite. Check no_diff. (* Logique du premier ordre classique *) Section classic. (* On importe un module permettant le raisonnement Classique *) Require Import Classical. Lemma not_all_ex: ~(forall x: D, P x) -> exists x:D, ~ P x. Proof. intro H. destruct (classic (exists x:D, ~ P x)). Admitted. Theorem drinkers : exists x:D,( P x -> forall y:D, P y). Proof. destruct D_not_empty. Admitted. End classic.