theory.naturals

Require Import
 workaround_tactics
 Relation_Definitions Ring
 abstract_algebra peano_naturals theory.rings
 categories.varieties theory.ua_transference.
Require Export
 interfaces.naturals.

Lemma to_semiring_involutive N `{Naturals N} N2 `{Naturals N2} x :
 naturals_to_semiring N2 N (naturals_to_semiring N N2 x) = x.

Lemma to_semiring_unique `{Naturals N} `{SemiRing SR} (f: N SR) `{!SemiRing_Morphism f} x :
 f x = naturals_to_semiring N SR x.

Lemma to_semiring_unique_alt `{Naturals N} `{SemiRing SR} (f g: N SR) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x :
  f x = g x.

Lemma morphisms_involutive `{Naturals N} `{SemiRing R} (f : R N) (g : N R)
  `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} x : f (g x) = x.

Lemma to_semiring_twice `{Naturals N} `{SemiRing R1} `{SemiRing R2} (f : R1 R2) (g : N R1) (h : N R2)
     `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} `{!SemiRing_Morphism h} x :
  f (g x) = h x.

Lemma to_semiring_self `{Naturals N} (f : N N) `{!SemiRing_Morphism f} x : f x = x.

Lemma to_semiring_injective `{Naturals N} `{SemiRing A}
   (f: A N) (g: N A) `{!SemiRing_Morphism f} `{!SemiRing_Morphism g}: Injective g.

Instance naturals_to_naturals_injective `{Naturals N} `{Naturals N2} (f: N N2) `{!SemiRing_Morphism f}:
  Injective f | 15.

Section retract_is_nat.
  Context `{Naturals N} `{SemiRing SR}.
  Context (f : N SR) `{inv_f : !Inverse f} `{!Surjective f} `{!SemiRing_Morphism f} `{!SemiRing_Morphism (f⁻¹)}.

  Definition retract_is_nat_to_sr : NaturalsToSemiRing SR := λ R _ _ _ _ , naturals_to_semiring N R f⁻¹.

  Section for_another_semirings.
    Context `{SemiRing R}.

    Instance: SemiRing_Morphism (naturals_to_semiring N R f⁻¹) := {}.

    Context (h : SR R) `{!SemiRing_Morphism h}.

    Lemma same_morphism: naturals_to_semiring N R f⁻¹ = h.
  End for_another_semirings.

  Program Definition retract_is_nat: Naturals SR (U:=retract_is_nat_to_sr).
End retract_is_nat.

Section contents.
Context `{Naturals N}.

Section borrowed_from_nat.
  Import universal_algebra.
  Import notations.

  Lemma induction
    (P: N Prop) `{!Proper ((=) ==> iff) P}:
    P 0 ( n, P n P (1 + n)) n, P n.

  Global Instance biinduction: Biinduction N.

  Lemma from_nat_stmt:
     (s: Statement varieties.semirings.theory) (w : Vars varieties.semirings.theory (varieties.semirings.object N) nat),
     ( v: Vars varieties.semirings.theory (varieties.semirings.object nat) nat,
       eval_stmt varieties.semirings.theory v s) eval_stmt varieties.semirings.theory w s.

  Let three_vars (x y z : N) (_: unit) v := match v with 0%nat => x | 1%nat => y | _ => z end.
  Let two_vars (x y : N) (_: unit) v := match v with 0%nat => x | _ => y end.
  Let no_vars (_: unit) (v: nat) := 0.

  Local Notation x' := (Var varieties.semirings.sig _ 0 tt).
  Local Notation y' := (Var varieties.semirings.sig _ 1 tt).
  Local Notation z' := (Var varieties.semirings.sig _ 2%nat tt).


  Global Instance: z : N, LeftCancellation (+) z.

  Global Instance: z : N, RightCancellation (+) z.

  Global Instance: z : N, PropHolds (z 0) LeftCancellation (.*.) z.

  Global Instance: z : N, PropHolds (z 0) RightCancellation (.*.) z.

  Instance nat_nontrivial: PropHolds ((1:N) 0).

  Instance nat_nontrivial_apart `{Apart N} `{!TrivialApart N} :
    PropHolds ((1:N) 0).

  Lemma zero_sum x y : x + y = 0 x = 0 y = 0.

  Lemma one_sum x y : x + y = 1 (x = 1 y = 0) (x = 0 y = 1).

  Global Instance: ZeroProduct N.
End borrowed_from_nat.

Lemma nz_one_plus_zero x : 1 + x 0.

Global Program Instance: x y: N, Decision (x = y) | 10 := λ x y,
  match decide (naturals_to_semiring _ nat x = naturals_to_semiring _ nat y) with
  | left E => left _
  | right E => right _
  end.

End contents.

Hint Extern 6 (PropHolds (1 0)) => eapply @nat_nontrivial : typeclass_instances.
Hint Extern 6 (PropHolds (1 0)) => eapply @nat_nontrivial_apart : typeclass_instances.