(** Introduction to Formal Reasoning (G52IFR) Nuo Li T07 **) Section CW4. Load Arith. Theorem mult_0_r : forall n, n * 0 = 0. intros. induction n. simpl. reflexivity. simpl. assumption. Qed. Theorem mult_comm : forall n m, n * m = m * n. intro n. induction n. simpl. symmetry. apply mult_0_r. intro. simpl. rewrite IHn. clear IHn. induction m. simpl. split. simpl. rewrite <- IHm. rewrite plus_assoc. pattern (m + n). rewrite plus_comm. rewrite plus_assoc. reflexivity. Qed. Theorem mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. induction n. simpl. reflexivity. intros. simpl. rewrite IHn. rewrite plus_assoc. split. Qed. (* How to prove it simply *) Theorem mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. intros. rewrite mult_comm. rewrite mult_plus_distr_r. rewrite mult_comm. pattern (p * n). rewrite mult_comm. reflexivity. Qed. Theorem mult_assoc : forall n m p, n * (m * p) = n * m * p. induction n. simpl. reflexivity. intros. simpl. rewrite IHn. rewrite mult_plus_distr_r. reflexivity. Qed. Notation "m <= n" := (leq m n). Theorem le_asym : forall (m n : nat), m <= n -> n <= m -> m=n. unfold leq. intros. destruct H. destruct H0. destruct x0. simpl in H0. assumption. rewrite H in H0. assert False. clear H. induction m. simpl in H0. discriminate H0. apply IHm. apply peano8. rewrite plus_n_Sm. rewrite plus_n_Sm. assumption. destruct H1. Qed. End CW4. Section CoqInCoq. Require Bool. Open Scope bool_scope. (* We define a type of boolean expressions with one variable. *) Inductive Expr : Set := | var : Expr | not : Expr -> Expr | and : Expr -> Expr -> Expr | or : Expr -> Expr -> Expr. (* To understand what is an "Expr", write an example *) Fixpoint eval (e : Expr)(x : bool) : bool := match e with | var => x | not e => negb (eval e x) | and e1 e2 => (eval e1 x) && (eval e2 x) | or e1 e2 => (eval e1 x) || (eval e2 x) end. Eval compute in (eval (and (not var) var) true). (** A small hint : To get an idea of compose, you should first understand what you have to prove Theorem composeThm : forall (e1 e2 : Expr)(b : bool), eval (compose e1 e2) b = eval e1 (eval e2 b). **) End CoqInCoq. Section Meta. 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. (* A 'coq' in coq, think them inversely *) Inductive ND_Proof : Hyps -> Formula -> Prop := (* Assumption *) | nd_ass : forall (Hs : Hyps)(P : Formula), ND_Proof (P :: Hs) P (* Weaken the Hs *) | nd_weak : forall (Hs : Hyps)(P Q : Formula), ND_Proof Hs P -> ND_Proof (Q :: Hs) P | nd_intro : forall (Hs : Hyps)(P Q : Formula), ND_Proof (P :: Hs) Q -> ND_Proof Hs (P ==> Q) | nd_apply : forall (Hs : Hyps)(P Q : Formula), ND_Proof Hs (P ==> Q) -> ND_Proof Hs P -> ND_Proof Hs Q (* The nd_split rule corresponds exactly to the split tactic. *) | nd_split : forall (Hs : Hyps)(P Q : Formula), ND_Proof Hs P -> ND_Proof Hs Q -> ND_Proof Hs (P //\\ Q) (* Our version of destruct is slightly different than the one implemented in Coq. Can you see the difference? *) | nd_destruct : forall (Hs : Hyps)(P Q R : Formula), ND_Proof (P :: Q :: Hs) R -> ND_Proof Hs (P //\\ Q) -> ND_Proof Hs R. (* eapply and eexact are important here *) Lemma nd_intro' : forall Hs P Q, ND_Proof (P :: Hs) Q -> (ND_Proof Hs P -> ND_Proof Hs Q) . intros. eapply nd_apply. apply nd_intro. eexact H. assumption. Qed. Lemma nd_apply' : forall (Hs : Hyps)(P Q : Formula), ND_Proof Hs (P ==> Q) -> ND_Proof (P :: Hs) Q. intros. eapply nd_apply. apply nd_weak. eexact H. apply nd_ass. Qed. Lemma nd_destruct' : forall (Hs : Hyps)(P Q R : Formula), ND_Proof (P :: Q :: Hs) R -> ND_Proof (P //\\ Q :: Hs) R. intros. eapply nd_apply. eapply nd_apply. apply nd_weak. apply nd_intro. apply nd_intro. eexact H. eapply nd_destruct. apply nd_weak. apply nd_ass. apply nd_ass. eapply nd_destruct. apply nd_ass. apply nd_ass. Qed. 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 cl_I : forall (Hs : Hyps)(P : Formula), CL_Proof Hs (P ==> P). intros. eapply cl_apply. eapply cl_apply. apply cl_S. apply cl_K. instantiate (1 := P ==> P). apply cl_K. Qed. (* You should extend this as well *) Lemma cl_intro : forall (Hs : Hyps)(P Q : Formula), CL_Proof (P :: Hs) Q -> CL_Proof Hs (P ==> Q). intros. dependent induction H. apply cl_I. eapply cl_apply. apply cl_K. exact H. eapply cl_apply. apply cl_K. apply cl_K. eapply cl_apply. apply cl_K. apply cl_S. (* You should find the general ways to prove the rest of them. Try to finish this by yourself, because they are part of your coureswork *) (* For combinatory logic : http://en.wikipedia.org/wiki/Combinatory_logic http://en.wikipedia.org/wiki/SKI_combinator_calculus *) (** Optional : Think of how to prove this (in CL) before next tutorial **) Lemma nd_compose_f : forall (Hs : Hyps)(P Q R : Formula), CL_Proof Hs ((P ==> Q) ==> (Q ==> R) ==> (P ==> R)). End Meta.