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 DiscrR.
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).
Require Import ZArith.
Require Export Ring_polynom.
Require 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 Zeq_bool.
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 :=
(
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_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 (
match lvar with
|(@
nil _) =>
match lparam with
|(@
nil _) =>
let r :=
eval red in (
list_reifyl (
lterm:=
lb))
in r
|
_ =>
match eval red in (
list_reifyl (
lterm:=
lb))
with
|
(?fv, ?le) =>
let fv :=
parametres_en_tete fv lparam in
let r :=
eval red in
(
list_reifyl (
lterm:=
lb) (
lvar:=
fv))
in r
end
end
|
_ =>
let fv :=
parametres_en_tete lvar lparam in
let r :=
eval red in (
list_reifyl (
lterm:=
lb) (
lvar:=
fv))
in r
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;
discrR ||
omega])
|| (
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.
Require Import Reals.
Require Import RealField.
Lemma Rsth :
Setoid_Theory R (@
eq R).
Instance Rops: (@
Ring_ops R 0%
R 1%
R Rplus Rmult Rminus Ropp (@
eq R)).
Instance Rri : (
Ring (
Ro:=
Rops)).
Defined.
Lemma R_one_zero: 1%
R <> 0%
R.
Instance Rcri: (
Cring (
Rr:=
Rri)).
Instance Rdi : (
Integral_domain (
Rcr:=
Rcri)).
Require Import QArith.
Instance Qops: (@
Ring_ops Q 0%
Q 1%
Q Qplus Qmult Qminus Qopp Qeq).
Instance Qri : (
Ring (
Ro:=
Qops)).
Defined.
Lemma Q_one_zero:
not (
Qeq 1%
Q 0%
Q).
Instance Qcri: (
Cring (
Rr:=
Qri)).
Instance Qdi : (
Integral_domain (
Rcr:=
Qcri)).
Lemma Z_one_zero: 1%
Z <> 0%
Z.
Instance Zcri: (
Cring (
Rr:=
Zr)).
Instance Zdi : (
Integral_domain (
Rcr:=
Zcri)).