(** * 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.