Library Coq.setoid_ring.Cring
Require Export List.
Require Import Setoid.
Require Import BinPos.
Require Import BinList.
Require Import Znumtheory.
Require Export Morphisms Setoid Bool.
Require Import ZArith_base.
Require Export Algebra_syntax.
Require Export Ncring.
Require Export Ncring_initial.
Require Export Ncring_tac.
Require Import InitialRing.
Class Cring {
R:
Type}`{
Rr:
Ring R} :=
cring_mul_comm:
forall x y:
R,
x * y == y * x.
Ltac reify_goal lvar lexpr lterm:=
match lexpr with
nil =>
idtac
| ?
e1::?
e2::_ =>
match goal with
|- (?
op ?
u1 ?
u2) =>
change (
op
(@
Ring_polynom.PEeval
_ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (
fun n:
N =>
n)
(@
Ring_theory.pow_N _ 1
multiplication)
lvar e1)
(@
Ring_polynom.PEeval
_ zero one _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (
fun n:
N =>
n)
(@
Ring_theory.pow_N _ 1
multiplication)
lvar e2))
end
end.
Section cring.
Context {
R:
Type}`{
Rr:
Cring R}.
Lemma cring_eq_ext:
ring_eq_ext _+_ _*_ -_ _==_.
Lemma cring_almost_ring_theory:
almost_ring_theory (
R:=
R)
zero one _+_ _*_ _-_ -_ _==_.
Lemma cring_morph:
ring_morph zero one _+_ _*_ _-_ -_ _==_
0%
Z 1%
Z Z.add Z.mul Z.sub Z.opp Zeq_bool
Ncring_initial.gen_phiZ.
Lemma cring_power_theory :
@
Ring_theory.power_theory R one _*_ _==_ N (
fun n:
N =>
n)
(@
Ring_theory.pow_N _ 1
multiplication).
Lemma cring_div_theory:
div_theory _==_ Z.add Z.mul Ncring_initial.gen_phiZ Z.quotrem.
End cring.
Ltac cring_gen :=
match goal with
|- ?
g =>
let lterm :=
lterm_goal g in
match eval red in (
list_reifyl (
lterm:=
lterm))
with
|
(?
fv, ?
lexpr) =>
reify_goal fv lexpr lterm;
match goal with
|- ?
g =>
generalize
(@
Ring_polynom.ring_correct _ 0 1
_+_ _*_ _-_ -_ _==_
ring_setoid
cring_eq_ext
cring_almost_ring_theory
Z 0%
Z 1%
Z Z.add Z.mul Z.sub Z.opp Zeq_bool
Ncring_initial.gen_phiZ
cring_morph
N
(
fun n:
N =>
n)
(@
Ring_theory.pow_N _ 1
multiplication)
cring_power_theory
Z.quotrem
cring_div_theory
O fv nil);
let rc :=
fresh "rc"
in
intro rc;
apply rc
end
end
end.
Ltac cring_compute:=
vm_compute;
reflexivity.
Ltac cring:=
intros;
cring_gen;
cring_compute.
Instance Zcri: (
Cring (
Rr:=
Zr)).
Ltac cring_simplify_aux lterm fv lexpr hyp :=
match lterm with
| ?
t0::?
lterm =>
match lexpr with
| ?
e::?
le =>
let t :=
constr:(@
Ring_polynom.norm_subst
Z 0%
Z 1%
Z Z.add Z.mul Z.sub Z.opp Zeq_bool Z.quotrem O nil e)
in
let te :=
constr:(@
Ring_polynom.Pphi_dev
_ 0 1
_+_ _*_ _-_ -_
Z 0%
Z 1%
Z Zeq_bool
Ncring_initial.gen_phiZ
get_signZ fv t)
in
let eq1 :=
fresh "ring"
in
let nft :=
eval vm_compute in t in
let t':=
fresh "t"
in
pose (
t' :=
nft);
assert (
eq1 :
t = t');
[
vm_cast_no_check (
eq_refl t')|
let eq2 :=
fresh "ring"
in
assert (
eq2:
(@
Ring_polynom.PEeval
_ zero _+_ _*_ _-_ -_ Z Ncring_initial.gen_phiZ N (
fun n:
N =>
n)
(@
Ring_theory.pow_N _ 1
multiplication)
fv e) == te);
[
let eq3 :=
fresh "ring"
in
generalize (@
ring_rw_correct _ 0 1
_+_ _*_ _-_ -_ _==_
ring_setoid
cring_eq_ext
cring_almost_ring_theory
Z 0%
Z 1%
Z Z.add Z.mul Z.sub Z.opp Zeq_bool
Ncring_initial.gen_phiZ
cring_morph
N
(
fun n:
N =>
n)
(@
Ring_theory.pow_N _ 1
multiplication)
cring_power_theory
Z.quotrem
cring_div_theory
get_signZ get_signZ_th
O nil fv I nil (
eq_refl nil) );
intro eq3;
apply eq3;
reflexivity|
match hyp with
| 1%
nat =>
rewrite eq2
| ?
H =>
try rewrite eq2 in H
end];
let P:=
fresh "P"
in
match hyp with
| 1%
nat =>
rewrite eq1;
pattern (@
Ring_polynom.Pphi_dev
_ 0 1
_+_ _*_ _-_ -_
Z 0%
Z 1%
Z Zeq_bool
Ncring_initial.gen_phiZ
get_signZ fv t');
match goal with
|- (?
p ?
t) =>
set (
P:=
p)
end;
unfold t' in *;
clear t' eq1 eq2;
unfold Pphi_dev,
Pphi_avoid;
simpl;
repeat (
unfold mkmult1,
mkmultm1,
mkmult_c_pos,
mkmult_c,
mkadd_mult,
mkmult_c_pos,
mkmult_pow,
mkadd_mult,
mkpow;
simpl)
| ?
H =>
rewrite eq1 in H;
pattern (@
Ring_polynom.Pphi_dev
_ 0 1
_+_ _*_ _-_ -_
Z 0%
Z 1%
Z Zeq_bool
Ncring_initial.gen_phiZ
get_signZ fv t')
in H;
match type of H with
| (?
p ?
t) =>
set (
P:=
p)
in H
end;
unfold t' in *;
clear t' eq1 eq2;
unfold Pphi_dev,
Pphi_avoid in H;
simpl in H;
repeat (
unfold mkmult1,
mkmultm1,
mkmult_c_pos,
mkmult_c,
mkadd_mult,
mkmult_c_pos,
mkmult_pow,
mkadd_mult,
mkpow in H;
simpl in H)
end;
unfold P in *;
clear P
];
cring_simplify_aux lterm fv le hyp
|
nil =>
idtac
end
|
nil =>
idtac
end.
Ltac set_variables fv :=
match fv with
|
nil =>
idtac
| ?
t::?
fv =>
let v :=
fresh "X"
in
set (
v:=
t)
in *;
set_variables fv
end.
Ltac deset n:=
match n with
| 0%
nat =>
idtac
|
S ?
n1 =>
match goal with
|
h:= ?
v : ?
t |- ?
g =>
unfold h in *;
clear h;
deset n1
end
end.
Ltac cring_simplify_gen a hyp :=
let lterm :=
match a with
|
_::_ =>
a
|
_ =>
constr:(
a::nil)
end in
match eval red in (
list_reifyl (
lterm:=
lterm))
with
|
(?
fv, ?
lexpr) =>
idtac lterm;
idtac fv;
idtac lexpr;
let n :=
eval compute in (
length fv)
in
idtac n;
let lt:=
fresh "lt"
in
set (
lt:=
lterm);
let lv:=
fresh "fv"
in
set (
lv:=
fv);
set_variables fv;
let lterm1 :=
eval unfold lt in lt in
let lv1 :=
eval unfold lv in lv in
idtac lterm1;
idtac lv1;
cring_simplify_aux lterm1 lv1 lexpr hyp;
clear lt lv;
deset n
end.
Tactic Notation "cring_simplify"
constr(
lterm):=
cring_simplify_gen lterm 1%
nat.
Tactic Notation "cring_simplify"
constr(
lterm) "in"
ident(
H):=
cring_simplify_gen lterm H.