Library Beroal.IntBipart
Integer numbers as Grothendieck's ring
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.
: 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
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).
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).
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.
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.
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).
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
0 is opposite to itself
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.
Add Relation int_bipart 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
Require Export Setoid.
Definition plus_eq_compat : forall a1 a2, a1 -= a2
-> forall b1 b2, b1 -= b2
-> a1 + b1 -= a2 + b2.
Add Morphism plus
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.
Add Morphism mult
with signature int_bipart_eq ==> int_bipart_eq ==> int_bipart_eq
as mult_mor.
Definition opp_compat : forall a1 a2, a1 -= a2 -> -a1 -= -a2.
Add Morphism opp
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.
Add Ring int_bipart_ring_name : int_bipart_rt.
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).