| Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
| Clear of loc * 'ident list
| ClearBody of loc * 'ident
- | Compose of loc * 'term * 'term * 'ident intros_spec
+ | Compose of loc * 'term * 'term option * int * 'ident intros_spec
| Constructor of loc * int
| Contradiction of loc
| Cut of loc * 'ident option * 'term
| Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)
| ClearBody (_,id) -> Printf.sprintf "clearbody %s" (pp_hyps [id])
| Constructor (_,n) -> "constructor " ^ string_of_int n
- | Compose (_,t1, t2, intro_specs) ->
- Printf.sprintf "compose %s %s%s" (term_pp t1) (term_pp t1)
+ | Compose (_,t1, t2, times, intro_specs) ->
+ Printf.sprintf "compose %s%s %s%s"
+ (if times > 0 then string_of_int times ^ " " else "")
+ (term_pp t1) (match t2 with None -> "" | Some t2 -> "with "^term_pp t2)
(pp_intros_specs " as " intro_specs)
| Contradiction _ -> "contradiction"
| Cut (_, ident, term) ->
Tactics.change ~pattern with_what
| GrafiteAst.Clear (_,id) -> Tactics.clear id
| GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
- | GrafiteAst.Compose (_,t1,t2,(howmany, names)) ->
- Tactics.compose t1 t2 ?howmany
+ | GrafiteAst.Compose (_,t1,t2,times,(howmany, names)) ->
+ Tactics.compose times t1 t2 ?howmany
~mk_fresh_name_callback:(namer_of names)
| GrafiteAst.Contradiction _ -> Tactics.contradiction
| GrafiteAst.Constructor (_, n) -> Tactics.constructor n
metasenv,GrafiteAst.Clear (loc,id)
| GrafiteAst.ClearBody (loc,id) ->
metasenv,GrafiteAst.ClearBody (loc,id)
- | GrafiteAst.Compose (loc, t1, t2, spec) ->
+ | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
let metasenv,t1 = disambiguate_term context metasenv t1 in
- let metasenv,t2 = disambiguate_term context metasenv t2 in
- metasenv, GrafiteAst.Compose (loc, t1, t2, spec)
+ let metasenv,t2 =
+ match t2 with
+ | None -> metasenv, None
+ | Some t2 ->
+ let m, t2 = disambiguate_term context metasenv t2 in
+ m, Some t2
+ in
+ metasenv, GrafiteAst.Compose (loc, t1, t2, times, spec)
| GrafiteAst.Constructor (loc,n) ->
metasenv,GrafiteAst.Constructor (loc,n)
| GrafiteAst.Contradiction loc ->
GrafiteAst.ClearBody (loc,id)
| IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Change (loc, what, t)
- | IDENT "compose"; t1 = tactic_term; t2 = tactic_term;
- specs = intros_spec ->
- GrafiteAst.Compose (loc, t1, t2, specs)
+ | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
+ OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
+ let times = match times with None -> 1 | Some i -> i in
+ GrafiteAst.Compose (loc, t1, t2, times, specs)
| IDENT "constructor"; n = int ->
GrafiteAst.Constructor (loc, n)
| IDENT "contradiction" ->
* both living in the same context and metasenv *)
let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
let module RT = RefinementTool in
+ let original_metasenv = metasenv in
let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
let rec mk_implicits = function
List.sort
(fun (i,ctx1,ty1) (j,ctx1,ty1) ->
try List.assoc i meta2no - List.assoc j meta2no
- with Not_found ->
- assert false)
+ with Not_found -> assert false)
body_metasenv
in
let namer l n =
let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
let term = CicMetaSubst.apply_subst subst term in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
let term, ty, metasenv, ugraph =
CicRefine.type_of_aux' metasenv context term ugraph
split_metasenv metasenv (spline_len + List.length context)
in
let term = purge_unused_lambdas lambdas_metasenv term in
+ let metasenv =
+ List.filter
+ (fun (i,_,_) ->
+ List.for_all
+ (fun (j,_,_) ->
+ i <> j || List.exists (fun (j,_,_) -> j=i) original_metasenv)
+ lambdas_metasenv)
+ metasenv
+ in
debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
term, metasenv, ugraph
* http://helm.cs.unibo.it/
*)
-let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 (proof, goal) =
+let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;;
+
+let compose_core t2 t1 (proof, goal) =
let _,metasenv,_subst,_,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let ty1,_ =
CicTypeChecker.type_of_aux' metasenv context t1 CicUniv.oblivion_ugraph
in
- let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 in
- let rec generate arity menv acc =
- if arity < 0 then acc, menv
- else
+ let ty2,_ =
+ CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph
+ in
+ let saturated_ty2, menv_for_saturated_ty2 =
+ let maxm = CicMkImplicit.new_meta metasenv [] in
+ let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in
+ ty2, menv
+ in
+ (* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
+ let unif menv t =
+ let m, menv2 =
+ let n = CicMkImplicit.new_meta menv [] in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ Cic.Meta (n,irl), ((n,context,t)::menv)
+ in
+ try
+ let _ =
+ CicUnification.fo_unif menv context t saturated_ty2
+ CicUniv.oblivion_ugraph
+ in
+ true, menv2, m
+ with
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ -> false, menv2, m
+ in
+ (* check which "positions" in the input arrow unifies with saturated_ty2 *)
+ let rec positions menv cur arity = function
+ | Cic.Prod (n,s,t) ->
+ let b, newmenv, sb = unif menv s in
+ if b then
+ (arity - cur - 1) ::
+ (positions newmenv (cur + 1) arity (CicSubstitution.subst sb t))
+ else
+ positions newmenv (cur + 1) arity (CicSubstitution.subst sb t)
+ | _ -> []
+ in
+ (* position is a list of arities, that is if t1 : a -> b -> c and arity is
+ * 0 then the computed term will be (t1 ? t2) of type a -> c
+ * if arity is 1 then (t1 t2 ?) of type b -> c *)
+ let rec generate positions menv acc =
+ match positions with
+ | [] -> acc, menv
+ | arity::tl ->
try
- let t, menv, _ =
- CloseCoercionGraph.generate_composite t1 t2 context menv
+ let t, menv1, _ =
+ CloseCoercionGraph.generate_composite t2 t1 context menv
CicUniv.oblivion_ugraph arity false
in
- generate (arity - 1) menv (t::acc)
+ assert (List.length menv1 = List.length menv);
+ generate tl menv (t::acc)
with
- | CloseCoercionGraph.UnableToCompose -> generate (arity - 1) menv acc
+ | CloseCoercionGraph.UnableToCompose -> generate tl menv acc
+ in
+ let terms, metasenv =
+ generate (positions menv_for_saturated_ty2 0 (count_pi ty1) ty1) metasenv []
in
- let terms, metasenv = generate (count_pi ty1) metasenv [] in
+ (* the new proof has the resulting metasenv (shouldn't it be the same?) *)
let proof =
let uri, _, _subst, bo, ty, attrs = proof in
uri, metasenv, _subst, bo, ty, attrs
in
+ (* now we have the terms, we generalize them and intros them *)
let proof, goal =
List.fold_left
(fun (proof,goal) t ->
proof,List.hd gl)
(proof,goal) terms
in
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
- (proof,goal)
+ (proof, goal), List.length terms
+;;
+
+let compose_tac ?howmany ?mk_fresh_name_callback n t1 t2 proofstatus =
+ let ((proof, goal), k), n =
+ match t2 with
+ | Some t2 -> compose_core t1 t2 proofstatus, n-1
+ | None ->
+ let k =
+ let proof, goal = proofstatus in
+ let _,metasenv,subst,_,_,_ = proof in
+ let _,_,ty = CicUtil.lookup_meta goal metasenv in
+ count_pi (CicMetaSubst.apply_subst subst ty)
+ in
+ (proofstatus, k), n
+ in
+ let (proof, goal), k =
+ (* fix iterates n times the composition *)
+ let rec fix proofstatus k t = function
+ | 0 -> proofstatus, k
+ | n ->
+ let t = CicSubstitution.lift k t in
+ let proof, gl =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.intros_tac
+ ~howmany:k ?mk_fresh_name_callback ()) proofstatus
+ in
+ assert (List.length gl = 1);
+ let goal = List.hd gl in
+ let k, proofstatus =
+ (* aux compose t with every previous result *)
+ let rec aux k proofstatus = function
+ | 0 -> k, proofstatus
+ | n ->
+ let (proof, goal), k1 =
+ compose_core t (Cic.Rel n) proofstatus
+ in
+ aux (k+k1) (proof, goal) (n-1)
+ in
+ aux 0 (proof, goal) k
+ in
+ fix proofstatus k t (n-1)
+ in
+ fix (proof, goal) k t1 n
+ in
+ let howmany =
+ match howmany with
+ | None -> None
+ | Some i ->
+ if i - k < 0 then (* we should generalize back and clear *) Some 0
+ else Some (i - k)
+ in
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
+ (proof,goal)
;;
-let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 =
+let compose_tac ?howmany ?mk_fresh_name_callback times t1 t2 =
ProofEngineTypes.mk_tactic
- (compose_tac ?howmany ?mk_fresh_name_callback t1 t2)
+ (compose_tac ?howmany ?mk_fresh_name_callback times t1 t2)
;;
val compose_tac:
?howmany:int ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- Cic.term -> Cic.term -> ProofEngineTypes.tactic
+ int (* times *) ->
+ Cic.term -> Cic.term option -> ProofEngineTypes.tactic
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jun 1 17:03:59 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Jun 4 13:44:18 CEST 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
val compose :
?howmany:int ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- Cic.term -> Cic.term -> ProofEngineTypes.tactic
+ int -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic
MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
$(CMOS) : $(LIB_DEPS)
$(CMXOS): $(LIBX_DEPS)
-ifeq ($(MAKECMDGOALS),opt)
- $(MLI:%.mli=%.cmi): $(LIBX_DEPS)
-else
- $(MLI:%.mli=%.cmi): $(LIB_DEPS)
-endif
LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES))
LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES))
$(H)echo " OCAMLDEP -native"
$(H)$(OCAMLDEP) -native *.ml *.mli > .depend.opt
-ifeq ($(MAKECMDGOALS),)
- include .depend
-endif
-
-ifeq ($(MAKECMDGOALS), all)
- include .depend
+# this should be sligtly better, since should work with 'make all opt'
+ifneq (,$(findstring all,$(MAKECMDGOALS)))
+ # if we 'make all opt' the deps for 'all' should be fine also for opt
+ # if we 'make opt all' it should not work...
+ TO_INCLUDE+=.depend
+ TO_DEPEND_ON=$(LIB_DEPS)
+else ifneq (,$(findstring opt,$(MAKECMDGOALS)))
+ TO_INCLUDE+=.depend.opt
+ TO_DEPEND_ON=$(LIBX_DEPS)
+else ifneq (,$(findstring world,$(MAKECMDGOALS)))
+ ifeq ($(HAVE_OCAMLOPT),yes)
+ TO_INCLUDE+=.depend.opt
+ TO_DEPEND_ON=$(LIBX_DEPS)
+ else
+ TO_INCLUDE+=.depend
+ TO_DEPEND_ON=$(LIB_DEPS)
+ endif
+else
+ TO_INCLUDE+=.depend
+ TO_DEPEND_ON=$(LIB_DEPS)
endif
-ifeq ($(MAKECMDGOALS), opt)
- include .depend.opt
-endif
+$(MLI:%.mli=%.cmi): $(TO_DEPEND_ON)
-ifeq ($(MAKECMDGOALS), world)
- include .depend.opt
-endif
+include $(TO_INCLUDE)
%.cmi: %.mli
$(H)echo " OCAMLC $<"
--- /dev/null
+set "baseuri" "cic:/matita/tests/compose/LCL002-1".
+include "logic/equality.ma".
+
+theorem an_1:
+∀ Univ:Set.
+∀ a:Univ.
+∀ is_a_theorem:Univ → Prop.
+∀ not:Univ → Univ.
+∀ or:Univ → Univ → Univ.
+∀ H0:∀ U:Univ.∀ V:Univ.∀ X:Univ.∀ Y:Univ.∀ Z:Univ.
+ is_a_theorem
+ (or (not (or (not (or (not X) Y)) (or Z (or U V))))
+ (or (not (or (not U) X)) (or Z (or V X)))).
+∀ H1:∀ X:Univ.∀ Y:Univ.
+ is_a_theorem (or (not X) Y) → is_a_theorem X → is_a_theorem Y.
+∀ ABS:∀ X.is_a_theorem X.
+True.
+.
+intros 5.
+intros (H H1 ABS).
+
+(* H1 o H *)
+compose (H) with (H1) (primo secondo).
+letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H ? ? ? ? ?));
+try assumption; [1,2: apply ABS]
+letin verifica_secondo ≝ (secondo ? ? ? ? ? ? ? = H1 ? ? (H ? ? ? ? ?) ?);
+try assumption; [1,2: apply ABS]
+clear verifica_primo verifica_secondo.
+compose (H) with (primo) (terzo).
+compose (H) with (secondo) (quarto).
+letin verifica_terzo_quarto ≝ (terzo ? ? ? ? ? = quarto ? ? ? ? ?);
+try assumption.
+clear verifica_terzo_quarto.
+clear primo secondo terzo quarto.
+
+(* H1 o H1 *)
+compose (H1) with (H1) (primo secondo).
+letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H1 ? ? ? ?));
+try assumption; [1,2,3,4,5,6: apply ABS]
+letin verifica_secondo ≝ (secondo ? ? ? ? ? ? = H1 ? ? (H1 ? ? ? ?) ?);
+try assumption; [1,2,3,4,5,6: apply ABS]
+clear verifica_primo verifica_secondo.
+clear primo secondo.
+
+(* close H1 o H1 with H *)
+compose H1 with H1 0.
+(*
+leaving the result under the sequent line and calling compose without
+the with parameter, will compose H with all the stuff under the sequent line
+*)
+compose 3 (H) (i1 i2 p1 p2 p3 p4 p5 p6 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12).
+exact I.
+qed.
projects / helm.git / commitdiff