(** Introduction to Formal Reasoning (G52IFR) Nuo Li T03 Read this part carefully in the course work. **) Section CW1. Variables P Q : Prop. (** Lemma ex04 : (P -> Q) -> ~P -> ~Q. not provable **) Lemma inv : forall P Q : Prop, (P -> Q) -> ~Q -> ~P. intros p q pq nq. intro. (** apply nq. apply pq. exact H. **) exact (nq (pq H)). Qed. Lemma ex05 : (P -> Q) -> ~~P -> ~~Q. intro. apply inv. apply inv. exact H. Qed. Lemma ex06 : ~( P <-> ~P ). intro. destruct H. assert (~P). intro. exact (H H1 H1). exact (H1 (H0 H1)). Qed. Require Import Coq.Logic.Classical. (* asserts the axiom classic : P \/ ~P *) Lemma ex08 : ~(P /\ Q) <-> ~P \/ ~Q. split;intros. destruct (classic P). right. intro. apply H. split;assumption. left. assumption. intro. destruct H0. destruct H. exact (H H0). exact (H H1). Qed. End CW1. Section T03. Require Import Coq.Bool.Bool. (* Which one we cannot simplify. Explain the reason *) Definition and (a b : bool) := match a with | true => b | false => false end. Lemma simp1 : forall b : bool, (true && b) = b. simpl. reflexivity. Qed. Lemma simp2 : forall b : bool, (b && true) = b. destruct b;simpl;reflexivity. Qed. Lemma T01 : forall a:bool, (exists b:bool,a || b = false) -> forall b, a && b = false. intros. destruct H. destruct a. simpl. destruct b. unfold orb in H. discriminate H. reflexivity. simpl. reflexivity. Qed. (* Redefine && and try to prove &&-associativity *) (* alternative way *) Definition andb (a b:bool) : bool := if b then a else false. (* Destruct as less as possible *) Lemma and_assoc : forall a b c : bool, andb (andb a b) c = andb a (andb b c). intros. destruct c;simpl; reflexivity. Qed. (* Use true table to find out the definition *) Definition xorb (a b : bool) : bool := if a then negb b else b. (* exists true, false is similar to left, right *) Lemma only_one: forall a : bool, exists b : bool, a && true = b || false . intro. destruct a. exists true. split. exists false. split. Qed. (* What is the negation of exists ? *) Lemma ne : forall P : bool -> Prop, ~ (exists a : bool , P a) -> forall a : bool, ~ (P a). intros. intro. apply H. exists a. exact H0. Qed. Lemma na : forall P : bool -> Prop, ~ (forall a : bool, P a) -> exists a : bool, ~ P a. intros. apply NNPP. intro. apply H. intro. apply NNPP. intro. apply H0. exists a. exact H1. Qed. Lemma impossible : (forall a b : bool, a && b = false) -> False. intro. discriminate (H true true). Qed. End T03. Section Pub. Require Import Classical. Variables People Pubs : Set. Variable Drinks : People -> Prop. Variable In : People -> Pubs -> Prop. Theorem drink : forall p:Pubs, (exists anybody:People,In anybody p) -> exists somebody:People,(In somebody p) /\ (Drinks somebody -> forall a : People, In a p -> Drinks a). intros. destruct H. destruct (classic (forall a : People, In a p -> Drinks a)). exists x. split. assumption. intro. assumption. apply NNPP. intro. apply H0. intros. apply NNPP. intro. apply H1. exists a. split. assumption. intro. destruct (H3 H4). Qed. End Pub.