diff options
Diffstat (limited to 'contrib/setoid_ring/Ring_tac.v')
| -rw-r--r-- | contrib/setoid_ring/Ring_tac.v | 386 |
1 files changed, 0 insertions, 386 deletions
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v deleted file mode 100644 index ad20fa08..00000000 --- a/contrib/setoid_ring/Ring_tac.v +++ /dev/null @@ -1,386 +0,0 @@ -Set Implicit Arguments. -Require Import Setoid. -Require Import BinPos. -Require Import Ring_polynom. -Require Import BinList. -Require Import InitialRing. - - -(* adds a definition id' on the normal form of t and an hypothesis id - stating that t = id' (tries to produces a proof as small as possible) *) -Ltac compute_assertion id id' t := - let t' := eval vm_compute in t in - pose (id' := t'); - assert (id : t = id'); - [vm_cast_no_check (refl_equal id')|idtac]. -(* [exact_no_check (refl_equal id'<: t = id')|idtac]). *) - -(********************************************************************) -(* Tacticals to build reflexive tactics *) - -Ltac OnEquation req := - match goal with - | |- req ?lhs ?rhs => (fun f => f lhs rhs) - | _ => fail 1 "Goal is not an equation (of expected equality)" - end. - -Ltac OnMainSubgoal H ty := - match ty with - | _ -> ?ty' => - let subtac := OnMainSubgoal H ty' in - fun tac => lapply H; [clear H; intro H; subtac tac | idtac] - | _ => (fun tac => tac) - end. - -Ltac ApplyLemmaThen lemma expr tac := - let nexpr := fresh "expr_nf" in - let H := fresh "eq_nf" in - let Heq := fresh "thm" in - let nf_spec := - match type of (lemma expr) with - forall x, ?nf_spec = x -> _ => nf_spec - | _ => fail 1 "ApplyLemmaThen: cannot find norm expression" - end in - compute_assertion H nexpr nf_spec; - assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma"; - clear H; - OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr). - -Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg := - let npe := fresh "expr_nf" in - let H := fresh "eq_nf" in - let Heq := fresh "thm" in - let npe_spec := - match type of (lemma expr) with - forall npe, ?npe_spec = npe -> _ => npe_spec - | _ => fail 1 "ApplyLemmaThenAndCont: cannot find norm expression" - end in - (compute_assertion H npe npe_spec; - (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma"); - clear H; - OnMainSubgoal Heq ltac:(type of Heq) - ltac:(try tac Heq; clear Heq npe;CONT_tac cont_arg)). - -(* General scheme of reflexive tactics using of correctness lemma - that involves normalisation of one expression *) - -Ltac ReflexiveRewriteTactic FV_tac SYN_tac MAIN_tac LEMMA_tac fv terms := - (* extend the atom list *) - let fv := list_fold_left FV_tac fv terms in - let RW_tac lemma := - let fcons term CONT_tac cont_arg := - let expr := SYN_tac term fv in - (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac cont_arg) in - (* rewrite steps *) - lazy_list_fold_right fcons ltac:(idtac) terms in - LEMMA_tac fv RW_tac. - -(********************************************************) - - -(* Building the atom list of a ring expression *) -Ltac FV Cst CstPow add mul sub opp pow t fv := - let rec TFV t fv := - match Cst t with - | 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 - | (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. - - (* syntaxification of ring expressions *) -Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := - let rec mkP t := - let f := - match Cst t with - | InitialRing.NotConstant => - match t with - | (radd ?t1 ?t2) => - fun _ => - let e1 := mkP t1 in - let e2 := mkP t2 in constr:(PEadd e1 e2) - | (rmul ?t1 ?t2) => - fun _ => - let e1 := mkP t1 in - let e2 := mkP t2 in constr:(PEmul e1 e2) - | (rsub ?t1 ?t2) => - fun _ => - let e1 := mkP t1 in - let e2 := mkP t2 in constr:(PEsub e1 e2) - | (ropp ?t1) => - fun _ => - let e1 := mkP t1 in constr:(PEopp e1) - | (rpow ?t1 ?n) => - match CstPow n with - | InitialRing.NotConstant => - fun _ => let p := Find_at t fv in constr:(PEX C p) - | ?c => fun _ => let e1 := mkP t1 in constr:(PEpow e1 c) - end - | _ => - fun _ => let p := Find_at t fv in constr:(PEX C p) - end - | ?c => fun _ => constr:(@PEc C c) - end in - f () - in mkP t. - -Ltac ParseRingComponents lemma := - match type of lemma with - | context [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] => - (fun f => f R add mul sub opp pow C) - | _ => fail 1 "ring anomaly: bad correctness lemma (parse)" - end. - -(* ring tactics *) - -Ltac relation_carrier req := - let ty := type of req in - match eval hnf in ty with - ?R -> _ => R - | _ => fail 1000 "Equality has no relation type" - end. - -Ltac FV_hypo_tac mkFV req lH := - let R := relation_carrier req in - let FV_hypo_l_tac h := - match h with @mkhypo (req ?pe _) _ => mkFV pe end in - let FV_hypo_r_tac h := - match h with @mkhypo (req _ ?pe) _ => mkFV pe end in - let fv := list_fold_right FV_hypo_l_tac (@nil R) lH in - list_fold_right FV_hypo_r_tac fv lH. - -Ltac mkHyp_tac C req mkPE lH := - let mkHyp h res := - match h with - | @mkhypo (req ?r1 ?r2) _ => - let pe1 := mkPE r1 in - let pe2 := mkPE r2 in - constr:(cons (pe1,pe2) res) - | _ => fail 1 "hypothesis is not a ring equality" - end in - list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH. - -Ltac proofHyp_tac lH := - let get_proof h := - match h with - | @mkhypo _ ?p => p - end in - let rec bh l := - match l with - | nil => constr:(I) - | cons ?h nil => get_proof h - | cons ?h ?tl => - let l := get_proof h in - let r := bh tl in - constr:(conj l r) - end in - bh lH. - -Definition ring_subst_niter := (10*10*10)%nat. - -Ltac Ring Cst_tac CstPow_tac lemma1 req n lH := - let Main lhs rhs R radd rmul rsub ropp rpow C := - let mkFV := FV Cst_tac CstPow_tac radd rmul rsub ropp rpow in - let mkPol := mkPolexpr C Cst_tac CstPow_tac radd rmul rsub ropp rpow in - let fv := FV_hypo_tac mkFV req lH in - let fv := mkFV lhs fv in - let fv := mkFV rhs fv in - check_fv fv; - let pe1 := mkPol lhs fv in - let pe2 := mkPol rhs fv in - let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in - let vlpe := fresh "hyp_list" in - let vfv := fresh "fv_list" in - pose (vlpe := lpe); - pose (vfv := fv); - (apply (lemma1 n vfv vlpe pe1 pe2) - || fail "typing error while applying ring"); - [ ((let prh := proofHyp_tac lH in exact prh) - || idtac "can not automatically proof hypothesis : maybe a left member of a hypothesis is not a monomial") - | vm_compute; - (exact (refl_equal true) || fail "not a valid ring equation")] in - ParseRingComponents lemma1 ltac:(OnEquation req Main). - -Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl := - let Main R add mul sub opp pow C := - let mkFV := FV Cst_tac CstPow_tac add mul sub opp pow in - let mkPol := mkPolexpr C Cst_tac CstPow_tac add mul sub opp pow in - let fv := FV_hypo_tac mkFV req lH in - let simpl_ring H := (protect_fv "ring" in H; f H) in - let lemma_tac fv RW_tac := - let rr_lemma := fresh "r_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 lemma2 with - | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _] - => - compute_assertion vlmp_eq vlmp - (mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe); - (assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq) - || fail 1 "type error when build the rewriting lemma"); - RW_tac rr_lemma; - try clear rr_lemma vlmp_eq vlmp vlpe - | _ => fail 1 "ring_simplify anomaly: bad correctness lemma" - end in - ReflexiveRewriteTactic mkFV mkPol simpl_ring lemma_tac fv rl in - ParseRingComponents lemma2 Main. - - -Ltac Ring_gen - req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl := - pre();Ring cst_tac pow_tac lemma1 req ring_subst_niter lH. - -Ltac Get_goal := match goal with [|- ?G] => G end. - -Tactic Notation (at level 0) "ring" := - let G := Get_goal in - ring_lookup Ring_gen [] G. - -Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" := - let G := Get_goal in - ring_lookup Ring_gen [lH] G. - -(* Simplification *) - -Ltac Ring_simplify_gen f := - fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => - let l := fresh "to_rewrite" in - pose (l:= rl); - generalize (refl_equal l); - unfold l at 2; - pre(); - let Tac RL := - let Heq := fresh "Heq" in - intros Heq;clear Heq l; - Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH RL; - post() in - let Main := - match goal with - | [|- l = ?RL -> _ ] => (fun f => f RL) - | _ => fail 1 "ring_simplify anomaly: bad goal after pre" - end in - Main Tac. - -Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H). - -Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := - let G := Get_goal in - ring_lookup Ring_simplify [] rl G. - -Tactic Notation (at level 0) - "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := - let G := Get_goal in - ring_lookup Ring_simplify [lH] rl G. - -(* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *) - -Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= - let G := Get_goal in - let t := type of H in - let g := fresh "goal" in - set (g:= G); - generalize H;clear H; - ring_lookup Ring_simplify [] rl t; - intro H; - unfold g;clear g. - -Tactic Notation - "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):= - let G := Get_goal in - let t := type of H in - let g := fresh "goal" in - set (g:= G); - generalize H;clear H; - ring_lookup Ring_simplify [lH] rl t; - intro H; - unfold g;clear g. - - - -(* LE RESTE MARCHE PAS DOMMAGE ..... *) - - - - - - - - - - - - - - - -(* - - - - - - - - -Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp). - - -Tactic Notation (at level 0) - "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := - match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl G end. - -Tactic Notation (at level 0) - "ring_simplify" constr_list(rl) := - match goal with [|- ?G] => ring_lookup Ring_simplify [] rl G end. - -Tactic Notation (at level 0) - "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):= - let t := type of h in - ring_lookup - (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => - pre(); - Ring_norm_gen ltac:(fun EQ => rewrite EQ in h) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; - post()) - [lH] rl t. -(* ring_lookup ltac:(Ring_simplify_in h) [lH] rl [t]. NE MARCHE PAS ??? *) - -Ltac Ring_simpl_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp). - -Tactic Notation (at level 0) - "ring_simplify" constr_list(rl) "in" constr(h):= - let t := type of h in - ring_lookup - (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => - pre(); - Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl; - post()) - [] rl t. - -Ltac rw_in H Heq := rewrite Heq in H. - -Ltac simpl_in H := - let t := type of H in - ring_lookup - (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => - pre(); - Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; - post()) - [] t. - - -*) |