(** Introduction to Formal Reasoning (G52IFR) Nuo Li T08 Revision **) Section CW5. Load Lists. Set Implicit Arguments. Implicit Arguments nil [A]. Infix "::" := cons (at level 60, right associativity). Infix "++" := app (right associativity, at level 60). Fixpoint count (n:nat)(ms:list nat) {struct ms} : nat := match ms with | nil => 0 | m::ms' => let cn := count n ms' in if eqnat n m then S cn else cn end. Definition Perm (ns ms:list nat) := forall n:nat,count n ns=count n ms. Theorem sort_perm : forall ms:list nat,Perm ms (sort ms). unfold Perm. induction ms. simpl. reflexivity. intro. simpl. rewrite IHms. clear IHms. (* What lemma do you think we should prove? *) induction (sort ms). simpl. reflexivity. simpl. (* If a <= a0, how can we prove it? *) destruct (leqb a a0). simpl. split. simpl. destruct (eqnat n a0). rewrite <- IHl. destruct (eqnat n a);split. assumption. Qed. End CW5. Section Prp. Variables P : Prop. (** Lemma t1_1 : P \/ ~P. unprovable **) Lemma t1_2 : ~~(P \/ ~P). intro. apply H. right. intro. apply H. left. exact H0. Qed. Lemma t1_3 : ~( P <-> ~P ). intro. destruct H as [pnp npp]. apply pnp; apply npp; intro; apply pnp; exact H. Qed. End Prp. Section classic. Require Import Coq.Logic.Classical. Lemma Pierce : forall P Q : Prop, ((P -> Q) -> P) -> P. intros P Q. destruct (classic P) as [H | f]. intro. exact H. intro. apply H. intro. destruct (f H0). Qed. End classic. Section Pred. Variable People : Set. Variables Male Female : People -> Prop. (*How to define they have no intersection? *) Axiom mfd : forall p : People, ~ (Male p /\ Female p). Variables Parent : People -> People -> Prop. Definition Father (x y : People) := Parent x y /\ Male x. Definition Mother (x y : People) := Parent x y /\ Female x. Lemma fnm : forall p, (exists c, Father p c) -> (forall other, ~ Mother p other). intros. intro. destruct H. unfold Father in H. destruct H. unfold Mother in H0. destruct H0. eapply mfd. split. eexact H1. exact H2. Qed. (* Lemma t4_2 : forall A P' Q', (forall x:A,P' x \/ Q' x) -> (forall x:A,P' x) \/ (forall x:A,Q' x). intros. unprovable *) End Pred. Section Bool. Require Import Coq.Bool.Bool. (* Just two lines is enough *) Lemma t3_1 : forall a : bool, (forall b : bool, b && a = b) -> a = true. intros. exact (H true). Qed. Lemma impossible : (forall a b : bool, a && b = false) -> False. intros. discriminate (H true true). Qed. Lemma IdF : forall (a : bool), a = a. split. Qed. Lemma t3_2_1 : forall a b : bool, a <> b -> a = negb b. intros. destruct a; destruct b. destruct (H (IdF true)). reflexivity. reflexivity. destruct (H (IdF false)). Qed. Lemma t3_2 : ~(exists a:bool, exists b:bool, exists c : bool, ~ (a = b) /\ ~(a = c) /\ ~ (b = c)). intro. destruct H as [a H]. destruct H as [b H]. destruct H as [c H]. destruct H. destruct H0. apply H. rewrite (t3_2_1 H0). rewrite (t3_2_1 H1). split. Qed. End Bool. Section Sets. Variables A B C : Set. Open Scope type_scope. Implicit Arguments inl [A B]. Implicit Arguments inr [A B]. Definition L : Set := (A + B) -> C. Definition R : Set := (A -> C) * (B -> C). (* The goal is two show that they are isomorphic ** by defining two functions phi and psi and then showing that they are inverse to each other. *) Definition phi : L -> R := fun (l : L) => (fun (a : A) => l (inl a), fun (b : B) => l (inr b)). Definition psi : R -> L := fun (r : R) => fun (u : A + B) => match r with | (ac , bc) => match u with | inl a => ac a | inr b => bc b end end. Axiom ext : forall (A B : Set)(f g : A -> B), (forall x:A,f x = g x) -> f = g. Lemma eta : forall (P Q : Set)(f : P -> Q), (fun x : P => f x) = f. intros. apply ext. split. Qed. Lemma psiphi : forall (l : L), psi (phi l) = l. unfold psi. unfold phi. intro. apply ext. intro. destruct x;split. Qed. Lemma phipsi : forall (r : R), phi (psi r) = r. intro. destruct r. unfold psi. unfold phi. rewrite (eta c). rewrite (eta c0). split. Qed. End Sets. Section Arith. Lemma n_Sn : forall n : nat, n <> S n. intros. intro. induction n. discriminate H. apply IHn. apply peano8. assumption. Qed. Notation "m <= n" := (leq m n). Lemma le_trans' : forall (l m n : nat), l <= m -> m <= n -> l <= n. intros l m n lm mn. destruct lm as [k klm]. destruct mn as [j jmn]. exists (j+k). rewrite<- plus_assoc. rewrite<- klm. assumption. Qed. End Arith. Section CoqInCoq. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Program.Equality. Inductive Formula : Set := | Var : string -> Formula | Impl : Formula -> Formula -> Formula | And : Formula -> Formula -> Formula. Notation "x ==> y" := (Impl x y) (at level 30, right associativity). Notation "x //\\ y" := (And x y) (at level 20, left associativity). Definition Hyps : Set := list Formula. Definition K (P Q : Formula) : Formula := P ==> Q ==> P. Definition S (P Q R : Formula) : Formula := (P ==> Q ==> R) ==> (P ==> Q) ==> P ==> R. Definition FST (P Q : Formula) : Formula := (P //\\ Q ==> P). Definition SND (P Q : Formula) : Formula := (P //\\ Q ==> Q). Definition PAIR (P Q : Formula) : Formula := (P ==> Q ==> P //\\ Q). Inductive CL_Proof : Hyps -> Formula -> Prop := | cl_ass : forall (Hs : Hyps)(P : Formula), CL_Proof (P :: Hs) P | cl_weak : forall (Hs : Hyps)(P Q : Formula), CL_Proof Hs P -> CL_Proof (Q :: Hs) P (* The following are combinators *) | cl_K : forall (Hs : Hyps)(P Q : Formula), CL_Proof Hs (K P Q) | cl_S : forall (Hs : Hyps)(P Q R: Formula), CL_Proof Hs (S P Q R) | cl_FST : forall (Hs : Hyps)(P Q : Formula), CL_Proof Hs (FST P Q) | cl_SND : forall (Hs : Hyps)(P Q : Formula), CL_Proof Hs (SND P Q) | cl_PAIR : forall (Hs : Hyps)(P Q : Formula), CL_Proof Hs (PAIR P Q) | cl_apply : forall (Hs : Hyps)(P Q : Formula), CL_Proof Hs (P ==> Q) -> CL_Proof Hs P -> CL_Proof Hs Q. Lemma nd_compose_f : forall (Hs : Hyps)(P Q R : Formula), CL_Proof Hs ((Q ==> R) ==> (P ==> Q) ==> (P ==> R)). intros. eapply cl_apply. eapply cl_apply. apply cl_S. eapply cl_apply. apply cl_K. apply cl_S. apply cl_K. Qed. End CoqInCoq.