Library s2_nat

Natural numbers

Coq knows about 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.

now we prove properties about addition

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.

additional exercises

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.
Check eq_nat_dec. SearchAbout 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.


This page has been generated by coqdoc