# 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.