From 4aec8fda1161953cf929b4e282eea9b672ab4058 Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 26 Sep 2006 12:13:06 +0000 Subject: commit de field + renommages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/setoid_ring/Field_tac.v | 161 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 161 insertions(+) create mode 100644 contrib/setoid_ring/Field_tac.v (limited to 'contrib/setoid_ring/Field_tac.v') diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v new file mode 100644 index 000000000..2ac96b826 --- /dev/null +++ b/contrib/setoid_ring/Field_tac.v @@ -0,0 +1,161 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + match t with + | (radd ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEadd C e1 e2) + | (rmul ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEmul C e1 e2) + | (rsub ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEsub C e1 e2) + | (ropp ?t1) => + let e1 := mkP t1 in constr:(FEopp C e1) + | (rdiv ?t1 ?t2) => + let e1 := mkP t1 in + let e2 := mkP t2 in constr:(FEdiv C e1 e2) + | (rinv ?t1) => + let e1 := mkP t1 in constr:(FEinv C e1) + | _ => + let p := Find_at t fv in constr:(FEX C p) + end + | ?c => constr:(FEc C c) + end + in mkP t. + +Ltac FFV Cst add mul sub opp div inv t fv := + let rec TFV t fv := + match Cst t with + | Ring_tac.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 + | _ => AddFvTail t fv + end + | _ => fv + end + in TFV t fv. + +(* simplifying the non-zero condition... *) + +Ltac fold_field_cond req rO := + 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 rO -> False => constr:(~ req x rO) + | _ => t + end in + match goal with + |- ?t => let ft := fold_concl t in change ft + end. + +Ltac simpl_PCond req rO := + protect_fv "field"; + try (exact I); + fold_field_cond req rO. + +(* Rewriting *) +Ltac Field_rewrite_list lemma Cond_lemma req Cst_tac := + let Make_tac := + match type of lemma with + | forall l fe nfe, + _ = nfe -> + PCond _ _ _ _ _ _ _ _ _ _ _ -> + req (FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv ?C ?phi l fe) _ => + let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in + let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in + let simpl_field H := (*protect_fv "field" in H*) +unfold Pphi_dev in H;simpl in H in + (fun f => f mkFV mkFE simpl_field lemma req; + try (apply Cond_lemma; simpl_PCond req rO)) + | _ => fail 1 "field anomaly: bad correctness lemma" + end in + Make_tac ReflexiveRewriteTactic. +(* Pb: second rewrite are applied to non-zero condition of first rewrite... *) + + +(* Generic form of field tactics *) +Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req := + let ParseLemma := + match type of lemma with + | forall l fe1 fe2 nfe1 nfe2, _ = nfe1 -> _ = nfe2 -> _ -> + PCond _ _ _ _ _ _ _ _ _ _ _ -> + req (FEeval ?R ?rO _ _ _ _ _ _ _ _ l fe1) _ => + (fun f => f R rO) + | _ => fail 1 "field anomaly: bad correctness lemma" + end in + let ParseExpr2 ilemma := + match type of ilemma with + forall nfe1 nfe2, ?fe1 = nfe1 -> ?fe2 = nfe2 -> _ => (fun f => f fe1 fe2) + | _ => fail 1 "field anomaly: cannot find norm expression" + end in + let Main r1 r2 R rO := + let fv := FV_tac r1 (@List.nil R) in + let fv := FV_tac r2 fv in + let fe1 := SYN_tac r1 fv in + let fe2 := SYN_tac r2 fv in + let nfrac1 := fresh "frac1" in + let norm_hyp1 := fresh "norm_frac1" in + let nfrac2 := fresh "frac2" in + let norm_hyp2 := fresh "norm_frac2" in + ParseExpr2 (lemma fv fe1 fe2) + ltac:(fun nfrac_val1 nfrac_val2 => + (compute_assertion norm_hyp1 nfrac1 nfrac_val1; + compute_assertion norm_hyp2 nfrac2 nfrac_val2; + (apply (lemma fv fe1 fe2 nfrac1 nfrac2 norm_hyp1 norm_hyp2) + || fail "field anomaly: failed in applying lemma"); + [ SIMPL_tac | apply Cond_lemma; simpl_PCond req rO]; + try clear nfrac1 nfrac2 norm_hyp1 norm_hyp2)) in + ParseLemma ltac:(OnEquation req Main). + + +Ltac ParseFieldComponents lemma req := + match type of lemma with + | forall l fe1 fe2 nfe1 nfe2, + _ = nfe1 -> _ = nfe2 -> _ -> PCond _ _ _ _ _ _ _ _ _ _ _ -> + req (FEeval ?R ?rO ?add ?mul ?sub ?opp ?div ?inv ?C ?phi l fe1) _ => + (fun f => f add mul sub opp div inv C) + | _ => fail 1 "field: bad correctness lemma" + end. + +(* solve completely a field equation, leaving non-zero conditions to be + proved *) +Ltac Make_field_tac lemma Cond_lemma req Cst_tac := + let Main radd rmul rsub ropp rdiv rinv C := + let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in + let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in + let Simpl := + vm_compute; (reflexivity || fail "not a valid field equation") in + Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in + ParseFieldComponents lemma req Main. + +(* transforms a field equation to an equivalent (simplified) ring equation, + and leaves non-zero conditions to be proved *) +Ltac Make_field_simplify_eq_tac lemma Cond_lemma req Cst_tac := + let Main radd rmul rsub ropp rdiv rinv C := + let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in + let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in + let Simpl := (unfold Pphi_dev; simpl) in + Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in + ParseFieldComponents lemma req Main. -- cgit v1.2.3