Library UniMath.NumberSystems.NaturalNumbers_le_Inductive

Natural numbers and their properties. Vladimir Voevodsky. Apr. - Sep. 2011

This file contains the formulations and proofs of general properties of natural numbers from the univalent perspecive.

Contents

  • Inductive types le with values in UU
    • A generalization of le and its properties
    • Inductive types le with values in UU are in hProp
    • Comparison between le with values in UU and natleh

Preamble

Settings
Imports.

Require Export UniMath.Foundations.NaturalNumbers.

Inductive types le with values in UU.

This part is included for illustration purposes only. In practice it is easier to work with natleh than with le.

A generalization of le and its properties.


Inductive leF {T : UU} (F : T -> T) (t : T) : T -> UU :=
| leF_O : leF F t t
| leF_S : ∏ t' : T, leF F t t' -> leF F t (F t').

Lemma leFiter {T : UU} (F : T -> T) (t : T) (n : nat) : leF F t (iteration F n t).
Show proof.
  intros. induction n as [ | n IHn ].
  - apply leF_O.
  - simpl. apply leF_S. assumption.

Lemma leFtototal2withnat {T : UU} (F : T -> T) (t t' : T) (a : leF F t t') :
  total2 (λ n : nat, (iteration F n t) = t').
Show proof.
  intros. induction a as [ | b H0 IH0 ].
  - split with O. apply idpath.
  - split with (S (pr1 IH0)). simpl.
    apply (@maponpaths _ _ F (iteration F (pr1 IH0) t) b).
    apply (pr2 IH0).

Lemma total2withnattoleF {T : UU} (F : T -> T) (t t' : T)
      (a : total2 (λ n : nat, (iteration F n t) = t')) : leF F t t'.
Show proof.
  intros. destruct a as [ n e ]. destruct e. apply leFiter.

Lemma leFtototal2withnat_l0 {T : UU} (F : T -> T) (t : T) (n : nat) :
  (leFtototal2withnat F t _ (leFiter F t n)) = (tpair _ n (idpath (iteration F n t))).
Show proof.
  intros. induction n as [ | n IHn ].
  - apply idpath.
  - simpl.
    set (h := fun ne : total2 (λ n0 : nat, paths (iteration F n0 t) (iteration F n t)) =>
                tpair (λ n0 : nat, paths (iteration F n0 t) (iteration F (S n) t)) (S (pr1 ne))
                      (maponpaths F (pr2 ne))).
    apply (@maponpaths _ _ h _ _ IHn).

Lemma isweqleFtototal2withnat {T : UU} (F : T -> T) (t t' : T) : isweq (leFtototal2withnat F t t').
Show proof.
  intros.
  set (f := leFtototal2withnat F t t').
  set (g := total2withnattoleF F t t').
  assert (egf : ∏ x : _, paths (g (f x)) x).
  {
    intro x. induction x as [ | y H0 IHH0 ].
    - apply idpath.
    - simpl. simpl in IHH0.
      destruct (leFtototal2withnat F t y H0) as [ m e ].
      destruct e. simpl. simpl in IHH0.
      apply (@maponpaths _ _ (leF_S F t (iteration F m t)) _ _ IHH0).
  }
  assert (efg : ∏ x : _, paths (f (g x)) x).
  {
    intro x. destruct x as [ n e ]. destruct e. simpl.
    apply leFtototal2withnat_l0.
  }
  apply (isweq_iso _ _ egf efg).

Definition weqleFtototalwithnat { T : UU } (F : T -> T) (t t' : T) :
  weq (leF F t t') (total2 (λ n : nat, (iteration F n t) = t')) :=
  make_weq _ (isweqleFtototal2withnat F t t').

Inductive types le with values in UU are in hProp


Definition le (n : nat) : nat -> UU := leF S n.

Definition le_n : ∏ t : nat, leF S t t := leF_O S.

Definition le_S : ∏ t t' : nat, leF S t t' → leF S t (S t') := leF_S S.

Theorem isaprople (n m : nat) : isaprop (le n m).
Show proof.
  intros.
  apply (isofhlevelweqb 1 (weqleFtototalwithnat S n m)).
  apply invproofirrelevance. intros x x'.
  set (i := @pr1 _ (λ n0 : nat, (iteration S n0 n) = m)).
  assert (is : isincl i) by apply (isinclpr1 _ (λ n0 : nat, isasetnat (iteration S n0 n) m)).
  apply (invmaponpathsincl _ is).
  destruct x as [ n1 e1 ]. destruct x' as [ n2 e2 ]. simpl.
  set (int1 := pathsinv0 (pathsitertoplus n1 n)).
  set (int2 := pathsinv0 (pathsitertoplus n2 n)).
  set (ee1 := pathscomp0 int1 e1).
  set (ee2 := pathscomp0 int2 e2).
  set (e := pathscomp0 ee1 (pathsinv0 ee2)).
  apply (invmaponpathsincl _ (isinclnatplusr n) n1 n2 e).

Comparison between le with values in UU and natleh.


Lemma letoleh (n m : nat) : le n m -> n ≤ m.
Show proof.
  intros H. induction H as [ | m H0 IHH0 ].
  - apply isreflnatleh.
  - apply natlehtolehs. assumption.

Lemma natlehtole (n m : nat) : n ≤ m -> le n m.
Show proof.
  intros H. induction m as [|m IHm].
  - assert (int := natleh0tois0 H). clear H. destruct int. apply le_n.
  - set (int2 := natlehchoice2 n (S m) H).
    destruct int2 as [ isnatleh | iseq ].
    apply (le_S n m (IHm isnatleh)). destruct iseq.
    apply le_n.

Lemma isweqletoleh (n m : nat) : isweq (letoleh n m).
Show proof.
  intros.
  set (is1 := isaprople n m). set (is2 := pr2 (n ≤ m)).
  apply (isweqimplimpl (letoleh n m) (natlehtole n m) is1 is2).

Definition weqletoleh (n m : nat) : le n m ≃ n ≤ m := make_weq _ (isweqletoleh n m).