Field.v

Require Import Field_theory 
  Ring_theory List NArith 
  Ring Field Utf8 Lia 
  Coq.Arith.PeanoNat
  Vector Fin Lia
  Epsilon 
  FunctionalExtensionality 
  ProofIrrelevance.
From mathcomp Require Import 
  all_ssreflect algebra.matrix
  algebra.ssralg algebra.finalg.

Import ListNotations.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Section Computation.
  


  Variable 
    (R : Type)
    (rO rI:R)
    (radd rmul rsub : R -> R -> R)
    (ropp : R -> R)
    (rdiv : R -> R -> R)
    (rinv : R -> R)
    (Radd_0_l: ∀ x : R, radd rO x = x)
    (Radd_comm: ∀ x y : R, radd x y = radd y x)
    (Radd_assoc: ∀ x y z : R,
                  radd x (radd y z) =
                  radd (radd x y) z)
    (Rmul_1_l: ∀ x : R, rmul rI x = x)
    (Rmul_comm: ∀ x y : R, rmul x y = rmul y x)
    (Rmul_assoc: ∀ x y z : R,
                  rmul x (rmul y z) =
                  rmul (rmul x y) z)
    (Rdistr_l: ∀ x y z : R,
                rmul (radd x y) z =
                radd (rmul x z) (rmul y z))
    (Rsub_def: ∀ x y : R,
                rsub x y = radd x (ropp y))
    (Ropp_def: ∀ x : R, radd x (ropp x) = rO)
    (F_1_neq_0: rI ≠ rO)
    (Fdiv_def: ∀ p q : R,
                rdiv p q = rmul p (rinv q))
    (Finv_l: ∀ p : R,
              p ≠ rO → rmul (rinv p) p = rI)
    (Rzero_ann : forall p : R, rmul rO p = rO)
    (Rnon_zero : forall r1 r2, r1 <> rO -> r2 <> rO -> rmul r1 r2 <> rO)
    (Hdec : forall r1 r2 : R, {r1 = r2} + {r1 <> r2}).
    
  
  Definition eqr (r1 r2 : R) : bool :=
    if Hdec r1 r2 is left _ then true else false.
  
  Lemma eqrP : Equality.axiom eqr.
  Proof.
    by move=> r1 r2; rewrite /eqr; case: 
    Hdec=> H; apply: (iffP idP).
  Qed.
  
  Canonical Structure R_eqMixin := EqMixin eqrP.
  Canonical Structure R_eqType := Eval hnf in EqType R R_eqMixin.

  Fact inhR : inhabited R.
  Proof. exact: (inhabits rO). Qed.

  



  Definition pickR (P : pred R) (n : nat) :=
  let x := epsilon inhR P in if P x then Some x else None.

  Fact pickR_some P n x : pickR P n = Some x -> P x.
  Proof. by rewrite /pickR; case: (boolP (P _)) => // Px [<-]. Qed.

  Fact pickR_ex (P : pred R) :
    (exists x : R, P x) -> exists n, pickR P n. 
  Proof. by rewrite /pickR; move=> /(epsilon_spec inhR)->; 
    exists 0%N. 
  Qed.

  Fact pickR_ext (P Q : pred R) : P =1 Q -> pickR P =1 pickR Q.
  Proof.
  move=> PEQ n; rewrite /pickR; set u := epsilon _ _; set v := epsilon _ _.
  suff->: u = v by rewrite PEQ.
  by congr epsilon; apply: functional_extensionality=> x; rewrite PEQ.
  Qed.

  Definition R_choiceMixin : choiceMixin R :=
  Choice.Mixin pickR_some pickR_ex pickR_ext.

  Canonical R_choiceType := Eval hnf in ChoiceType R R_choiceMixin.

  Lemma radd_assoc : associative radd.
  Proof.
    move =>x y z.
    apply Radd_assoc.
  Qed.

  
  Lemma radd_comm : commutative radd.
  Proof.
    move =>x y.
    apply Radd_comm.
  Qed.

  Lemma radd_left_id : left_id rO radd.
  Proof.
    move => x.
    apply Radd_0_l.
  Qed.
  
 
  Lemma radd_left_inv : left_inverse rO ropp radd.
  Proof.
    move =>x.
    rewrite Radd_comm.
    apply Ropp_def.
  Qed.
   

  Definition R_zmodmixin := 
      ZmodMixin radd_assoc radd_comm radd_left_id radd_left_inv.

 
  Canonical R_zmodtype := ZmodType R R_zmodmixin.
  

  Lemma rmul_assoc : associative rmul.
  Proof.
    move =>x y z. 
    apply Rmul_assoc.
  Qed.
  
  Lemma rmul_comm : commutative rmul.
  Proof.
    move =>x y.
    apply Rmul_comm.
  Qed.
  

  Lemma rmul_left_id : left_id rI rmul.
  Proof.
    move =>x.
    apply Rmul_1_l.
  Qed.
  
  Lemma rmul_dist_l : left_distributive rmul radd.
  Proof.
    move =>x y z. 
    apply Rdistr_l.
  Qed.

  Lemma rO_neq_rI : is_true (rI != rO%R).
  Proof.
    by apply/eqP/F_1_neq_0.
  Qed.
  
  
  Definition R_comringmixin := 
    ComRingMixin rmul_assoc rmul_comm 
    rmul_left_id rmul_dist_l rO_neq_rI.


  Canonical R_ring := RingType R R_comringmixin.
  Canonical R_comring := ComRingType R Rmul_comm.
  
  

  Import Monoid.

  Lemma radd_right_id : right_id rO radd.
  Proof.
    move => x.
    rewrite <-Radd_comm.
    apply Radd_0_l.
  Qed.

  Lemma rmul_right_id : right_id rI rmul.
  Proof.
    move =>x.
    rewrite Rmul_comm.
    apply Rmul_1_l.
  Qed.


  Canonical Radd_monoid := 
    Law radd_assoc Radd_0_l radd_right_id.
  Canonical Radd_comoid := 
    ComLaw radd_comm.

  Canonical Rmul_monoid := Law rmul_assoc rmul_left_id rmul_right_id.
  Canonical Rmul_comoid := ComLaw rmul_comm.

 
  (* How does 0 interact with rmul? *)
  Lemma rmul_0_l : left_zero rO rmul.
  Proof.
    move => x.
    apply Rzero_ann.
  Qed.

  Lemma rmul_0_r : right_zero rO rmul.
  Proof.
    move => x.
    rewrite Rmul_comm.
    apply Rzero_ann.
  Qed.
  

  Lemma rmul_plus_dist_l : left_distributive rmul radd.
  Proof.
    move => x y z.
    apply Rdistr_l.
  Qed.

  Lemma rmul_plus_dist_r : right_distributive rmul radd.
  Proof.
    move => x y z.
    pose proof Rdistr_l y z x as H.
    rewrite Rmul_comm.
    rewrite H.
    rewrite Rmul_comm.
    f_equal.
    apply Rmul_comm.
  Qed.
  



  Canonical Rmul_mul_law := MulLaw rmul_0_l rmul_0_r.
  Canonical Radd_add_law := 
    AddLaw rmul_plus_dist_l rmul_plus_dist_r.

  Definition Rinvx r := if (r != rO) then rinv r else r.

  Definition unit_R r := r != rO.

  Lemma RmultRinvx : {in unit_R, left_inverse rI Rinvx rmul}.
  Proof.
    move=> r; rewrite -topredE /unit_R /Rinvx => /= rNZ /=.
    by rewrite rNZ Finv_l //; apply /eqP.
  Qed.
  
  Lemma Finv_r: ∀ p : R, p ≠ rO → rmul p (rinv p) = rI.
  Proof.
    intros ? Hp.
    rewrite Rmul_comm.
    apply Finv_l.
    exact Hp.
  Qed.

  Lemma RinvxRmult : {in unit_R, right_inverse rI Rinvx rmul}.
  Proof.
    move=> r; rewrite -topredE /unit_R /Rinvx => /= rNZ /=.
    by rewrite rNZ Finv_r //; apply/eqP.
  Qed.

  Lemma intro_unit_R x y : 
    rmul y x = rI /\ rmul x y = rI -> unit_R x.
  Proof.
    move=> [yxE1 xyE1]; apply/eqP=> xZ.
    rewrite xZ in yxE1.
    rewrite rmul_0_r in yxE1.
    unfold not in F_1_neq_0.
    apply F_1_neq_0.
    symmetry.
    exact yxE1.
  Qed.
    

  Lemma Rinvx_out : {in predC unit_R, Rinvx =1 id}.
  Proof. by move=> x; rewrite inE /= /Rinvx -if_neg => ->. Qed.

  Definition R_unitRingMixin :=
    UnitRingMixin RmultRinvx RinvxRmult intro_unit_R Rinvx_out.

  Canonical Structure R_unitRing :=
    Eval hnf in UnitRingType R R_unitRingMixin.

  Canonical Structure R_comUnitRingType :=
    Eval hnf in [comUnitRingType of R].

  
  Lemma R_idomainMixin x y : rmul x y = rO -> (x == rO) || (y == rO).
  Proof.
    
    (do 2 case: (boolP (_ == _))=> // /eqP)=> yNZ xNZ xyZ.
    by case: (@Rnon_zero _ _ xNZ yNZ).
  Qed.


  Canonical Structure R_idomainType :=
    Eval hnf in IdomainType R R_idomainMixin.
  
  Lemma R_fieldMixin : GRing.Field.mixin_of [unitRingType of R].
  Proof. done. Qed.

  Definition R_fieldIdomainMixin := FieldIdomainMixin R_fieldMixin.

  Canonical Structure R_field := FieldType R R_fieldMixin.


End Computation.