(* verifiez que votre fichier d'initialisation d'emacs contient la ligne (load-file "/usr/share/emacs/site-lisp/proofgeneral/generic/proof-site.el") *) (** premiers pas en Coq *) Section Declarations. Variables P Q R S T : Prop. Lemma imp_dist: (P -> Q -> R) -> (P -> Q) -> P -> R. Proof. intro H. intro H0. intro H1. apply H. assumption. apply H0. assumption. Qed. (* exemple de preuve d'un sequent *) Section S1. Hypothesis H : P -> Q. Hypothesis H0 : P -> Q -> R. Lemma L2 : P -> R. Proof. intro p. apply H0. assumption. apply H. assumption. Qed. End S1. Section About_cuts. Hypothesis H : P -> Q. Hypothesis H0 : P -> Q -> R. Hypothesis H1 : Q -> R -> S. Hypothesis H2 : Q -> R -> S -> T. (* preuve avec coupures *) Lemma L3 : P -> T. intro p. assert (q: Q). { apply H; assumption. } assert (r: R). { apply H0; assumption. } assert (s : S). { apply H1; assumption. } apply H2; assumption. Qed. (* preuve sans lemme (coupure) *) Lemma L3' : P -> T. Admitted. End About_cuts. (* Exercices Reprendre les exemples vus en TD, en utilisant les tactiques assumption, apply et intros Remplacer la commande Admitted par une preuve correcte suivie de la commande Qed. *) Lemma IdP : P -> P. Proof. Admitted. Lemma IdPP : (P -> P) -> P -> P. Proof. Admitted. (* un autre preuve *) Lemma IdPP' : (P -> P) -> P -> P. Proof. Admitted. Lemma imp_trans : (P -> Q) -> (Q -> R) -> P -> R. Proof. Admitted. Section proof_of_hyp_switch. Hypothesis H : P -> Q -> R. Lemma hyp_switch : Q -> P -> R. Proof. Admitted. End proof_of_hyp_switch. Check hyp_switch. Section proof_of_add_hypothesis. Hypothesis H : P -> R. Lemma add_hypothesis : P -> Q -> R. Proof. Admitted. End proof_of_add_hypothesis. (* prouver le sequent (P -> P -> Q) |- P -> Q *) (* meme exercice avec P -> Q , P -> R , Q -> R -> T |- P -> T Meme exercice avec (P -> Q) -> R |- Q -> R Meme exercice avec (((P->Q) -> Q) -> Q) |- P -> Q. *) Lemma weak_Peirce : ((((P -> Q) -> P)-> P) -> Q) -> Q. Proof. Admitted. (* S'il reste du temps : compositions tac ; tac' tac ; trivial tac ; try tac' tac ; [tac1 | tac2 | ... | tacn] auto. Reprendre les exemples precedents en essayant d'avoir les scrots de preuve les plus concis. *) (* Essayer de donner directement le terme de preuve des exercices precedents comme par exemple : *) Definition imp_dist' : (P -> Q -> R) -> (P -> Q) -> P -> R := fun (H : P -> Q -> R) (H0 : P -> Q) (p: P) => H p (H0 p). End Declarations.