Core.v

(* -*- mode: coq; mode: visual-line -*- *)
Require Import Basics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export Basics.Nat.

Local Set Universe Minimization ToSet.

Local Unset Elimination Schemes.

Scheme nat_ind := Induction for nat Sort Type.
Scheme nat_rect := Induction for nat Sort Type.
Scheme nat_rec := Minimality for nat Sort Type.

(** * Theorems about the natural numbers *)

(** Many of these definitions and proofs have been ported from the coq stdlib. *)

(** Some results are prefixed with [nat_] and some are not.  Should we be more consistent? *)

(** We want to close the trunc_scope so that notations from there don't conflict here. *)
Local Close Scope trunc_scope.
Local Open Scope nat_scope.

(** ** Basic operations on naturals *)

(** It is common to call [S] [succ] so we add it as a parsing only notation. *)
Notation succ := S (only parsing).

(** The predecessor of a natural number. *)
Definition pred n : nat :=
  match n with
  | 0 => n
  | S n' => n'
  end.

(** Addition of natural numbers *)
Fixpoint add n m : nat :=
  match n with
  | 0 => m
  | S n' => S (add n' m)
  end.

Notation "n + m" := (add n m) : nat_scope.

Definition double n : nat := n + n.

Fixpoint mul n m : nat :=
  match n with
  | 0 => 0
  | S n' => m + (mul n' m)
  end.

Notation "n * m" := (mul n m) : nat_scope.

(** Truncated subtraction: [n - m] is [0] if [n <= m] *)
Fixpoint sub n m : nat :=
  match n, m with
  | S n' , S m' => sub n' m'
  | _ , _ => n
  end.

Notation "n - m" := (sub n m) : nat_scope.

(** ** Minimum, maximum *)

Fixpoint max n m :=
  match n, m with
  | 0 , _ => m
  | S n' , 0 => n'.+1
  | S n' , S m' => (max n' m').+1
  end.

Fixpoint min n m :=
  match n, m with
  | 0 , _ => 0
  | S n' , 0 => 0
  | S n' , S m' => S (min n' m')
  end.

(** ** Power *)

Fixpoint pow n m :=
  match m with
  | 0 => 1
  | S m' => n * (pow n m')
  end.

(** ** Euclidean division *)

(** This division is linear and tail-recursive. In [divmod], [y] is the predecessor of the actual divisor, and [u] is [y] sub the real remainder. *)

Fixpoint divmod x y q u : nat * nat :=
  match x with
  | 0 => (q , u)
  | S x' =>
    match u with
    | 0 => divmod x' y (S q) y
    | S u' => divmod x' y q u'
    end
  end.

Definition div x y : nat :=
  match y with
    | 0 => y
    | S y' => fst (divmod x y' 0 y')
  end.

Definition modulo x y : nat :=
  match y with
    | 0 => y
    | S y' => y' - snd (divmod x y' 0 y')
  end.

Infix "/" := div : nat_scope.
Infix "mod" := modulo : nat_scope.

(** ** Greatest common divisor *)

(** We use Euclid algorithm, which is normally not structural, but Coq is now clever enough to accept this (behind modulo there is a subtraction, which now preserves being a subterm) *)

Fixpoint gcd a b :=
  match a with
  | O => b
  | S a' => gcd (b mod a'.+1) a'.+1
  end.

(** ** Square *)

Definition square n : nat := n * n.

(** ** Square root *)

(** The following square root function is linear (and tail-recursive).
  With Peano representation, we can't do better. For faster algorithm,
  see Psqrt/Zsqrt/Nsqrt...

  We search the square root of n = k + p^2 + (q - r)
  with q = 2p and 0<=r<=q. We start with p=q=r=0, hence
  looking for the square root of n = k. Then we progressively
  decrease k and r. When k = S k' and r=0, it means we can use (S p)
  as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2.
  When k reaches 0, we have found the biggest p^2 square contained
  in n, hence the square root of n is p.
*)

Fixpoint sqrt_iter k p q r : nat :=
  match k with
  | O => p
  | S k' =>
    match r with
    | O => sqrt_iter k' p.+1 q.+2 q.+2
    | S r' => sqrt_iter k' p q r'
    end
  end.

Definition sqrt n : nat := sqrt_iter n 0 0 0.

(** ** Log2 *)

(** This base-2 logarithm is linear and tail-recursive.

  In [log2_iter], we maintain the logarithm [p] of the counter [q],
  while [r] is the distance between [q] and the next power of 2,
  more precisely [q + S r = 2^(S p)] and [r<2^p]. At each
  recursive call, [q] goes up while [r] goes down. When [r]
  is 0, we know that [q] has almost reached a power of 2,
  and we increase [p] at the next call, while resetting [r]
  to [q].

  Graphically (numbers are [q], stars are [r]) :

<<
                    10
                  9
                8
              7   *
            6       *
          5           ...
        4
      3   *
    2       *
  1   *       *
0   *   *       *
>>

  We stop when [k], the global downward counter reaches 0.
  At that moment, [q] is the number we're considering (since
  [k+q] is invariant), and [p] its logarithm.
*)

