Library Stdlib.nsatz.ENsatzTactic
From Stdlib Require Import BinPos.
From Stdlib Require Import BinList.
From Stdlib Require Import BinNat.
From Stdlib Require Import BinInt.
From Stdlib Require Import Ncring.
From Stdlib Require Import NsatzTactic.
Section ensatz.
Context {R:Type}`{Rid:Integral_domain R}.
Local Fixpoint TTL {A: Type} (l : list A) {struct l} : Type :=
match l with
| nil => unit
| _ :: l0 => (A * TTL l0)%type
end.
Local Fixpoint add_coef
(l: list PolZ) (a : list PolZ) (c : PolZ)
{struct l} : (TTL l -> TTL l) :=
match l, a return (TTL l -> TTL l) with
| nil, _ => (fun _ => tt)
| _, nil => (fun x => x)
| _ :: q , hx :: qx =>
let coef := PolZmul c hx in
fun x => (PolZadd coef (fst x), add_coef q qx c (snd x))
end.
Local Fixpoint cofactors_aux
(lpe: list PolZ) (lq: list PEZ): TTL lpe :=
match lpe, lq return (TTL lpe) with
| nil, _ => tt
| h::q, nil=> (P0Z, cofactors_aux q lq)
| h1::q1, h2::q2=> (norm h2, cofactors_aux q1 q2 )
end.
Local Fixpoint cofactors
(lla : list (list PEZ)) (lpe: list PolZ)
(lq: list PEZ) : TTL lpe :=
match lla return (TTL lpe) with
| nil => cofactors_aux lpe lq
| h::q =>
let l := cofactors q ((mult_l h lpe) :: lpe) lq in
add_coef lpe (map norm h) (fst l) (snd l)
end.
Local Fixpoint ideal_witness
(A : Type) (Interp : A -> R) (l : list A) {struct l} :
(TTL l -> R) :=
match l return (TTL l -> R) with
| nil => fun _ => ring0
| a :: l0 =>
fun n => add
(mul (Interp (fst n)) (Interp a))
(ideal_witness A Interp l0 (snd n))
end.
Local Definition PhiR := @PhiR R ring0 ring1 add mul opp.
Local Lemma factories_compute_list :
forall lla l lpe lq,
PhiR l (mult_l lq (compute_list lla lpe)) ==
ideal_witness PolZ (PhiR l) lpe (cofactors lla lpe lq).
Local Fixpoint TTTL
{A : Type} (B: Type) (l : list (bool * A)) {struct l} : Type :=
match l with
| nil => unit
| (true, _) :: l0 => (B * TTTL B l0)%type
| (false, _) :: l0 => TTTL B l0
end.
Local Fixpoint get_tagged
(A B : Type) (norm : A -> B) (l: list (bool*A))
{struct l} : (TTL (map norm (map snd l)) -> TTTL B l) :=
match l return (TTL (map norm (map snd l)) -> TTTL B l) with
| nil => fun _ => tt
| (true, _) :: q => fun x => (fst x, get_tagged A B norm q (snd x))
| (false, _) :: q => fun x => (get_tagged A B norm q (snd x))
end.
Local Definition tagged_cofactors (lpe: list (prod bool PEZ)) lci lq:=
let p := cofactors lci (map norm (map snd lpe)) lq in
get_tagged PEZ PolZ norm lpe p.
Local Fixpoint denotHyps
{A : Type} (Interp : A -> R) (l : list (bool * A)) {struct l} : Prop :=
match l with
| nil => True
| (true, a) :: l0 => (denotHyps Interp l0)
| (false, a) :: l0 => ((Interp a) == 0) /\ (denotHyps Interp l0)
end.
Local Fixpoint t_ideal_witness
{A B : Type} (Interp : A -> R) (Interp' : B -> R) (l : list (bool * A))
{struct l} : (TTTL B l -> R) :=
match l return (TTTL B l -> R) with
| nil => (fun _ => ring0)
| (true, a) :: l0 => (fun n => add (mul (Interp' (fst n)) (Interp a))
(t_ideal_witness Interp Interp' l0 (snd n)))
| (false, a) :: l0 => t_ideal_witness Interp Interp' l0
end.
Local Theorem check_correct:
forall l lpe qe lci lq ,
check (map snd lpe) qe (lci,lq) = true ->
denotHyps (PEevalR l) lpe ->
(PEevalR l qe) ==
t_ideal_witness (PEevalR l) (PhiR l) lpe (tagged_cofactors lpe lci lq).
Local Fixpoint inter
{A B: Type} (Interp: B -> R) (l: list (bool*A)) {struct l} :
(TTTL B l -> TTTL R l) :=
match l return (TTTL B l -> TTTL R l) with
| nil => fun _ => tt
| (true, _) :: q => fun x => (Interp (fst x), inter Interp q (snd x))
| (false, _) :: q => fun x => inter Interp q x
end.
Local Corollary check_correct_exists :
forall l lpe qe lci lq ,
check (map snd lpe) qe (lci,lq) = true ->
denotHyps (PEevalR l) lpe ->
exists n, ((PEevalR l qe) == t_ideal_witness (PEevalR l) (fun x => x) lpe n).
End ensatz.
Module Tag_pl.
Local Definition tag_polynome (l:list (PExpr Z)) n :=
let l := List.rev l in
let hdn_true := List.map (pair true) (firstn n l) in
let tln_false := List.map (pair false) (skipn n l) in
let l := hdn_true ++ tln_false in
List.rev l.
Ltac tag_pl lp21 n :=
eval compute in (tag_polynome lp21 n).
End Tag_pl.
Section poly_sort.
Context {T:Type}.
Context (compare : T -> T -> comparison).
Inductive MPoly : Type:=
| Poly : MPoly -> (PExpr Z) -> T -> MPoly
| Pc : (PExpr Z) -> MPoly.
Local Fixpoint mult_mpoly (c : PExpr Z) (p : MPoly) : MPoly :=
match p with
| Pc e => Pc (PEmul e c)
| Poly p e v => Poly (mult_mpoly c p) (PEmul e c) v
end.
Inductive Monom : Type:=
| Mon : (PExpr Z) -> T -> Monom
| Monc : (PExpr Z) -> Monom.
Local Fixpoint add_monom_poly (p: MPoly) (m: Monom) :=
match p with
| Pc e1 =>
match m with
| Monc e2 => Pc (PEadd e1 e2)
| Mon e2 v => Poly p e2 v
end
| Poly p' e1 v1 =>
match m with
| Monc e2 => Poly (add_monom_poly p' m) e1 v1
| Mon e2 v2 =>
match compare v1 v2 with
| Eq => Poly p' (PEadd e1 e2) v1
| Gt => Poly (add_monom_poly p' m) e1 v1
| Lt => Poly p e2 v2
end
end
end.
Local Fixpoint add_mpoly (p1 p2 : MPoly) : MPoly :=
match p1 with
| Pc e1 => add_monom_poly p2 (Monc e1)
| Poly p1' e1 v1 => add_mpoly p1' (add_monom_poly p2 (Mon e1 v1))
end.
Local Fixpoint opp_mpoly (p: MPoly) : MPoly :=
match p with
| Pc e => Pc (PEopp e)
| Poly p e v => Poly (opp_mpoly p) (PEopp e) v
end.
Local Fixpoint get_coef (p: MPoly) :=
match p with
| Pc e => e :: nil
| Poly p e v => e :: get_coef p
end.
End poly_sort.
Module Ensatz_solve.
Local Ltac mk_tuple R l f :=
match l with
| (?a :: ?h) =>
let t := mk_tuple R h f in
constr:((t, f a))
| (?a1 :: ?a2 :: @nil R) => constr:((f a2,f a1))
end.
Local Ltac destr_tuple R l f :=
match goal with
| x : (R * ?A)%type |- _ =>
let z := fresh "z" in
destruct x as [z x];
let l := constr:(z :: l) in
destr_tuple R l f
| x : (unit)%type |- _ =>
let l := eval compute in (l) in
let t := mk_tuple R l f in
exists t
end.
Ltac mk_exists R x f :=
match goal with
| x : (R * unit)%type |- _ =>
let z := fresh "z" in
destruct x as [z x]; exists (f z)
| x : (R * ?A)%type |- _ =>
destr_tuple R constr:(@nil R) f
end.
Ltac ensatz_solve cr R p2 lp2 n fv info :=
let p21 := fresh "p21" in
let lp21 := fresh "lp21" in
let n21 := fresh "n21" in
let lv := fresh "lv" in
set (p21:=p2); set (lp21:=lp2); set (n21:= n); set(lv := fv);
NsatzTactic.nsatz_call 1%N info 0%Z p2 lp2
ltac:(fun c r lq lci =>
let Hg := fresh "Hg" in
let c21 := fresh "c" in
set (c21 := c);
let p211 := constr: (PEmul c p21) in
let pl := Tag_pl.tag_pl lp21 n in
assert (Hg:check lp21 p211 (lci,lq) = true);
[vm_compute; reflexivity |];
assert (Hg2: denotHyps (PEevalR lv) pl);
[repeat (split;[assumption|idtac]); exact I|];
generalize (@check_correct_exists
_ _ _ _ _ _ _ _ _ _ _
lv pl p211 lci lq Hg Hg2);
let x := fresh "x" in
let H1 := fresh "H" in
intros [x H1];
cbv delta [TTTL] iota beta match in x;
match c with
| PEc((-1)%Z) => mk_exists R x constr:(fun x:R => -x);
symmetry in H1
| PEc(1%Z) => mk_exists R x constr:(fun x:R => x)
end;
cbv delta [lv p21] in H1;
cbv delta
[PEevalR
t_ideal_witness
Ring_polynom.PEeval
gen_phiZ gen_phiPOS
InitialRing.gen_phiZ
InitialRing.gen_phiPOS
BinList.nth
jump fst snd hd]
iota beta match in H1;
repeat unfold snd;
repeat unfold fst;
apply NsatzTactic.psos_r1b;
NsatzTactic.equalities_to_goal cr;
intros <-; cring
).
Module Reifi.
Inductive Var {A: Type}: Type :=
| mRef: A -> Var
| fstVar : forall B, @Var (A*B) -> @Var A
| sndVar : forall B, @Var (B*A) -> @Var A.
Local Ltac reify_evar_aux term :=
match term with
| (fun e => fst (@?P e)) =>
let term' := reify_evar_aux P in
constr:(fun x => @fstVar _ _ (term' x))
| (fun e => snd (@?P e)) =>
let term' := reify_evar_aux P in
constr:(fun x => @sndVar _ _ (term' x))
| (fun e:?T => e) => constr:(fun e :T => mRef e)
end.
Local Ltac reify_evar R term :=
match term with
| (fun e => fst _) =>
let term' := reify_evar_aux term in
constr:
(fun e' =>
@Poly (@Var R) (@Pc (@Var R) (PEc 0%Z)) (PEc 1%Z) (term' e'))
| (fun e => snd _) =>
let term' := reify_evar_aux term in
constr:
(fun e' =>
@Poly (@Var R) (@Pc (@Var R) (PEc 0%Z)) (PEc 1%Z) (term' e'))
| (fun e:?T => e) =>
constr:
(fun e':T =>
@Poly (@Var T) (@Pc (@Var T) (PEc 0%Z)) (PEc 1%Z) (mRef e'))
end.
Local Fixpoint compare
{A1 A2: Type} (v1 : @Var A1) (v2 : @Var A2): comparison :=
match v1, v2 with
| mRef _, mRef _ => Eq
| fstVar _ v1, fstVar _ v2 => compare v1 v2
| sndVar _ v1, sndVar _ v2 => compare v1 v2
| fstVar _ _, sndVar _ _ => Gt
| sndVar _ _, fstVar _ _ => Lt
| _, mRef _ => Gt
| mRef _, _ => Lt
end.
Local Definition add_mpoly
{A: Type} (p1 p2 : @MPoly (@Var A)) : @MPoly (@Var A):=
add_mpoly compare p1 p2.
Local Ltac reify_aux R ring0 ring1 add mul sub opp lvar term:=
match term with
| (fun e1 => ?op (@?E1 e1) (@?E2 e1)) =>
let _ := match goal with _ => convert add op end in
let E1' := reify_aux R ring0 ring1 add mul sub opp lvar E1 in
let E2' := reify_aux R ring0 ring1 add mul sub opp lvar E2 in
constr:(fun x => add_mpoly (E1' x) (E2' x))
| (fun e1 => ?op (@?E1 e1) (@?E2 e1)) =>
let _ := match goal with _ => convert sub op end in
let E1' := reify_aux R ring0 ring1 add mul sub opp lvar E1 in
let E2' := reify_aux R ring0 ring1 add mul sub opp lvar E2 in
constr:(fun x => add_mpoly (E1' x) (opp_mpoly (E2' x)))
| (fun e1 => ?op ?E (@?E1 e1)) =>
let _ := match goal with _ => convert mul op end in
let E1' := reify_aux R ring0 ring1 add mul sub opp lvar E1 in
let E' := reify_term R ring0 ring1 add mul sub opp lvar E in
constr:(fun x => mult_mpoly E' (E1' x))
| (fun e1 => ?op (@?E1 e1) ?E) =>
let _ := match goal with _ => convert mul op end in
let E1' := reify_aux R ring0 ring1 add mul sub opp lvar E1 in
let E' := reify_term R ring0 ring1 add mul sub opp lvar E in
constr:(fun x => mult_mpoly E' (E1' x))
| (fun e => @?E e) => reify_evar R E
| (fun e => ?op (@?E e)) =>
let _ := match goal with _ => convert opp op end in
let E' := reify_aux R ring0 ring1 add mul sub opp lvar E in
constr:(fun x => opp_mpoly (E' x))
| (fun _:?T => ?E) =>
let E' := reify_term R ring0 ring1 add mul sub opp lvar E in
constr:(fun _:T => @Pc (@Var R) E')
end.
Local Ltac reify R Tring lv e :=
lazymatch Tring with
| Ring (T:=?R) (ring0:=?ring0) (ring1:=?ring1)
(add:=?add) (mul:=?mul) (sub:=?sub) (opp:=?opp) =>
reify_aux R ring0 ring1 add mul sub opp lv e
end.
Local Definition coef {A R:Type} (p: A -> @MPoly (@Var R)) :=
fun x => get_coef (p x).
Local Definition merge {A R:Type} (p1 p2: A -> @MPoly (@Var R)) :=
fun x => add_mpoly (p1 x) (opp_mpoly (p2 x)).
Ltac reify_goal R Tring e :=
match e with
| (fun e1 : _ => ?eq (@?P1 e1) (@?P2 e1)) =>
let lvar := open_constr:(_ :> list R) in
let xl := reify R Tring lvar P1 in
let xr := reify R Tring lvar P2 in
let x :=
eval cbv delta
[merge
coef
get_coef
add_mpoly
ENsatzTactic.add_mpoly
mult_mpoly
add_monom_poly
compare
opp_mpoly]
beta iota in (coef (merge xr xl))
in
constr:((lvar,x))
end.
End Reifi.
Ltac hterm R g :=
match g with
| (exists _: _, _ ) => constr:((@nil R))
| ?b1 == ?b2 -> ?g =>
let l := hterm R g in
constr:((b1 :: l))
end.
End Ensatz_solve.
Module Eensatz_solve.
Local Ltac econstrain_aux R ring0 ring1 add mul opp l lc lv z:=
match open_constr:((lc, lv)) with
|((?c, ?q1), @cons _ ?v ?q2) =>
let c := eval cbv delta [l] in (@PhiR R ring0 ring1 add mul opp l c) in
let c :=
eval cbv delta
[PhiR
NsatzTactic.PhiR
Pphi
gen_phiZ
gen_phiPOS
pow_pos
jump hd tl]
iota beta match in c
in
let v := eval cbv delta [l] in (PEevalR l v) in
let v :=
eval cbv delta
[PEevalR
t_ideal_witness
Ring_polynom.PEeval
gen_phiZ gen_phiPOS
InitialRing.gen_phiZ
InitialRing.gen_phiPOS
BinList.nth
jump tl fst snd hd]
iota beta match in v
in
assert (v = z * c) by reflexivity;
econstrain_aux R ring0 ring1 add mul opp l q1 q2 z
| (_, _) => idtac
end.
Local Ltac econstrain R Tring l lc lv z :=
lazymatch Tring with
| Ring (T:=?R) (ring0:=?ring0) (ring1:=?ring1)
(add:=?add) (mul:=?mul) (sub:=?sub) (opp:=?opp) =>
econstrain_aux R ring0 ring1 add mul opp l lc lv z
end.
Ltac ensatz_solve R Tring p2 lp2 n fv vs info :=
let p21 := fresh "p21" in
let lp21 := fresh "lp21" in
let lv := fresh "lv" in
let lvs := fresh "lvs" in
set (p21:=p2);set (lp21:=lp2); set(lv := fv); set (lvs := vs);
NsatzTactic.nsatz_call 1%N info 0%Z p2 lp2
ltac:(fun c r lq lci =>
let Hg := fresh "Hg" in
let c21 := fresh "c" in
let p211 := constr: (PEmul c p21) in
let pl := Tag_pl.tag_pl lp21 n in
assert (Hg:check lp21 p211 (lci,lq) = true);
[vm_compute; reflexivity |];
assert (Hg2: denotHyps (PEevalR lv) pl);
[repeat (split;[assumption|idtac]); exact I|];
generalize (@check_correct
_ _ _ _ _ _ _ _ _ _ _
lv pl p211 lci lq Hg Hg2);
let Hc := fresh "Hc" in
intro Hc;
let Cert := fresh "Cert" in
let cert := constr: (tagged_cofactors pl lci lq) in
set (Cert := cert);
specialize (eq_refl Cert);
unfold Cert at 2;
let HCert := fresh "HCert" in
intro HCert;
fold Cert in Hc;
compute in Cert;
let y := eval simpl in (map (PEevalR lv) vs) in
let cert := eval cbv delta [Cert] in Cert in
match c with
| PEc ((-1)%Z) => econstrain R Tring lv cert vs ((-1)%Z);
symmetry in Hc
| PEc (1%Z) => econstrain R Tring lv cert vs (1%Z)
end;
cbv delta [Cert lv p21] in Hc;
cbv delta
[PEevalR
t_ideal_witness
Ring_polynom.PEeval
gen_phiZ gen_phiPOS
InitialRing.gen_phiZ
InitialRing.gen_phiPOS
BinList.nth
jump tl fst snd hd]
iota beta match in Hc;
cbv delta
[PhiR
NsatzTactic.PhiR
Pphi gen_phiZ
gen_phiPOS
pow_pos
jump hd tl]
iota beta match in Hc;
apply NsatzTactic.psos_r1b;
apply psos_r1 in Hc;
etransitivity;[|apply Hc];
cring
).
Module Reifi.
Local Definition add_mpoly (p1 p2 : @MPoly positive) : @MPoly positive:=
add_mpoly Pos.compare p1 p2.
Local Ltac reify_aux R ring0 ring1 add mul sub opp lvar term:=
match term with
| ?E =>
let __ := match E with _ => is_ground E end in
let E' := reify_term R ring0 ring1 add mul sub opp lvar E in
constr:((@Pc positive E'))
| ?E =>
let __ := match E with _ => is_evar E end in
let E' := reify_term R ring0 ring1 add mul sub opp lvar E in
let n :=
match E' with
| PEX _ ?n => n
end
in
constr:(@Poly positive (@Pc positive (PEc 0%Z)) (PEc 1%Z) n)
| ?op ?E1 ?E2 =>
let _ := match goal with _ => convert mul op end in
let _ := match E1 with _ => is_ground E1 end in
let _ := match E2 with _ => has_evar E2 end in
let E1' := reify_term R ring0 ring1 add mul sub opp lvar E1 in
let E2' := reify_aux R ring0 ring1 add mul sub opp lvar E2 in
constr:(mult_mpoly E1' E2')
| ?op ?E1 ?E2 =>
let _ := match goal with _ => convert mul op end in
let _ := match E1 with _ => has_evar E1 end in
let _ := match E2 with _ => is_ground E2 end in
let E1' := reify_aux R ring0 ring1 add mul sub opp lvar E1 in
let E2' := reify_term R ring0 ring1 add mul sub opp lvar E2 in
constr:(mult_mpoly E2' E1')
| ?op ?E1 ?E2 =>
let _ := match goal with _ => convert add op end in
let E1' := reify_aux R ring0 ring1 add mul sub opp lvar E1 in
let E2' := reify_aux R ring0 ring1 add mul sub opp lvar E2 in
constr:(add_mpoly E1' E2')
| ?op ?E1 ?E2 =>
let _ := match goal with _ => convert sub op end in
let E1' := reify_aux R ring0 ring1 add mul sub opp lvar E1 in
let E2' := reify_aux R ring0 ring1 add mul sub opp lvar E2 in
constr:(add_mpoly E1' (opp_mpoly E2'))
| ?op ?E =>
let _ := match goal with _ => convert opp op end in
let E' := reify_aux R ring0 ring1 add mul sub opp lvar E in
constr:(opp_mpoly E')
end.
Local Ltac areify R Tring lv e :=
lazymatch Tring with
| Ring (T:=?R) (ring0:=?ring0) (ring1:=?ring1)
(add:=?add) (mul:=?mul) (sub:=?sub) (opp:=?opp) =>
reify_aux R ring0 ring1 add mul sub opp lv e
end.
Local Fixpoint variables (p: @MPoly positive) :=
match p with
| Pc e => nil
| Poly p e v => (PEX Z v) :: variables p
end.
Ltac reify_goal R Tring :=
match goal with
| |- ?eq ?E1 ?E2 =>
let lvar := open_constr:(_ :> list R) in
let xl := areify R Tring lvar E1 in
let xr := areify R Tring lvar E2 in
let poly := eval vm_compute in (add_mpoly xr (opp_mpoly xl)) in
let x := eval vm_compute in (get_coef poly) in
let v := eval vm_compute in (variables poly) in
constr:((lvar,x, v))
end.
End Reifi.
Ltac hterm R g :=
match g with
| ?eq ?b1 ?b2 => constr:((@nil R))
| ?b1 == ?b2 -> ?g =>
let l := hterm R g in
constr:((b1 :: l))
end.
End Eensatz_solve.
Local Ltac reify_h lv lb :=
match lb with
| @nil ?R =>
let _ := match goal with _ => close_varlist lv end in
constr:((lv, (@nil (PExpr Z))))
| @cons ?R _ _ =>
let R_ring := constr:(_ :> Ring (T:=R)) in
list_reifyl R_ring lv lb
end.
Ltac nsatz_guess_domain :=
let eq := lazymatch goal with
| |- @ex _ (fun _ : _ => ?eq _ _ ) => eq
| |- ?eq _ _ => eq
end
in
let di :=
lazymatch
open_constr:(ltac:(typeclasses eauto):Integral_domain (ring_eq:=eq))
with?di => di end
in
let __ := match di with _ => assert_fails (is_evar di) end in
di.
Local Lemma efactor:
forall A B P, (exists x : A * B, P (fst x) (snd x)) -> (exists x : A, exists y: B, P x y).
Ltac ensatz_default info :=
intros;
repeat apply efactor;
let di := nsatz_guess_domain in
let r := lazymatch type of di with Integral_domain(R:=?r) => r end in
let cr := lazymatch type of di with Integral_domain(Rcr:=?cr) => cr end in
let R_ring := constr:(_ :> Ring (T:=r)) in
let Tring := type of R_ring in
match goal with
| |- @ex _ ?e =>
match Ensatz_solve.Reifi.reify_goal r Tring e with
| (?lvar, (fun _: _ => ?x)) =>
let b :=
eval cbv delta [List.last] iota beta match
in (List.last x (PEc 0%Z))
in
let b := constr: (PEopp b) in
let l := constr: (List.removelast x) in
let n := eval compute in (List.length l) in
repeat NsatzTactic.equalities_to_goal cr;
match goal with
|- ?g =>
let lb := Ensatz_solve.hterm r g in
intros;
match reify_h lvar lb with
| (?fv, ?le) =>
let l := constr: (List.rev_append le l) in
let le := constr: (b :: l) in
let lpol := eval compute in le in
match lpol with
| ?p2::?lp2 => Ensatz_solve.ensatz_solve cr r p2 lp2 n fv info
| ?g => idtac "polynomial not in the ideal"
end
end
end
end
| |- ?eq ?E1 ?E2 =>
match Eensatz_solve.Reifi.reify_goal r Tring with
| (?lvar, ?x, ?v) =>
let b := eval cbv delta [List.last] iota beta match
in (List.last x (PEc 0%Z))
in
let b := constr: (PEopp b) in
let l := constr: (List.removelast x) in
let n := eval compute in (List.length l) in
repeat NsatzTactic.equalities_to_goal cr;
match goal with
|- ?g =>
let lb := Eensatz_solve.hterm r g in
intros;
match reify_h lvar lb with
| (?fv, ?le) =>
let l := constr: (List.rev_append le l) in
let le := constr: (b :: l) in
let lpol := eval compute in le in
match lpol with
| ?p2::?lp2 => Eensatz_solve.ensatz_solve r Tring p2 lp2 n fv v info
| ?g => idtac "polynomial not in the ideal"
end
end
end
end
end.
Tactic Notation "ensatz" := ensatz_default 1%Z.
Tactic Notation "ensatz" "with"
"strategy" ":=" constr(info) :=
ensatz_default info.