Library Stdlib.setoid_ring.Cring

From Stdlib Require Export List.
From Stdlib Require Import Setoid.
From Stdlib Require Import BinPos.
From Stdlib Require Import BinList.
From Stdlib Require Import Znumtheory.
From Stdlib Require Export Morphisms Setoid Bool.
From Stdlib Require Import BinInt.
From Stdlib Require Export Algebra_syntax.
From Stdlib Require Export Ncring.
From Stdlib Require Export Ncring_initial.
From Stdlib Require Export Ncring_tac.
From Stdlib Require Import InitialRing.

Class Cring {R:Type}`{Rr:Ring R} :=
 cring_mul_comm: forall x y:R, x * y == y * x.

Ltac reify_goal lvar lexpr lterm:=
  
  match lexpr with
     nil => idtac
   | ?e1::?e2::_ =>
        match goal with
          |- (?op ?u1 ?u2) =>
           change (op
             (@Ring_polynom.PEeval
               _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
               (@Ring_theory.pow_N _ 1 multiplication) lvar e1)
             (@Ring_polynom.PEeval
               _ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
               (@Ring_theory.pow_N _ 1 multiplication) lvar e2))
        end
  end.

Section cring.
Context {R:Type}`{Rr:Cring R}.

Lemma cring_eq_ext: ring_eq_ext _+_ _*_ -_ _==_.

Lemma cring_almost_ring_theory:
   almost_ring_theory (R:=R) zero one _+_ _*_ _-_ -_ _==_.

Lemma cring_morph:
  ring_morph zero one _+_ _*_ _-_ -_ _==_
             0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb
             Ncring_initial.gen_phiZ.

Lemma cring_power_theory :
  @Ring_theory.power_theory R one _*_ _==_ N (fun n:N => n)
  (@Ring_theory.pow_N _ 1 multiplication).

Lemma cring_div_theory:
  div_theory _==_ Z.add Z.mul Ncring_initial.gen_phiZ Z.quotrem.

End cring.

Ltac cring_gen :=
  match goal with
    |- ?g =>
      let lterm := lterm_goal g in
      let reif := list_reifyl0 lterm in
        match reif with
          | (?fv, ?lexpr) =>
           
           reify_goal fv lexpr lterm;
           match goal with
             |- ?g =>
               generalize
                 (@Ring_polynom.ring_correct _ 0 1 _+_ _*_ _-_ -_ _==_
                        ring_setoid
                        cring_eq_ext
                        cring_almost_ring_theory
                        Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb
                        Ncring_initial.gen_phiZ
                        cring_morph
                        N
                        (fun n:N => n)
                        (@Ring_theory.pow_N _ 1 multiplication)
                        cring_power_theory
                        Z.quotrem
                        cring_div_theory
                        O fv nil);
                 let rc := fresh "rc"in
                   intro rc; apply rc
           end
        end
  end.

Ltac cring_compute:= vm_compute; reflexivity.

Ltac cring:=
  intros;
  cring_gen;
  cring_compute.

#[global]
Instance Zcri: (Cring (Rr:=Zr)).



Ltac cring_simplify_aux lterm fv lexpr hyp :=
    match lterm with
      | ?t0::?lterm =>
    match lexpr with
      | ?e::?le =>
        let t := constr:(@Ring_polynom.norm_subst
          Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb Z.quotrem O nil e) in
        let te :=
          constr:(@Ring_polynom.Pphi_dev
            _ 0 1 _+_ _*_ _-_ -_
            Z 0%Z 1%Z Z.eqb
            Ncring_initial.gen_phiZ
            get_signZ fv t) in
        let eq1 := fresh "ring" in
        let nft := eval vm_compute in t in
        let t':= fresh "t" in
        pose (t' := nft);
        assert (eq1 : t = t');
        [vm_cast_no_check (eq_refl t')|
        let eq2 := fresh "ring" in
        assert (eq2:(@Ring_polynom.PEeval
          _ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (fun n:N => n)
          (@Ring_theory.pow_N _ 1 multiplication) fv e) == te);
        [let eq3 := fresh "ring" in
          generalize (@ring_rw_correct _ 0 1 _+_ _*_ _-_ -_ _==_
            ring_setoid
            cring_eq_ext
            cring_almost_ring_theory
            Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb
            Ncring_initial.gen_phiZ
            cring_morph
            N
            (fun n:N => n)
            (@Ring_theory.pow_N _ 1 multiplication)
            cring_power_theory
            Z.quotrem
            cring_div_theory
            get_signZ get_signZ_th
            O nil fv I nil (eq_refl nil) );
          intro eq3; apply eq3; reflexivity|
              match hyp with
                | 1%nat => rewrite eq2
                | ?H => try rewrite eq2 in H
              end];
        let P:= fresh "P" in
        match hyp with
          | 1%nat =>
            rewrite eq1;
            pattern (@Ring_polynom.Pphi_dev
            _ 0 1 _+_ _*_ _-_ -_

            Z 0%Z 1%Z Z.eqb
            Ncring_initial.gen_phiZ
            get_signZ fv t');
            match goal with
              |- (?p ?t) => set (P:=p)
            end;
              unfold t' in *; clear t' eq1 eq2;
              unfold Pphi_dev, Pphi_avoid; simpl;
                repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
                  mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
                  mkpow;simpl)
          | ?H =>
               rewrite eq1 in H;
               pattern (@Ring_polynom.Pphi_dev
            _ 0 1 _+_ _*_ _-_ -_
            Z 0%Z 1%Z Z.eqb
            Ncring_initial.gen_phiZ
            get_signZ fv t') in H;
               match type of H with
                  | (?p ?t) => set (P:=p) in H
               end;
               unfold t' in *; clear t' eq1 eq2;
               unfold Pphi_dev, Pphi_avoid in H; simpl in H;
                repeat (unfold mkmult1, mkmultm1, mkmult_c_pos, mkmult_c,
                  mkadd_mult, mkmult_c_pos, mkmult_pow, mkadd_mult,
                  mkpow in H;simpl in H)
        end; unfold P in *; clear P
        ]; cring_simplify_aux lterm fv le hyp
      | nil => idtac
    end
    | nil => idtac
    end.

Ltac set_variables fv :=
  match fv with
    | nil => idtac
    | ?t::?fv =>
        let v := fresh "X" in
        set (v:=t) in *; set_variables fv
  end.

Ltac deset n:=
   match n with
    | 0%nat => idtac
    | S ?n1 =>
      match goal with
        | h:= ?v : ?t |- ?g => unfold h in *; clear h; deset n1
      end
   end.


Ltac cring_simplify_gen a hyp :=
  let lterm :=
    match a with
      | _::_ => a
      | _ => constr:(a::nil)
    end in
   let reif := list_reifyl0 lterm in
    match reif with
      | (?fv, ?lexpr) => idtac lterm; idtac fv; idtac lexpr;
      let n := eval compute in (length fv) in
      idtac n;
      let lt:=fresh "lt" in
      set (lt:= lterm);
      let lv:=fresh "fv" in
      set (lv:= fv);
      
      set_variables fv;
      let lterm1 := eval unfold lt in lt in
      let lv1 := eval unfold lv in lv in
        idtac lterm1; idtac lv1;
      cring_simplify_aux lterm1 lv1 lexpr hyp;
      clear lt lv;
      
      deset n
    end.

Tactic Notation "cring_simplify" constr(lterm):=
 cring_simplify_gen lterm 1%nat.

Tactic Notation "cring_simplify" constr(lterm) "in" ident(H):=
 cring_simplify_gen lterm H.