(** 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.