# Library Beroal.IntBipart

Integer numbers as Grothendieck's ring

Require Export Relation_Definitions.
Require Coq.Arith.Plus.
Require Import ArithRing.

# Definitions

Record int_bipart : Set := {pneg : nat; ppos : nat}.

if both parts are equal than int_bipart-s are equal
Definition int_bipart_eq_part
: forall an bn, an = bn -> forall ap bp, ap = bp
-> Build_int_bipart an ap = Build_int_bipart bn bp.

a blank of n := min (pneg n) (ppos n)

see Check after is0
Definition blank_0 blank := Build_int_bipart blank blank.

a canonical integer zero
Definition no_blank_0 := blank_0 0.

Definition nat2int_bipart absolute := Build_int_bipart 0 absolute.

Notation "a !+ b" := (Peano.plus a b) (at level 50, left associativity).
Definition plus a b := Build_int_bipart
(pneg a !+ pneg b) (ppos a !+ ppos b).
Notation "a + b" := (plus a b).

Notation "a !* b" := (Peano.mult a b) (at level 40, left associativity).
Definition mult a b := Build_int_bipart
(pneg a !* ppos b !+ ppos a !* pneg b)
(pneg a !* pneg b !+ ppos a !* ppos b).
Notation "a * b" := (mult a b) (at level 40, left associativity).

# Ring

## +, ×

Definition plus_0_l : forall n, no_blank_0 + n = n.

Definition plus_comm : forall n m, n + m = m + n.

Definition plus_assoc : forall n m p, n + (m + p) = (n + m) + p.

Definition mult_1_l : forall n, (nat2int_bipart 1) * n = n.

Definition mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.

Definition mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.

Definition mult_comm : forall n m, n * m = m * n.

Definition mult_assoc : forall n m p, n * (m * p) = n * m * p.

## Opposite

Definition opp a := Build_int_bipart (ppos a) (pneg a).
Notation "- a" := (opp a).
Notation "a !- b" := (Peano.minus a b) (at level 50, left associativity).
Definition minus a b := a + (-b).
Notation "a - b" := (minus a b).

Definition opp_involution : forall n, n = - (- n).

Definition opp_plus : forall n m, - (n + m) = - m + - n.

# Equality of int_bipart and integer zero

Definition is0 a := ppos a = pneg a.

blank_0 gives integer zero
Check fun blank => (refl_equal _) : is0 (blank_0 blank).

Definition int_bipart_eq a b := is0 (- a + b).
Notation "a -= b" := (int_bipart_eq a b) (at level 70, no associativity).

(0 -=) and is0 are judgementally equal, so we don't need a theorem
Check fun n => (refl_equal _) : is0 n = (no_blank_0 -= n).

0 is opposite to itself
Definition is0_opp : forall n, is0 n <-> is0 (- n).

Definition minus_diag : forall n, is0 (n - n).

## int_bipart_eq is an equivalence relation

Definition int_bipart_eq_refl : reflexive _ int_bipart_eq.

Definition int_bipart_eq_trans : transitive _ int_bipart_eq.

Definition int_bipart_eq_sym : symmetric _ int_bipart_eq.

Definition int_bipart_eq_equiv := (Build_equivalence _ _
int_bipart_eq_refl int_bipart_eq_trans int_bipart_eq_sym
) : equivalence _ int_bipart_eq.

reflexivity proved by (int_bipart_eq_refl)
symmetry proved by (int_bipart_eq_sym)
transitivity proved by (int_bipart_eq_trans)
as int_bipart_eq_rel.

eq is included in int_bipart_eq

## Ring operations are morphisms

Require Export Setoid.

Definition plus_eq_compat : forall a1 a2, a1 -= a2
-> forall b1 b2, b1 -= b2
-> a1 + b1 -= a2 + b2.

with signature int_bipart_eq ==> int_bipart_eq ==> int_bipart_eq
as plus_mor.

Definition mult_eq_compat : forall a1 a2, a1 -= a2
-> forall b1 b2, b1 -= b2
-> a1 * b1 -= a2 * b2.

with signature int_bipart_eq ==> int_bipart_eq ==> int_bipart_eq
as mult_mor.

Definition opp_compat : forall a1 a2, a1 -= a2 -> -a1 -= -a2.

with signature int_bipart_eq ==> int_bipart_eq
as opp_mor.

Definition int_bipart_rt : ring_theory no_blank_0 (nat2int_bipart 1)
plus mult minus opp int_bipart_eq.

# int_bipart is an extension of nat

Definition eq_nat (n : nat) (i : int_bipart) := ppos i = n !+ pneg i.

Definition eq_nat_equiv n i : eq_nat n i <-> nat2int_bipart n -= i.

Definition nat_ext_plus an ai bn bi
: eq_nat an ai -> eq_nat bn bi -> eq_nat (an !+ bn) (ai + bi).

Definition nat_ext_mult an ai bn bi
: eq_nat an ai -> eq_nat bn bi -> eq_nat (an !* bn) (ai * bi).

Definition nat_ext_is0 n i : eq_nat n i -> (~ IsSucc n <-> is0 i).