))
~continuation:
(T.then_
- ~start:(EqualityTactics.rewrite_simpl_tac ~term)
+ ~start:(EqualityTactics.rewrite_simpl_tac ~term ())
~continuation:EqualityTactics.reflexivity_tac
)
])
~continuation:
(
T.then_
- ~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
+ ~start:(EqualityTactics.rewrite_back_simpl_tac
+ ~term ())
~continuation:(IntroductionTactics.constructor_tac ~n:1)
))
(proof',goal')
* For details, see the HELM World-Wide-Web page,
* http://cs.unibo.it/helm/.
*)
+
-let rewrite ~term:equality ?(direction=`Left) (proof,goal) =
+let rewrite ~term:equality ?where ?(direction=`Left) (proof,goal) =
let module C = Cic in
let module U = UriManager in
let module PET = ProofEngineTypes in
+ let module PER = ProofEngineReduction in
+ let module PEH = ProofEngineHelpers in
let module PT = PrimitiveTactics in
let module HLO = HelmLibraryObjects in
let if_left a b =
(* now we always do as if direction was `Left *)
let gty' = CicSubstitution.lift 1 gty in
let t1' = CicSubstitution.lift 1 t1 in
+ let eq_kind, what =
+ match where with
+ | None
+ | Some ([], None) ->
+ PER.alpha_equivalence, [t1']
+ | Some (hp_paths, goal_path) ->
+ assert (hp_paths = []);
+ match goal_path with
+ | None -> assert false (* (==), [t1'] *)
+ | Some path ->
+ let roots = CicUtil.select ~term:gty' ~context:path in
+ let subterms =
+ List.fold_left (
+ fun acc (i, r) ->
+ let wanted = CicSubstitution.lift i t1' in
+ PEH.find_subterms ~eq:PER.alpha_equivalence ~wanted r @ acc
+ ) [] roots
+ in
+ (==), subterms
+ in
+ let with_what =
+ let rec aux = function
+ | 0 -> []
+ | n -> C.Rel 1 :: aux (n-1)
+ in
+ aux (List.length what)
+ in
let gty'' =
ProofEngineReduction.replace_lifting
- ~equality:ProofEngineReduction.alpha_equivalence
- ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
+ ~equality:eq_kind ~what ~with_what ~where:gty'
in
let gty_red = CicSubstitution.subst t2 gty'' in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
(proof',[fresh_meta])
-let rewrite_tac ~term =
- let rewrite_tac ~term status =
- rewrite ~term ~direction:`Right status
+let rewrite_tac ?where ~term () =
+ let rewrite_tac ?where ~term status =
+ rewrite ?where ~term ~direction:`Right status
in
- ProofEngineTypes.mk_tactic (rewrite_tac ~term)
+ ProofEngineTypes.mk_tactic (rewrite_tac ?where ~term)
-let rewrite_simpl_tac ~term =
- let rewrite_simpl_tac ~term status =
+let rewrite_simpl_tac ?where ~term () =
+ let rewrite_simpl_tac ?where ~term status =
ProofEngineTypes.apply_tactic
(Tacticals.then_
- ~start:(rewrite_tac ~term)
+ ~start:(rewrite_tac ?where ~term ())
~continuation:
- (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
+ (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern))
status
in
ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
;;
-let rewrite_back_tac ~term =
- let rewrite_back_tac ~term status =
- rewrite ~term ~direction:`Left status
+let rewrite_back_tac ?where ~term () =
+ let rewrite_back_tac ?where ~term status =
+ rewrite ?where ~term ~direction:`Left status
in
- ProofEngineTypes.mk_tactic (rewrite_back_tac ~term)
+ ProofEngineTypes.mk_tactic (rewrite_back_tac ?where ~term)
-let rewrite_back_simpl_tac ~term =
- let rewrite_back_simpl_tac ~term status =
+let rewrite_back_simpl_tac ?where ~term () =
+ let rewrite_back_simpl_tac ?where ~term status =
ProofEngineTypes.apply_tactic
(Tacticals.then_
- ~start:(rewrite_back_tac ~term)
+ ~start:(rewrite_back_tac ?where ~term ())
~continuation:
- (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
+ (ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern))
status
in
ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)
with_what]))
~continuations:[
- T.then_ ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
+ T.then_ ~start:(rewrite_simpl_tac ~term:(C.Rel 1) ())
~continuation:(
ProofEngineStructuralRules.clear
~hyp:(List.hd context)) ;
* http://cs.unibo.it/helm/.
*)
-val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_back_tac: term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_back_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic
-val replace_tac: what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
+val rewrite_tac:
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+val rewrite_simpl_tac:
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+val rewrite_back_tac:
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+val rewrite_back_simpl_tac:
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+
+val replace_tac:
+ what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
val reflexivity_tac: ProofEngineTypes.tactic
val symmetry_tac: ProofEngineTypes.tactic
let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
let (proof,goals) = apply_tactic
- (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)))
+ (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ())
((curi,metasenv',pbo,pty),goal)
in
let new_goals = fresh_meta::goals in
(Tacticals.thens
~start:(intros_tac ())
~continuations:
- [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None])
+ [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern])
;;
exception NotConvertible
(function (i,_,_) ->
not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
;;
+
+(** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
+let find_subterms ~eq ~wanted t =
+ let rec find wanted t =
+ if eq wanted t then
+ [t]
+ else
+ match t with
+ | Cic.Sort _
+ | Cic.Rel _ -> []
+ | Cic.Meta (_, ctx) ->
+ List.fold_left (
+ fun acc e ->
+ match e with
+ | None -> acc
+ | Some t -> find wanted t @ acc
+ ) [] ctx
+ | Cic.Lambda (_, t1, t2)
+ | Cic.Prod (_, t1, t2)
+ | Cic.LetIn (_, t1, t2) ->
+ find wanted t1 @ find (CicSubstitution.lift 1 wanted) t2
+ | Cic.Appl l ->
+ List.fold_left (fun acc t -> find wanted t @ acc) [] l
+ | Cic.Cast (t, ty) -> find wanted t @ find wanted ty
+ | Cic.Implicit _ -> assert false
+ | Cic.Const (_, esubst)
+ | Cic.Var (_, esubst)
+ | Cic.MutInd (_, _, esubst)
+ | Cic.MutConstruct (_, _, _, esubst) ->
+ List.fold_left (fun acc (_, t) -> find wanted t @ acc) [] esubst
+ | Cic.MutCase (_, _, outty, indterm, patterns) ->
+ find wanted outty @ find wanted indterm @
+ List.fold_left (fun acc p -> find wanted p @ acc) [] patterns
+ | Cic.Fix (_, funl) ->
+ List.fold_left (
+ fun acc (_, _, ty, bo) -> find wanted ty @ find wanted bo @ acc
+ ) [] funl
+ | Cic.CoFix (_, funl) ->
+ List.fold_left (
+ fun acc (_, ty, bo) -> find wanted ty @ find wanted bo @ acc
+ ) [] funl
+ in
+ find wanted t
oldmetasenv *)
val compare_metasenvs :
oldmetasenv:Cic.metasenv -> newmetasenv:Cic.metasenv -> int list
+
+(** Finds the _pointers_ to subterms that are alpha-equivalent to wanted in t.
+ * wanted is properly lifted when binders are crossed *)
+val find_subterms :
+ eq:(Cic.term -> Cic.term -> bool) ->
+ wanted:Cic.term -> Cic.term ->
+ Cic.term list
+
(** creates an opaque tactic from a status->proof*goal list function *)
let mk_tactic t = t
+type pattern = (string * Cic.term) list * Cic.term option
+let goal_pattern = [],None
+
(** tactic failure *)
exception Fail of string
type tactic
val mk_tactic: (status -> proof * goal list) -> tactic
+(** the type of a tactic application domain
+ * [ hypothesis_name * path ] * goal_path
+ *)
+type pattern = (string * Cic.term) list * Cic.term option
+
+(** the pattern for the whole goal *)
+val goal_pattern : pattern
+
(** tactic failure *)
exception Fail of string
*)
(* The default of term is the thesis of the goal to be prooved *)
-let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let terms =
- match terms with None -> [ty] | Some l -> l
- in
+let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* We don't know if [term] is a subterm of [ty] or a subterm of *)
(* the type of one metavariable. So we replace it everywhere. *)
(*CSC: Il vero problema e' che non sapendo dove sia il term non *)
(*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *)
(*CSC: e' meglio prima cercare il termine e scoprirne il *)
(*CSC: contesto, poi ridurre e infine rimpiazzare. *)
- let replace context where=
-(*CSC: Per il momento se la riduzione fallisce significa solamente che *)
-(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
-(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
- try
- let terms' = List.map (reduction context) terms in
- ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
- ~where:where
- with
- _ -> where
- in
- let ty' = replace context ty in
- let context' =
- if also_in_hypotheses then
- List.fold_right
- (fun entry context ->
- match entry with
- Some (name,Cic.Def (t,None)) ->
- (Some (name,Cic.Def ((replace context t),None)))::context
- | Some (name,Cic.Decl t) ->
- (Some (name,Cic.Decl (replace context t)))::context
- | None -> None::context
- | Some (_,Cic.Def (_,Some _)) -> assert false
- ) context []
- else
- context
- in
- let metasenv' =
- List.map
- (function
- (n,_,_) when n = metano -> (metano,context',ty')
- | _ as t -> t
- ) metasenv
- in
- (curi,metasenv',pbo,pty), [metano]
+ let replace context where terms =
+ (*CSC: Per il momento se la riduzione fallisce significa solamente che *)
+ (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
+ (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
+ try
+ let terms' = List.map (reduction context) terms in
+ ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+ ~where:where
+ with
+ _ -> where
+ in
+ let find_pattern_for name =
+ try Some (snd(List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
+ with Not_found -> None
+ in
+ let ty' =
+ match goal_pattern with
+ | None -> replace context ty [ty]
+ | Some pat ->
+ let terms = CicUtil.select ~term:ty ~context:pat in
+ let terms = List.map snd terms in
+ replace context ty terms
+ in
+ let context' =
+ if hyp_patterns <> [] then
+ List.fold_right
+ (fun entry context ->
+ match entry with
+ | Some (name,Cic.Decl term) ->
+ (match find_pattern_for name with
+ | None -> entry::context
+ | Some pat ->
+ let terms = CicUtil.select ~term ~context:pat in
+ let terms = List.map snd terms in
+ let where = replace context term terms in
+ let entry = Some (name,Cic.Decl where) in
+ entry::context)
+ | Some (name,Cic.Def (term, None)) ->
+ (match find_pattern_for name with
+ | None -> entry::context
+ | Some pat ->
+ let terms = CicUtil.select ~term ~context:pat in
+ let terms = List.map snd terms in
+ let where = replace context term terms in
+ let entry = Some (name,Cic.Def (where,None)) in
+ entry::context)
+ | _ -> entry::context
+ ) context []
+ else
+ context
+ in
+ let metasenv' =
+ List.map (function
+ | (n,_,_) when n = metano -> (metano,context',ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ (curi,metasenv',pbo,pty), [metano]
;;
-let simpl_tac ~also_in_hypotheses ~terms =
- mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.simpl
- ~also_in_hypotheses ~terms);;
+let simpl_tac ~pattern =
+ mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
-let reduce_tac ~also_in_hypotheses ~terms =
- mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.reduce
- ~also_in_hypotheses ~terms);;
+let reduce_tac ~pattern =
+ mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
-let whd_tac ~also_in_hypotheses ~terms =
- mk_tactic ( reduction_tac ~reduction:CicReduction.whd
- ~also_in_hypotheses ~terms);;
+let whd_tac ~pattern =
+ mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
-let normalize_tac ~also_in_hypotheses ~terms =
- mk_tactic ( reduction_tac ~reduction:CicReduction.normalize
- ~also_in_hypotheses ~terms);;
+let normalize_tac ~pattern =
+ mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );;
let fold_tac ~reduction ~also_in_hypotheses ~term =
let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
*)
(* The default of term is the thesis of the goal to be prooved *)
-val simpl_tac:
- also_in_hypotheses:bool -> terms:(Cic.term list option) ->
- ProofEngineTypes.tactic
-val reduce_tac:
- also_in_hypotheses:bool -> terms:(Cic.term list option) ->
- ProofEngineTypes.tactic
-val whd_tac:
- also_in_hypotheses:bool -> terms:(Cic.term list option) ->
- ProofEngineTypes.tactic
-val normalize_tac:
- also_in_hypotheses:bool -> terms:(Cic.term list option) ->
- ProofEngineTypes.tactic
+val simpl_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val fold_tac:
reduction:(Cic.context -> Cic.term -> Cic.term) ->
let decide_equality = DiscriminationTactics.decide_equality_tac
let decompose = EliminationTactics.decompose_tac
let discriminate = DiscriminationTactics.discriminate_tac
-let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac
let elim_intros = PrimitiveTactics.elim_intros_tac
+let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac
let elim_type = EliminationTactics.elim_type_tac
let exact = PrimitiveTactics.exact_tac
let exists = IntroductionTactics.exists_tac
let fold = ReductionTactics.fold_tac
let fourier = FourierR.fourier_tac
+let fwd_simpl = FwdSimplTactic.fwd_simpl_tac
let generalize = VariousTactics.generalize_tac
-let set_goal = VariousTactics.set_goal
let injection = DiscriminationTactics.injection_tac
let intros = PrimitiveTactics.intros_tac
+let lapply = FwdSimplTactic.lapply_tac
let left = IntroductionTactics.left_tac
let letin = PrimitiveTactics.letin_tac
+let normalize = ReductionTactics.normalize_tac
let reduce = ReductionTactics.reduce_tac
let reflexivity = EqualityTactics.reflexivity_tac
let replace = EqualityTactics.replace_tac
+let rewrite = EqualityTactics.rewrite_tac
let rewrite_back = EqualityTactics.rewrite_back_tac
let rewrite_back_simpl = EqualityTactics.rewrite_back_simpl_tac
-let rewrite = EqualityTactics.rewrite_tac
let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
let right = IntroductionTactics.right_tac
let ring = Ring.ring_tac
+let set_goal = VariousTactics.set_goal
let simpl = ReductionTactics.simpl_tac
let split = IntroductionTactics.split_tac
let symmetry = EqualityTactics.symmetry_tac
let transitivity = EqualityTactics.transitivity_tac
let whd = ReductionTactics.whd_tac
-let normalize = ReductionTactics.normalize_tac
-let fwd_simpl = FwdSimplTactic.fwd_simpl_tac
-let lapply = FwdSimplTactic.lapply_tac
val letin :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
Cic.term -> ProofEngineTypes.tactic
-val reduce :
- also_in_hypotheses:bool ->
- terms:Cic.term list option -> ProofEngineTypes.tactic
+val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val reflexivity : ProofEngineTypes.tactic
val replace : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
-val rewrite_back : term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_back_simpl : term:Cic.term -> ProofEngineTypes.tactic
-val rewrite : term:Cic.term -> ProofEngineTypes.tactic
-val rewrite_simpl : term:Cic.term -> ProofEngineTypes.tactic
+val rewrite_back :
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+val rewrite_back_simpl :
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+val rewrite :
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
+val rewrite_simpl :
+ ?where:ProofEngineTypes.pattern ->
+ term:Cic.term -> unit -> ProofEngineTypes.tactic
val right : ProofEngineTypes.tactic
val ring : ProofEngineTypes.tactic
-val simpl :
- also_in_hypotheses:bool ->
- terms:Cic.term list option -> ProofEngineTypes.tactic
+val simpl : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val split : ProofEngineTypes.tactic
val symmetry : ProofEngineTypes.tactic
val transitivity : term:Cic.term -> ProofEngineTypes.tactic
-val whd :
- also_in_hypotheses:bool ->
- terms:Cic.term list option -> ProofEngineTypes.tactic
-val normalize :
- also_in_hypotheses:bool ->
- terms:Cic.term list option -> ProofEngineTypes.tactic
+val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
+val normalize : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic
val fwd_simpl : hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
val lapply :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
projects / helm.git / commitdiff