Section Peano. (* Peano arithmetics is built up on the following definition of natural numbers: Inductive nat: Set := | O : nat | S : nat -> nat. This declaration defines a series of names, starting with nat: Set (* nat is the set of natural numbers*) O : nat (* O is a natural number, signifying zero *) S : nat -> nat (* the successor function S*) Numbers can be written in the normal way, but behind the scene it is constructed from O-s and S-s. 0 ≡ O 1 ≡ S O 2 ≡ S S O 3 ≡ S S S O 4 ≡ S S S S O ... *) (*1*) Theorem eq_S : forall n m:nat, n = m -> S n = S m. Proof. Qed. (* There are two introduction rules: "apply O" and "apply S". To eliminate some natural number, you can firstly use "destruct" to separate into cases where the number is zero or larger than zero. Γ├ P 0 Γ, m: nat├ P (S m) ------------------------------------------ destruct n as [|m] Γ, n: nat├ P n *) (*2*) Lemma varIsZeroOrLarger: forall n, n = 0 \/ (exists m, S m = n). Proof. Qed. (* Now we look at two ways how to prove "forall n, S n <> O". It is more tricky than you may think, unless we use the "discriminate" rule. But first, we try to get by without discrimination. Look at the definition and prove the two following lemmas. *) Definition Is_zero (x: nat) := match x with | 0 => True | (S _) => False end. (* Is_zero looks at the number it is given as an argument, and returns True for zero and False for bigger arguments. Note that it is an definition --- you can unfold it. *) (*3*) Lemma O_is_zero: forall m, m = 0 -> Is_zero m. Proof. Qed. (* As in "fold" and "unfold", you can use the "in ..." part also in "apply" and "rewrite" : Γ, p: A -> B, q: B├ C ----------------------------- apply p in q Γ, p: A -> B, q: A├ C Prove the following by using the previous lemma. *) (*4*) Theorem S_is_not_O: forall n, S n <> O. Proof. Qed. (* Prove the same thing by using the "discriminate p" meta-rule (tactic). It proves inequalities that contain varables such that instanciating the variables cannot give you the equality. There is no natural number n such that "S n = O". Inside, it goes through the same steps as we did before. *) (*5*) Theorem S_is_not_O_2: forall n, S n <> O. Proof. Qed. (* The reason why we look at Peano arithmetics, is that it gives us a simple setting to use induction --- the true elimination rule of natural numbers. Γ├ P O Γ, m: nat, p: P m├ P (S m) ----------------------------------------------------- induction n as [|m p] Γ, n: nat├ P n It can, for example, be used insread of the "destruct" rule. *) (*6*) Lemma exPred: forall n: nat, n=0 \/ (exists m: nat, S m = n). Proof. Qed. (* Lets look at addition. It is defined as Fixpoint plus (n m:nat) : nat := match n with | O => m | S p => S (plus p m) end. Notation "n + m" := (plus n m). A "Fixpoint" definiton is similar to a normal definition, but it can be recursive. If a definition is recursive and it has a "match" in it, then that can be taken as a hint to use induction on the variable that is matched over. A trick to simplify an arithmetic expression is to identify some operation where the definition can be unrolled, then apply unfold and then immediately fold. *) (*7*) Lemma plus_n_O : forall n:nat, n = n + 0. Proof. Qed. (*8*) Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). Proof. Qed. (*9*) Lemma plus_O_n : forall n:nat, 0 + n = n. Proof. Qed. (*10*) Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. Qed. (*11*) Lemma plus_sym: forall n m: nat, n + m = m + n. Proof. Qed. (*12*) Lemma plus_assoc_reverse: forall m n k:nat, (m+n)+k = m+(n+k). Proof. Qed. (*13*) Lemma eq_add_n: forall n m k, m=k -> n + m = n + k. Proof. Qed. (*14*) Lemma plus_permute: forall n m k, n + (m + k) = m + (n+k). Proof. Qed. (*15*) Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. Proof. Qed. (*16*) Lemma add_diff: forall x y, exists p, x + y = S (y + p). Proof. Qed. (*17*) Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m. Proof. Qed. (*18*) Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0. Proof. Qed. (*19*) Lemma succ_plus_discr : forall n m, n <> S (m + n). Proof. Qed. End Peano.