Fixpoint log2_iter k p q r : nat :=
  match k with
  | O    => p
  | S k' =>
    match r with
    | O => log2_iter k' (S p) (S q) q
    | S r' => log2_iter k' p (S q) r'
    end
  end.

Definition log2 n : nat := log2_iter (pred n) 0 1 0.

Local Definition ap_S := @ap _ _ S.
Local Definition ap_nat := @ap nat.
#[export] Hint Resolve ap_S : core.
#[export] Hint Resolve ap_nat : core.

Theorem pred_Sn : forall n:nat, n = pred (S n).forall n : nat, n = pred n.+1
Proof.forall n : nat, n = pred n.+1
  auto.
Defined.

(** Injectivity of successor *)

Definition path_nat_S n m (H : S n = S m) : n = m := ap pred H.
#[export] Hint Immediate path_nat_S : core.

Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.forall n m : nat, n <> m -> n.+1 <> m.+1
Proof.forall n m : nat, n <> m -> n.+1 <> m.+1
  auto.
Defined.
#[export] Hint Resolve not_eq_S : core.

(** TODO: keep or remove? *)
Definition IsSucc (n: nat) : Type0 :=
  match n with
  | O => Empty
  | S p => Unit
  end.

(** Zero is not the successor of a number *)

Theorem not_eq_O_S : forall n:nat, 0 <> S n.forall n : nat, 0 <> n.+1
Proof.forall n : nat, 0 <> n.+1
  discriminate.
Defined.
#[export] Hint Resolve not_eq_O_S : core.

Theorem not_eq_n_Sn : forall n:nat, n <> S n.forall n : nat, n <> n.+1
Proof.forall n : nat, n <> n.+1
  simple_induction' n; auto.
Defined.
#[export] Hint Resolve not_eq_n_Sn : core.

Local Definition ap011_add := @ap011 _ _ _ add.
Local Definition ap011_nat := @ap011 nat nat.
#[export] Hint Resolve ap011_add : core.
#[export] Hint Resolve ap011_nat : core.

Lemma add_n_O : forall (n : nat), n = n + 0.forall n : nat, n = n + 0
Proof.forall n : nat, n = n + 0
  simple_induction' n; simpl; auto.
Defined.
#[export] Hint Resolve add_n_O : core.

Lemma add_O_n : forall (n : nat), 0 + n = n.forall n : nat, 0 + n = n
Proof.forall n : nat, 0 + n = n
  auto.
Defined.

Lemma add_n_Sm : forall n m:nat, S (n + m) = n + S m.forall n m : nat, (n + m).+1 = n + m.+1
Proof.forall n m : nat, (n + m).+1 = n + m.+1
  simple_induction' n; simpl; auto.
Defined.
#[export] Hint Resolve add_n_Sm: core.

Lemma add_Sn_m : forall n m:nat, S n + m = S (n + m).forall n m : nat, n.+1 + m = (n + m).+1
Proof.forall n m : nat, n.+1 + m = (n + m).+1
  auto.
Defined.

(** Multiplication *)

Local Definition ap011_mul := @ap011 _ _ _  mul.
#[export] Hint Resolve ap011_mul : core.

Lemma mul_n_O : forall n:nat, 0 = n * 0.forall n : nat, 0 = n * 0
Proof.forall n : nat, 0 = n * 0
  simple_induction' n; simpl; auto.
Defined.
#[export] Hint Resolve mul_n_O : core.

Lemma mul_n_Sm : forall n m:nat, n * m + n = n * S m.forall n m : nat, n * m + n = n * m.+1
Proof.forall n m : nat, n * m + n = n * m.+1
  intros; simple_induction n p H; simpl; auto.m, p: nat
H: p * m + p = p * m.+1
m + p * m + p.+1 = (m + p * m.+1).+1
  destruct H; rewrite <- add_n_Sm; apply ap.m, p: nat
m + p * m + p = m + (p * m + p)
  pattern m at 1 3; elim m; simpl; auto.
Defined.
#[export] Hint Resolve mul_n_Sm: core.

(** Standard associated names *)

Notation mul_0_r_reverse := mul_n_O (only parsing).
Notation mul_succ_r_reverse := mul_n_Sm (only parsing).

(** ** Equality of natural numbers *)

(** *** Boolean equality and its properties *)

(** [nat] has decidable paths *)
Global Instance decidable_paths_nat : DecidablePaths nat.DecidablePaths nat
Proof.DecidablePaths nat
  intros n; induction n as [|n IHn];
  intros m; destruct m.Decidable (0 = 0)
m: nat
Decidable (0 = m.+1)
n: nat
IHn: forall y : nat, Decidable (n = y)
Decidable (n.+1 = 0)
n: nat
IHn: forall y : nat, Decidable (n = y)
m: nat
Decidable (n.+1 = m.+1)
  -Decidable (0 = 0) exact (inl idpath).
  -m: nat
Decidable (0 = m.+1) exact (inr (not_eq_O_S m)).
  -n: nat
IHn: forall y : nat, Decidable (n = y)
Decidable (n.+1 = 0) exact (inr (fun p => not_eq_O_S n p^)).
  -n: nat
