(* rudiments de la logique du premier ordre *) (* On declare une constante Individus dont le type est Set (univers ou sorte des objets consideres) *) Parameter Individus : Set. (* déclarations de constantes *) Parameter socrate : Individus. Parameter king_kong : Individus. Parameter platon : Individus. Check socrate. Check Individus. (* Un predicat est une fonction *) Parameter humain : Individus -> Prop. Parameter animal : Individus -> Prop. Parameter mortel : Individus -> Prop. Parameter singe : Individus -> Prop. Check (singe platon). (* Un axiome est une déclaration de variable globale dont le type est une proposition (acceptée sans preuve) *) Axiom h_socrate : humain socrate. Axiom s_king_kong : singe king_kong. Axiom h_platon : humain platon. (* Les axiomes suivant utilisent la quantification universelle DU PREMIER ORDRE (c.a.d; sur des objets du domaine considere) *) (* Tout humain est mortel *) Axiom humain_mortel : forall i : Individus, humain i -> mortel i. Axiom animal_non_humain : forall i:Individus, animal i -> ~ humain i. Axiom singe_animal : forall i:Individus, singe i -> animal i. Lemma m_socrate : mortel socrate. Proof. (* La commande suivante va appliquer l'axiome humain_mortel en substituant la variable liee "x" par "socrate" *) apply humain_mortel. apply h_socrate. Qed. (* cette commande peermet à "auto" d'utiliser un des axiomes suivants *) Hint Resolve humain_mortel animal_non_humain singe_animal h_socrate s_king_kong h_platon. Lemma m_socrate' : mortel socrate. Proof. auto. Qed. Lemma non_mortel_non_humain : forall x:Individus, ~mortel x -> ~humain x. Proof. (* La tactique d'introduction pour "forall x:A, B" est intro x. (ou intro y ...) *) intros x Hm H. elim Hm. apply humain_mortel. assumption. Qed. Lemma exists_non_humain : exists x:Individus, ~ humain x. Proof. (* La tactique d'introduction pour une proposition de la forme exists x:A, B est "exists t" où t est un terme de type A (appelé "témoin"); il faut alors vérifier que le témoin t satisfait bien la proposition associée *) exists king_kong. apply animal_non_humain. apply singe_animal. apply s_king_kong. Restart. exists king_kong;auto. Qed. Lemma not_all_human : ~ (forall i, humain i). Proof. intro H. (* La tactique d'élimination d'une proposition de la forme (exists x:A, B) pour prouver un but C engendre le but : forall x:A, B -> C. *) elim exists_non_humain. intros x Hx. elim Hx. apply H. Qed. Lemma impossibilite : ~(exists i:Individus, humain i /\ singe i). Proof. intro H;elim H. intros x Hx. elim Hx. intros H0 H1. (* Ici, nous utilisons une tactqie utile en cas de difficulté: Si C est le but courant, la tactique "assert A" engendre deux buts: a) prouver A b) montrer A -> C Cela correspond a la notion bien connue de lemme *) assert (~ humain x). auto. elim H2. assumption. Qed. (* l'égalité *) Theorem eq_exemple : exists i:Individus, i=socrate. Proof. exists socrate. reflexivity. Qed. (* t1 <> t2 est une abréviation de ~(t1=t2) *) Theorem socrate_not_king_kong : socrate <> king_kong. Proof. intro e. elim impossibilite. exists socrate. split;auto. (* Si e a pour type t1=t2, la tactique "rewrite e" remplace t1 par t2 dans le but courant. Variantes : rewrite <- e. (remplace t2 par t1) subst t1. remplace PARTOUT t1 par t2 voir doc *) rewrite e. auto. Qed. Theorem singe_diff_humain : forall i j : Individus, singe i -> humain j -> ~ i = j. Proof. intros i j Hi Hj e. subst i. (* La commande suivante utilise le fait que animal_non_humain j a pour type animal j -> ~humain j *) elim (animal_non_humain j);auto. Qed.