Module Shadow_Nat. Inductive nat : Set := | Z : nat (* Coq uses the letter O, alas *) | S : nat -> nat. (* Special Coq shorthand for predefined nats: 0, 1, 2... *) (* definition of recursive function *) Fixpoint plus (n : nat) (m : nat) : nat := match n with | Z => m | S n' => S (plus n' m) end. (* telling Coq about infix notation *) Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope. Fixpoint mult (n m : nat) : nat := match n with | Z => Z | S n' => plus m (mult n' m) end. Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope. Definition pred (n: nat) : nat := match n with | Z => Z | (S n') => n' end. Theorem pred_removes_S : forall n, n = pred (S n). Proof. reflexivity. Qed. Theorem S_injective : forall n m, S n = S m -> n = m. Proof. intros n m H. rewrite pred_removes_S. rewrite <- H. reflexivity. Qed. Theorem S_injective' : forall n m, S n = S m -> n = m. Proof. intros n m H1. assert (H2: n = pred (S n)). { reflexivity. } rewrite H1 in H2. rewrite H2. reflexivity. Qed. Theorem S_injective'' : forall n m, S n = S m -> n = m. Proof. intros n m H. injection H. intros H1. apply H1. Qed. Definition disc_fn (n: nat) : Prop := match n with | Z => True | S _ => False end. Theorem disc2 : ~ (Z = S Z). Proof. intro H1. assert (H2 : disc_fn Z). { apply I. } rewrite H1 in H2. apply H2. Qed. Theorem disc1 : ~ (Z = S Z). Proof. intro H. discriminate H. Qed. Theorem plus_n_0 : forall n, n + Z = n. Proof. intros n. case n. - reflexivity. - intros n0. simpl. Abort. Theorem plus_n_0 : forall n, n + Z = n. Proof. intros n. destruct n. - reflexivity. - simpl. Abort. Theorem plus_n_0 : forall n, n + Z = n. Proof. intros [ | n']. - reflexivity. - simpl. Abort. Check nat_ind. Check nat_rect. Print nat_rect. Theorem plus_n_0 : forall n, n + Z = n. Proof. apply nat_ind. - reflexivity. - intros n IH. simpl. rewrite IH. reflexivity. Qed. Theorem plus_n_0' : forall n, n + Z = n. Proof. intro n. elim n. - reflexivity. - intros n0 IH. simpl. rewrite IH. reflexivity. Qed. Theorem plus_n_0'' : forall n, n + Z = n. Proof. induction n. - reflexivity. - simpl. rewrite IHn. reflexivity. Qed. Theorem plus_n_0''' : forall n, n + Z = n. Proof. induction n as [| n' IHn']. - reflexivity. - simpl. rewrite IHn'. reflexivity. Qed. (* evenness *) Inductive ev : nat -> Prop := | ev_0 : ev Z | ev_SS : forall n : nat, ev n -> ev (S (S n)). Example ev_zero : ev Z. Proof. apply ev_0. Qed. Example ev_four : ev (S (S (S (S Z)))). Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed. Theorem ev_minus2' : forall n, ev n -> ev (pred (pred n)). Proof. intros n E. destruct E as [| n' E']. - (* E = ev_0 *) simpl. apply ev_0. - (* E = ev_SS n' E' *) simpl. apply E'. Qed. Theorem evSS_ev : forall n, ev (S (S n)) -> ev n. Proof. intros n H. destruct H. Abort. Theorem ev_inversion : forall (n : nat), ev n -> (n = Z) \/ (exists n', n = S (S n') /\ ev n'). Proof. intros n Hev. destruct Hev as [ | n' Hn']. - left. reflexivity. - right. exists n'. split. reflexivity. apply Hn'. Qed. Theorem evSS_ev : forall n, ev (S (S n)) -> ev n. Proof. intros n H. apply ev_inversion in H. destruct H. - discriminate H. - destruct H as [n' [Hnn' Hevn']]. injection Hnn'. intro Heq. rewrite Heq. apply Hevn'. Qed. Theorem evSS_ev' : forall n, ev (S (S n)) -> ev n. Proof. intros n H. inversion H as [| x Hn Hx]. apply Hn. Qed. Theorem one_not_even : ~ ev (S Z). Proof. intros H. apply ev_inversion in H. destruct H as [ | [n' [Hn' _]]]. - discriminate H. - discriminate Hn'. Qed. Theorem one_not_even' : ~ ev (S Z). intros H. inversion H. Qed. (* definition of <= as inductive proposition *) Inductive le : nat -> nat -> Prop := | le_n : forall n, le n n | le_S : forall n m, (le n m) -> (le n (S m)). Check le_ind. Notation "m <= n" := (le m n). Definition lt (n m:nat) := le (S n) m. Notation "m < n" := (lt m n). Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. Proof. intros n m p H1 H2. induction H2 as [m | m p' H IH]. - apply H1. - apply le_S. apply IH. apply H1. Qed. (* definition of the = relation as an inductive proposition *) Inductive EQ {A : Type} (x : A) : A -> Type := | eq_refl': EQ x x. Check EQ_ind. Print EQ_rect. (* predefined has 'eq', 'eq_refl', and notation for infix = *) (* above done in lecture *) (* below is homework *) Fixpoint nateq (n m : nat) : bool := match n with | Z => match m with | Z => true | S _ => false end | S n' => match m with | Z => false | S m' => nateq n' m' end end. (* Below is homework *) (* Replace 'Admitted.' with a proper proof ending with Qed. *) (* eq_is_nateq : 3 points *) Theorem eq_is_nateq : forall n m, n = m -> nateq n m = true. Admitted. (* nateq_is_eq : 3 points *) Theorem nateq_is_eq : forall n m, nateq n m = true -> n = m. Admitted. (* Z_le_n : 1 point *) Theorem Z_le_n : forall n, Z <= n. Admitted. (* Sn_le_n_le : 2 points *) Theorem Sn_le_n_le : forall n m, S n <= m -> n <= m. Admitted. (* S_le_m_n : 2 points *) Theorem S_le_m_n : forall n m, (S n <= S m) -> n <= m. Admitted. (* not_Sn_le_n : 3 points *) Theorem not_Sn_le_n : forall n, ~ (S n <= n). Admitted. (* S_fn : 1 point *) Theorem S_fn : forall n m, n = m -> S n = S m. Admitted. (* both_les_eq : 4 points *) Theorem both_les_eq : forall n m, n <= m -> m <= n -> n = m. Admitted. End Shadow_Nat.