IHn: forall y : nat, Decidable (n = y)
m: nat
Decidable (n.+1 = m.+1) destruct (IHn m) as [p|q].n: nat
IHn: forall y : nat, Decidable (n = y)
m: nat
p: n = m
Decidable (n.+1 = m.+1)
n: nat
IHn: forall y : nat, Decidable (n = y)
m: nat
q: n <> m
Decidable (n.+1 = m.+1)
    +n: nat
IHn: forall y : nat, Decidable (n = y)
m: nat
p: n = m
Decidable (n.+1 = m.+1) exact (inl (ap S p)).
    +n: nat
IHn: forall y : nat, Decidable (n = y)
m: nat
q: n <> m
Decidable (n.+1 = m.+1) exact (inr (fun p => q (path_nat_S _ _ p))).
Defined.

(** And is therefore a HSet *)
Global Instance hset_nat : IsHSet nat := _.

(** ** Inequality of natural numbers *)

Cumulative Inductive leq (n : nat) : nat -> Type0 :=
| leq_n : leq n n
| leq_S : forall m, leq n m -> leq n (S m).

Scheme leq_ind := Induction for leq Sort Type.
Scheme leq_rect := Induction for leq Sort Type.
Scheme leq_rec := Minimality for leq Sort Type.

Notation "n <= m" := (leq n m) : nat_scope.
#[export] Hint Constructors leq : core.

Existing Class leq.
Global Existing Instances leq_n leq_S.

Notation leq_refl := leq_n (only parsing).
Global Instance reflexive_leq : Reflexive leq := leq_n.

Lemma leq_trans {x y z} : x <= y -> y <= z -> x <= z.x, y, z: nat
x <= y -> y <= z -> x <= z
Proof.x, y, z: nat
x <= y -> y <= z -> x <= z
  induction 2; auto.
Defined.

Global Instance transitive_leq : Transitive leq := @leq_trans.

Lemma leq_n_pred n m : leq n m -> leq (pred n) (pred m).n, m: nat
n <= m -> pred n <= pred m
Proof.n, m: nat
n <= m -> pred n <= pred m
  induction 1; auto.n, m: nat
H: n <= m
IHleq: pred n <= pred m
pred n <= pred m.+1
  destruct m; simpl; auto.
Defined.

Lemma leq_S_n : forall n m, n.+1 <= m.+1 -> n <= m.forall n m : nat, n.+1 <= m.+1 -> n <= m
Proof.forall n m : nat, n.+1 <= m.+1 -> n <= m
  intros n m.n, m: nat
n.+1 <= m.+1 -> n <= m
  apply leq_n_pred.
Defined.

Lemma leq_S_n' n m : n <= m -> n.+1 <= m.+1.n, m: nat
n <= m -> n.+1 <= m.+1
Proof.n, m: nat
n <= m -> n.+1 <= m.+1
  induction 1; auto.
Defined.
Global Existing Instance leq_S_n' | 100.

Lemma not_leq_Sn_n n : ~ (n.+1 <= n).n: nat
~ (n.+1 <= n)
Proof.n: nat
~ (n.+1 <= n)
  simple_induction n n IHn.~ (1 <= 0)
n: nat
IHn: ~ (n.+1 <= n)
~ (n.+2 <= n.+1)
  {~ (1 <= 0) intro p.p: 1 <= 0
Empty
    inversion p. }n: nat
IHn: ~ (n.+1 <= n)
~ (n.+2 <= n.+1)
  intros p.n: nat
IHn: ~ (n.+1 <= n)
p: n.+2 <= n.+1
Empty
  by apply IHn, leq_S_n.
Defined.

(** A general form for injectivity of this constructor *)
Definition leq_n_inj_gen n k (p : n <= k) (r : n = k) : p = r # leq_n n.n, k: nat
p: n <= k
r: n = k
p = transport (leq n) r (leq_n n)
Proof.n, k: nat
p: n <= k
r: n = k
p = transport (leq n) r (leq_n n)
  destruct p.n: nat
r: n = n
leq_n n = transport (leq n) r (leq_n n)
n, m: nat
p: n <= m
r: n = m.+1
leq_S n m p = transport (leq n) r (leq_n n)
  +n: nat
r: n = n
leq_n n = transport (leq n) r (leq_n n) assert (c : idpath = r) by apply path_ishprop.n: nat
r: n = n
c: 1 = r
leq_n n = transport (leq n) r (leq_n n)
    destruct c.n: nat
leq_n n = transport (leq n) 1 (leq_n n)
    reflexivity.
  +n, m: nat
p: n <= m
r: n = m.+1
leq_S n m p = transport (leq n) r (leq_n n) destruct r^.m: nat
p: m.+1 <= m
r: m.+1 = m.+1
leq_S m.+1 m p = transport (leq m.+1) r (leq_n m.+1)
    contradiction (not_leq_Sn_n _ p).
Defined.

(** Which we specialise to this lemma *)
Definition leq_n_inj n (p : n <= n) : p = leq_n n
  := leq_n_inj_gen n n p idpath.

Fixpoint leq_S_inj_gen n m k (p : n <= k) (q : n <= m) (r : m.+1 = k)
  : p = r # leq_S n m q.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m, k: nat
