# Library Coq.nsatz.NsatzTactic

Require Import List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Export Morphisms Setoid Bool.
Require Export Algebra_syntax.
Require Export Ncring.
Require Export Ncring_initial.
Require Export Ncring_tac.
Require Export Integral_domain.
Require Import ZArith.
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 :=

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

Definition PolZeq := @Peq Z Zeq_bool.

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

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 :=
(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
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

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.

We only make use of discrR if nsatz support for reals is loaded. To do this, we redefine this tactic in Nsatz.v to make use of real discrimination.
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
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"
"strategy" ":=" constr(info)
"parameters" ":=" constr(lparam)
"variables" ":=" constr(lvar):=
intros;
try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _);
match goal with |- (@equality ?r _ _ _) =>
repeat equalities_to_goal;
end.

Require Import QArith.

#[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.