Library Coq.field.LegacyField_Tactic
Require Import List.
Require Import LegacyRing.
Require Export LegacyField_Compl.
Require Export LegacyField_Theory.
Ltac get_component a s :=
eval cbv beta iota delta [
a]
in (
a s).
Ltac body_of s :=
eval cbv beta iota delta [
s]
in s.
Ltac mem_assoc var lvar :=
match constr:
lvar with
|
nil =>
constr:
false
| ?
X1 :: ?X2 =>
match constr:(
X1 = var)
with
| (?
X1 = ?X1) =>
constr:
true
|
_ =>
mem_assoc var X2
end
end.
Ltac number lvar :=
let rec number_aux lvar cpt :=
match constr:
lvar with
| (@
nil ?
X1) =>
constr:(@
nil (
prod X1 nat))
| ?
X2 :: ?X3 =>
let l2 :=
number_aux X3 (
S cpt)
in
constr:(
(X2,cpt) :: l2)
end
in number_aux lvar 0.
Ltac build_varlist FT trm :=
let rec seek_var lvar trm :=
let AT :=
get_component A FT
with AzeroT :=
get_component Azero FT
with AoneT :=
get_component Aone FT
with AplusT :=
get_component Aplus FT
with AmultT :=
get_component Amult FT
with AoppT :=
get_component Aopp FT
with AinvT :=
get_component Ainv FT in
match constr:
trm with
|
AzeroT =>
lvar
|
AoneT =>
lvar
| (
AplusT ?
X1 ?
X2) =>
let l1 :=
seek_var lvar X1 in
seek_var l1 X2
| (
AmultT ?
X1 ?
X2) =>
let l1 :=
seek_var lvar X1 in
seek_var l1 X2
| (
AoppT ?
X1) =>
seek_var lvar X1
| (
AinvT ?
X1) =>
seek_var lvar X1
| ?
X1 =>
let res :=
mem_assoc X1 lvar in
match constr:
res with
|
true =>
lvar
|
false =>
constr:(
X1 :: lvar)
end
end in
let AT :=
get_component A FT in
let lvar :=
seek_var (@
nil AT)
trm in
number lvar.
Ltac assoc elt lst :=
match constr:
lst with
|
nil =>
fail
|
(?X1,?X2) :: ?X3 =>
match constr:(
elt = X1)
with
| (?
X1 = ?X1) =>
constr:
X2
|
_ =>
assoc elt X3
end
end.
Ltac interp_A FT lvar trm :=
let AT :=
get_component A FT
with AzeroT :=
get_component Azero FT
with AoneT :=
get_component Aone FT
with AplusT :=
get_component Aplus FT
with AmultT :=
get_component Amult FT
with AoppT :=
get_component Aopp FT
with AinvT :=
get_component Ainv FT in
match constr:
trm with
|
AzeroT =>
constr:
EAzero
|
AoneT =>
constr:
EAone
| (
AplusT ?
X1 ?
X2) =>
let e1 :=
interp_A FT lvar X1 with e2 :=
interp_A FT lvar X2 in
constr:(
EAplus e1 e2)
| (
AmultT ?
X1 ?
X2) =>
let e1 :=
interp_A FT lvar X1 with e2 :=
interp_A FT lvar X2 in
constr:(
EAmult e1 e2)
| (
AoppT ?
X1) =>
let e :=
interp_A FT lvar X1 in
constr:(
EAopp e)
| (
AinvT ?
X1) =>
let e :=
interp_A FT lvar X1 in
constr:(
EAinv e)
| ?
X1 =>
let idx :=
assoc X1 lvar in
constr:(
EAvar idx)
end.
Ltac remove e l :=
match constr:
l with
|
nil =>
l
|
e :: ?X2 =>
constr:
X2
| ?
X2 :: ?X3 =>
let nl :=
remove e X3 in constr:(
X2 :: nl)
end.
Ltac union l1 l2 :=
match constr:
l1 with
|
nil =>
l2
| ?
X2 :: ?X3 =>
let nl2 :=
remove X2 l2 in
let nl :=
union X3 nl2 in
constr:(
X2 :: nl)
end.
Ltac raw_give_mult trm :=
match constr:
trm with
| (
EAinv ?
X1) =>
constr:(
X1 :: nil)
| (
EAopp ?
X1) =>
raw_give_mult X1
| (
EAplus ?
X1 ?
X2) =>
let l1 :=
raw_give_mult X1 with l2 :=
raw_give_mult X2 in
union l1 l2
| (
EAmult ?
X1 ?
X2) =>
let l1 :=
raw_give_mult X1 with l2 :=
raw_give_mult X2 in
eval compute in (
app l1 l2)
|
_ =>
constr:(@
nil ExprA)
end.
Ltac give_mult trm :=
let ltrm :=
raw_give_mult trm in
constr:(
mult_of_list ltrm).
Ltac apply_assoc FT lvar trm :=
let t :=
eval compute in (
assoc trm)
in
match constr:(
t = trm)
with
| (?
X1 = ?X1) =>
idtac
|
_ =>
rewrite <- (
assoc_correct FT trm);
change (
assoc trm)
with t in |- *
end.
Ltac apply_distrib FT lvar trm :=
let t :=
eval compute in (
distrib trm)
in
match constr:(
t = trm)
with
| (?
X1 = ?X1) =>
idtac
|
_ =>
rewrite <- (
distrib_correct FT trm);
change (
distrib trm)
with t in |- *
end.
Ltac grep_mult :=
match goal with
|
id:(
interp_ExprA _ _ _ <> _) |-
_ =>
id
end.
Ltac weak_reduce :=
match goal with
| |-
context [(
interp_ExprA ?
X1 ?
X2 _)] =>
cbv beta iota zeta
delta [
interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero
Aone Aplus Amult Aopp Ainv]
in |- *
end.
Ltac multiply mul :=
match goal with
| |- (
interp_ExprA ?
FT ?
X2 ?
X3 = interp_ExprA ?
FT ?
X2 ?
X4) =>
let AzeroT :=
get_component Azero FT in
cut (
interp_ExprA FT X2 mul <> AzeroT);
[
intro; (
let id :=
grep_mult in apply (
mult_eq FT X3 X4 mul X2 id))
|
weak_reduce;
(
let AoneT :=
get_component Aone ltac:(
body_of FT)
with AmultT :=
get_component Amult ltac:(
body_of FT)
in
try
match goal with
| |-
context [(
AmultT _ AoneT)] =>
rewrite (
AmultT_1r FT)
end;
clear FT X2) ]
end.
Ltac apply_multiply FT lvar trm :=
let t :=
eval compute in (
multiply trm)
in
match constr:(
t = trm)
with
| (?
X1 = ?X1) =>
idtac
|
_ =>
rewrite <- (
multiply_correct FT trm);
change (
multiply trm)
with t in |- *
end.
Ltac apply_inverse mul FT lvar trm :=
let t :=
eval compute in (
inverse_simplif mul trm)
in
match constr:(
t = trm)
with
| (?
X1 = ?X1) =>
idtac
|
_ =>
rewrite <- (
inverse_correct FT trm mul);
[
change (
inverse_simplif mul trm)
with t in |- * |
assumption ]
end.
Ltac strong_fail tac :=
first [
tac |
fail 2 ].
Ltac inverse_test_aux FT trm :=
let AplusT :=
get_component Aplus FT
with AmultT :=
get_component Amult FT
with AoppT :=
get_component Aopp FT
with AinvT :=
get_component Ainv FT in
match constr:
trm with
| (
AinvT _) =>
fail 1
| (
AoppT ?
X1) =>
strong_fail ltac:(
inverse_test_aux FT X1;
idtac)
| (
AplusT ?
X1 ?
X2) =>
strong_fail ltac:(
inverse_test_aux FT X1;
inverse_test_aux FT X2)
| (
AmultT ?
X1 ?
X2) =>
strong_fail ltac:(
inverse_test_aux FT X1;
inverse_test_aux FT X2)
|
_ =>
idtac
end.
Ltac inverse_test FT :=
let AplusT :=
get_component Aplus FT in
match goal with
| |- (?
X1 = ?X2) =>
inverse_test_aux FT (
AplusT X1 X2)
end.
Ltac apply_simplif sfun :=
match goal with
| |- (
interp_ExprA ?
X1 ?
X2 ?
X3 = interp_ExprA _ _ _) =>
sfun X1 X2 X3
end;
match goal with
| |- (
interp_ExprA _ _ _ = interp_ExprA ?
X1 ?
X2 ?
X3) =>
sfun X1 X2 X3
end.
Ltac unfolds FT :=
match get_component Aminus FT with
|
Some ?
X1 =>
unfold X1 in |- *
|
_ =>
idtac
end;
match get_component Adiv FT with
|
Some ?
X1 =>
unfold X1 in |- *
|
_ =>
idtac
end.
Ltac reduce FT :=
let AzeroT :=
get_component Azero FT
with AoneT :=
get_component Aone FT
with AplusT :=
get_component Aplus FT
with AmultT :=
get_component Amult FT
with AoppT :=
get_component Aopp FT
with AinvT :=
get_component Ainv FT in
(
cbv beta iota zeta delta -[
AzeroT AoneT AplusT AmultT AoppT AinvT]
in |- * ||
compute in |- *).
Ltac field_gen_aux FT :=
let AplusT :=
get_component Aplus FT in
match goal with
| |- (?
X1 = ?X2) =>
let lvar :=
build_varlist FT (
AplusT X1 X2)
in
let trm1 :=
interp_A FT lvar X1 with trm2 :=
interp_A FT lvar X2 in
let mul :=
give_mult (
EAplus trm1 trm2)
in
cut
(
let ft :=
FT in
let vm :=
lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2);
[
compute in |- *;
auto
|
intros ft vm;
apply_simplif apply_distrib;
apply_simplif apply_assoc;
multiply mul;
[
apply_simplif apply_multiply;
apply_simplif ltac:(
apply_inverse mul);
(
let id :=
grep_mult in
clear id;
weak_reduce;
clear ft vm;
first
[
inverse_test FT;
legacy ring |
field_gen_aux FT ])
|
idtac ] ]
end.
Ltac field_gen FT :=
unfolds FT; (
inverse_test FT;
legacy ring) ||
field_gen_aux FT.
Ltac init_exp FT trm :=
let e :=
(
match get_component Aminus FT with
|
Some ?
X1 =>
eval cbv beta delta [
X1]
in trm
|
_ =>
trm
end)
in
match get_component Adiv FT with
|
Some ?
X1 =>
eval cbv beta delta [
X1]
in e
|
_ =>
e
end.
Ltac simpl_inv trm :=
match constr:
trm with
| (
EAplus ?
X1 ?
X2) =>
let e1 :=
simpl_inv X1 with e2 :=
simpl_inv X2 in
constr:(
EAplus e1 e2)
| (
EAmult ?
X1 ?
X2) =>
let e1 :=
simpl_inv X1 with e2 :=
simpl_inv X2 in
constr:(
EAmult e1 e2)
| (
EAopp ?
X1) =>
let e :=
simpl_inv X1 in
constr:(
EAopp e)
| (
EAinv ?
X1) =>
SimplInvAux X1
| ?
X1 =>
constr:
X1
end
with SimplInvAux trm :=
match constr:
trm with
| (
EAinv ?
X1) =>
simpl_inv X1
| (
EAmult ?
X1 ?
X2) =>
let e1 :=
simpl_inv (
EAinv X1)
with e2 :=
simpl_inv (
EAinv X2)
in
constr:(
EAmult e1 e2)
| ?
X1 =>
let e :=
simpl_inv X1 in
constr:(
EAinv e)
end.
Ltac map_tactic fcn lst :=
match constr:
lst with
|
nil =>
lst
| ?
X2 :: ?X3 =>
let r :=
fcn X2 with t :=
map_tactic fcn X3 in
constr:(
r :: t)
end.
Ltac build_monom_aux lst trm :=
match constr:
lst with
|
nil =>
eval compute in (
assoc trm)
| ?
X1 :: ?X2 =>
build_monom_aux X2 (
EAmult trm X1)
end.
Ltac build_monom lnum lden :=
let ildn :=
map_tactic ltac:(
fun e =>
constr:(
EAinv e))
lden in
let ltot :=
eval compute in (
app lnum ildn)
in
let trm :=
build_monom_aux ltot EAone in
match constr:
trm with
| (
EAmult _ ?
X1) =>
constr:
X1
| ?
X1 =>
constr:
X1
end.
Ltac simpl_monom_aux lnum lden trm :=
match constr:
trm with
| (
EAmult (
EAinv ?
X1) ?
X2) =>
let mma :=
mem_assoc X1 lnum in
match constr:
mma with
|
true =>
let newlnum :=
remove X1 lnum in
simpl_monom_aux newlnum lden X2
|
false =>
simpl_monom_aux lnum (
X1 :: lden)
X2
end
| (
EAmult ?
X1 ?
X2) =>
let mma :=
mem_assoc X1 lden in
match constr:
mma with
|
true =>
let newlden :=
remove X1 lden in
simpl_monom_aux lnum newlden X2
|
false =>
simpl_monom_aux (
X1 :: lnum)
lden X2
end
| (
EAinv ?
X1) =>
let mma :=
mem_assoc X1 lnum in
match constr:
mma with
|
true =>
let newlnum :=
remove X1 lnum in
build_monom newlnum lden
|
false =>
build_monom lnum (
X1 :: lden)
end
| ?
X1 =>
let mma :=
mem_assoc X1 lden in
match constr:
mma with
|
true =>
let newlden :=
remove X1 lden in
build_monom lnum newlden
|
false =>
build_monom (
X1 :: lnum)
lden
end
end.
Ltac simpl_monom trm :=
simpl_monom_aux (@
nil ExprA) (@
nil ExprA)
trm.
Ltac simpl_all_monomials trm :=
match constr:
trm with
| (
EAplus ?
X1 ?
X2) =>
let e1 :=
simpl_monom X1 with e2 :=
simpl_all_monomials X2 in
constr:(
EAplus e1 e2)
| ?
X1 =>
simpl_monom X1
end.
Ltac assoc_distrib trm :=
eval compute in (
assoc (
distrib trm)).
Ltac eval_weak_reduce trm :=
eval
cbv beta iota zeta
delta [
interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero Aone Aplus
Amult Aopp Ainv]
in trm.
Ltac field_term FT exp :=
let newexp :=
init_exp FT exp in
let lvar :=
build_varlist FT newexp in
let trm :=
interp_A FT lvar newexp in
let tma :=
eval compute in (
assoc trm)
in
let tsmp :=
simpl_all_monomials
ltac:(
assoc_distrib ltac:(
simpl_all_monomials ltac:(
simpl_inv tma)))
in
let trep :=
eval_weak_reduce (
interp_ExprA FT lvar tsmp)
in
(
replace exp with trep; [
legacy ring trep |
field_gen FT ]).