p: n <= k
q: n <= m
r: m.+1 = k
p = transport (leq n) r (leq_S n m q)
Proof.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m, k: nat
p: n <= k
q: n <= m
r: m.+1 = k
p = transport (leq n) r (leq_S n m q)
  revert m q r.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, k: nat
p: n <= k
forall (m : nat) (q : n <= m) (r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
  destruct p.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n: nat
forall (m : nat) (q : n <= m) (r : m.+1 = n),
leq_n n = transport (leq n) r (leq_S n m q)
leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m: nat
p: n <= m
forall (m0 : nat) (q : n <= m0) 
(r : m0.+1 = m.+1),
leq_S n m p = transport (leq n) r (leq_S n m0 q)
  +leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n: nat
forall (m : nat) (q : n <= m) (r : m.+1 = n),
leq_n n = transport (leq n) r (leq_S n m q) intros k p r.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, k: nat
p: n <= k
r: k.+1 = n
leq_n n = transport (leq n) r (leq_S n k p)
    destruct r.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
k: nat
p: k.+1 <= k
leq_n k.+1 = transport (leq k.+1) 1 (leq_S k.+1 k p)
    contradiction (not_leq_Sn_n _ p).
  +leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m: nat
p: n <= m
forall (m0 : nat) (q : n <= m0) (r : m0.+1 = m.+1),
leq_S n m p = transport (leq n) r (leq_S n m0 q) intros m' q r.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m: nat
p: n <= m
m': nat
q: n <= m'
r: m'.+1 = m.+1
leq_S n m p = transport (leq n) r (leq_S n m' q)
    pose (r' := path_nat_S _ _ r).leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m: nat
p: n <= m
m': nat
q: n <= m'
r: m'.+1 = m.+1
r':= path_nat_S m' m r: m' = m
leq_S n m p = transport (leq n) r (leq_S n m' q)
    destruct r'.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m': nat
p, q: n <= m'
r: m'.+1 = m'.+1
leq_S n m' p = transport (leq n) r (leq_S n m' q)
    assert (t : idpath = r) by apply path_ishprop.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m': nat
p, q: n <= m'
r: m'.+1 = m'.+1
t: 1 = r
leq_S n m' p = transport (leq n) r (leq_S n m' q)
    destruct t.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m': nat
p, q: n <= m'
leq_S n m' p = transport (leq n) 1 (leq_S n m' q)
    cbn.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m': nat
p, q: n <= m'
leq_S n m' p = leq_S n m' q apply ap.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m': nat
p, q: n <= m'
p = q
    destruct q.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n: nat
p: n <= n
p = leq_n n
leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m: nat
p: n <= m.+1
q: n <= m
p = leq_S n m q
    1:  apply leq_n_inj.leq_S_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p = transport (leq n) r (leq_S n m q)
n, m: nat
p: n <= m.+1
q: n <= m
p = leq_S n m q
    apply (leq_S_inj_gen n m _ p q idpath).
Defined.

Definition leq_S_inj n m (p : n <= m.+1) (q : n <= m) : p = leq_S n m q
  := leq_S_inj_gen n m m.+1 p q idpath.

Global Instance ishprop_leq n m : IsHProp (n <= m).n, m: nat
IsHProp (n <= m)
Proof.n, m: nat
IsHProp (n <= m)
  apply hprop_allpath.n, m: nat
forall x y : n <= m, x = y
  intros p q; revert p.n, m: nat
q: n <= m
forall p : n <= m, p = q
  induction q.n: nat
forall p : n <= n, p = leq_n n
n, m: nat
q: n <= m
IHq: forall p : n <= m, p = q
forall p : n <= m.+1, p = leq_S n m q
  +n: nat
forall p : n <= n, p = leq_n n intros y.n: nat
y: n <= n
y = leq_n n
    rapply leq_n_inj.
  +n, m: nat
q: n <= m
IHq: forall p : n <= m, p = q
forall p : n <= m.+1, p = leq_S n m q intros y.n, m: nat
q: n <= m
IHq: forall p : n <= m, p = q
y: n <= m.+1
y = leq_S n m q
    rapply leq_S_inj.
Defined.

Global Instance leq_0_n n : 0 <= n | 10.n: nat
0 <= n
Proof.n: nat
0 <= n
  simple_induction' n; auto.
Defined.

Lemma not_leq_Sn_0 n : ~ (n.+1 <= 0).n: nat
~ (n.+1 <= 0)
Proof.n: nat
~ (n.+1 <= 0)
  intros p.n: nat
p: n.+1 <= 0
Empty
  apply (fun x => leq_trans x (leq_0_n n)) in p.n: nat
p: n.+1 <= n
Empty
  contradiction (not_leq_Sn_n _ p).
Defined.

Definition equiv_leq_S_n n m : n.+1 <= m.+1 <~> n <= m.n, m: nat
n.+1 <= m.+1 <~> n <= m
Proof.n, m: nat
n.+1 <= m.+1 <~> n <= m
  srapply equiv_iff_hprop.n, m: nat
n.+1 <= m.+1 -> n <= m
  apply leq_S_n.
Defined.

Global Instance decidable_leq n m : Decidable (n <= m).n, m: nat
Decidable (n <= m)
Proof.n, m: nat
Decidable (n <= m)
  revert n.m: nat
forall n : nat, Decidable (n <= m)
  simple_induction' m; intros n.n: nat
Decidable (n <= 0)
m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
Decidable (n <= m.+1)
  -n: nat
Decidable (n <= 0) destruct n.Decidable (0 <= 0)
n: nat
Decidable (n.+1 <= 0)
    +Decidable (0 <= 0) left; exact _.
    +n: nat
Decidable (n.+1 <= 0) right; apply not_leq_Sn_0.
  -m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
Decidable (n <= m.+1) destruct n.m: nat
IH: forall n : nat, Decidable (n <= m)
Decidable (0 <= m.+1)
m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
Decidable (n.+1 <= m.+1)
    +m: nat
IH: forall n : nat, Decidable (n <= m)
Decidable (0 <= m.+1) left; exact _.
    +m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
Decidable (n.+1 <= m.+1) rapply decidable_equiv'.m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
?n <= m <~> n.+1 <= m.+1
      symmetry.m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
n.+1 <= m.+1 <~> ?n <= m
      apply equiv_leq_S_n.
Defined.

Fixpoint leq_add n m : n <= (m + n).leq_add: forall n m : nat, n <= m + n
n, m: nat
n <= m + n
Proof.leq_add: forall n m : nat, n <= m + n
n, m: nat
n <= m + n
  destruct m.leq_add: forall n m : nat, n <= m + n
n: nat
n <= 0 + n
leq_add: forall n m : nat, n <= m + n
n, m: nat
n <= m.+1 + n
  1: apply leq_n.leq_add: forall n m : nat, n <= m + n
n, m: nat
n <= m.+1 + n
  apply leq_S, leq_add.
Defined.

(** We define the less-than relation [lt] in terms of [leq] *)
Definition lt n m : Type0 := leq (S n) m.

(** We declare it as an existing class so typeclass search is performed on its goals. *)
Existing Class lt.
#[export] Hint Unfold lt : core typeclass_instances.
Infix "<" := lt : nat_scope.
(** We add a typeclass instance for unfolding the definition so lemmas about [leq] can be used. *)
Global Instance lt_is_leq n m : leq n.+1 m -> lt n m | 100 := idmap.

(** We should also give them their various typeclass instances *)
Global Instance transitive_lt : Transitive lt.Transitive lt
Proof.Transitive lt
  hnf; unfold lt in *.forall x y z : nat,
x.+1 <= y -> y.+1 <= z -> x.+1 <= z
  intros x y z p q.x, y, z: nat
p: x.+1 <= y
q: y.+1 <= z
x.+1 <= z
  rapply leq_trans.
Defined.

Global Instance decidable_lt n m : Decidable (lt n m) := _.

Definition ge n m := leq m n.
Existing Class ge.
#[export] Hint Unfold ge : core typeclass_instances.
Infix ">=" := ge : nat_scope.
Global Instance ge_is_leq n m : leq m n -> ge n m | 100 := idmap.

Global Instance reflexive_ge : Reflexive ge := leq_n.
Global Instance transitive_ge : Transitive ge := fun x y z p q => leq_trans q p.
Global Instance decidable_ge n m : Decidable (ge n m) := _.

Definition gt n m := lt m n.
Existing Class gt.
#[export] Hint Unfold gt : core typeclass_instances.
Infix ">" := gt : nat_scope.
Global Instance gt_is_leq n m : leq m.+1 n -> gt n m | 100 := idmap.

Global Instance transitive_gt : Transitive gt
  := fun x y z p q => transitive_lt _ _ _ q p.
Global Instance decidable_gt n m : Decidable (gt n m) := _.

Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
Notation "x <= y < z"  := (x <= y /\  y < z) : nat_scope.
Notation "x < y < z"   := (x < y  /\  y < z) : nat_scope.
Notation "x < y <= z"  := (x < y  /\ y <= z) : nat_scope.

(** Principle of double induction *)

Theorem nat_double_ind (R : nat -> nat -> Type)
  (H1 : forall n, R 0 n) (H2 : forall n, R (S n) 0)
  (H3 : forall n m, R n m -> R (S n) (S m))
  : forall n m:nat, R n m.R: nat -> nat -> Type
H1: forall n : nat, R 0 n
H2: forall n : nat, R n.+1 0
H3: forall n m : nat, R n m -> R n.+1 m.+1
forall n m : nat, R n m
Proof.R: nat -> nat -> Type
H1: forall n : nat, R 0 n
H2: forall n : nat, R n.+1 0
H3: forall n m : nat, R n m -> R n.+1 m.+1
forall n m : nat, R n m
  simple_induction' n; auto.R: nat -> nat -> Type
H1: forall n : nat, R 0 n
H2: forall n : nat, R n.+1 0
H3: forall n m : nat, R n m -> R n.+1 m.+1
n: nat
IH: forall m : nat, R n m
forall m : nat, R n.+1 m
  destruct m; auto.
Defined.

(** Maximum and minimum : definitions and specifications *)

Lemma max_n_n n : max n n = n.n: nat
max n n = n
Proof.n: nat
max n n = n
  simple_induction' n; cbn; auto.
Defined.
#[export] Hint Resolve max_n_n : core.

Lemma max_Sn_n n : max (S n) n = S n.n: nat
max n.+1 n = n.+1
Proof.n: nat
max n.+1 n = n.+1
  simple_induction' n; cbn; auto.
Defined.
#[export] Hint Resolve max_Sn_n : core.

Lemma max_comm n m : max n m = max m n.n, m: nat
max n m = max m n
Proof.n, m: nat
max n m = max m n
  revert m; simple_induction' n; destruct m; cbn; auto.
Defined.

Lemma max_0_n n : max 0 n = n.n: nat
max 0 n = n
Proof.n: nat
max 0 n = n
  auto.
Defined.
#[export] Hint Resolve max_0_n : core.

Lemma max_n_0 n : max n 0 = n.n: nat
max n 0 = n
Proof.n: nat
max n 0 = n
  by rewrite max_comm.
Defined.
#[export] Hint Resolve max_n_0 : core.

Theorem max_l : forall n m, m <= n -> max n m = n.forall n m : nat, m <= n -> max n m = n
Proof.forall n m : nat, m <= n -> max n m = n
  intros n m; revert n; simple_induction m m IHm; auto.m: nat
IHm: forall n : nat, m <= n -> max n m = n
forall n : nat, m.+1 <= n -> max n m.+1 = n
  intros [] p.m: nat
IHm: forall n : nat, m <= n -> max n m = n
p: m.+1 <= 0
max 0 m.+1 = 0
m: nat
IHm: forall n : nat, m <= n -> max n m = n
n: nat
p: m.+1 <= n.+1
max n.+1 m.+1 = n.+1
  1: inversion p.m: nat
IHm: forall n : nat, m <= n -> max n m = n
n: nat
p: m.+1 <= n.+1
max n.+1 m.+1 = n.+1
  cbn; by apply ap_S, IHm, leq_S_n.
Defined.

Theorem max_r : forall n m : nat, n <= m -> max n m = m.forall n m : nat, n <= m -> max n m = m
Proof.forall n m : nat, n <= m -> max n m = m
  intros; rewrite max_comm; by apply max_l.
Defined.

Lemma min_comm : forall n m, min n m = min m n.forall n m : nat, min n m = min m n
Proof.forall n m : nat, min n m = min m n
  simple_induction' n; destruct m; cbn; auto.
Defined.

Theorem min_l : forall n m : nat, n <= m -> min n m = n.forall n m : nat, n <= m -> min n m = n
Proof.forall n m : nat, n <= m -> min n m = n
  simple_induction n n IHn; auto.n: nat
IHn: forall m : nat, n <= m -> min n m = n
forall m : nat, n.+1 <= m -> min n.+1 m = n.+1
  intros [] p.n: nat
IHn: forall m : nat, n <= m -> min n m = n
p: n.+1 <= 0
min n.+1 0 = n.+1
n: nat
IHn: forall m : nat, n <= m -> min n m = n
n0: nat
p: n.+1 <= n0.+1
min n.+1 n0.+1 = n.+1
  1: inversion p.n: nat
IHn: forall m : nat, n <= m -> min n m = n
n0: nat
p: n.+1 <= n0.+1
min n.+1 n0.+1 = n.+1
  cbn; by apply ap_S, IHn, leq_S_n.
Defined.

Theorem min_r : forall n m : nat, m <= n -> min n m = m.forall n m : nat, m <= n -> min n m = m
Proof.forall n m : nat, m <= n -> min n m = m
  intros; rewrite min_comm; by apply min_l.
Defined.

(** [n]th iteration of the function [f : A -> A].  We have definitional equalities [nat_iter 0 f x = x] and [nat_iter n.+1 f x = f (nat_iter n f x)].  We make this a notation, so it doesn't add a universe variable for the universe containing [A]. *)
Notation nat_iter n f x
  := ((fix F (m : nat)
      := match m with
        | 0 => x
        | m'.+1 => f (F m')
        end) n).

Lemma nat_iter_succ_r n {A} (f : A -> A) (x : A)
  : nat_iter (S n) f x = nat_iter n f (f x).n: nat
A: Type
f: A -> A
x: A
nat_iter n.+1 f x = nat_iter n f (f x)
Proof.n: nat
A: Type
f: A -> A
x: A
nat_iter n.+1 f x = nat_iter n f (f x)
  simple_induction n n IHn; simpl; trivial.A: Type
f: A -> A
x: A
n: nat
IHn: f (nat_iter n f x) = nat_iter n f (f x)
f (f (nat_iter n f x)) = f (nat_iter n f (f x))
  exact (ap f IHn).
Defined.

Theorem nat_iter_add (n m : nat) {A} (f : A -> A) (x : A)
  : nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).n, m: nat
