(** Introduction to Formal Reasoning (G52IFR) Nuo Li T05 **) Section CW2. Variable People : Set. Variables Male Female : People -> Prop. (* Male x = x is a male Female x = x is a female *) Variable Parent : People -> People -> Prop. (* Parent x y = x is the parent of y *) Definition Father (x y : People) := Male x /\ Parent x y. Definition Mother (x y : People) := Female x /\ Parent x y. Definition Sibling (x y : People) := ~ (x = y) /\ exists p : People, Parent p x /\ Parent p y. Definition halfSibling (x y : People) := Sibling x y /\ (exists p, (Parent p x /\ ~ Parent p y) \/ (Parent p y /\ ~Parent p x)). Definition halfSibling2 (x y : People) := ~ ((exists f : People, Father f x /\ Father f y) <-> (exists m : People, Mother m x /\ Mother m y)). Require Import Coq.Logic.Classical. Variable A B : Set. Variable P : A -> Prop. Variables R : A -> B -> Prop. Lemma demorgan2 : (~ forall x : A, P x) <-> exists x : A, ~ P x. split; intro. apply NNPP. intro. apply H. intro. apply NNPP. intro. apply H0. exists x. assumption. destruct H. intro. apply H. apply H0. Qed. Lemma dp : (exists x:A, True) -> exists x:A, P x -> forall x:A, P x. intros. destruct H. destruct (classic (forall x : A, P x)). exists x. intro. exact H0. assert (exists x0 : A, ~P x0). apply demorgan2. exact H0. destruct H1. exists x0. intro. destruct (H1 H2). Qed. End CW2. Section T5. Load Arith. (** try to find out some useful lemmas in Arith **) Lemma n_Sn : forall n : nat, n <> S n. intro. intro. induction n. discriminate H. apply IHn. apply peano8. assumption. Qed. Lemma eq_les_S : forall m n : nat, m = n -> S m = S n. intros. rewrite H. reflexivity. Qed. Lemma eq_add_S : forall m n, S m = S n -> m = n. intros. fold (pred (S m)). rewrite H. unfold pred. reflexivity. Qed. Fixpoint g (m n : nat) {struct m} : nat := match m with | 0 => n | S m' => S (g m' n) end. (* What is g? Try a few examples *) Eval compute in (g 1 2). Eval compute in (g 10 12). (* How to define mutiplication *) Fixpoint mul (m n : nat) {struct m} : nat := match m with | 0 => 0 | S m' => n + (mul m' n) end. (* The decidable even function *) Fixpoint even (m : nat) : bool := match m with | 0 => true | S m' => negb (even m') end. Theorem nneven : forall n: nat, even (n + n) = true. intro. induction n. simpl. reflexivity. simpl. rewrite plus_comm. simpl. rewrite IHn. simpl. reflexivity. Qed. Theorem sym : forall a b : nat, a = b -> b = a. intros. symmetry. assumption. Qed. (* These should be proved by yourselves *) Axiom mult_comm : forall n m, n * m = m * n. Axiom mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. Axiom mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. Theorem binomial : forall m n : nat, (m + n) * (m + n) = m * m + 2 * m * n + n * n. intros. rewrite mult_plus_distr_r. rewrite mult_plus_distr_l. rewrite mult_plus_distr_l. rewrite plus_assoc. assert (m * n + n * m = 2 * m * n). simpl. rewrite<- plus_n_O. rewrite mult_plus_distr_r. pattern (n * m). rewrite mult_comm. reflexivity. rewrite<- H. rewrite plus_assoc. reflexivity. Qed. Lemma t2 : forall n, n = S n -> n = n + 1. intros. destruct (n_Sn n H). Qed. (* Do not erase the following line in your cw *) Notation "m <= n" := (leq m n). Theorem le2n : forall n : nat, n <= (n + n). intro. unfold leq. exists n. reflexivity. Qed. (**To prove Even is decidable (optional) Notice : the proofs use inversion which may not be allowed to use in cw, here just the idea of how to prove some predicates are decidable **) Inductive Even : nat -> Prop := | z : Even 0 | e : forall n: nat, Even n -> Even (S (S n)). Lemma even_odd : forall n, exists k, n = k + k \/ n = S (k + k). induction n. exists 0. left. split. destruct IHn. destruct H. exists x. right. rewrite H. split. exists (S x). left. rewrite H. rewrite plus_n_Sm. split. Qed. Lemma double_even : forall k, even (k + k) = true. intros. induction k. split. rewrite<- plus_n_Sm. simpl. rewrite IHk. split. Qed. Lemma double_Even : forall k, Even (k + k). intros. induction k. exact z. rewrite<- plus_n_Sm. exact (e (k + k) IHk). Qed. Lemma not_Even : forall k, ~ Even (S (k + k)). intros. intro. induction k. inversion H. apply IHk. rewrite<- plus_n_Sm in H. inversion H. exact H1. Qed. Theorem e_sound : forall m, Even m -> even m = true. intros. destruct (even_odd m). destruct H0. rewrite H0. apply double_even. rewrite H0 in H. destruct (not_Even x H). Qed. Theorem e_compl : forall m, even m = true -> Even m. intros. destruct (even_odd m). destruct H0. rewrite H0. apply double_Even. rewrite H0. rewrite H0 in H. simpl in H. rewrite double_even in H. discriminate H. Qed. Theorem e_dec : forall m, Even m <-> even m = true. split. apply e_sound. apply e_compl. Qed. End T5.