# Natural numbers

Check 5.

Check 5+5.

and how to compute with them

Eval compute in 5*5.

these are `unary' numbers, built out of 0 and S (successor)

Set Printing All.
Check 5.
Unset Printing All.

a definition by case, to compute the predecessor

Definition pred n :=
match n with
| 0 ⇒ 0
| S nn
end.

Eval compute in pred 5.

a recursive definition by case, to compute addition

Fixpoint plus n m :=
match n with
| 0 ⇒ m
| S nS (plus n m)
end.

Eval compute in plus 5 5.

Infix "+" := plus: nat_scope.

Check 5+5.

Lemma plus_0n: n, 0+n = n.
Proof.
intro n.
simpl.
reflexivity.
Qed.

Lemma plus_n0: n, n+0 = n.
Proof.
induction n.
reflexivity.
simpl. rewrite IHn. reflexivity.
Qed.

Lemma plus_assoc: n m p, n+(m+p) = (n+m)+p.
Proof.
intros n m p.
induction n.
reflexivity.
simpl. now rewrite IHn.
Qed.

Lemma plus_nS: n m, n+(S m) = S (n+m).
Proof.
intros n m.
induction n.
reflexivity.
simpl. now rewrite IHn.
Qed.

Lemma plus_comm: n m, n+m = m+n.
Proof.
intros n m.
induction n; simpl.
- rewrite plus_n0. reflexivity.
- rewrite plus_nS, IHn. reflexivity.
Qed.

define multiplication, and prove a few properties about it

Fixpoint mult n m :=
match n with
| 0 ⇒ 0
| S nm + mult n m
end.

Infix "*" := mult: nat_scope.

Lemma mult_n0: n, n*0 = 0.
Proof.
now induction n.
Qed.

Lemma mult_nS: n m, n*(S m) = n+n×m.
Proof.
intros n m.
induction n.
reflexivity.
simpl. rewrite IHn. rewrite 2plus_assoc, (plus_comm m). reflexivity.
Qed.

Lemma mult_comm: n m, n×m = m×n.
Proof.
intros n m.
induction n; simpl.
- now rewrite mult_n0.
- now rewrite mult_nS, IHn.
Qed.

Lemma mult_distr_plus_l: n m p, (n+m)*p = n×p+m×p.
Proof.
intros n m p.
induction n.
- reflexivity.
- simpl. rewrite IHn. apply plus_assoc.
Qed.

Lemma mult_assoc: n m p, n*(m×p) = (n×m)*p.
Proof.
intros n m p.
induction n.
reflexivity.
simpl. now rewrite IHn, mult_distr_plus_l.
Qed.

Lemma mult_distr_plus_r: n m p, p*(n+m) = p×n+p×m.
Proof.
intros n m p. rewrite mult_comm, mult_distr_plus_l, 2(mult_comm p). reflexivity.
Qed.

Lemma remarquable: n m, (n+m)*(n+m) = n×n + 2*n×m + m×m.
Proof.
intros n m.
rewrite mult_distr_plus_r, 2mult_distr_plus_l.
rewrite (mult_comm m).
simpl. rewrite 2mult_distr_plus_l.
simpl. rewrite plus_n0.
rewrite 2plus_assoc.
reflexivity.
Qed.

## high-level tactics

NB: the above lemmas can be proved by a single call to the ring tactic, which solves polynomial equations over rings

Require Import Peano Arith.

Lemma remarquable': n m: nat, (n+m)*(n+m) = n×n + 2*n×m + m×m.
Proof. intros. ring. Qed.

Another useful high-level tactic is lia, which solves linear (in)equations over integers

Require Import Psatz.

Goal n m p, n < mp → 2*p-m < 2*p-n.
Proof. intros. lia. Qed.

Goal n m p, n < mp → ~(p<n).
Proof. intros. lia. Qed.

Goal n m, nmm - (m - n) = n.
Proof. intros. lia. Qed.

Goal n m, m - (m - n) = nm < n.
Proof. intros. lia. Qed.

x double recursion scheme

Lemma nat_ind_2 (P: natProp):
P 0 → P 1 → ( n, P nP (2+n)) → n, P n.
Proof.
intros H0 H1 HSS.
assert (G: m, P mP (S m)).
induction m. split; assumption.
split. apply IHm. apply HSS, IHm.
apply G.
Qed.

xx strong recursion scheme

Require Import Peano_dec Lt.
Lemma nat_ind_lt (P: natProp):
( n, ( m, m<nP m) → P n) → n, P n.
Proof.
intros HP.
assert (G: n m, m<nP m).
induction n; intros m Hm.
lia.
case (eq_nat_dec m n).
intros →. apply HP, IHn.
intro D. apply IHn. lia.
intro n. apply (G (S n) n). lia.

below: same proof without lia
Restart.
intros HP.
assert (G: n m, m<nP m).
induction n; intros m Hm.
inversion Hm.
case (eq_nat_dec m n).
intros →. apply HP, IHn.
intro D. apply IHn. apply nat_total_order in D as [D|D]. assumption.
apply lt_n_Sm_le in Hm. apply (le_lt_trans _ _ _ Hm) in D.
destruct (lt_irrefl _ D).
intro n. apply (G (S n) n). apply lt_n_Sn.
Qed.