A: Type
f: A -> A
x: A
nat_iter (n + m) f x = nat_iter n f (nat_iter m f x)
Proof.n, m: nat
A: Type
f: A -> A
x: A
nat_iter (n + m) f x = nat_iter n f (nat_iter m f x)
  simple_induction n n IHn; simpl; trivial.m: nat
A: Type
f: A -> A
x: A
n: nat
IHn: nat_iter (n + m) f x = nat_iter n f (nat_iter m f x)
f (nat_iter (n + m) f x) =
f (nat_iter n f (nat_iter m f x))
  exact (ap f IHn).
Defined.

(** Preservation of invariants : if [f : A -> A] preserves the invariant [P], then the iterates of [f] also preserve it. *)
Theorem nat_iter_invariant (n : nat) {A} (f : A -> A) (P : A -> Type)
  : (forall x, P x -> P (f x)) -> forall x, P x -> P (nat_iter n f x).n: nat
A: Type
f: A -> A
P: A -> Type
(forall x : A, P x -> P (f x)) ->
forall x : A, P x -> P (nat_iter n f x)
Proof.n: nat
A: Type
f: A -> A
P: A -> Type
(forall x : A, P x -> P (f x)) ->
forall x : A, P x -> P (nat_iter n f x)
  simple_induction n n IHn; simpl; trivial.A: Type
