(***************************************************************************) (* This is part of aac_tactics, it is distributed under the terms of the *) (* GNU Lesser General Public License version 3 *) (* (see file LICENSE for more details) *) (* *) (* Copyright 2009-2010: Thomas Braibant, Damien Pous. *) (***************************************************************************) (** aac_rewrite -- rewriting modulo A or AC*) open Ltac_plugin module Control = struct let debug = false let printing = false let time = false end module Debug = Helper.Debug (Control) open Debug let time_tac msg tac = if Control.time then Coq.tclTIME msg tac else tac let tac_or_exn tac exn msg = fun gl -> try tac gl with e -> let env = Tacmach.pf_env gl in let sigma = Tacmach.project gl in pr_constr env sigma "last goal" (Tacmach.pf_concl gl); exn msg e let retype = Coq.retype open EConstr open Names open Proof_type (** aac_lift : the ideal type beyond AAC_rewrite.v/Lift A base relation r, together with an equivalence relation, and the proof that the former lifts to the later. Howver, we have to ensure manually the invariant : r.carrier == e.carrier, and that lift connects the two things *) type aac_lift = { r : Coq.Relation.t; e : Coq.Equivalence.t; lift : constr } type rewinfo = { hypinfo : Coq.Rewrite.hypinfo; in_left : bool; (** are we rewriting in the left hand-sie of the goal *) pattern : constr; subject : constr; morph_rlt : Coq.Relation.t; (** the relation we look for in morphism *) eqt : Coq.Equivalence.t; (** the equivalence we use as workbase *) rlt : Coq.Relation.t; (** the relation in the goal *) lifting: aac_lift } let infer_lifting (rlt: Coq.Relation.t) (k : lift:aac_lift -> Proof_type.tactic) : Proof_type.tactic = Coq.cps_evar_relation rlt.Coq.Relation.carrier (fun e -> let lift_ty = mkApp (Lazy.force Theory.Stubs.lift, [| rlt.Coq.Relation.carrier; rlt.Coq.Relation.r; e |] ) in Coq.cps_resolve_one_typeclass ~error:(Pp.strbrk "Cannot infer a lifting") lift_ty (fun lift goal -> let x = rlt.Coq.Relation.carrier in let r = rlt.Coq.Relation.r in let eq = (Coq.nf_evar goal e) in let equiv = Coq.lapp Theory.Stubs.lift_proj_equivalence [| x;r;eq; lift |] in let lift = { r = rlt; e = Coq.Equivalence.make x eq equiv; lift = lift; } in k ~lift:lift goal )) (** Builds a rewinfo, once and for all *) let dispatch in_left (left,right,rlt) hypinfo (k: rewinfo -> Proof_type.tactic ) : Proof_type.tactic= let l2r = hypinfo.Coq.Rewrite.l2r in infer_lifting rlt (fun ~lift -> let eq = lift.e in k { hypinfo = hypinfo; in_left = in_left; pattern = if l2r then hypinfo.Coq.Rewrite.left else hypinfo.Coq.Rewrite.right; subject = if in_left then left else right; morph_rlt = Coq.Equivalence.to_relation eq; eqt = eq; lifting = lift; rlt = rlt } ) (** {1 Tactics} *) (** Build the reifiers, the reified terms, and the evaluation fonction *) let handle eqt zero envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) k = let (x,r,_) = Coq.Equivalence.split eqt in Theory.Trans.mk_reifier (Coq.Equivalence.to_relation eqt) zero envs (fun (maps, reifier) -> (* fold through a term and reify *) let t = Theory.Trans.reif_constr_of_t reifier t in let t' = Theory.Trans.reif_constr_of_t reifier t' in (* Some letins *) let eval = (mkApp (Lazy.force Theory.Stubs.eval, [|x;r; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_bin; maps.Theory.Trans.env_units|])) in Coq.cps_mk_letin "eval" eval (fun eval -> Coq.cps_mk_letin "left" t (fun t -> Coq.cps_mk_letin "right" t' (fun t' -> k maps eval t t')))) (** [by_aac_reflexivity] is a sub-tactic that closes a sub-goal that is merely a proof of equality of two terms modulo AAC *) let by_aac_reflexivity zero eqt envs (t : Matcher.Terms.t) (t' : Matcher.Terms.t) : Proof_type.tactic = handle eqt zero envs t t' (fun maps eval t t' -> let (x,r,e) = Coq.Equivalence.split eqt in let decision_thm = Coq.lapp Theory.Stubs.decide_thm [|x;r;e; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_bin; maps.Theory.Trans.env_units; t;t'; |] in (* This convert is required to deal with evars in a proper way *) let convert_to = mkApp (r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Constr.VMcast) in let apply_tac = Proofview.V82.of_tactic (Tactics.apply decision_thm) in (Tacticals.tclTHENLIST [ retype decision_thm; retype convert_to; convert ; tac_or_exn apply_tac Coq.user_error (Pp.strbrk "unification failure"); tac_or_exn (time_tac "vm_norm" (Proofview.V82.of_tactic (Tactics.normalise_in_concl))) Coq.anomaly "vm_compute failure"; Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity) (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) ]) ) let by_aac_normalise zero lift ir t t' = let eqt = lift.e in let rlt = lift.r in handle eqt zero ir t t' (fun maps eval t t' -> let (x,r,e) = Coq.Equivalence.split eqt in let normalise_thm = Coq.lapp Theory.Stubs.lift_normalise_thm [|x;r;e; maps.Theory.Trans.env_sym; maps.Theory.Trans.env_bin; maps.Theory.Trans.env_units; rlt.Coq.Relation.r; lift.lift; t;t'; |] in (* This convert is required to deal with evars in a proper way *) let convert_to = mkApp (rlt.Coq.Relation.r, [| mkApp (eval,[| t |]); mkApp (eval, [|t'|])|]) in let convert = Proofview.V82.of_tactic (Tactics.convert_concl convert_to Constr.VMcast) in let apply_tac = Proofview.V82.of_tactic (Tactics.apply normalise_thm) in (Tacticals.tclTHENLIST [ retype normalise_thm; retype convert_to; convert ; apply_tac; ]) ) (** A handler tactic, that reifies the goal, and infer the liftings, and then call its continuation *) let aac_conclude (k : constr -> aac_lift -> Theory.Trans.ir -> Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic) = fun goal -> let (equation : types) = Tacmach.pf_concl goal in let envs = Theory.Trans.empty_envs () in let left, right,r = match Coq.match_as_equation goal equation with | None -> Coq.user_error @@ Pp.strbrk "The goal is not an applied relation" | Some x -> x in try infer_lifting r (fun ~lift goal -> let eq = Coq.Equivalence.to_relation lift.e in let tleft,tright, goal = Theory.Trans.t_of_constr goal eq envs (left,right) in let goal, ir = Theory.Trans.ir_of_envs goal eq envs in let concl = Tacmach.pf_concl goal in let env = Tacmach.pf_env goal in let sigma = Tacmach.project goal in let _ = pr_constr env sigma "concl "concl in let evar_map = Tacmach.project goal in Tacticals.tclTHEN (Refiner.tclEVARS evar_map) (k left lift ir tleft tright) goal )goal with | Not_found -> Coq.user_error @@ Pp.strbrk "No lifting from the goal's relation to an equivalence" open Tacexpr let aac_normalise = fun goal -> let ids = Tacmach.pf_ids_of_hyps goal in let mp = MPfile (DirPath.make (List.map Id.of_string ["AAC"; "AAC_tactics"])) in let norm_tac = KerName.make2 mp (Label.make "internal_normalize") in let norm_tac = Locus.ArgArg (None, norm_tac) in Tacticals.tclTHENLIST [ aac_conclude by_aac_normalise; Proofview.V82.of_tactic (Tacinterp.eval_tactic (TacArg (None, TacCall (None, (norm_tac, []))))); Proofview.V82.of_tactic (Tactics.keep ids) ] goal let aac_reflexivity = fun goal -> aac_conclude (fun zero lift ir t t' -> let x,r = Coq.Relation.split (lift.r) in let r_reflexive = (Coq.Classes.mk_reflexive x r) in Coq.cps_resolve_one_typeclass ~error:(Pp.strbrk "The goal's relation is not reflexive") r_reflexive (fun reflexive -> let lift_reflexivity = mkApp (Lazy.force (Theory.Stubs.lift_reflexivity), [| x; r; lift.e.Coq.Equivalence.eq; lift.lift; reflexive |]) in Tacticals.tclTHEN (Tacticals.tclTHEN (retype lift_reflexivity) (Proofview.V82.of_tactic (Tactics.apply lift_reflexivity))) (fun goal -> let concl = Tacmach.pf_concl goal in let env = Tacmach.pf_env goal in let sigma = Tacmach.project goal in let _ = pr_constr env sigma "concl "concl in by_aac_reflexivity zero lift.e ir t t' goal) ) ) goal (** A sub-tactic to lift the rewriting using Lift *) let lift_transitivity in_left (step:constr) preorder lifting (using_eq : Coq.Equivalence.t): tactic = fun goal -> (* catch the equation and the two members*) let concl = Tacmach.pf_concl goal in let (left, right, _ ) = match Coq.match_as_equation goal concl with | Some x -> x | None -> Coq.user_error @@ Pp.strbrk "The goal is not an equation" in let lift_transitivity = let thm = if in_left then Lazy.force Theory.Stubs.lift_transitivity_left else Lazy.force Theory.Stubs.lift_transitivity_right in mkApp (thm, [| preorder.Coq.Relation.carrier; preorder.Coq.Relation.r; using_eq.Coq.Equivalence.eq; lifting; step; left; right; |]) in Tacticals.tclTHENLIST [ retype lift_transitivity; Proofview.V82.of_tactic (Tactics.apply lift_transitivity) ] goal (** The core tactic for aac_rewrite. Env and sigma are for the constr *) let core_aac_rewrite ?abort rewinfo subst (by_aac_reflexivity : Matcher.Terms.t -> Matcher.Terms.t -> Proof_type.tactic) env sigma (tr : constr) t left : tactic = pr_constr env sigma "transitivity through" tr; let tran_tac = lift_transitivity rewinfo.in_left tr rewinfo.rlt rewinfo.lifting.lift rewinfo.eqt in Coq.Rewrite.rewrite ?abort rewinfo.hypinfo subst (fun rew -> Tacticals.tclTHENSV (tac_or_exn (tran_tac) Coq.anomaly "Unable to make the transitivity step") ( if rewinfo.in_left then [| by_aac_reflexivity left t ; rew |] else [| by_aac_reflexivity t left ; rew |] ) ) exception NoSolutions (** Choose a substitution from a [(int * Terms.t * Env.env Search_monad.m) Search_monad.m ] *) (* WARNING: Beware, since the printing function can change the order of the printed monad, this function has to be updated accordingly *) let choose_subst subterm sol m= try let (depth,pat,envm) = match subterm with | None -> (* first solution *) List.nth ( List.rev (Search_monad.to_list m)) 0 | Some x -> List.nth ( List.rev (Search_monad.to_list m)) x in let env = match sol with None -> List.nth ( (Search_monad.to_list envm)) 0 | Some x -> List.nth ( (Search_monad.to_list envm)) x in pat, env with | _ -> raise NoSolutions (** rewrite the constr modulo AC from left to right in the left member of the goal *) let aac_rewrite_wrap ?abort rew ?(l2r=true) ?(show = false) ?(in_left=true) ?strict ~occ_subterm ~occ_sol ?extra : Proof_type.tactic = fun goal -> let envs = Theory.Trans.empty_envs () in let (concl : types) = Tacmach.pf_concl goal in let (_,_,rlt) as concl = match Coq.match_as_equation goal concl with | None -> Coq.user_error @@ Pp.strbrk "The goal is not an applied relation" | Some (left, right, rlt) -> left,right,rlt in let check_type x = Tacmach.pf_conv_x goal x rlt.Coq.Relation.carrier in Coq.Rewrite.get_hypinfo rew ~l2r ?check_type:(Some check_type) (fun hypinfo -> dispatch in_left concl hypinfo ( fun rewinfo -> let goal = match extra with | Some t -> Theory.Trans.add_symbol goal rewinfo.morph_rlt envs (EConstr.to_constr (Tacmach.project goal) t) | None -> goal in let pattern, subject, goal = Theory.Trans.t_of_constr goal rewinfo.morph_rlt envs (rewinfo.pattern , rewinfo.subject) in let goal, ir = Theory.Trans.ir_of_envs goal rewinfo.morph_rlt envs in let units = Theory.Trans.ir_to_units ir in let m = Matcher.subterm ?strict units pattern subject in (* We sort the monad in increasing size of contet *) let m = Search_monad.sort (fun (x,_,_) (y,_,_) -> x - y) m in if show then Print.print rewinfo.morph_rlt ir m (hypinfo.Coq.Rewrite.context) else try let pat,subst = choose_subst occ_subterm occ_sol m in let tr_step = Matcher.Subst.instantiate subst pat in let tr_step_raw = Theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt [] tr_step in let conv = (Theory.Trans.raw_constr_of_t ir rewinfo.morph_rlt (hypinfo.Coq.Rewrite.context)) in let subst = Matcher.Subst.to_list subst in let subst = List.map (fun (x,y) -> x, conv y) subst in let by_aac_reflexivity = (by_aac_reflexivity rewinfo.subject rewinfo.eqt ir) in let env = Tacmach.pf_env goal in let sigma = Tacmach.project goal in (* I'm not sure whether this is the right env/sigma for printing tr_step_raw *) core_aac_rewrite ?abort rewinfo subst by_aac_reflexivity env sigma tr_step_raw tr_step subject with | NoSolutions -> Tacticals.tclFAIL 0 (Pp.str (if occ_subterm = None && occ_sol = None then "No matching occurrence modulo AC found" else "No such solution")) ) ) goal let get k l = try Some (List.assoc k l) with Not_found -> None let get_lhs l = try ignore (List.assoc "in_right" l); false with Not_found -> true let aac_rewrite ~args = aac_rewrite_wrap ~occ_subterm:(get "at" args) ~occ_sol:(get "subst" args) ~in_left:(get_lhs args) let rec add k x = function | [] -> [k,x] | k',_ as ky::q -> if k'=k then Coq.user_error @@ Pp.strbrk ("redondant argument ("^k^")") else ky::add k x q let pr_aac_args _ _ _ l = List.fold_left (fun acc -> function | ("in_right" as s,_) -> Pp.(++) (Pp.str s) acc | (k,i) -> Pp.(++) (Pp.(++) (Pp.str k) (Pp.int i)) acc ) (Pp.str "") l