(** 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.
Proof.
refine (fun _ _ eqn _ _ eqp => _).
refine (eq_ind _ (fun n => _ = Build_int_bipart n _) _ _ eqn).
refine (f_equal _ eqp).
Qed.



(** 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.
Proof.
refine (fun n => _).
unfold plus.
simpl.
destruct n.
simpl.
refine (refl_equal _).
Qed.

Definition plus_comm : forall n m, n + m = m + n.
Proof.
refine (fun n m => int_bipart_eq_part _ _ _ _ _ _); ring. 
Qed.

Definition plus_assoc : forall n m p, n + (m + p) = (n + m) + p.
Proof.
refine (fun n m p => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
Qed.

Definition mult_1_l : forall n, (nat2int_bipart 1) * n = n.
Proof.
refine (fun n => _).
destruct n as [pneg0 ppos0].
unfold mult, plus.
refine (int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
Qed.

Definition mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.
Proof.
refine (fun n m p => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
Qed.

Definition mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
Proof.
refine (fun n m p => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
Qed.

Definition mult_comm : forall n m, n * m = m * n.
Proof.
refine (fun n m => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
Qed.

Definition mult_assoc : forall n m p, n * (m * p) = n * m * p.
Proof.
refine (fun n m p => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
Qed.



(** ** 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).
Proof.
refine (fun n => _).
destruct n.
unfold opp.
simpl.
refine (refl_equal _).
Qed.

Definition opp_plus : forall n m, - (n + m) = - m + - n.
Proof.
refine (fun n m => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
Qed.



(** * 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).
Proof.
refine (fun n => _).
destruct n.
unfold is0.
simpl.
refine (conj (@sym_eq _ _ _) (@sym_eq _ _ _)).
Qed.

Definition minus_diag : forall n, is0 (n - n).
Proof.
refine (fun n => _).
unfold int_bipart_eq.
unfold is0.
simpl.
ring.
Qed.



(** ** [int_bipart_eq] is an equivalence relation *)

Definition int_bipart_eq_refl : reflexive _ int_bipart_eq.
Proof.
unfold reflexive.
refine (fun n => _).
unfold int_bipart_eq.
unfold is0.
simpl.
ring.
Qed.

Definition int_bipart_eq_trans : transitive _ int_bipart_eq.
Proof.
unfold transitive.
refine (fun n m p => _).
unfold int_bipart_eq.
unfold minus.
unfold is0.
simpl.
refine (fun nm mp => _).
refine (Coq.Arith.Plus.plus_reg_l _ _ (pneg m !+ ppos m) _).
refine (trans_eq _ (_ : (ppos n !+ pneg m) !+ (ppos m !+ pneg p) = _)).
refine (eq_ind _ (fun dep => _ = dep !+ _) _ _ nm).
	refine (eq_ind _ (fun dep => _ = _ !+ dep) _ _ mp).
	ring.
ring.
Qed.

Definition int_bipart_eq_sym : symmetric _ int_bipart_eq.
Proof.
unfold symmetric.
refine (fun n m => _).
unfold int_bipart_eq.
unfold minus.
unfold is0.
simpl.
refine (fun p => _).
refine (trans_eq _ (_ : ppos n !+ pneg m = _)).
ring.
refine (eq_ind _ (fun dep => dep = _) _ _ p).
	ring.
Qed.

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] *)
Definition int_bipart_eq_std : inclusion _ (@eq _) int_bipart_eq.
Proof.
unfold inclusion.
refine (fun n m eq0 => _).
refine (eq_ind _ (fun dep => _ -= dep) _ _ eq0).
refine (int_bipart_eq_refl _).
Qed.



(** ** 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.
Proof.
unfold int_bipart_eq.
unfold minus.
unfold is0.
simpl.
refine (fun a1 a2 eqa b1 b2 eqb => _).
refine (trans_eq _ (_ : (ppos a1 !+ pneg a2) !+ (ppos b1 !+ pneg b2) = _)).
refine (eq_ind _ (fun dep => _ = dep !+ _) _ _ eqa).
	refine (eq_ind _ (fun dep => _ = _ !+ dep) _ _ eqb).
	ring.
ring.
Qed.

Add Morphism plus
with signature int_bipart_eq ==> int_bipart_eq ==> int_bipart_eq
as plus_mor.
Proof. refine (plus_eq_compat). Qed.

Definition mult_eq_compat : forall a1 a2, a1 -= a2
	-> forall b1 b2, b1 -= b2
	-> a1 * b1 -= a2 * b2.
Proof.
unfold int_bipart_eq.
unfold minus.
unfold is0.
simpl.
refine (fun a1 a2 eqa b1 b2 eqb => _).
refine (Coq.Arith.Plus.plus_reg_l _ _ 
	(ppos a2 !* pneg b1 !+ pneg a2 !* ppos b1
		!+ pneg a2 !* pneg b1 !+ ppos a2 !* ppos b1)
	_).
refine (trans_eq _ (_
	: (pneg a1 !+ ppos a2) !* pneg b1
		!+ (ppos a1 !+ pneg a2) !* ppos b1
		!+ pneg a2 !* (ppos b1 !+ pneg b2)
		!+ ppos a2 !* (pneg b1 !+ ppos b2)
	= _)).
refine (eq_ind _ (fun dep => _ = _ !+ dep !* _ !+ _ !+ _)
		_ _ eqa).
	refine (eq_ind _ (fun dep => _ = dep !* _ !+ _ !+ _ !+ _)
		_ _ (sym_eq eqa)).
	ring.
refine (eq_ind _ (fun dep => _ !+ _ !+ _ !* dep !+ _ = _)
		_ _ eqb).
	refine (eq_ind _ (fun dep => _ !+ _ !+ _ !+ _ !* dep = _)
		_ _ (sym_eq eqb)).
	ring.
Qed.

Add Morphism mult
with signature int_bipart_eq ==> int_bipart_eq ==> int_bipart_eq
as mult_mor.
Proof. refine (mult_eq_compat). Qed.

Definition opp_compat : forall a1 a2, a1 -= a2 -> -a1 -= -a2.
Proof.
refine (fun a1 a2 => _).
unfold int_bipart_eq.
unfold minus.
unfold is0.
simpl.
refine (@sym_eq _ _ _).
Qed.

Add Morphism opp
with signature int_bipart_eq ==> int_bipart_eq
as opp_mor.
Proof. refine (opp_compat). Qed.

Definition int_bipart_rt : ring_theory no_blank_0 (nat2int_bipart 1)
	plus mult minus opp int_bipart_eq.
Proof.
refine (mk_rt _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
refine (fun n => int_bipart_eq_std _ _ (plus_0_l n)).
refine (fun _ _ => int_bipart_eq_std _ _ (plus_comm _ _)).
refine (fun _ _ _ => int_bipart_eq_std _ _ (plus_assoc _ _ _)).
refine (fun _ => int_bipart_eq_std _ _ (mult_1_l _)).
refine (fun _ _ => int_bipart_eq_std _ _ (mult_comm _ _)).
refine (fun _ _ _ => int_bipart_eq_std _ _ (mult_assoc _ _ _)).
refine (fun _ _ _ => int_bipart_eq_std _ _ (mult_plus_distr_r _ _ _)).
unfold minus.
	refine (fun n m => int_bipart_eq_std _ _ (refl_equal _)).
refine (fun n => int_bipart_eq_sym _ _ _).
	change (is0 (n + - n)).
	refine (minus_diag _).
Qed.

Add Ring int_bipart_ring_name : int_bipart_rt.



(** * [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.
Proof. firstorder. Qed.

Definition nat_ext_plus an ai bn bi
	: eq_nat an ai -> eq_nat bn bi -> eq_nat (an !+ bn) (ai + bi).
Proof.
unfold eq_nat.
unfold plus.
refine (fun an ai bn bi eqa eqb => _).
simpl.
rewrite eqa.
rewrite eqb.
ring.
Qed.

Definition nat_ext_mult an ai bn bi
	: eq_nat an ai -> eq_nat bn bi -> eq_nat (an !* bn) (ai * bi).
Proof.
unfold eq_nat.
unfold mult.
refine (fun an ai bn bi eqa eqb => _).
simpl.
rewrite eqa.
rewrite eqb.
ring.
Qed.

Definition nat_ext_is0 n i : eq_nat n i -> (~ IsSucc n <-> is0 i).
Proof.
refine (fun n i eq0 => conj (fun p0 => _) (fun p0 p1 => _)).
destruct n.
	firstorder.
	firstorder.
unfold eq_nat in eq0.
	unfold is0 in p0.
	destruct n.
	firstorder.
	refine (Coq.Arith.Plus.succ_plus_discr _ _
		(eq_ind _ (fun dep => dep = _) eq0 _ p0)).
Qed.