f: A -> A
P: A -> Type
n: nat
IHn: (forall x : A, P x -> P (f x)) -> forall x : A, P x -> P (nat_iter n f x)
(forall x : A, P x -> P (f x)) ->
forall x : A, P x -> P (f (nat_iter n f x))
  intros Hf x Hx.A: Type
f: A -> A
P: A -> Type
n: nat
IHn: (forall x : A, P x -> P (f x)) -> forall x : A, P x -> P (nat_iter n f x)
Hf: forall x : A, P x -> P (f x)
x: A
Hx: P x
P (f (nat_iter n f x))
  apply Hf, IHn; trivial.
Defined.

(** ** Arithmetic *)

Lemma nat_add_n_Sm (n m : nat) : (n + m).+1 = n + m.+1.n, m: nat
(n + m).+1 = n + m.+1
Proof.n, m: nat
(n + m).+1 = n + m.+1
  simple_induction' n; simpl.m: nat
m.+1 = m.+1
m, n: nat
IH: (n + m).+1 = n + m.+1
(n + m).+2 = (n + m.+1).+1
  -m: nat
m.+1 = m.+1 reflexivity.
  -m, n: nat
IH: (n + m).+1 = n + m.+1
(n + m).+2 = (n + m.+1).+1 apply ap; assumption.
Defined.

