Library Coq.setoid_ring.Ncring_tac
Require
Import
List
.
Require
Import
Setoid
.
Require
Import
BinPos
.
Require
Import
BinList
.
Require
Import
Znumtheory
.
Require
Export
Morphisms
Setoid
Bool
.
Require
Import
ZArith
.
Require
Import
Algebra_syntax
.
Require
Export
Ncring
.
Require
Import
Ncring_polynom
.
Require
Import
Ncring_initial
.
Set Implicit Arguments
.
Class
nth
(
R
:
Type
) (
t
:
R
) (
l
:
list
R
) (
i
:
nat
).
Instance
Ifind0
(
R
:
Type
) (
t
:
R
)
l
:
nth
t
(
t
::
l
) 0.
Defined
.
Instance
IfindS
(
R
:
Type
) (
t2
t1
:
R
)
l
i
{
_
:
nth
t1
l
i
}
:
nth
t1
(
t2
::
l
) (
S
i
) | 1.
Defined
.
Class
closed
(
T
:
Type
) (
l
:
list
T
).
Instance
Iclosed_nil
T
:
closed
(
T
:=
T
)
nil
.
Defined
.
Instance
Iclosed_cons
T
t
(
l
:
list
T
)
{
_
:
closed
l
}
:
closed
(
t
::
l
).
Defined
.
Class
reify
(
R
:
Type
)`{
Rr
:
Ring
(
T
:=
R
)} (
e
:
PExpr
Z
) (
lvar
:
list
R
) (
t
:
R
).
Instance
reify_zero
(
R
:
Type
)
lvar
op
`{
Ring
(
T
:=
R
)(
ring0
:=
op
)
}
:
reify
(
ring0
:=
op
)(
PEc
0%
Z
)
lvar
op
.
Defined
.
Instance
reify_one
(
R
:
Type
)
lvar
op
`{
Ring
(
T
:=
R
)(
ring1
:=
op
)
}
:
reify
(
ring1
:=
op
) (
PEc
1%
Z
)
lvar
op
.
Defined
.
Instance
reifyZ0
(
R
:
Type
)
lvar
`{
Ring
(
T
:=
R
)
}
:
reify
(
PEc
Z0
)
lvar
Z0
|11.
Defined
.
Instance
reifyZpos
(
R
:
Type
)
lvar
(
p
:
positive
)
`{
Ring
(
T
:=
R
)
}
:
reify
(
PEc
(
Zpos
p
))
lvar
(
Zpos
p
)|11.
Defined
.
Instance
reifyZneg
(
R
:
Type
)
lvar
(
p
:
positive
)
`{
Ring
(
T
:=
R
)
}
:
reify
(
PEc
(
Zneg
p
))
lvar
(
Zneg
p
)|11.
Defined
.
Instance
reify_add
(
R
:
Type
)
e1
lvar
t1
e2
t2
op
`{
Ring
(
T
:=
R
)(
add
:=
op
)
}
{
_
:
reify
(
add
:=
op
)
e1
lvar
t1
}
{
_
:
reify
(
add
:=
op
)
e2
lvar
t2
}
:
reify
(
add
:=
op
) (
PEadd
e1
e2
)
lvar
(
op
t1
t2
).
Defined
.
Instance
reify_mul
(
R
:
Type
)
e1
lvar
t1
e2
t2
op
`{
Ring
(
T
:=
R
)(
mul
:=
op
)
}
{
_
:
reify
(
mul
:=
op
)
e1
lvar
t1
}
{
_
:
reify
(
mul
:=
op
)
e2
lvar
t2
}
:
reify
(
mul
:=
op
) (
PEmul
e1
e2
)
lvar
(
op
t1
t2
)|10.
Defined
.
Instance
reify_mul_ext
(
R
:
Type
) `{
Ring
R
}
lvar
(
z
:
Z
)
e2
t2
`{
Ring
(
T
:=
R
)
}
{
_
:
reify
e2
lvar
t2
}
:
reify
(
PEmul
(
PEc
z
)
e2
)
lvar
(@
multiplication
Z
_
_
z
t2
)|9.
Defined
.
Instance
reify_sub
(
R
:
Type
)
e1
lvar
t1
e2
t2
op
`{
Ring
(
T
:=
R
)(
sub
:=
op
)
}
{
_
:
reify
(
sub
:=
op
)
e1
lvar
t1
}
{
_
:
reify
(
sub
:=
op
)
e2
lvar
t2
}
:
reify
(
sub
:=
op
) (
PEsub
e1
e2
)
lvar
(
op
t1
t2
).
Defined
.
Instance
reify_opp
(
R
:
Type
)
e1
lvar
t1
op
`{
Ring
(
T
:=
R
)(
opp
:=
op
)
}
{
_
:
reify
(
opp
:=
op
)
e1
lvar
t1
}
:
reify
(
opp
:=
op
) (
PEopp
e1
)
lvar
(
op
t1
).
Defined
.
Instance
reify_pow
(
R
:
Type
) `{
Ring
R
}
e1
lvar
t1
n
`{
Ring
(
T
:=
R
)
}
{
_
:
reify
e1
lvar
t1
}
:
reify
(
PEpow
e1
n
)
lvar
(
pow_N
t1
n
)|1.
Defined
.
Instance
reify_var
(
R
:
Type
)
t
lvar
i
`{
nth
R
t
lvar
i
}
`{
Rr
:
Ring
(
T
:=
R
)}
:
reify
(
Rr
:=
Rr
) (
PEX
Z
(
Pos.of_succ_nat
i
))
lvar
t
| 100.
Defined
.
Class
reifylist
(
R
:
Type
)`{
Rr
:
Ring
(
T
:=
R
)} (
lexpr
:
list
(
PExpr
Z
)) (
lvar
:
list
R
)
(
lterm
:
list
R
).
Instance
reify_nil
(
R
:
Type
)
lvar
`{
Rr
:
Ring
(
T
:=
R
)}
:
reifylist
(
Rr
:=
Rr
)
nil
lvar
(@
nil
R
).
Defined
.
Instance
reify_cons
(
R
:
Type
)
e1
lvar
t1
lexpr2
lterm2
`{
Rr
:
Ring
(
T
:=
R
)}
{
_
:
reify
(
Rr
:=
Rr
)
e1
lvar
t1
}
{
_
:
reifylist
(
Rr
:=
Rr
)
lexpr2
lvar
lterm2
}
:
reifylist
(
Rr
:=
Rr
) (
e1
::
lexpr2
)
lvar
(
t1
::
lterm2
).
Defined
.
Definition
list_reifyl
(
R
:
Type
)
lexpr
lvar
lterm
`{
Rr
:
Ring
(
T
:=
R
)}
{
_
:
reifylist
(
Rr
:=
Rr
)
lexpr
lvar
lterm
}
`{
closed
(
T
:=
R
)
lvar
} :=
(
lvar
,
lexpr
)
.
Unset Implicit Arguments
.
Ltac
lterm_goal
g
:=
match
g
with
| ?
t1
==
?
t2
=>
constr
:(
t1
::
t2
::
nil
)
| ?
t1
=
?
t2
=>
constr
:(
t1
::
t2
::
nil
)
| (
_
?
t1
?
t2
) =>
constr
:(
t1
::
t2
::
nil
)
end
.
Lemma
Zeqb_ok
:
forall
x
y
:
Z
,
Zeq_bool
x
y
=
true
->
x
==
y
.
Ltac
reify_goal
lvar
lexpr
lterm
:=
match
lexpr
with
nil
=>
idtac
| ?
e1
::
?
e2
::
_
=>
match
goal
with
|- (?
op
?
u1
?
u2
) =>
change
(
op
(@
PEeval
Z
_
_
_
_
_
_
_
_
_
(@
gen_phiZ
_
_
_
_
_
_
_
_
_
)
N
(
fun
n
:
N
=>
n
) (@
pow_N
_
_
_
_
_
_
_
_
_
)
lvar
e1
)
(@
PEeval
Z
_
_
_
_
_
_
_
_
_
(@
gen_phiZ
_
_
_
_
_
_
_
_
_
)
N
(
fun
n
:
N
=>
n
) (@
pow_N
_
_
_
_
_
_
_
_
_
)
lvar
e2
))
end
end
.
Lemma
comm
:
forall
(
R
:
Type
)`{
Ring
R
}(
c
:
Z
) (
x
:
R
),
x
*
(
gen_phiZ
c
)
==
(
gen_phiZ
c
)
*
x
.
Ltac
ring_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
=>
apply
(@
ring_correct
Z
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
_
(@
gen_phiZ
_
_
_
_
_
_
_
_
_
)
_
(@
comm
_
_
_
_
_
_
_
_
_
_
)
Zeq_bool
Zeqb_ok
N
(
fun
n
:
N
=>
n
)
(@
pow_N
_
_
_
_
_
_
_
_
_
));
[
apply
mkpow_th
;
reflexivity
|
vm_compute
;
reflexivity
]
end
end
end
.
Ltac
non_commutative_ring
:=
intros
;
ring_gen
.
Ltac
ring_simplify_aux
lterm
fv
lexpr
hyp
:=
match
lterm
with
| ?
t0
::
?
lterm
=>
match
lexpr
with
| ?
e
::
?
le
=>
let
t
:=
constr
:(@
Ncring_polynom.norm_subst
Z
0%
Z
1%
Z
Z.add
Z.mul
Z.sub
Z.opp
(@
eq
Z
)
Zops
Zeq_bool
e
)
in
let
te
:=
constr
:(@
Ncring_polynom.Pphi
Z
_
0 1
_
+
_
_
*
_
_
-
_
-
_
_
==
_
_
Ncring_initial.gen_phiZ
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
:
(
@
Ncring_polynom.PEeval
Z
_
0 1
_
+
_
_
*
_
_
-
_
-
_
_
==
_
_
Ncring_initial.gen_phiZ
N
(
fun
n
:
N
=>
n
)
(@
Ring_theory.pow_N
_
1
multiplication
)
fv
e
)
==
te
);
[
apply
(@
Ncring_polynom.norm_subst_ok
Z
_
0%
Z
1%
Z
Z.add
Z.mul
Z.sub
Z.opp
(@
eq
Z
)
_
_
0 1
_
+
_
_
*
_
_
-
_
-
_
_
==
_
_
_
Ncring_initial.gen_phiZ
_
(@
comm
_
0 1
_
+
_
_
*
_
_
-
_
-
_
_
==
_
_
_
)
_
Zeqb_ok
);
apply
mkpow_th
;
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
=>
idtac
"ok";
rewrite
eq1
;
pattern
(@
Ncring_polynom.Pphi
Z
_
0 1
_
+
_
_
*
_
_
-
_
-
_
_
==
_
_
Ncring_initial.gen_phiZ
fv
t'
);
match
goal
with
|- (?
p
?
t
) =>
set
(
P
:=
p
)
end
;
unfold
t'
in
*;
clear
t'
eq1
eq2
;
simpl
| ?
H
=>
rewrite
eq1
in
H
;
pattern
(@
Ncring_polynom.Pphi
Z
_
0 1
_
+
_
_
*
_
_
-
_
-
_
_
==
_
_
Ncring_initial.gen_phiZ
fv
t'
)
in
H
;
match
type
of
H
with
| (?
p
?
t
) =>
set
(
P
:=
p
)
in
H
end
;
unfold
t'
in
*;
clear
t'
eq1
eq2
;
simpl
in
H
end
;
unfold
P
in
*;
clear
P
];
ring_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
ring_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
;
ring_simplify_aux
lterm1
lv1
lexpr
hyp
;
clear
lt
lv
;
deset
n
end
.
Tactic Notation
"non_commutative_ring_simplify"
constr
(
lterm
):=
ring_simplify_gen
lterm
1%
nat
.
Tactic Notation
"non_commutative_ring_simplify"
constr
(
lterm
) "in"
ident
(
H
):=
ring_simplify_gen
lterm
H
.