(* Apprentissage de Coq : Preuves et tactiques Utilisation de Proof General Logique propositionnelle minimale *) Section Exos_LMP. Variables P Q R S T : Prop. Check P. Check (P->Q). Check (P -> (Q -> P)). Theorem id_P : P -> P. Proof. intro p. assumption. Qed. Lemma id_PP : (P->P)->(P->P). Proof. intro H. assumption. Qed. Theorem imp_dist: (P -> (Q -> R)) -> (P -> Q) -> (P -> R). Proof. intros H H0. intro p. apply H. assumption. apply H0. assumption. Qed. (* Pour chaque résultat prouvé : a) utiliser les tactiques intro, intros, apply, et assumption. b) sur papier, ecrire les preuves associées en notation de séquent c) essayer la commende Restart, et essayer les tactiques composées et les tactiques trivial et auto. *) Lemma imp_perm : (P->Q->R)->(Q->P->R). Proof. Qed. Theorem imp_trans : (P -> Q) -> (Q -> R) -> P -> R. Proof. Qed. Lemma ignore_Q : (P->R)->P->Q->R. Proof. Qed. Proof. Qed. Lemma delta_impR : (P->Q)->(P->P->Q). Proof. Qed. Lemma diamond : (P->Q)->(P->R)->(Q->R->S)->P->S. Proof. Qed. Theorem P3Q: (((P -> Q) -> Q) -> Q) -> P -> Q. Proof. Qed. Lemma weak_Peirce : ((((P->Q)->P)->P)->Q)->Q. Proof. Qed. (* L'énoncé suivant est improvable en logique minimale Essayer quand même quelques tactiques .... *) Lemma Peirce : ((P -> Q) -> P) -> P. Proof. Abort. End Exos_LMP.