Definition nat_add_comm (n m : nat) : n + m = m + n.n, m: nat
n + m = m + n
Proof.n, m: nat
n + m = m + n
  simple_induction n n IHn; simpl.m: nat
m = m + 0
m, n: nat
IHn: n + m = m + n
(n + m).+1 = m + n.+1
  -m: nat
m = m + 0 exact (add_n_O m).
  -m, n: nat
IHn: n + m = m + n
(n + m).+1 = m + n.+1 transitivity (m + n).+1.m, n: nat
IHn: n + m = m + n
(n + m).+1 = (m + n).+1
m, n: nat
IHn: n + m = m + n
(m + n).+1 = m + n.+1
    +m, n: nat
IHn: n + m = m + n
(n + m).+1 = (m + n).+1 apply ap, IHn.
    +m, n: nat
IHn: n + m = m + n
(m + n).+1 = m + n.+1 apply nat_add_n_Sm.
Defined.

(** ** Exponentiation *)

Fixpoint nat_exp (n m : nat) : nat
  := match m with
       | 0 => 1
       | S m => nat_exp n m * n
     end.

(** ** Factorials *)

Fixpoint factorial (n : nat) : nat
  := match n with
       | 0 => 1
       | S n => S n * factorial n
     end.

(** ** Natural number ordering *)

(** ** Theorems about natural number ordering *)

Lemma leq_antisym {x y} : x <= y -> y <= x -> x = y.x, y: nat
x <= y -> y <= x -> x = y
Proof.x, y: nat
x <= y -> y <= x -> x = y
  intros p q.x, y: nat
p: x <= y
q: y <= x
x = y
  destruct p.x: nat
q: x <= x
x = x
x, m: nat
p: x <= m
q: m.+1 <= x
x = m.+1
  1: reflexivity.x, m: nat
p: x <= m
q: m.+1 <= x
x = m.+1
  destruct x; [inversion q|].x, m: nat
p: x.+1 <= m
q: m.+1 <= x.+1
x.+1 = m.+1
  apply leq_S_n in q.x, m: nat
p: x.+1 <= m
q: m <= x
x.+1 = m.+1
  pose (r := leq_trans p q).x, m: nat
p: x.+1 <= m
q: m <= x
r:= leq_trans p q: x.+1 <= x
x.+1 = m.+1
  by apply not_leq_Sn_n in r.
Defined.

Definition not_lt_n_n n : ~ (n < n) := not_leq_Sn_n n.

Definition leq_1_Sn {n} : 1 <= n.+1 := leq_S_n' 0 n (leq_0_n _).

Fixpoint leq_dichot {m} {n} : (m <= n) + (m > n).leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m, n: nat
((m <= n) + (m > n))%type
Proof.leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m, n: nat
((m <= n) + (m > n))%type
  simple_induction' m; simple_induction' n.leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
