(** Petite Ecole : Cours N° 2 *) (** Rappel du cours N° 1 *) Check 3. Check 3+5. Compute 3+5. Require Import ZArith. Open Scope Z_scope. Compute leb (5*7) (9*4). Definition double (n:Z) := n*2. Definition square (n:Z) := n *n. Definition Z_compose (g f : Z -> Z) (z:Z) := g (f z). Compute Z_compose square double 2. Compute Z_compose double square 2. Definition compose (A B C: Type)(g : B -> C)(f : A -> B) (a:A) := g (f a). Check compose. SearchAbout (nat->Z). Compute compose _ _ _ square Z.of_nat (3%nat). Arguments compose [A B C] g f a. Compute compose square Z.of_nat (3%nat). Definition compose_succ (A:Type)(f: nat-> A) := compose f S. Compute compose_succ _ (fun n => square (Z.of_nat n)) 4. (** Fin des rappels *) (** Un peu de logique *) Check 3=3. Check 2=3. Check True. Check False. Check true. Check Prop. Section Propositional_logic. Variables P Q R S : Prop. Check P -> Q. Check (P -> Q)->(Q -> R) -> (P -> R). Check (fun p:P => p). Check fun (H : P -> Q)(H0 : Q -> R) (p:P) => H0 (H p). Lemma imp_trans : (P -> Q) -> (Q -> R) -> P -> R. Proof fun (H : P -> Q)(H0 : Q -> R) (p:P) => H0 (H p). Lemma imp_refl : P -> P. Proof fun p:P => p. Lemma imp_trans' : (P -> Q) -> (Q -> R) -> P -> R. Proof. intro H. intro H0. intro p. apply H0. apply H. assumption. Qed. Lemma imp_trans'' : (P -> Q) -> (Q -> R) -> P -> R. Proof. intros H H0 p. apply H0. apply H. assumption. Qed. Lemma imp_trans''' : (P -> Q) -> (Q -> R) -> P -> R. Proof. intros H H0 p;apply H0;apply H; trivial. Qed. Lemma imp_trans_4 : (P -> Q) -> (Q -> R) -> P -> R. Proof. auto. Qed. (** proofs with various subgoals *) Lemma imp_dist : (P -> Q -> R) -> (P -> Q) -> P-> R. Proof. intros H H0 p. apply H. assumption. apply H0;assumption. Qed. Print imp_dist. (** Exercise: Remove the "auto" in the following proofs and use only the tactics intros, apply and assumption *) Lemma L1 : (P-> Q -> R) -> (Q -> P -> R). auto. Qed. Lemma L2 : (((P->Q)->Q)->Q)-> P -> Q. auto. Qed. (** Falsehood and negation *) Check False. (** The negation of a proposition is defined by Definition not (P:Prop) := P -> False. The notation ~P is usable for (not P) Replacing a negation by an implication is easily done - in the conclusion of the goal by "unfold not" - in a hypothesis H by "unfold not in H" *) Lemma double_neg_i : P -> ~(~ P). Proof. intros p H. (** introducing H forces the unfolding of not *) apply H; trivial. Qed. Lemma triple_neg : ~(~(~P)) -> ~P. Proof. auto (* exercise *). Qed. Lemma contraposee : (P -> Q) -> ~Q -> ~P. auto. Qed. (** Falsehood (2) : Elimination *) Lemma L23 : False -> 2 = 3. Proof. intro H. elim H. Qed. Lemma L4 : ~P -> P -> Q. Proof. intros H H0. Check (H H0). elim (H H0). Qed. Lemma L4' : ~P -> P -> Q. Proof. intros H H0. unfold not in H. (* unnecessary *) destruct H. assumption. Qed. Lemma L4'' : ~P -> P -> Q. Proof. tauto. Qed. (** Proofs with sublemmas *) Lemma L4''' : ~P -> P -> Q. Proof. intros H H0. assert (H1 : False). now apply H. destruct H1. Qed. Lemma L4'''' : ~P -> P -> Q. Proof. intros H H0. destruct H. trivial. Qed. Lemma L4''''' : ~P -> P -> Q. Proof. intros; elimtype False. auto. Qed. (** Exercise : remove the tauto tactic ! *) Lemma L5 : (P -> ~P) -> ~P. tauto. Qed. Lemma L6 : (P -> Q) -> (~P -> Q) -> ~~Q. Proof. tauto. Qed. (** Connectives *) Lemma L7 : P -> P \/ Q. Proof. intro H;left. trivial. Qed. Lemma L8 : (P -> R) -> (Q -> R) -> P \/ Q -> R. Proof. intros H H0 H1. destruct H1. (* elim H1, case H1 *) now apply H. now apply H0. Qed. Lemma L8' : (P -> R) -> (Q -> R) -> P \/ Q -> R. Proof. intros H H0 H1. destruct H1;[apply H|apply H0];trivial. Qed. Lemma L9 : P\/Q -> Q \/ P. Proof. tauto. Qed. Lemma L10 : P /\ Q -> P. Proof. intro H;destruct H. assumption. Qed. Lemma L11 : P -> Q -> P /\ Q. Proof. intros p q;split. assumption. assumption. Qed. Lemma L12 : ~(P \/ Q) -> ~P /\ ~Q. Proof. tauto. Qed. (** 1 star exercise *) Lemma L13 : ~(P /\ Q) -> ~~ (~P \/ ~Q). Proof. tauto. Qed. Lemma L14 : ~~(P \/ ~P). Proof. tauto. Qed. End Propositional_logic. (** Teasing *) Lemma exm : (forall P:Prop,~~P ->P) -> (forall P:Prop, P \/ ~P). Proof. intros H P. apply H. intro H0. apply H0. right. intro H1. apply H0. left. assumption. Qed. Lemma exm' : (forall P:Prop, P \/ ~P) -> (forall P:Prop,~~P ->P). Admitted. Lemma Peirce : (forall P:Prop, P \/ ~P)-> forall P Q:Prop, ((P -> Q)-> P)->P. Proof. intros exm P Q. destruct (exm P). Admitted. Lemma Peirce' : (forall P Q:Prop, ((P -> Q)-> P)->P) -> (forall P:Prop, P \/ ~P). Proof. intro H. apply exm. intros P. intro. generalize (H P False). Admitted.