diff options
Diffstat (limited to 'contrib/setoid_ring/Field_tac.v')
-rw-r--r-- | contrib/setoid_ring/Field_tac.v | 405 |
1 files changed, 405 insertions, 0 deletions
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v new file mode 100644 index 00000000..aad3a580 --- /dev/null +++ b/contrib/setoid_ring/Field_tac.v @@ -0,0 +1,405 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Ring_tac BinList Ring_polynom InitialRing. +Require Export Field_theory. + + (* syntaxification *) + Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv := + let rec mkP t := + match Cst t with + | InitialRing.NotConstant => + match t with + | (radd ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEadd e1 e2) + | (rmul ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEmul e1 e2) + | (rsub ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEsub e1 e2) + | (ropp ?t1) => + let e1 := mkP t1 in constr:(FEopp e1) + | (rdiv ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEdiv e1 e2) + | (rinv ?t1) => + let e1 := mkP t1 in constr:(FEinv e1) + | (rpow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => + let p := Find_at t fv in constr:(@FEX C p) + | ?c => let e1 := mkP t1 in constr:(FEpow e1 c) + end + + | _ => + let p := Find_at t fv in constr:(@FEX C p) + end + | ?c => constr:(FEc c) + end + in mkP t. + +Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := + let rec TFV t fv := + match Cst t with + | InitialRing.NotConstant => + match t with + | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) + | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) + | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) + | (opp ?t1) => TFV t1 fv + | (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) + | (inv ?t1) => TFV t1 fv + | (pow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => AddFvTail t fv + | _ => TFV t1 fv + end + | _ => AddFvTail t fv + end + | _ => fv + end + in TFV t fv. + +Ltac ParseFieldComponents lemma := + match type of lemma with + | context [ + (* PCond _ _ _ _ _ _ _ _ _ _ _ -> *) + (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv + ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) ] => + (fun f => f radd rmul rsub ropp rdiv rinv rpow C) + | _ => fail 1 "field anomaly: bad correctness lemma (parse)" + end. + +(* simplifying the non-zero condition... *) + +Ltac fold_field_cond req := + let rec fold_concl t := + match t with + ?x /\ ?y => + let fx := fold_concl x in let fy := fold_concl y in constr:(fx/\fy) + | req ?x ?y -> False => constr:(~ req x y) + | _ => t + end in + match goal with + |- ?t => let ft := fold_concl t in change ft + end. + +Ltac simpl_PCond req := + protect_fv "field_cond"; + (try exact I); + fold_field_cond req. + +Ltac simpl_PCond_BEURK req := + protect_fv "field_cond"; + fold_field_cond req. + +(* Rewriting (field_simplify) *) +Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl := + let Main radd rmul rsub ropp rdiv rinv rpow C := + let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let mkFE := + mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let fv := FV_hypo_tac mkFV req lH in + let simpl_field H := (protect_fv "field" in H;f H) in + let lemma_tac fv RW_tac := + let rr_lemma := fresh "f_rw_lemma" in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let vlpe := fresh "list_hyp" in + let vlmp := fresh "list_hyp_norm" in + let vlmp_eq := fresh "list_hyp_norm_eq" in + let prh := proofHyp_tac lH in + pose (vlpe := lpe); + match type of lemma with + | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] => + compute_assertion vlmp_eq vlmp + (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe); + (assert (rr_lemma := lemma n vlpe fv prh vlmp vlmp_eq) + || fail "type error when build the rewriting lemma"); + RW_tac rr_lemma; + try clear rr_lemma vlmp_eq vlmp vlpe + | _ => fail 1 "field_simplify anomaly: bad correctness lemma" + end in + ReflexiveRewriteTactic mkFFV mkFE simpl_field lemma_tac fv rl; + try (apply Cond_lemma; simpl_PCond req) in + ParseFieldComponents lemma Main. + +Ltac Field_simplify_gen f := + fun req cst_tac pow_tac _ _ field_simplify_ok _ cond_ok pre post lH rl => + pre(); + Field_norm_gen f cst_tac pow_tac field_simplify_ok cond_ok req + ring_subst_niter lH rl; + post(). + +Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H). + +Tactic Notation (at level 0) + "field_simplify" constr_list(rl) := + match goal with [|- ?G] => field_lookup Field_simplify [] rl [G] end. + +Tactic Notation (at level 0) + "field_simplify" "[" constr_list(lH) "]" constr_list(rl) := + match goal with [|- ?G] => field_lookup Field_simplify [lH] rl [G] end. + +Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= + let G := getGoal in + let t := type of H in + let g := fresh "goal" in + set (g:= G); + generalize H;clear H; + field_lookup Field_simplify [] rl [t]; + intro H; + unfold g;clear g. + +Tactic Notation "field_simplify" "["constr_list(lH) "]" constr_list(rl) "in" hyp(H):= + let G := getGoal in + let t := type of H in + let g := fresh "goal" in + set (g:= G); + generalize H;clear H; + field_lookup Field_simplify [lH] rl [t]; + intro H; + unfold g;clear g. + +(* +Ltac Field_simplify_in hyp:= + Field_simplify_gen ltac:(fun H => rewrite H in hyp). + +Tactic Notation (at level 0) + "field_simplify" constr_list(rl) "in" hyp(h) := + let t := type of h in + field_lookup (Field_simplify_in h) [] rl [t]. + +Tactic Notation (at level 0) + "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) := + let t := type of h in + field_lookup (Field_simplify_in h) [lH] rl [t]. +*) + +(** Generic tactic for solving equations *) + +Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH := + let Main radd rmul rsub ropp rdiv rinv rpow C := + let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let mkFE := + mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let rec ParseExpr ilemma := + match type of ilemma with + forall nfe, ?fe = nfe -> _ => + (fun t => + let x := fresh "fld_expr" in + let H := fresh "norm_fld_expr" in + compute_assertion H x fe; + ParseExpr (ilemma x H) t; + try clear x H) + | _ => (fun t => t ilemma) + end in + let Main_eq t1 t2 := + let fv := FV_hypo_tac mkFV req lH in + let fv := mkFFV t1 fv in + let fv := mkFFV t2 fv in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let prh := proofHyp_tac lH in + let vlpe := fresh "list_hyp" in + let fe1 := mkFE t1 fv in + let fe2 := mkFE t2 fv in + pose (vlpe := lpe); + let nlemma := fresh "field_lemma" in + (assert (nlemma := lemma n fv vlpe fe1 fe2 prh) + || fail "field anomaly:failed to build lemma"); + ParseExpr nlemma + ltac:(fun ilemma => + apply ilemma + || fail "field anomaly: failed in applying lemma"; + [ Simpl_tac | apply Cond_lemma; simpl_PCond req]); + clear vlpe nlemma in + OnEquation req Main_eq in + ParseFieldComponents lemma Main. + +(* solve completely a field equation, leaving non-zero conditions to be + proved (field) *) + +Ltac FIELD := + let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in + fun req cst_tac pow_tac field_ok _ _ _ cond_ok pre post lH rl => + pre(); + Field_Scheme Simpl cst_tac pow_tac field_ok cond_ok req + Ring_tac.ring_subst_niter lH; + try exact I; + post(). + +Tactic Notation (at level 0) "field" := + let G := getGoal in field_lookup FIELD [] [G]. + +Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" := + let G := getGoal in field_lookup FIELD [lH] [G]. + +(* transforms a field equation to an equivalent (simplified) ring equation, + and leaves non-zero conditions to be proved (field_simplify_eq) *) + +Ltac FIELD_SIMPL := + let Simpl := (protect_fv "field") in + fun req cst_tac pow_tac _ field_simplify_eq_ok _ _ cond_ok pre post lH rl => + pre(); + Field_Scheme Simpl cst_tac pow_tac field_simplify_eq_ok cond_ok + req Ring_tac.ring_subst_niter lH; + post(). + +Tactic Notation (at level 0) "field_simplify_eq" := + let G := getGoal in field_lookup FIELD_SIMPL [] [G]. + +Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" := + let G := getGoal in field_lookup FIELD_SIMPL [lH] [G]. + +(* Same as FIELD_SIMPL but in hypothesis *) + +Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH := + let Main radd rmul rsub ropp rdiv rinv rpow C := + let hyp := fresh "hyp" in + intro hyp; + match type of hyp with + | req ?t1 ?t2 => + let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let mkFE := + mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let rec ParseExpr ilemma := + match type of ilemma with + | forall nfe, ?fe = nfe -> _ => + (fun t => + let x := fresh "fld_expr" in + let H := fresh "norm_fld_expr" in + compute_assertion H x fe; + ParseExpr (ilemma x H) t; + try clear H x) + | _ => (fun t => t ilemma) + end in + let fv := FV_hypo_tac mkFV req lH in + let fv := mkFFV t1 fv in + let fv := mkFFV t2 fv in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let prh := proofHyp_tac lH in + let fe1 := mkFE t1 fv in + let fe2 := mkFE t2 fv in + let vlpe := fresh "vlpe" in + ParseExpr (lemma n fv lpe fe1 fe2 prh) + ltac:(fun ilemma => + match type of ilemma with + | req _ _ -> _ -> ?EQ => + let tmp := fresh "tmp" in + assert (tmp : EQ); + [ apply ilemma; + [ exact hyp | apply Cond_lemma; simpl_PCond_BEURK req] + | protect_fv "field" in tmp; + generalize tmp;clear tmp ]; + clear hyp + end) + end in + ParseFieldComponents lemma Main. + +Ltac FIELD_SIMPL_EQ := + fun req cst_tac pow_tac _ _ _ lemma cond_ok pre post lH rl => + pre(); + Field_simplify_eq cst_tac pow_tac lemma cond_ok req + Ring_tac.ring_subst_niter lH; + post(). + +Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) := + let t := type of H in + generalize H; + field_lookup FIELD_SIMPL_EQ [] [t]; + [ try exact I + | clear H;intro H]. + + +Tactic Notation (at level 0) + "field_simplify_eq" "[" constr_list(lH) "]" "in" hyp(H) := + let t := type of H in + generalize H; + field_lookup FIELD_SIMPL_EQ [lH] [t]; + [ try exact I + |clear H;intro H]. + +(* Adding a new field *) + +Ltac ring_of_field f := + match type of f with + | almost_field_theory _ _ _ _ _ _ _ _ _ => constr:(AF_AR f) + | field_theory _ _ _ _ _ _ _ _ _ => constr:(F_R f) + | semi_field_theory _ _ _ _ _ _ _ => constr:(SF_SR f) + end. + +Ltac coerce_to_almost_field set ext f := + match type of f with + | almost_field_theory _ _ _ _ _ _ _ _ _ => f + | field_theory _ _ _ _ _ _ _ _ _ => constr:(F2AF set ext f) + | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f) + end. + +Ltac field_elements set ext fspec pspec sspec rk := + let afth := coerce_to_almost_field set ext fspec in + let rspec := ring_of_field fspec in + ring_elements set ext rspec pspec sspec rk + ltac:(fun arth ext_r morph p_spec s_spec f => f afth ext_r morph p_spec s_spec). + +Ltac field_lemmas set ext inv_m fspec pspec sspec rk := + let simpl_eq_lemma := + match pspec with + | None => constr:(Field_simplify_eq_correct) + | Some _ => constr:(Field_simplify_eq_pow_correct) + end in + let simpl_eq_in_lemma := + match pspec with + | None => constr:(Field_simplify_eq_in_correct) + | Some _ => constr:(Field_simplify_eq_pow_in_correct) + end in + let rw_lemma := + match pspec with + | None => constr:(Field_rw_correct) + | Some _ => constr:(Field_rw_pow_correct) + end in + field_elements set ext fspec pspec sspec rk + ltac:(fun afth ext_r morph p_spec s_spec => + match p_spec with + | mkhypo ?pp_spec => match s_spec with + | mkhypo ?ss_spec => + let field_simpl_eq_ok := + constr:(simpl_eq_lemma _ _ _ _ _ _ _ _ _ _ + set ext_r inv_m afth + _ _ _ _ _ _ _ _ _ morph + _ _ _ pp_spec _ ss_spec) in + let field_simpl_ok := + constr:(rw_lemma _ _ _ _ _ _ _ _ _ _ + set ext_r inv_m afth + _ _ _ _ _ _ _ _ _ morph + _ _ _ pp_spec _ ss_spec) in + let field_simpl_eq_in := + constr:(simpl_eq_in_lemma _ _ _ _ _ _ _ _ _ _ + set ext_r inv_m afth + _ _ _ _ _ _ _ _ _ morph + _ _ _ pp_spec _ ss_spec) in + let field_ok := + constr:(Field_correct set ext_r inv_m afth morph pp_spec ss_spec) in + let cond1_ok := + constr:(Pcond_simpl_gen set ext_r afth morph pp_spec) in + let cond2_ok := + constr:(Pcond_simpl_complete set ext_r afth morph pp_spec) in + (fun f => + f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok field_simpl_eq_in + cond1_ok cond2_ok) + | _ => fail 2 "bad sign specification" + end + | _ => fail 1 "bad power specification" + end). + |