Library UniMath.NumberSystems.NaturalNumbersAlgebra

Facts about the natural numbers that depend on definitions from algebra


Require Export UniMath.Foundations.NaturalNumbers.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.NegativePropositions.

Require Export UniMath.Algebra.Archimedean.
Require Export UniMath.Algebra.Domains_and_Fields.
Require Export UniMath.Algebra.IteratedBinaryOperations.

Definition nataddabmonoid : abmonoid :=
  make_abmonoid (make_setwithbinop natset (λ n m : nat, n + m))
               (make_dirprod
                  (make_dirprod natplusassoc
                               (@make_isunital natset _ 0 (make_dirprod natplusl0 natplusr0)))
                  natpluscomm).

Definition natmultabmonoid : abmonoid :=
  make_abmonoid
    (make_setwithbinop natset (λ n m : nat, n * m))
    (make_dirprod
       (make_dirprod natmultassoc (@make_isunital natset _ 1 (make_dirprod natmultl1 natmultr1)))
       natmultcomm).

Submonoid of non-zero elements in nat


Local Open Scope nat_scope.
Definition natnonzero : @subabmonoid natmultabmonoid.
Show proof.
  split with (λ a : natset, a ≠ 0). unfold issubmonoid. split.
  - unfold issubsetwithbinop. intros a a'.
    apply (natneq0andmult _ _ (pr2 a) (pr2 a')).
  - apply (ct (natneq, isdecrel_natneq, 1, 0)).

Lemma natnonzerocomm (a b : natnonzero) :
  (@op natnonzero a b) = (@op natnonzero b a).
Show proof.
  intros.
  apply (invmaponpathsincl _ (isinclpr1carrier _) (@op natnonzero a b) (@op natnonzero b a)).
  simpl. apply natmultcomm.

Theorem nat_plus_commutativity : isCommutative_fun_mon nataddabmonoid.
Show proof.
  intros ? ? ?. apply weqtoeqstn.
  intermediate_weq (∑ i, stn (x i)).
  - intermediate_weq (∑ i, stn (x(f i))).
    + apply invweq. rewrite iterop_fun_nat. apply weqstnsum1.
    + apply (weqfp _ (stn∘x)).
  - rewrite iterop_fun_nat. apply weqstnsum1.

Arguments nat_plus_commutativity {_} _ _.

Definition finsum {X} (fin : isfinite X) (f : X -> nat) : nat.
Show proof.
  intros.
  unfold isfinite,finstruct,nelstruct in fin.
  simple refine (squash_to_set
                    isasetnat
                    (λ (x : ∑ n, stn n ≃ X), iterop_fun_mon (M := nataddabmonoid) (f ∘ pr2 x))
                    _ fin).
  intros.
  induction x as [n x].
  induction x' as [n' x'].
  assert (p := weqtoeqstn (invweq x' ∘ x)%weq).
  induction p.
  assert (w := nat_plus_commutativity (f ∘ x') (invweq x' ∘ x)%weq).
  simple refine (_ @ w).
  unfold iterop_fun_mon.
  apply maponpaths. rewrite weqcomp_to_funcomp. apply funextfun; intro i.
  simpl. apply maponpaths. exact (! homotweqinvweq x' (x i)).

nat as a commutative rig


Definition natcommrig : commrig.
Show proof.
  split with (make_setwith2binop natset (make_dirprod (λ n m : nat, n + m) (λ n m : nat, n * m))).
  split.
  - split.
    + split with
      (make_dirprod
         (make_dirprod
            (make_dirprod natplusassoc (@make_isunital natset _ 0 (make_dirprod natplusl0 natplusr0)))
            natpluscomm)
         (make_dirprod natmultassoc (@make_isunital natset _ 1 (make_dirprod natmultl1 natmultr1)))).
      apply (make_dirprod natmult0n natmultn0).
    + apply (make_dirprod natldistr natrdistr).
  - unfold iscomm. apply natmultcomm.

Lemma nattorig_nat :
  ∏ n : nat, nattorig (X := natcommrig) n = n.
Show proof.
  induction n as [|n IHn].
  reflexivity.
  rewrite nattorigS, IHn.
  reflexivity.

Properties of comparisons in the terminology of algebra1.v


Local Open Scope rig_scope.

natgth

Lemma isplushrelnatgth : @isbinophrel nataddabmonoid natgth.
Show proof.
  split. apply natgthandplusl. apply natgthandplusr.

Lemma isinvplushrelnatgth : @isinvbinophrel nataddabmonoid natgth.
Show proof.
  split. apply natgthandpluslinv. apply natgthandplusrinv.

Lemma isinvmulthrelnatgth : @isinvbinophrel natmultabmonoid natgth.
Show proof.
  split.
  - intros a b c r. apply (natlthandmultlinv _ _ _ r).
  - intros a b c r. apply (natlthandmultrinv _ _ _ r).

Lemma isrigmultgtnatgth : isrigmultgt natcommrig natgth.
Show proof.
  intros a.
  induction a as [|a IHa].
  - intros ? ? ? rab rcd. contradicts rab (negnatgth0n b).
  - intros ? ? ? rab rcd.
    induction b as [|b IHb].
    + simpl.
      rewrite 2 natplusr0.
      apply natlthandmultl.
      * exact tt.
      * exact rcd.
    + simpl.
      set (rer := abmonoidrer nataddabmonoid).
      unfold op1, op2; simpl.
      rewrite (rer _ _ _ d). rewrite (rer _ _ _ c).
      unfold op1, op2; simpl.
      rewrite (natpluscomm c d).
      apply (natlthandplusr (a * d + b * c) (a * c + b * d) (d + c)).
      apply (IHa _ _ _ rab rcd).

Lemma isinvrigmultgtnatgth : isinvrigmultgt natcommrig natgth.
Show proof.
  set (rer := abmonoidrer nataddabmonoid).
  simpl in rer. apply isinvrigmultgtif.
  intros a b c d. generalize a b c. clear a b c.
  induction d as [ | d IHd ].
  - intros a b c g gab. change (pr1 ((a * c + b * 0) > (a * 0 + b * c))) in g.
    destruct c as [ | c ].
    + rewrite (natmultn0 _) in g. destruct (isirreflnatgth _ g).
    + apply natgthsn0.
  - intros a b c g gab. destruct c as [ | c ].
    + change (pr1 ((a * 0 + b * S d) > (a * S d + b * 0))) in g.
      rewrite (natmultn0 _) in g. rewrite (natmultn0 _) in g.
      rewrite (natplusl0 _) in g. rewrite (natplusr0 _) in g.
      set (g' := natgthandmultrinv _ _ _ g).
      destruct (isasymmnatgth _ _ gab g').
    + change (pr1 (natgth (a * S c + b * S d) (a * S d + b * S c))) in g.
      rewrite (multnsm _ _) in g. rewrite (multnsm _ _) in g.
      rewrite (multnsm _ _) in g. rewrite (multnsm _ _) in g.
      rewrite (rer _ (a * c) _ _) in g. rewrite (rer _ (a * d) _ _) in g.
      set (g' := natgthandpluslinv _ _ (a + b) g). apply (IHd a b c g' gab).

natlth

Lemma isplushrelnatlth : @isbinophrel nataddabmonoid natlth.
Show proof.
  split.
  - intros a b c. apply (natgthandplusl b a c).
  - intros a b c. apply (natgthandplusr b a c).

Lemma isinvplushrelnatlth : @isinvbinophrel nataddabmonoid natlth.
Show proof.
  split.
  - intros a b c. apply (natgthandpluslinv b a c).
  - intros a b c. apply (natgthandplusrinv b a c).

Lemma isinvmulthrelnatlth : @isinvbinophrel natmultabmonoid natlth.
Show proof.
  split.
  - intros a b c r. apply (natlthandmultlinv _ _ _ r).
  - intros a b c r. apply (natlthandmultrinv _ _ _ r).

natleh

Lemma isplushrelnatleh : @isbinophrel nataddabmonoid natleh.
Show proof.
  split. apply natlehandplusl. apply natlehandplusr.

Lemma isinvplushrelnatleh : @isinvbinophrel nataddabmonoid natleh.
Show proof.
  split. apply natlehandpluslinv. apply natlehandplusrinv.

Lemma ispartinvmulthrelnatleh : @ispartinvbinophrel natmultabmonoid (λ x, x ≠ 0) natleh.
Show proof.
  split.
  - intros a b c s r. apply (natlehandmultlinv _ _ _ s r).
  - intros a b c s r. apply (natlehandmultrinv _ _ _ s r).

natgeh

Lemma isplushrelnatgeh : @isbinophrel nataddabmonoid natgeh.
Show proof.
  split.
  - intros a b c. apply (natlehandplusl b a c).
  - intros a b c. apply (natlehandplusr b a c).

Lemma isinvplushrelnatgeh : @isinvbinophrel nataddabmonoid natgeh.
Show proof.
  split.
  - intros a b c. apply (natlehandpluslinv b a c).
  - intros a b c. apply (natlehandplusrinv b a c).

Lemma ispartinvmulthrelnatgeh : @ispartinvbinophrel natmultabmonoid (λ x, x ≠ 0) natgeh.
Show proof.
  split.
  - intros a b c s r. apply (natlehandmultlinv _ _ _ s r).
  - intros a b c s r. apply (natlehandmultrinv _ _ _ s r).

nat is an archimedean rig


Lemma isarchnat_diff :
  ∏ (y1 y2 : nat),
  y1 > y2 → ∃ n : nat, n * y1 > 1 + n * y2.
Show proof.
  intros y1 y2 Hy.
  apply natlthchoice2 in Hy.
  induction Hy as [Hy | <-].
  - apply hinhpr.
    exists 1%nat.
    exact Hy.
  - apply hinhpr.
    exists 2%nat.
    rewrite !multsnm ; simpl.
    rewrite natplusr0.
    apply natgthandplusl, natgthsnn.

Lemma isarchnat_gth :
  ∏ x : nat, ∃ n : nat, n > x.
Show proof.
  intros n.
  apply hinhpr.
  exists (S n).
  now apply natgthsnn.

Lemma isarchnat_pos :
  ∏ x : nat, ∃ n : nat, n + x > 0.
Show proof.
  intros n.
  apply hinhpr.
  now exists 1%nat.

Lemma isarchnat :
  isarchrig (X := natcommrig) natgth.
Show proof.
  repeat split.
  - intros y1 y2 Hy.
    generalize (isarchnat_diff y1 y2 Hy).
    apply hinhfun.
    intros n.
    exists (pr1 n).
    rewrite nattorig_nat.
    exact (pr2 n).
  - intros n.
    generalize (isarchnat_gth n).
    apply hinhfun.
    intros n'.
    exists (pr1 n').
    rewrite nattorig_nat.
    exact (pr2 n').
  - intros n.
    generalize (isarchnat_pos n).
    apply hinhfun.
    intros n'.
    exists (pr1 n').
    rewrite nattorig_nat.
    exact (pr2 n').