# 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 ]).