Require Import List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Import Ring_polynom Ring_tac InitialRing.
Require Export Morphisms Setoid Bool.
Class Zero (
A :
Type) := {
zero :
A}.
Notation "0" :=
zero.
Class One (
A :
Type) := {
one :
A}.
Notation "1" :=
one.
Class Addition (
A :
Type) := {
addition :
A ->
A ->
A}.
Notation "x + y" := (
addition x y).
Class Multiplication (
A :
Type) := {
multiplication :
A ->
A ->
A}.
Notation "x * y" := (
multiplication x y).
Class Subtraction (
A :
Type) := {
subtraction :
A ->
A ->
A}.
Notation "x - y" := (
subtraction x y).
Class Opposite (
A :
Type) := {
opposite :
A ->
A}.
Notation "- x" := (
opposite x).
Class Ring (
R:
Type) := {
ring0:
R;
ring1:
R;
ring_plus:
R->
R->
R;
ring_mult:
R->
R->
R;
ring_sub:
R->
R->
R;
ring_opp:
R->
R;
ring_eq :
R ->
R ->
Prop;
ring_ring:
ring_theory ring0 ring1 ring_plus ring_mult ring_sub
ring_opp ring_eq;
ring_setoid:
Equivalence ring_eq;
ring_plus_comp:
Proper (
ring_eq==>ring_eq==>ring_eq)
ring_plus;
ring_mult_comp:
Proper (
ring_eq==>ring_eq==>ring_eq)
ring_mult;
ring_sub_comp:
Proper (
ring_eq==>ring_eq==>ring_eq)
ring_sub;
ring_opp_comp:
Proper (
ring_eq==>ring_eq)
ring_opp
}.
Class Domain (
R :
Type) := {
domain_ring:>
Ring R;
domain_axiom_product:
forall x y,
ring_eq (
ring_mult x y)
ring0 ->
(ring_eq x ring0) \/ (ring_eq y ring0);
domain_axiom_one_zero:
not (
ring_eq ring1 ring0)}.
Section domain.
Variable R:
Type.
Variable Rd:
Domain R.
Add Ring Rr: (@
ring_ring R (@
domain_ring R Rd)).
Instance zero_ring :
Zero R := {
zero :=
ring0}.
Instance one_ring :
One R := {
one :=
ring1}.
Instance addition_ring :
Addition R := {
addition x y :=
ring_plus x y}.
Instance multiplication_ring :
Multiplication R := {
multiplication x y :=
ring_mult x y}.
Instance subtraction_ring :
Subtraction R := {
subtraction x y :=
ring_sub x y}.
Instance opposite_ring :
Opposite R := {
opposite x :=
ring_opp x}.
Infix "==" :=
ring_eq (
at level 70,
no associativity).
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).
Require Import ZArith.
Definition PolZ :=
Pol Z.
Definition PEZ :=
PExpr Z.
Definition P0Z :
PolZ := @
P0 Z 0%
Z.
Definition PolZadd :
PolZ ->
PolZ ->
PolZ :=
@
Padd Z 0%
Z Zplus Zeq_bool.
Definition PolZmul :
PolZ ->
PolZ ->
PolZ :=
@
Pmul Z 0%
Z 1%
Z Zplus Zmult Zeq_bool.
Definition PolZeq := @
Peq Z Zeq_bool.
Definition norm :=
@
norm_aux Z 0%
Z 1%
Z Zplus Zmult Zminus Zopp 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 :=
(
Pphi 0
ring_plus ring_mult (
gen_phiZ 0 1
ring_plus ring_mult ring_opp)).
Definition pow (
r :
R) (
n :
nat) :=
pow_N 1
ring_mult r (
Nnat.N_of_nat n).
Definition PEevalR :
list R ->
PEZ ->
R :=
PEeval 0
ring_plus ring_mult ring_sub ring_opp
(
gen_phiZ 0 1
ring_plus ring_mult ring_opp)
Nnat.nat_of_N pow.
Lemma P0Z_correct :
forall l,
PhiR l P0Z = 0.
Lemma Rext:
ring_eq_ext ring_plus ring_mult ring_opp ring_eq.
Lemma Rset :
Setoid_Theory R ring_eq.
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
:
power_theory 1
ring_mult ring_eq Nnat.nat_of_N 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.
Lemma pow_not_zero:
forall p n,
pow p n == 0 ->
p == 0.
Lemma Rdomain_pow:
forall c p r,
~c == ring0 ->
ring_mult c (
pow p r)
== ring0 ->
p == ring0.
Definition R2:=
ring_plus ring1 ring1.
Fixpoint IPR p {
struct p}:
R :=
match p with
xH =>
ring1
|
xO xH =>
ring_plus ring1 ring1
|
xO p1 =>
ring_mult R2 (
IPR p1)
|
xI xH =>
ring_plus ring1 (
ring_plus ring1 ring1)
|
xI p1 =>
ring_plus ring1 (
ring_mult R2 (
IPR p1))
end.
Definition IZR1 z :=
match z with Z0 =>
ring0
|
Zpos p =>
IPR p
|
Zneg p =>
ring_opp(
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 (
ring_plus v1 v2)
| (
PEmul t1 t2) =>
let v1 :=
interpret3 t1 fv in
let v2 :=
interpret3 t2 fv in (
ring_mult v1 v2)
| (
PEsub t1 t2) =>
let v1 :=
interpret3 t1 fv in
let v2 :=
interpret3 t2 fv in (
ring_sub v1 v2)
| (
PEopp t1) =>
let v1 :=
interpret3 t1 fv in (
ring_opp v1)
| (
PEpow t1 t2) =>
let v1 :=
interpret3 t1 fv in pow v1 (
Nnat.nat_of_N t2)
| (
PEc t1) => (
IZR1 t1)
| (
PEX n) =>
List.nth (
pred (
nat_of_P n))
fv 0
end.
End domain.
Ltac equalities_to_goal :=
lazymatch goal with
|
H: (@
ring_eq _ _ ?
x ?
y) |-
_ =>
try generalize (@
psos_r1 _ _ _ _ H);
clear H
end.
Ltac nsatz_domain_begin tacsimpl :=
intros;
try apply (@
psos_r1b _ _);
repeat equalities_to_goal;
tacsimpl.
Ltac generalise_eq_hyps:=
repeat
(
match goal with
|
h : (@
ring_eq _ _ ?
p ?
q)|-
_ =>
revert h
end).
Ltac lpol_goal t :=
match t with
| ?
a = ring0 -> ?
b =>
let r:=
lpol_goal b in
constr:(
a::r)
| ?
a = ring0 =>
constr:(
a::nil)
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 _;
set (
lci:=
lci0);
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 (
Nminus radicalmax (
Npred n))
in
nsatz_call_n info nparam p r lp kont) ||
let n' :=
eval compute in (
Npred n)
in try_n n'
end in
try_n radicalmax.
Class Cclosed_seq T (
l:
list T) := {}.
Instance Iclosed_nil T :
Cclosed_seq (
T:=
T)
nil.
Instance Iclosed_cons T t l `{
Cclosed_seq (
T:=
T)
l} :
Cclosed_seq (
T:=
T) (
t::l).
Class Cfind_at (
R:
Type) (
b:
R) (
l:
list R) (
i:
nat) := {}.
Instance Ifind0 (
R:
Type) (
b:
R)
l:
Cfind_at b (
b::l) 0.
Instance IfindS (
R:
Type) (
b2 b1:
R)
l i `{
Cfind_at R b1 l i} :
Cfind_at b1 (
b2::l) (
S i) | 1.
Definition Ifind0' :=
Ifind0.
Definition IfindS' :=
IfindS.
Definition li_find_at (
R:
Type) (
b:
R)
l i `{
Cfind_at R b l i} {
H:
Cclosed_seq (
T:=
R)
l} :=
(l,i).
Class Creify (
R:
Type) (
e:
PExpr Z) (
l:
list R) (
b:
R) := {}.
Instance Ireify_zero (
R:
Type) (
Rd:
Domain R)
l :
Creify (
PEc 0%
Z)
l ring0.
Instance Ireify_one (
R:
Type) (
Rd:
Domain R)
l :
Creify (
PEc 1%
Z)
l ring1.
Instance Ireify_plus (
R:
Type) (
Rd:
Domain R)
e1 l b1 e2 b2 `{
Creify R e1 l b1} `{
Creify R e2 l b2}
:
Creify (
PEadd e1 e2)
l (
ring_plus b1 b2).
Instance Ireify_mult (
R:
Type) (
Rd:
Domain R)
e1 l b1 e2 b2 `{
Creify R e1 l b1} `{
Creify R e2 l b2}
:
Creify (
PEmul e1 e2)
l (
ring_mult b1 b2).
Instance Ireify_sub (
R:
Type) (
Rd:
Domain R)
e1 l b1 e2 b2 `{
Creify R e1 l b1} `{
Creify R e2 l b2}
:
Creify (
PEsub e1 e2)
l (
ring_sub b1 b2).
Instance Ireify_opp (
R:
Type) (
Rd:
Domain R)
e1 l b1 `{
Creify R e1 l b1}
:
Creify (
PEopp e1)
l (
ring_opp b1).
Instance Ireify_var (
R:
Type)
b l i `{
Cfind_at R b l i}
:
Creify (
PEX _ (
P_of_succ_nat i))
l b | 100.
Class Creifylist (
R:
Type) (
le:
list (
PExpr Z)) (
l:
list R) (
lb:
list R) := {}.
Instance Creify_nil (
R:
Type)
l :
Creifylist nil l (@
nil R).
Instance Creify_cons (
R:
Type)
e1 l b1 le2 lb2 `{
Creify R e1 l b1} `{
Creifylist R le2 l lb2}
:
Creifylist (
e1::le2)
l (
b1::lb2).
Definition li_reifyl (
R:
Type)
le l lb `{
Creifylist R le l lb}
{
H:
Cclosed_seq (
T:=
R)
l} :=
(l,le).
Ltac lterm_goal g :=
match g with
ring_eq ?
b1 ?
b2 =>
constr:(
b1::b2::nil)
|
ring_eq ?
b1 ?
b2 -> ?
g =>
let l :=
lterm_goal g in constr:(
b1::b2::l)
end.
Ltac reify_goal l le lb Rd:=
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 _ Rd e l);
clear x;
reify_goal l le1 lb1 Rd
end
end.
Ltac get_lpol g :=
match g with
ring_eq (
interpret3 _ _ ?
p _)
_ =>
constr:(
p::nil)
|
ring_eq (
interpret3 _ _ ?
p _)
_ -> ?
g =>
let l :=
get_lpol g in constr:(
p::l)
end.
Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd :=
match goal with
|- ?
g =>
let lb :=
lterm_goal g in
match eval red in (
li_reifyl (
lb:=
lb))
with
|
(?fv, ?le) =>
let fv :=
match lvar with
(@
nil _) =>
fv
|
_ =>
lvar
end in
let nparam :=
eval compute in (
Z_of_nat (
List.length lparam))
in
let fv :=
parametres_en_tete fv lparam in
match eval red in (
li_reifyl (
l:=
fv) (
lb:=
lb))
with
|
(?fv, ?le) =>
reify_goal fv le lb Rd;
match goal with
|- ?
g =>
let lp :=
get_lpol g in
let lpol :=
eval compute in (
List.rev lp)
in
tacsimpl;
intros;
let SplitPolyList kont :=
match lpol with
| ?
p2::?lp2 =>
kont p2 lp2
|
_ =>
idtac "polynomial not in the ideal"
end in
tacsimpl;
SplitPolyList ltac:(
fun p lp =>
set (
p21:=
p) ;
set (
lp21:=
lp);
nsatz_call radicalmax info nparam p lp ltac:(
fun c r lq lci =>
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:
ring_eq (
interpret3 _ Rd q fv)
ring0);
[
tacsimpl;
apply (@
check_correct _ Rd fv lp21 q (lci,lq) Hg);
tacsimpl;
repeat (
split;[
assumption|
idtac]);
exact I
|
simpl in Hg2;
tacsimpl;
apply Rdomain_pow with (
interpret3 _ Rd c fv) (
Nnat.nat_of_N r);
auto with domain;
tacsimpl;
apply domain_axiom_one_zero
|| (
simpl) ||
idtac "could not prove discrimination result"
]
]
)
)
end end end end .
Ltac nsatz_domainpv pretac radicalmax info lparam lvar tacsimpl rd :=
pretac;
nsatz_domain_begin tacsimpl;
auto with domain;
nsatz_domain_generic radicalmax info lparam lvar tacsimpl rd.
Ltac nsatz_domain:=
intros;
match goal with
|- (@
ring_eq _ (@
domain_ring ?
r ?
rd)
_ _ ) =>
nsatz_domainpv ltac:
idtac 6%
N 1%
Z (@
nil r) (@
nil r)
ltac:(
simpl)
rd
end.
Require Import Reals.
Require Import RealField.
Instance Rri :
Ring R := {
ring0 := 0%
R;
ring1 := 1%
R;
ring_plus :=
Rplus;
ring_mult :=
Rmult;
ring_sub :=
Rminus;
ring_opp :=
Ropp;
ring_eq := @
eq R;
ring_ring :=
RTheory}.
Lemma Raxiom_one_zero: 1%
R <> 0%
R.
Instance Rdi :
Domain R := {
domain_ring :=
Rri;
domain_axiom_product :=
Rmult_integral;
domain_axiom_one_zero :=
Raxiom_one_zero}.
Hint Resolve ring_setoid ring_plus_comp ring_mult_comp ring_sub_comp ring_opp_comp:
domain.
Ltac replaceR:=
replace 0%
R with (@
ring0 _ (@
domain_ring _ Rdi))
in *;[
idtac|
reflexivity];
replace 1%
R with (@
ring1 _ (@
domain_ring _ Rdi))
in *;[
idtac|
reflexivity];
replace Rplus with (@
ring_plus _ (@
domain_ring _ Rdi))
in *;[
idtac|
reflexivity];
replace Rmult with (@
ring_mult _ (@
domain_ring _ Rdi))
in *;[
idtac|
reflexivity];
replace Rminus with (@
ring_sub _ (@
domain_ring _ Rdi))
in *;[
idtac|
reflexivity];
replace Ropp with (@
ring_opp _ (@
domain_ring _ Rdi))
in *;[
idtac|
reflexivity];
replace (@
eq R)
with (@
ring_eq _ (@
domain_ring _ Rdi))
in *;[
idtac|
reflexivity].
Ltac simplR:=
simpl;
replaceR.
Ltac pretacR:=
replaceR;
replace Rri with (@
domain_ring _ Rdi)
in *; [
idtac |
reflexivity].
Ltac nsatz_domainR:=
nsatz_domainpv ltac:
pretacR 6%
N 1%
Z (@
Datatypes.nil R) (@
Datatypes.nil R)
ltac:
simplR Rdi;
discrR.
Goal forall x y:
R,
x = y -> (
x*x-x+1)%
R = (
(y*y-y)+1
+0)%
R.
Instance Zri :
Ring Z := {
ring0 := 0%
Z;
ring1 := 1%
Z;
ring_plus :=
Zplus;
ring_mult :=
Zmult;
ring_sub :=
Zminus;
ring_opp :=
Zopp;
ring_eq := (@
eq Z);
ring_ring :=
Zth}.
Lemma Zaxiom_one_zero: 1%
Z <> 0%
Z.
Instance Zdi :
Domain Z := {
domain_ring :=
Zri;
domain_axiom_product :=
Zmult_integral;
domain_axiom_one_zero :=
Zaxiom_one_zero}.
Ltac replaceZ :=
replace 0%
Z with (@
ring0 _ (@
domain_ring _ Zdi))
in *;[
idtac|
reflexivity];
replace 1%
Z with (@
ring1 _ (@
domain_ring _ Zdi))
in *;[
idtac|
reflexivity];
replace Zplus with (@
ring_plus _ (@
domain_ring _ Zdi))
in *;[
idtac|
reflexivity];
replace Zmult with (@
ring_mult _ (@
domain_ring _ Zdi))
in *;[
idtac|
reflexivity];
replace Zminus with (@
ring_sub _ (@
domain_ring _ Zdi))
in *;[
idtac|
reflexivity];
replace Zopp with (@
ring_opp _ (@
domain_ring _ Zdi))
in *;[
idtac|
reflexivity];
replace (@
eq Z)
with (@
ring_eq _ (@
domain_ring _ Zdi))
in *;[
idtac|
reflexivity].
Ltac simplZ:=
simpl;
replaceZ.
Ltac pretacZ :=
replaceZ;
replace Zri with (@
domain_ring _ Zdi)
in *; [
idtac |
reflexivity].
Ltac nsatz_domainZ:=
nsatz_domainpv ltac:
pretacZ 6%
N 1%
Z (@
Datatypes.nil Z) (@
Datatypes.nil Z)
ltac:
simplZ Zdi.
Require Import QArith.
Instance Qri :
Ring Q := {
ring0 := 0%
Q;
ring1 := 1%
Q;
ring_plus :=
Qplus;
ring_mult :=
Qmult;
ring_sub :=
Qminus;
ring_opp :=
Qopp;
ring_eq :=
Qeq;
ring_ring :=
Qsrt}.
Lemma Qaxiom_one_zero:
not (
Qeq 1%
Q 0%
Q).
Instance Qdi :
Domain Q := {
domain_ring :=
Qri;
domain_axiom_product :=
Qmult_integral;
domain_axiom_one_zero :=
Qaxiom_one_zero}.
Ltac replaceQ :=
replace 0%
Q with (@
ring0 _ (@
domain_ring _ Qdi))
in *;[
idtac|
reflexivity];
replace 1%
Q with (@
ring1 _ (@
domain_ring _ Qdi))
in *;[
idtac|
reflexivity];
replace Qplus with (@
ring_plus _ (@
domain_ring _ Qdi))
in *;[
idtac|
reflexivity];
replace Qmult with (@
ring_mult _ (@
domain_ring _ Qdi))
in *;[
idtac|
reflexivity];
replace Qminus with (@
ring_sub _ (@
domain_ring _ Qdi))
in *;[
idtac|
reflexivity];
replace Qopp with (@
ring_opp _ (@
domain_ring _ Qdi))
in *;[
idtac|
reflexivity];
replace Qeq with (@
ring_eq _ (@
domain_ring _ Qdi))
in *;[
idtac|
reflexivity].
Ltac simplQ:=
simpl;
replaceQ.
Ltac pretacQ :=
replaceQ;
replace Qri with (@
domain_ring _ Qdi)
in *; [
idtac |
reflexivity].
Ltac nsatz_domainQ:=
nsatz_domainpv ltac:
pretacQ 6%
N 1%
Z (@
Datatypes.nil Q) (@
Datatypes.nil Q)
ltac:
simplQ Qdi.
Ltac nsatz :=
intros;
match goal with
| |- (@
eq R _ _) =>
nsatz_domainR
| |- (@
eq Z _ _) =>
nsatz_domainZ
| |- (@
Qeq _ _) =>
nsatz_domainQ
| |-
_ =>
nsatz_domain
end.