Library Stdlib.nsatz.NsatzTactic

From Stdlib Require Import 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 Export Algebra_syntax.
From Stdlib Require Export Ncring.
From Stdlib Require Export Ncring_initial.
From Stdlib Require Export Ncring_tac.
From Stdlib Require Export Integral_domain.
From Stdlib Require Import ZArith.
From Stdlib Require Import Lia.


Section nsatz1.

Context {R:Type}`{Rid:Integral_domain R}.

Lemma psos_r1b: forall x y:R, x - y == 0 -> x == y.

Lemma psos_r1: forall x y, x == y -> x - y == 0.

Lemma nsatzR_diff: forall x y:R, not (x == y) -> not (x - y == 0).

Export Ring_polynom.
Export InitialRing.

Definition PolZ := Pol Z.
Definition PEZ := PExpr Z.

Definition P0Z : PolZ := P0 (C:=Z) 0%Z.

Definition PolZadd : PolZ -> PolZ -> PolZ :=
  @Padd Z 0%Z Z.add Z.eqb.

Definition PolZmul : PolZ -> PolZ -> PolZ :=
  @Pmul Z 0%Z 1%Z Z.add Z.mul Z.eqb.

Definition PolZeq := @Peq Z Z.eqb.

Definition norm :=
  @norm_aux Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Z.eqb.

Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ :=
 match la, lp with
 | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp)
 | _, _ => P0Z
 end.

Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) :=
 match lla with
 | List.nil => lp
 | la::lla => compute_list lla ((mult_l la lp)::lp)
 end.

Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) :=
 let (lla, lq) := certif in
 let lp := List.map norm lpe in
 PolZeq (norm qe) (mult_l lq (compute_list lla lp)).

Definition PhiR : list R -> PolZ -> R :=
  (Pphi ring0 add mul
    (InitialRing.gen_phiZ ring0 ring1 add mul opp)).

Definition PEevalR : list R -> PEZ -> R :=
   PEeval ring0 ring1 add mul sub opp
    (gen_phiZ ring0 ring1 add mul opp)
         N.to_nat pow.

Lemma P0Z_correct : forall l, PhiR l P0Z = 0.

Lemma Rext: ring_eq_ext add mul opp _==_.

Lemma Rset : Setoid_Theory R _==_.

Definition Rtheory:ring_theory ring0 ring1 add mul sub opp _==_.
Defined.

Lemma PolZadd_correct : forall P' P l,
  PhiR l (PolZadd P P') == ((PhiR l P) + (PhiR l P')).

Lemma PolZmul_correct : forall P P' l,
  PhiR l (PolZmul P P') == ((PhiR l P) * (PhiR l P')).

Lemma R_power_theory
     : Ring_theory.power_theory ring1 mul _==_ N.to_nat pow.

Lemma norm_correct :
  forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe).

Lemma PolZeq_correct : forall P P' l,
  PolZeq P P' = true ->
  PhiR l P == PhiR l P'.

Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop :=
  match l with
  | List.nil => True
  | a::l => Interp a == 0 /\ Cond0 A Interp l
  end.

Lemma mult_l_correct : forall l la lp,
  Cond0 PolZ (PhiR l) lp ->
  PhiR l (mult_l la lp) == 0.

Lemma compute_list_correct : forall l lla lp,
  Cond0 PolZ (PhiR l) lp ->
  Cond0 PolZ (PhiR l) (compute_list lla lp).

Lemma check_correct :
  forall l lpe qe certif,
    check lpe qe certif = true ->
    Cond0 PEZ (PEevalR l) lpe ->
    PEevalR l qe == 0.


Definition R2:= 1 + 1.

Fixpoint IPR p {struct p}: R :=
  match p with
    xH => ring1
  | xO xH => 1+1
  | xO p1 => R2*(IPR p1)
  | xI xH => 1+(1+1)
  | xI p1 => 1+(R2*(IPR p1))
  end.

Definition IZR1 z :=
  match z with Z0 => 0
             | Zpos p => IPR p
             | Zneg p => -(IPR p)
  end.

Fixpoint interpret3 t fv {struct t}: R :=
  match t with
  | (PEadd t1 t2) =>
       let v1 := interpret3 t1 fv in
       let v2 := interpret3 t2 fv in (v1 + v2)
  | (PEmul t1 t2) =>
       let v1 := interpret3 t1 fv in
       let v2 := interpret3 t2 fv in (v1 * v2)
  | (PEsub t1 t2) =>
       let v1 := interpret3 t1 fv in
       let v2 := interpret3 t2 fv in (v1 - v2)
  | (PEopp t1) =>
       let v1 := interpret3 t1 fv in (-v1)
  | (PEpow t1 t2) =>
       let v1 := interpret3 t1 fv in pow v1 (N.to_nat t2)
  | (PEc t1) => (IZR1 t1)
  | PEO => 0
  | PEI => 1
  | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0
  end.

End nsatz1.

Ltac equality_to_goal H x y:=
   try (generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H)
.

Ltac equalities_to_goal :=
  lazymatch goal with
  | H: (_ ?x ?y) |- _ => equality_to_goal H x y
  | H: (_ _ ?x ?y) |- _ => equality_to_goal H x y
  | H: (_ _ _ ?x ?y) |- _ => equality_to_goal H x y
  | H: (_ _ _ _ ?x ?y) |- _ => equality_to_goal H x y

  | H: (?x == ?y) |- _ => equality_to_goal H x y
   end.


Ltac parametres_en_tete fv lp :=
    match fv with
     | (@nil _) => lp
     | (@cons _ ?x ?fv1) =>
       let res := AddFvTail x lp in
         parametres_en_tete fv1 res
    end.

Ltac append1 a l :=
 match l with
 | (@nil _) => constr:(cons a l)
 | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l')
 end.

Ltac rev l :=
  match l with
   |(@nil _) => l
   | (cons ?x ?l) => let l' := rev l in append1 x l'
  end.

Ltac nsatz_call_n info nparam p rr lp kont :=

  let ll := constr:(PEc info :: PEc nparam :: PEpow p rr :: lp) in

  nsatz_compute ll;

  match goal with
  | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ =>
    intros _;
    let lci := fresh "lci" in
    set (lci:=lci0);
    let lq := fresh "lq" in
    set (lq:=lq0);
    kont c rr lq lci
  end.

Ltac nsatz_call radicalmax info nparam p lp kont :=
  let rec try_n n :=
    lazymatch n with
    | 0%N => fail
    | _ =>
        (let r := eval compute in (N.sub radicalmax (N.pred n)) in
         nsatz_call_n info nparam p r lp kont) ||
         let n' := eval compute in (N.pred n) in try_n n'
    end in
  try_n radicalmax.

Ltac lterm_goal g :=
  match g with
    ?b1 == ?b2 => constr:(b1::b2::nil)
  | ?b1 == ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l)
  end.

Ltac reify_goal l le lb:=
  match le with
     nil => idtac
   | ?e::?le1 =>
        match lb with
         ?b::?lb1 =>
           let x := fresh "B" in
           set (x:= b) at 1;
           change x with (interpret3 e l);
           clear x;
           reify_goal l le1 lb1
        end
  end.

Ltac get_lpol g :=
  match g with
  (interpret3 ?p _) == _ => constr:(p::nil)
  | (interpret3 ?p _) == _ -> ?g =>
       let l := get_lpol g in constr:(p::l)
  end.

Ltac nsatz_internal_discrR := idtac.

Ltac nsatz_generic radicalmax info lparam lvar :=
 let nparam := eval compute in (Z.of_nat (List.length lparam)) in
 match goal with
  |- ?g => let lb := lterm_goal g in
     match (lazymatch lvar with
              |(@nil _) =>
                 lazymatch lparam with
                 |(@nil _) =>
                    let r := list_reifyl0 lb in
                    r
                   |_ =>
                     let reif := list_reifyl0 lb in
                     match reif with
                       |(?fv, ?le) =>
                         let fv := parametres_en_tete fv lparam in
                           
                         list_reifyl fv lb
                     end
                  end
              |_ =>
                 let fv := parametres_en_tete lvar lparam in
                list_reifyl fv lb
            end) with
          |(?fv, ?le) =>
            reify_goal fv le lb ;
            match goal with
                   |- ?g =>
                       let lp := get_lpol g in
                       let lpol := eval compute in (List.rev lp) in
                       intros;

  let SplitPolyList kont :=
    match lpol with
    | ?p2::?lp2 => kont p2 lp2
    | _ => idtac "polynomial not in the ideal"
    end in

  SplitPolyList ltac:(fun p lp =>
    let p21 := fresh "p21" in
    let lp21 := fresh "lp21" in
    set (p21:=p) ;
    set (lp21:=lp);

    nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci =>
      let q := fresh "q" in
      set (q := PEmul c (PEpow p21 r));
      let Hg := fresh "Hg" in
      assert (Hg:check lp21 q (lci,lq) = true);
      [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate"
      | let Hg2 := fresh "Hg" in
            assert (Hg2: (interpret3 q fv) == 0);
        [ idtac;
          generalize (@check_correct _ _ _ _ _ _ _ _ _ _ _ fv lp21 q (lci,lq) Hg);
          let cc := fresh "H" in
              idtac; intro cc; apply cc; clear cc;
           idtac;
          repeat (split;[assumption|idtac]); exact I
        | idtac;
          apply Rintegral_domain_pow with (interpret3 c fv) (N.to_nat r);
           idtac;
            try apply integral_domain_one_zero;
            try apply integral_domain_minus_one_zero;
            try trivial;
            try exact integral_domain_one_zero;
            try exact integral_domain_minus_one_zero
          || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation,
                     one, one_notation, multiplication, mul_notation, zero, zero_notation;
                     nsatz_internal_discrR || lia ])
          || ( idtac) || idtac "could not prove discrimination result"
        ]
      ]
)
)
end end end .

Ltac nsatz_default:=
  intros;
  try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _);
  match goal with |- (@equality ?r _ _ _) =>
    repeat equalities_to_goal;
    nsatz_generic 6%N 1%Z (@nil r) (@nil r)
  end.

Tactic Notation "nsatz" := nsatz_default.

Tactic Notation "nsatz" "with"
 "radicalmax" ":=" constr(radicalmax)
 "strategy" ":=" constr(info)
 "parameters" ":=" constr(lparam)
 "variables" ":=" constr(lvar):=
  intros;
  try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _);
  match goal with |- (@equality ?r _ _ _) =>
    repeat equalities_to_goal;
    nsatz_generic radicalmax info lparam lvar
  end.

From Stdlib Require Import QArith_base.

#[global]
Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
Defined.

#[global]
Instance Qri : (Ring (Ro:=Qops)).
Defined.

Lemma Q_one_zero: not (Qeq 1%Q 0%Q).

#[global]
Instance Qcri: (Cring (Rr:=Qri)).


#[global]
Instance Qdi : (Integral_domain (Rcr:=Qcri)).
Defined.

Lemma Z_one_zero: 1%Z <> 0%Z.

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


#[global]
Instance Zdi : (Integral_domain (Rcr:=Zcri)).
Defined.