((0 <= 0) + (0 > 0))%type
leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
n: nat
IH: ((0 <= n) + (0 > n))%type
((0 <= n.+1) + (0 > n.+1))%type
leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m: nat
(m <= 0) + (m > 0) -> ((m.+1 <= 0) + (m.+1 > 0))%type
leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m, n: nat
IH0: (m <= n) + (m > n) ->
((m.+1 <= n) + (m.+1 > n))%type
(m <= n.+1) + (m > n.+1) ->
((m.+1 <= n.+1) + (m.+1 > n.+1))%type
  -leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
((0 <= 0) + (0 > 0))%type left; reflexivity.
  -leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
n: nat
IH: ((0 <= n) + (0 > n))%type
((0 <= n.+1) + (0 > n.+1))%type left; apply leq_0_n.
  -leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m: nat
(m <= 0) + (m > 0) -> ((m.+1 <= 0) + (m.+1 > 0))%type right; unfold lt; apply leq_1_Sn.
  -leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m, n: nat
IH0: (m <= n) + (m > n) ->
((m.+1 <= n) + (m.+1 > n))%type
(m <= n.+1) + (m > n.+1) ->
((m.+1 <= n.+1) + (m.+1 > n.+1))%type assert ((m <= n) + (n < m)) as X by apply leq_dichot.leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m, n: nat
IH0: (m <= n) + (m > n) ->
((m.+1 <= n) + (m.+1 > n))%type
X: ((m <= n) + (n < m))%type
(m <= n.+1) + (m > n.+1) ->
((m.+1 <= n.+1) + (m.+1 > n.+1))%type
    destruct X as [leqmn|ltnm].leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m, n: nat
IH0: (m <= n) + (m > n) ->
((m.+1 <= n) + (m.+1 > n))%type
leqmn: m <= n
(m <= n.+1) + (m > n.+1) ->
((m.+1 <= n.+1) + (m.+1 > n.+1))%type
leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m, n: nat
IH0: (m <= n) + (m > n) ->
((m.+1 <= n) + (m.+1 > n))%type
ltnm: n < m
(m <= n.+1) + (m > n.+1) ->
((m.+1 <= n.+1) + (m.+1 > n.+1))%type
    +leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m, n: nat
IH0: (m <= n) + (m > n) ->
((m.+1 <= n) + (m.+1 > n))%type
leqmn: m <= n
(m <= n.+1) + (m > n.+1) ->
((m.+1 <= n.+1) + (m.+1 > n.+1))%type left; apply leq_S_n'; assumption.
    +leq_dichot: forall m n : nat,
((m <= n) + (m > n))%type
m, n: nat
IH0: (m <= n) + (m > n) ->
((m.+1 <= n) + (m.+1 > n))%type
ltnm: n < m
(m <= n.+1) + (m > n.+1) ->
((m.+1 <= n.+1) + (m.+1 > n.+1))%type right; apply leq_S_n'; assumption.
Defined.

Lemma not_lt_n_0 n : ~ (n < 0).n: nat
~ (n < 0)
Proof.n: nat
~ (n < 0)
  apply not_leq_Sn_0.
Defined.

(** ** Arithmetic relations between [trunc_index] and [nat]. *)

Lemma trunc_index_add_nat_add (n : nat)
  : trunc_index_add n n = n.+1 + n.+1.n: nat
(n +2+ n)%trunc = n.+1 + n.+1
Proof.n: nat
(n +2+ n)%trunc = n.+1 + n.+1
  induction n as [|n IH]; only 1: reflexivity.n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
((n.+1)%nat +2+ (n.+1)%nat)%trunc = n.+2 + n.+2
  refine (trunc_index_add_succ _ _ @ _).n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
(((n.+1)%nat +2+ (trunc_index_inc (-2) n.+1).+1).+1)%trunc =
n.+2 + n.+2
  refine (ap trunc_S _ @ _).n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
((n.+1)%nat +2+ (trunc_index_inc (-2) n.+1).+1)%trunc =
?Goal
n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
(?Goal.+1)%trunc = n.+2 + n.+2
  {n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
((n.+1)%nat +2+ (trunc_index_inc (-2) n.+1).+1)%trunc =
?Goal refine (trunc_index_add_comm _ _ @ _).n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
((trunc_index_inc (-2) n.+1).+1 +2+ (n.+1)%nat)%trunc =
?Goal
    refine (trunc_index_add_succ _ _ @ _).n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
(((trunc_index_inc (-2) n.+1).+1 +2+
  (trunc_index_inc (-2) n.+1).+1).+1)%trunc = ?Goal
    exact (ap trunc_S IH). }n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
((n.+1 + n.+1).+2)%trunc = n.+2 + n.+2
  refine (_ @ ap nat_to_trunc_index _).n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
((n.+1 + n.+1).+2)%trunc = ?Goal0
n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
?Goal0 = n.+2 + n.+2
  2: exact (ap _ (add_Sn_m _ _)^ @ add_n_Sm _ _).n: nat
IH: (n +2+ n)%trunc = n.+1 + n.+1
((n.+1 + n.+1).+2)%trunc = (n.+1 + n.+1).+2
  reflexivity.
Defined.