(** * Natural numbers Natural numbers are pre-defined in Coq, as shown by the next query. Syntactic sugar is also available to write e.g. [2] instead of [S (S O)]. *) Print nat. Goal 2 = S (S O). Proof. reflexivity. Qed. (** The inductive definition of [nat] is outside of the capabilities of first-order logic: it has a number of implicit consequences shown next. Note here the use of [inversion] on equalities between constructors of the inductive type [nat]. *) Goal forall x:nat, O <> S x. Proof. intros x H. inversion H. Qed. Goal forall x y : nat, S x = S y -> x = y. Proof. intros x y H. inversion H. reflexivity. Qed. (** We can use [destruct] to perform case analysis over a natural number. *) Goal forall x:nat, x = O \/ exists y:nat, x = S y. Proof. intro x. destruct x. + left. reflexivity. + right. exists x. reflexivity. Qed. (** An induction principle is also derived from the inductive definition, which is implicitly used through the [induction] tactic. Note that the induction principle is a higher-order formula, quantifying over [Prop]. *) Check nat_ind. Lemma Sx_x : forall x:nat, S x <> x. Proof. intros x H. induction x. + inversion H. + inversion H. apply IHx. exact H1. Qed. (** * Addition [x+y] is a notation for [plus x y]. Unlike in first-order logic, [plus] is not an abstract function symbol whose interpretation is constrained by axioms. Rather, it is defined as a recursive function over natural numbers. In Coq, all functions are total: termination is guaranteed and there are no errors. *) Print plus. (** In the next proof we use simpl to compute [1+1]. Note that the proof script works without this explicit simplification step. *) Goal 2 = 1+1. Proof. simpl. reflexivity. Qed. Goal forall x y : nat, S x + y = S (x+y). Proof. intros. reflexivity. Qed. (** The next proofs are not obvious computations for Coq: induction will be needed instead. In order to use an equality hypothesis, you will need the [rewrite] tactic. *) Goal forall x y z : nat, x = y -> x + z = y + z. Proof. intros x y z Heq. rewrite Heq. reflexivity. Qed. Lemma plus_S : forall x y : nat, x + S y = S (x + y). Proof. Admitted. Lemma plus_O : forall x:nat, x + O = x. Proof. Admitted. Lemma commutativity : forall x y : nat, x + y = y + x. Proof. Admitted. (** * Order [x <= y] is a notation for [le x y], where [le] is inductively defined as shown by the next query. The constructors [le_n] and [le_S] that define [le] can be used as hypothesis / lemmas e.g. in the [apply] tactic. *) Print le. Goal le 2 3. Proof. apply le_S. apply le_n. Qed. (** If [x <= y] holds it must have been obtained through one of the two constructors: the corresponding case analysis rule is given by the [inversion] tactic. *) Goal forall x y : nat, x <= y -> x = y \/ x <= pred y. Proof. intros x y H. inversion H. + left. reflexivity. + right. (* The next step is optional, it helps you see what's identical for Coq: [simpl] computes what can be computed. *) simpl. exact H0. Qed. Theorem le_O : forall x:nat, O <= x. Proof. Admitted. Theorem le_S_S : forall x:nat, forall y:nat, S x <= S y -> x <= y. Proof. Admitted. (** [x x <= y. Proof. Admitted. Theorem lt_S_case : forall x:nat, forall y:nat, x < S y -> x = y \/ x < y. Proof. Admitted. (** * Strong induction With the above ingredients, you should be able to prove a strong induction principle, expressed using a quantification over natural number predicates. *) Theorem strong_induction : forall (P:nat->Prop), (forall x:nat, (forall y:nat, y < x -> P y) -> P x) -> (forall x:nat, P x). Proof. Admitted. (** * Reasoning about multiples One last exercise for this tutorial! *) Inductive multiple : nat -> nat -> Prop := | multiple_O : forall n:nat, multiple n O | multiple_step : forall n:nat, forall m:nat, multiple n m -> multiple n (n+m). Goal forall x:nat, multiple 2 x -> multiple 3 x -> multiple 6 x. Proof. Admitted.