(* Fill the proofs by replacing "Admitted" by a complete proof script, which ends with Qed. *) Parameter A B C : Prop. Lemma AimpA : A -> A. Proof. intros a. exact a. Qed. Lemma imp_trans : (A -> B) -> (B -> C) -> A -> C. Proof. intros ab bc a. apply bc. apply ab. exact a. Qed. (* What is the computational behaviour illustrated here? *) Print AimpA. (* AimpA is the identity function *) Print imp_trans. (* imp_trans is the composition of functions: - a proof of (A->B) is a function from proofs of A to proofs of B - similarly with B and C - then one proof of (A->C) if the composition of the above functions *) Lemma and_comm : A /\ B -> B /\ A. Proof. intros. destruct H. split. assumption. assumption. Qed. Lemma A_nnA : A -> ~ ~ A. Proof. (* Observe the definition of negation. (use Ctrl-P to display the goal without using notation ~) *) Unset Printing Notations. (* Refold default notations *) Set Printing Notations. intros a nota. apply nota. exact a. Qed. Lemma and_distrib_or : (A \/ B) /\ C -> A /\ C \/ B /\ C. Proof. intros. destruct H. (* breaks the conjunction *) destruct H. (* breaks the disjunction *) left. split. assumption. assumption. right. split. assumption. assumption. Qed. Lemma em_equiv : (forall A : Prop, A \/ ~A) <-> (forall A : Prop, ~~A -> A). Proof. split. (* excluded-middle implies negation elimination *) intros em A nnA. destruct (em A). (* A holds *) assumption. (* A does not hold: ~~A (a.k.a ~A -> False) is absurd *) destruct nnA. assumption. (* negation elimination implies excluded_middle *) intros neg_elim A. apply neg_elim. intro. (* H is intuitionisitcally equivalent to ~A /\ ~~A... *) apply H. right. intro a. apply H. left. assumption. Qed. (* Drinker's paradox *) Parameter Person : Type. Parameter Drinks : Person -> Prop. Parameter em : forall A : Prop, A \/ ~A. Lemma drinker : Person -> exists p, Drinks p -> forall p', Drinks p'. (* If everybody drinks, then p may be any person (by proving the conclusion of the implication without needing the premisse (Drinks p)) If someone is not drinking, then p can be that person, and the implication holds by the absurdity of its premisse. Since we use the person that does not drink in the second case, we apply excluded-middle to the existence of a person that does not drink, rather than to the fact that everybody drinks... *) intros q. destruct (em (exists p, ~ Drinks p)). (* someone is not drinking. *) destruct H as (p,p_not_drinking). exists p. intros. destruct p_not_drinking. assumption. (* nobody drinks. *) exists q. intros. (* we need to prove Drinks p', but H may only derive its double-negation. Hence we need the excluded-middle again *) destruct (em (Drinks p')). assumption. (* now H1 contradicts H *) destruct H. exists p'. assumption. Qed. (* Try the same proof using only nnpp (and without using its equivalence with em ... *) Parameter nnpp : forall A:Prop, ~~A -> A. Lemma drinker' : Person -> exists p, Drinks p -> forall p', Drinks p'. Proof. intros p. apply nnpp. intros h. apply h. exists p. intros. apply nnpp. intros np'. apply h. exists p'. intros. destruct np'. assumption. Qed.