let metasenv, ugraph = [], Un.default_ugraph in
let ety = H.get_type "elim_inferred_type" context using in
let _splits, args_no = PEH.split_with_whd (context, ety) in
- let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim
- ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no
+ let _metasenv, _subst, predicate, _arg, actual_args =
+ PT.mk_predicate_for_elim
+ ~context ~metasenv ~subst:[] ~ugraph ~goal ~arg ~using ~cpattern ~args_no
in
let ty = C.Appl (predicate :: actual_args) in
let upto = List.length actual_args in
gallina8Parser.cmi: types.cmx
grafiteParser.cmi: types.cmx
grafite.cmi: types.cmx
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
| _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
| _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
-and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
- ugraph
+and type_of_aux' ?(clean_dummy_dependent_types=true)
+ ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph
=
let rec type_of_aux subst metasenv context t ugraph =
let module C = Cic in
(* eat prods ends here! *)
let t',ty,subst',metasenv',ugraph1 =
- type_of_aux [] metasenv context t ugraph
+ type_of_aux subst metasenv context t ugraph
in
let substituted_t = CicMetaSubst.apply_subst subst' t' in
let substituted_ty = CicMetaSubst.apply_subst subst' ty in
else
substituted_metasenv
in
- (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
+ (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1)
+;;
+
+let type_of metasenv subst context t ug =
+ type_of_aux' metasenv subst context t ug
+;;
+
+let type_of_aux'
+ ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug
+=
+ let t,ty,m,s,ug =
+ type_of_aux' ?clean_dummy_dependent_types ?localization_tbl
+ metasenv [] context t ug
+ in
+ t,ty,m,ug
;;
let undebrujin uri typesno tys t =
Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph
+ (* this is the correct one and should be used by tactics to fold subst *)
+val type_of:
+ Cic.metasenv -> Cic.substitution ->
+ Cic.context -> Cic.term -> CicUniv.universe_graph ->
+ Cic.term * Cic.term * Cic.metasenv * Cic.substitution *CicUniv.universe_graph
+
(* typecheck metasenv uri obj graph *)
(* refines [obj] and returns the refined form of [obj], *)
(* the new metasenv and universe graph. *)
let after = ProofEngineTypes.goals_of_proof proof in
let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
let proof, opened_goals =
- let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in
+ let uri, metasenv_after_tactic, subst, t, ty, attrs = proof in
let reordered_metasenv, opened_goals =
reorder_metasenv
starting_metasenv
metasenv_after_refinement metasenv_after_tactic
opened goal always_opens_a_goal
in
- let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in
+ let proof' = uri, reordered_metasenv, [], t, ty, attrs in
proof', opened_goals
in
let incomplete_proof =
let term = CicUtil.term_of_uri uri in
let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
let tkeys = Universe.keys [] ty in
- let index_cmd =
- List.map
- (fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri))
- tkeys
+ let universe = automation_cache.AutomationCache.univ in
+ let universe, index_cmd =
+ List.fold_left
+ (fun (universe,acc) key ->
+ let cands = Universe.get_candidates universe key in
+ let tys =
+ List.map
+ (fun t ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph
+ in
+ ty)
+ cands
+ in
+ if List.for_all
+ (fun cty ->
+ not (fst(CicReduction.are_convertible [] ty cty
+ CicUniv.oblivion_ugraph))) tys
+ then
+ Universe.index universe key term,
+ GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri)::acc
+ else
+ universe, acc)
+ (universe,[]) tkeys
in
let is_equational = is_equational_fact ty in
let select_cmd =
else
[]
in
- let universe = automation_cache.AutomationCache.univ in
- let universe = Universe.index_term_and_unfolded_term universe [] term ty in
let automation_cache =
if is_equational then
AutomationCache.add_term_to_active automation_cache [] [] [] term None
| IDENT "timeout"
| IDENT "library"
| IDENT "type"
- | IDENT "steps"
| IDENT "all"
]
];
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
?dbd ~use_library ~use_context
automation_cache restricted_univ (proof, goal)
=
- let _, metasenv, _, _, _, _ = proof in
+ let _, metasenv, subst, _, _, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
+ let is_prop m s c t =
+ let ty,_ =
+ CicTypeChecker.type_of_aux' m ~subst:s c t CicUniv.oblivion_ugraph
+ in
+ let sort,_ =
+ CicTypeChecker.type_of_aux' m ~subst:s c ty CicUniv.oblivion_ugraph
+ in
+ match CicReduction.whd ~subst c sort with
+ | Cic.Sort Cic.Prop | Cic.Sort (Cic.CProp _) -> true
+ | _ -> false
+ in
if restricted_univ = [] then
let ct =
if use_context then find_context_theorems context metasenv else []
in
let cache = AutoCache.cache_empty in
let cache = cache_add_list cache context (ct@lt) in
- let tables =
- let env = metasenv, context, CicUniv.oblivion_ugraph in
- List.fold_left
- (fun (a,p,b) (t,ty) ->
- let mes = CicUtil.metas_of_term ty in
- Saturation.add_to_active b a p env ty t
- (List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv))
- automation_cache.AutomationCache.tables ct
+ let automation_cache, _ =
+ List.fold_left
+ (fun (c,maxmeta) (t,ty) ->
+ let head, metasenv, args, maxmeta =
+ TermUtil.saturate_term maxmeta metasenv context ty 0
+ in
+ if List.exists (is_prop metasenv subst context) args then
+ c,maxmeta
+ else
+ let st = if args = [] then t else Cic.Appl (t::args) in
+ AutomationCache.add_term_to_active
+ c metasenv [] context st (Some head), maxmeta)
+ (automation_cache,CicMkImplicit.new_meta metasenv subst) ct
in
-(* AutomationCache.pp_cache { automation_cache with AutomationCache.tables =
- * tables }; *)
- automation_cache.AutomationCache.univ, tables, cache
+(* AutomationCache.pp_cache automation_cache; *)
+ automation_cache.AutomationCache.univ,
+ automation_cache.AutomationCache.tables,
+ cache
else
let metasenv, t_ty, s_t_ty, _ =
List.fold_left
- (fun (metasenv,acc, sacc, maxmeta) t ->
+ (fun (metasenv as orig,acc, sacc, maxmeta) t ->
let ty, _ =
CicTypeChecker.type_of_aux'
metasenv ~subst:[] context t CicUniv.oblivion_ugraph
let head, metasenv, args, maxmeta =
TermUtil.saturate_term maxmeta metasenv context ty 0
in
- let st = if args = [] then t else Cic.Appl (t::args) in
- metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
- (metasenv, [],[], CicMkImplicit.new_meta metasenv []) restricted_univ
+ if List.exists (is_prop metasenv subst context) args then
+ orig, (t,ty)::acc, sacc, maxmeta
+ else
+ let st = if args = [] then t else Cic.Appl (t::args) in
+ metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
+ (metasenv, [],[], CicMkImplicit.new_meta metasenv subst) restricted_univ
in
let automation_cache = AutomationCache.empty () in
let automation_cache =
(active,passive,bag), cache
;;
-let find_context_equalities tables context proof (universe:Universe.universe) cache
+let find_context_equalities dbd tables context proof (universe:Universe.universe) cache
=
let module C = Cic in
let module S = CicSubstitution in
AutoTypes.skip_context = skip_context;
}
+
+let eq_of_goal = function
+ | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
+ uri
+ | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
+(* performs steps of rewrite with the universe, obtaining if possible
+ * a trivial goal *)
+let solve_rewrite ~automation_cache ~params:(univ,params) (proof,goal)=
+ let steps = int_of_string (string params "steps" "4") in
+ let use_context = bool params "use_context" true in
+ let universe, tables, cache =
+ init_cache_and_tables ~use_library:false ~use_context
+ automation_cache univ (proof,goal)
+ in
+ let actives, passives, bag = tables in
+ let pa,metasenv,subst,pb,pc,pd = proof in
+ let _,context,ty = CicUtil.lookup_meta goal metasenv in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ let context = CicMetaSubst.apply_subst_context subst context in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ let eq_uri = eq_of_goal ty in
+ let initgoal = [], metasenv, ty in
+ let table =
+ let equalities = (Saturation.list_of_passive passives) in
+ List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd actives) equalities
+ in
+ let env = metasenv,context,CicUniv.oblivion_ugraph in
+ debug_print (lazy ("demod to solve: " ^ CicPp.ppterm ty));
+ match Indexing.solve_demodulating bag env table initgoal steps with
+ | Some (bag, gproof, metasenv, sub_subst, proof) ->
+ let subst_candidates,extra_infos =
+ List.split
+ (HExtlib.filter_map
+ (fun (i,c,_) ->
+ if i <> goal && c = context then Some (i,(c,ty)) else None)
+ metasenv)
+ in
+ let proofterm,proto_subst =
+ let proof = Equality.add_subst sub_subst proof in
+ Equality.build_goal_proof
+ bag eq_uri gproof proof ty subst_candidates context metasenv
+ in
+ let proofterm = Subst.apply_subst sub_subst proofterm in
+ let extrasubst =
+ HExtlib.filter_map
+ (fun (i,((c,ty),t)) ->
+ match t with
+ | Cic.Meta (j,_) when i=j -> None
+ | _ -> Some (i,(c,t,ty)))
+ (List.combine subst_candidates
+ (List.combine extra_infos proto_subst))
+ in
+ let subst = subst @ extrasubst in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ let proofterm, _, metasenv,subst, _ =
+ CicRefine.type_of metasenv subst context proofterm
+ CicUniv.oblivion_ugraph
+ in
+ let status = (pa,metasenv,subst,pb,pc,pd), goal in
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm) status
+ | None ->
+ raise
+ (ProofEngineTypes.Fail (lazy
+ ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
+;;
+
+(* Demodulate thorem *)
+let open_type ty bo =
+ let rec open_type_aux context ty k args =
+ match ty with
+ | Cic.Prod (n,s,t) ->
+ let n' =
+ FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in
+ let entry = match n' with
+ | Cic.Name _ -> Some (n',(Cic.Decl s))
+ | Cic.Anonymous -> None
+ in
+ open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args)
+ | Cic.LetIn (n,s,sty,t) ->
+ let entry = Some (n,(Cic.Def (s,sty)))
+ in
+ open_type_aux (entry::context) t (k+1) args
+ | _ -> context, ty, args
+ in
+ let context, ty, args = open_type_aux [] ty 1 [] in
+ match args with
+ | [] -> context, ty, bo
+ | _ -> context, ty, Cic.Appl (bo::args)
+;;
+
+let rec close_type bo ty context =
+ match context with
+ | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty)
+ | Some (n,(Cic.Decl s))::tl ->
+ close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl
+ | Some (n,(Cic.Def (s,sty)))::tl ->
+ close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl
+ | _ -> assert false
+;;
+
+let is_subsumed univ context ty =
+ let candidates = Universe.get_candidates univ ty in
+ List.fold_left
+ (fun res cand ->
+ match res with
+ | Some found -> Some found
+ | None ->
+ try
+ let mk_irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable in
+ let metasenv = [(0,context,ty)] in
+ let fake_proof =
+ None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[]
+ in
+ let (_,metasenv,subst,_,_,_), open_goals =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:cand)
+ (fake_proof,0)
+ in
+ let prop_goals, other =
+ split_goals_in_prop metasenv subst open_goals
+ in
+ if prop_goals = [] then Some cand else None
+ with
+ | ProofEngineTypes.Fail s -> None
+ | CicUnification.Uncertain s -> None
+ ) None candidates
+;;
+
+let demodulate_theorem ~automation_cache uri =
+ let eq_uri =
+ match LibraryObjects.eq_URI () with
+ | Some (uri) -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
+ let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ let context,ty,bo =
+ match obj with
+ | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[]))
+ | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem"))
+ in
+ if CicUtil.is_closed ty then
+ raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction")));
+ let initgoal = [], [], ty in
+ (* compute the signature *)
+ let signature =
+ let ty_set = MetadataConstraints.constants_of ty in
+ let hyp_set = MetadataQuery.signature_of_hypothesis context [] in
+ let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in
+ MetadataQuery.close_with_types set [] context
+ in
+ (* retrieve equations from the universe universe *)
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
+ let equations =
+ retrieve_equations true signature universe AutoCache.cache_empty context []
+ in
+ debug_print
+ (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
+ let eqs_and_types =
+ HExtlib.filter_map
+ (fun t ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph
+ in
+ (* retrieve_equations could also return flexible terms *)
+ if is_an_equality ty then Some(t,ty)
+ else
+ try
+ let ty' = unfold context ty in
+ if is_an_equality ty' then Some(t,ty') else None
+ with ProofEngineTypes.Fail _ -> None)
+ equations
+ in
+ let bag = Equality.mk_equality_bag () in
+
+ let bag, units, _, newmeta =
+ partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types
+ in
+ let table =
+ List.fold_left
+ (fun tbl eq -> Indexing.index tbl eq)
+ Indexing.empty units
+ in
+ let changed,(newproof,newmetasenv, newty) =
+ Indexing.demod bag
+ ([],context,CicUniv.oblivion_ugraph) table initgoal in
+ if changed then
+ begin
+ let oldproof = Equality.Exact bo in
+ let proofterm,_ =
+ Equality.build_goal_proof (~contextualize:false) (~forward:true) bag
+ eq_uri newproof oldproof ty [] context newmetasenv
+ in
+ if newmetasenv <> [] then
+ raise (ProofEngineTypes.Fail (lazy ("metasenv not empty")))
+ else
+ begin
+ assert_proof_is_valid proofterm newmetasenv context newty;
+ match is_subsumed universe context newty with
+ | Some t -> raise
+ (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t)))
+ | None -> close_type proofterm newty context
+ end
+ end
+ else (* if newty = ty then *)
+ raise (ProofEngineTypes.Fail (lazy "no progress"))
+ (*else ProofEngineTypes.apply_tactic
+ (ReductionTactics.simpl_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
+;;
+
+
+(* NEW DEMODULATE *)
+let demodulate ~dbd ~automation_cache ~params:(univ, params) (proof,goal)=
+ let universe, tables, cache =
+ init_cache_and_tables
+ ~dbd ~use_library:false ~use_context:true
+ automation_cache univ (proof,goal)
+ in
+ let eq_uri =
+ match LibraryObjects.eq_URI () with
+ | Some (uri) -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
+ let active, passive, bag = tables in
+ let curi,metasenv,subst,pbo,pty, attrs = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let initgoal = [], metasenv, ty in
+ let equalities = (Saturation.list_of_passive passive) in
+ (* we demodulate using both actives passives *)
+ let env = metasenv,context,CicUniv.empty_ugraph in
+ debug_print (lazy ("PASSIVES:" ^ string_of_int(List.length equalities)));
+ List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
+ equalities;
+ let table =
+ List.fold_left
+ (fun tbl eq -> Indexing.index tbl eq)
+ (snd active) equalities
+ in
+ let changed,(newproof,newmetasenv, newty) =
+ (* Indexing.demodulation_goal bag *)
+ Indexing.demod bag
+ (metasenv,context,CicUniv.oblivion_ugraph) table initgoal
+ in
+ if changed then
+ begin
+ let maxm = CicMkImplicit.new_meta metasenv subst in
+ let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
+ let subst_candidates = List.map (fun (i,_,_) -> i) metasenv in
+ let subst_candidates = List.filter (fun x-> x <> goal) subst_candidates in
+ let proofterm, proto_subst =
+ Equality.build_goal_proof (~contextualize:false) bag
+ eq_uri newproof opengoal ty subst_candidates context metasenv
+ in
+ (* XXX understan what to do with proto subst *)
+ let metasenv = (maxm,context,newty)::metasenv in
+ let proofterm, _, metasenv, subst, _ =
+ CicRefine.type_of metasenv subst context proofterm
+ CicUniv.oblivion_ugraph
+ in
+ let extended_status = (curi,metasenv,subst,pbo,pty, attrs),goal in
+ let proof,gl =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm) extended_status
+ in
+ proof,maxm::gl
+ end
+ else
+ raise (ProofEngineTypes.Fail (lazy "no progress"))
+;;
+
+let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache =
+ ProofEngineTypes.mk_tactic
+ (fun status ->
+ let all = bool flags "all" false in
+ if all then
+ solve_rewrite ~params ~automation_cache status
+ else
+ demodulate ~dbd ~params ~automation_cache status)
+;;
(***************** applyS *******************)
let apply_smart_aux
- dbd flags automation_cache univ proof goal newmeta' metasenv'
- context term' ty termty goal_arity
+ dbd automation_cache params proof goal newmeta' metasenv' subst
+ context term' ty termty goal_arity
=
-(* let ppterm = ppterm context in *)
- let (consthead,newmetasenv,arguments,_) =
+ let consthead,newmetasenv,arguments,_ =
TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
let term'' =
- match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
+ match arguments with
+ | [] -> term'
+ | _ -> Cic.Appl (term'::arguments)
in
- let proof',oldmetasenv =
- let (puri,metasenv,_subst,pbo,pty, attrs) = proof in
- (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv
+ let consthead =
+ let rec aux t = function
+ | [] ->
+ let t = CicReduction.normalize ~delta:false context t in
+ (match t, ty with
+ | Cic.Appl (hd1::_), Cic.Appl (hd2::_) when hd1 <> hd2 ->
+ let t = ProofEngineReduction.unfold context t in
+ (match t with
+ | Cic.Appl (hd1'::_) when hd1' = hd2 -> t
+ | _ -> raise (ProofEngineTypes.Fail (lazy "incompatible head")))
+ | _ -> t)
+ | arg :: tl ->
+ match CicReduction.whd context t with
+ | Cic.Prod (_,_,tgt) ->
+ aux (CicSubstitution.subst arg tgt) tl
+ | _ -> assert false
+ in
+ aux termty arguments
in
let goal_for_paramod =
match LibraryObjects.eq_URI () with
| Some uri ->
- Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
+ Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Implicit (Some `Type); consthead; ty]
| None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
in
- let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
- let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
- let proof'' =
- let uri,_,_subst,p,ty, attrs = proof' in
- uri,metasenv_for_paramod,_subst,p,ty, attrs
- in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let proof''',goals =
- ProofEngineTypes.apply_tactic
- (EqualityTactics.rewrite_tac ~direction:`RightToLeft
- ~pattern:(ProofEngineTypes.conclusion_pattern None)
- (Cic.Meta(newmeta,irl)) [])
- (proof'',goal)
- in
- let goal = match goals with [g] -> g | _ -> assert false in
- let proof'''', _ =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac term'')
- (proof''',goal)
- in
- let universe, tables, cache =
- init_cache_and_tables ~dbd ~use_library:flags.use_library
- ~use_context:true automation_cache univ (proof'''',newmeta)
- in
- let active, passive, bag = tables in
- match
- Saturation.given_clause bag (proof'''',newmeta) active passive
- 20 10 flags.timeout
- with
- | None, _,_,_ ->
- raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
- | Some (_,proof''''',_), active,passive,bag ->
- proof''''',
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
-(*
- debug_print
- (lazy
- ("SUBSUMPTION SU: " ^ string_of_int newmeta ^ " " ^ ppterm goal_for_paramod));
- let res, maxmeta =
- Saturation.all_subsumed bag maxm (proof'''',newmeta) active passive
- in
- if res = [] then
- raise (ProofEngineTypes.Fail (lazy("BUM")))
- else let (_,proof''''',_) = List.hd res in
- proof''''',ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
+ try
+ let goal_for_paramod, _, newmetasenv, subst, _ =
+ CicRefine.type_of newmetasenv subst context goal_for_paramod
+ CicUniv.oblivion_ugraph
+ in
+ let newmeta = CicMkImplicit.new_meta newmetasenv subst in
+ let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
+ let proof'' =
+ let uri,_,_,p,ty, attrs = proof in
+ uri,metasenv_for_paramod,subst,p,ty, attrs
+ in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+(*
+ prerr_endline ("------ prima di rewrite su ------ " ^ string_of_int goal);
+ prerr_endline ("menv:\n"^CicMetaSubst.ppmetasenv [] metasenv_for_paramod);
+ prerr_endline ("subst:\n"^CicMetaSubst.ppsubst
+ ~metasenv:(metasenv_for_paramod)
+ subst);
*)
-;;
-let rec count_prods context ty =
- match CicReduction.whd context ty with
- Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
- | _ -> 0
+ let (proof''',goals) =
+ ProofEngineTypes.apply_tactic
+ (EqualityTactics.rewrite_tac ~direction:`RightToLeft
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ (Cic.Meta(newmeta,irl)) []) (proof'',goal)
+ in
+ let goal = match goals with [g] -> g | _ -> assert false in
+ let proof'''', _ =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac term'')
+ (proof''',goal)
+ in
+ let (_,m,_,_,_,_ as p),_ =
+ solve_rewrite ~params ~automation_cache (proof'''',newmeta)
+ in
+ let open_goals =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv' ~newmetasenv:m
+ in
+ p, open_goals
+ with
+ CicRefine.RefineFailure msg ->
+ raise (ProofEngineTypes.Fail msg)
+;;
let apply_smart
- ~dbd ~term ~subst ~automation_cache ~params:(univ,params) (proof, goal)
+ ~dbd ~term ~automation_cache ~params (proof, goal)
=
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
- let (_,metasenv,_subst,_,_, _) = proof in
+ let (_,metasenv,subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let flags = flags_of_params params ~for_applyS:true () in
let newmeta = CicMkImplicit.new_meta metasenv subst in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
in
let metasenv' = metasenv@newmetasenvfragment in
let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
+ CicTypeChecker.type_of_aux'
+ metasenv' ~subst context term' CicUniv.oblivion_ugraph
in
let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
- let goal_arity = count_prods context ty in
- let proof, gl, active, passive =
- apply_smart_aux dbd flags automation_cache univ proof goal
- newmeta' metasenv' context term' ty termty goal_arity
+ let goal_arity =
+ let rec count_prods context ty =
+ match CicReduction.whd ~subst context ty with
+ | Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+ in
+ count_prods context ty
in
- proof, gl, active, passive
+ apply_smart_aux dbd automation_cache params proof goal
+ newmeta' metasenv' subst context term' ty termty goal_arity
;;
-(****************** AUTO ********************)
-
-
-
-(*
-let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
-*)
-
-let calculate_timeout flags =
+let applyS_tac ~dbd ~term ~params ~automation_cache =
+ ProofEngineTypes.mk_tactic
+ (fun status ->
+ try
+ apply_smart ~dbd ~term ~params ~automation_cache status
+ with
+ | CicUnification.UnificationFailure msg
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ raise (ProofEngineTypes.Fail msg))
+;;
+
+
+(****************** AUTO ********************)
+
+let calculate_timeout flags =
if flags.timeout = 0. then
(debug_print (lazy "AUTO WITH NO TIMEOUT");
{flags with timeout = infinity})
let ensure_equational t =
if is_an_equational_goal t then true
else false
- (*
- let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
- raise (ProofEngineTypes.Fail (lazy msg))
- *)
in
(flags.use_paramod && is_an_equational_goal goalty) ||
(flags.use_only_paramod && ensure_equational goalty)
;;
-(*
-let cache_add_success sort cache k v =
- if sort = P then cache_add_success cache k v else cache_remove_underinspection
- cache k
-;;
-*)
type menv = Cic.metasenv
type subst = Cic.substitution
let cc,_,goalty = List.assoc goalno s in
(* XXX applicare la subst al contesto? *)
Some (cc, CicMetaSubst.apply_subst s goalty)
- with Not_found -> None
+ with Not_found ->
+ None
;;
let pp_status ctx status =
let close_failures (fl : fail list) (cache : cache) =
List.fold_left
(fun cache ((gno,depth,_),gty) ->
- debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
- cache_add_failure cache gty depth)
+ if CicUtil.is_meta_closed gty then
+ ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
+ cache_add_failure cache gty depth)
+ else
+ cache)
cache fl
;;
let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
;;
+
let equational_case
tables cache depth fake_proof goalno goalty subst context
flags
let goal_steps, saturation_steps, timeout =
max_int,max_int,flags.timeout
in
-
match
Saturation.given_clause bag status active passive
goal_steps saturation_steps timeout
end
else
begin
- debug_print
- (lazy
- ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
+ let params = ([],["use_context","false"]) in
+ let automation_cache = {
+ AutomationCache.tables = tables ;
+ AutomationCache.univ = Universe.empty; }
+ in
+ try
+ let ((_,metasenv,subst,_,_,_),open_goals) =
+ solve_rewrite ~params ~automation_cache
+ (fake_proof, goalno)
+ in
+ let proof = lazy (Cic.Meta (-1,[])) in
+ [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
+ with ProofEngineTypes.Fail _ -> [], tables, cache, flags
+(*
let res = Saturation.all_subsumed bag status active passive in
let res' =
List.map
res
in
res', (active,passive,bag), cache, flags
+*)
end
;;
-let try_candidate
+let sort_new_elems =
+ List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
+ let p1 = List.length (prop_only l1) in
+ let p2 = List.length (prop_only l2) in
+ if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
+;;
+
+
+let try_candidate dbd
goalty tables subst fake_proof goalno depth context cand
=
let ppterm = ppterm context in
try
let actives, passives, bag = tables in
- let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
- (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:(Equality.maxmeta bag) ~term:cand)
+ let (_,metasenv,subst,_,_,_), open_goals =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:cand)
(fake_proof,goalno)
in
- let tables = actives, passives, Equality.push_maxmeta bag maxmeta in
+ let tables = actives, passives,
+ Equality.push_maxmeta bag
+ (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
+ in
debug_print (lazy (" OK: " ^ ppterm cand));
let metasenv = CicRefine.pack_coercion_metasenv metasenv in
let open_goals = order_new_goals metasenv subst open_goals ppterm in
| CicUnification.Uncertain s -> None,tables
;;
-let sort_new_elems =
- List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
- List.length (prop_only l1) - List.length (prop_only l2))
+let applicative_case dbd
+ tables depth subst fake_proof goalno goalty metasenv context universe
+ cache flags
+=
+ let goalty_aux =
+ match goalty with
+ | Cic.Appl (hd::tl) ->
+ Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
+ | _ -> goalty
+ in
+ let candidates =
+ get_candidates flags.skip_trie_filtering universe cache goalty_aux
+ in
+ let tables, elems =
+ List.fold_left
+ (fun (tables,elems) cand ->
+ match
+ try_candidate dbd goalty
+ tables subst fake_proof goalno depth context cand
+ with
+ | None, tables -> tables, elems
+ | Some x, tables -> tables, x::elems)
+ (tables,[]) candidates
+ in
+ let elems = sort_new_elems elems in
+ elems, tables, cache
;;
-let applicative_case
+let try_smart_candidate dbd
+ goalty tables subst fake_proof goalno depth context cand
+=
+ let ppterm = ppterm context in
+ try
+ let params = ([],[]) in
+ let automation_cache = {
+ AutomationCache.tables = tables ;
+ AutomationCache.univ = Universe.empty; }
+ in
+ debug_print (lazy ("candidato per " ^ string_of_int goalno
+ ^ ": " ^ CicPp.ppterm cand));
+(*
+ let (_,metasenv,subst,_,_,_) = fake_proof in
+ prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
+ prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
+*)
+ let ((_,metasenv,subst,_,_,_),open_goals) =
+ apply_smart ~dbd ~term:cand ~params ~automation_cache
+ (fake_proof, goalno)
+ in
+ let metasenv = CicRefine.pack_coercion_metasenv metasenv in
+ let open_goals = order_new_goals metasenv subst open_goals ppterm in
+ let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
+ incr candidate_no;
+ Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
+ with
+ | ProofEngineTypes.Fail s -> None,tables
+ | CicUnification.Uncertain s -> None,tables
+;;
+
+let smart_applicative_case dbd
tables depth subst fake_proof goalno goalty metasenv context universe
cache flags
=
- let candidates = get_candidates flags.skip_trie_filtering universe cache goalty in
+ let signature = MetadataQuery.signature_of metasenv goalno in
+ let goalty_aux =
+ match goalty with
+ | Cic.Appl (hd::tl) ->
+ Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
+ | _ -> goalty
+ in
+ let smart_candidates =
+ get_candidates flags.skip_trie_filtering universe cache goalty_aux
+ in
+ let candidates =
+ get_candidates flags.skip_trie_filtering universe cache goalty
+ in
+ let smart_candidates =
+ List.filter
+ (fun x -> not(List.mem x candidates)) smart_candidates
+ in
+ let candidates = List.filter (only signature context metasenv) candidates in
+ let smart_candidates =
+ List.filter (only signature context metasenv) smart_candidates
+ in
+(*
+ let penalty cand depth =
+ if only signature context metasenv cand then depth else ((prerr_endline (
+ "penalizzo " ^ CicPp.ppterm cand));depth -1)
+ in
+*)
let tables, elems =
List.fold_left
(fun (tables,elems) cand ->
match
- try_candidate goalty
+ try_candidate dbd goalty
tables subst fake_proof goalno depth context cand
with
| None, tables -> tables, elems
| Some x, tables -> tables, x::elems)
(tables,[]) candidates
in
- let elems = sort_new_elems elems in
+ let tables, smart_elems =
+ List.fold_left
+ (fun (tables,elems) cand ->
+ match
+ try_smart_candidate dbd goalty
+ tables subst fake_proof goalno 1 context cand
+ with
+ | None, tables -> tables, elems
+ | Some x, tables -> tables, x::elems)
+ (tables,[]) smart_candidates
+ in
+ let elems = sort_new_elems (elems @ smart_elems) in
elems, tables, cache
;;
-let equational_and_applicative_case
+let equational_and_applicative_case dbd
universe flags m s g gty tables cache context
=
let goalno, depth, sort = g in
if flags.use_only_paramod then
[],tables, cache
else
- applicative_case
+ applicative_case dbd
tables depth s fake_proof goalno
gty m context universe cache flags
in
elems@more_elems, tables, cache, flags
else
let elems, tables, cache =
- applicative_case tables depth s fake_proof goalno
- gty m context universe cache flags
+ match LibraryObjects.eq_URI () with
+ | Some _ ->
+ smart_applicative_case dbd tables depth s fake_proof goalno
+ gty m context universe cache flags
+ | None ->
+ applicative_case dbd tables depth s fake_proof goalno
+ gty m context universe cache flags
in
elems, tables, cache, flags
;;
in
List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
;;
-let filter_prune_hint l =
+let filter_prune_hint c l =
let prune = !prune_hint in
prune_hint := []; (* possible race... *)
- if prune = [] then l
- else List.filter (condition_for_prune_hint prune) l
+ if prune = [] then c,l
+ else
+ cache_reset_underinspection c,
+ List.filter (condition_for_prune_hint prune) l
;;
-let auto_main tables context flags universe cache elems =
+let auto_main dbd tables context flags universe cache elems =
auto_context := context;
let rec aux tables flags cache (elems : status) =
-(* pp_status context elems; *)
+ pp_status context elems;
(* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
auto_status := elems;
check_pause ();
*)
- let elems = filter_prune_hint elems in
+ let cache, elems = filter_prune_hint cache elems in
match elems with
| (m, s, size, don, todo, fl)::orlist when !hint <> None ->
debug_print (lazy "skip");
CicPp.ppterm gty));
(* elems are possible computations for proving gty *)
let elems, tables, cache, flags =
- equational_and_applicative_case
+ equational_and_applicative_case dbd
universe flags m s g gty tables cache context
in
if elems = [] then
let
- auto_all_solutions tables universe cache context metasenv gl flags
+ auto_all_solutions dbd tables universe cache context metasenv gl flags
=
let goals = order_new_goals metasenv [] gl CicPp.ppterm in
let goals =
in
let elems = [metasenv,[],1,[],goals,[]] in
let rec aux tables solutions cache elems flags =
- match auto_main tables context flags universe cache elems with
+ match auto_main dbd tables context flags universe cache elems with
| Gaveup (tables,cache) ->
solutions,cache, tables
| Proved (metasenv,subst,others,tables,cache) ->
(******************* AUTO ***************)
-let auto flags metasenv tables universe cache context metasenv gl =
+let auto dbd flags metasenv tables universe cache context metasenv gl =
let initial_time = Unix.gettimeofday() in
let goals = order_new_goals metasenv [] gl CicPp.ppterm in
let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
let elems = [metasenv,[],1,[],goals,[]] in
- match auto_main tables context flags universe cache elems with
+ match auto_main dbd tables context flags universe cache elems with
| Proved (metasenv,subst,_, tables,cache) ->
debug_print(lazy
("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
None,cache
;;
-let applyS_tac ~dbd ~term ~params ~automation_cache =
- ProofEngineTypes.mk_tactic
- (fun status ->
- try
- let proof, gl,_,_ =
- apply_smart ~dbd ~term ~subst:[] ~params ~automation_cache status
- in
- proof, gl
- with
- | CicUnification.UnificationFailure msg
- | CicTypeChecker.TypeCheckerFailure msg ->
- raise (ProofEngineTypes.Fail msg))
-
let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
let flags = flags_of_params params () in
let use_library = flags.use_library in
~dbd ~use_library ~use_context:(not flags.skip_context)
automation_cache univ (proof, goal)
in
- let _,metasenv,_subst,_,_, _ = proof in
+ let _,metasenv,subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let tables,cache =
if flags.close_more then
close_more
tables context (proof, goal)
- auto_all_solutions universe cache
+ (auto_all_solutions dbd) universe cache
else tables,cache in
let initial_time = Unix.gettimeofday() in
- let (_,oldmetasenv,_subst,_,_, _) = proof in
+ let (_,oldmetasenv,_,_,_, _) = proof in
hint := None;
let elem =
- metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
+ metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
in
- match auto_main tables context flags universe cache [elem] with
+ match auto_main dbd tables context flags universe cache [elem] with
| Proved (metasenv,subst,_, tables,cache) ->
debug_print (lazy
("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
let auto_tac ~dbd ~params ~automation_cache =
ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~automation_cache);;
-let eq_of_goal = function
- | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
- uri
- | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
-;;
-
-(* performs steps of rewrite with the universe, obtaining if possible
- * a trivial goal *)
-let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal)=
- let steps = int_of_string (string params "steps" "1") in
- let use_context = bool params "use_context" true in
- let universe, tables, cache =
- init_cache_and_tables ~use_library:false ~use_context
- automation_cache univ (proof,goal)
- in
- let actives, passives, bag = tables in
- let pa,metasenv,_subst,pb,pc,pd = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let eq_uri = eq_of_goal ty in
- let initgoal = [], metasenv, ty in
- let table =
- let equalities = (Saturation.list_of_passive passives) in
- List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd actives) equalities
- in
- let env = metasenv,context,CicUniv.oblivion_ugraph in
- match Indexing.solve_demodulating bag env table initgoal steps with
- | Some (proof, metasenv, newty) ->
- let refl =
- match newty with
- | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
- Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
- | _ -> assert false
- in
- let proofterm,_ =
- Equality.build_goal_proof
- bag eq_uri proof refl newty [] context metasenv
- in
- let proofterm, _, metasenv, _ =
- CicRefine.type_of_aux' metasenv context proofterm
- CicUniv.oblivion_ugraph
- in
- let status = (pa,metasenv,_subst,pb,pc,pd), goal in
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm) status
- | None ->
- raise
- (ProofEngineTypes.Fail (lazy
- ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
-;;
-let solve_rewrite_tac ~params ~automation_cache () =
- ProofEngineTypes.mk_tactic (solve_rewrite_tac ~automation_cache ~params)
-;;
-
-(* Demodulate thorem *)
-let open_type ty bo =
- let rec open_type_aux context ty k args =
- match ty with
- | Cic.Prod (n,s,t) ->
- let n' =
- FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in
- let entry = match n' with
- | Cic.Name _ -> Some (n',(Cic.Decl s))
- | Cic.Anonymous -> None
- in
- open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args)
- | Cic.LetIn (n,s,sty,t) ->
- let entry = Some (n,(Cic.Def (s,sty)))
- in
- open_type_aux (entry::context) t (k+1) args
- | _ -> context, ty, args
- in
- let context, ty, args = open_type_aux [] ty 1 [] in
- match args with
- | [] -> context, ty, bo
- | _ -> context, ty, Cic.Appl (bo::args)
-;;
-
-let rec close_type bo ty context =
- match context with
- | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty)
- | Some (n,(Cic.Decl s))::tl ->
- close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl
- | Some (n,(Cic.Def (s,sty)))::tl ->
- close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl
- | _ -> assert false
-;;
-
-let is_subsumed univ context ty =
- let candidates = Universe.get_candidates univ ty in
- List.fold_left
- (fun res cand ->
- match res with
- | Some found -> Some found
- | None ->
- try
- let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in
- let metasenv = [(0,context,ty)] in
- let fake_proof = None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] in
- let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
- (PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0)
- in
- let prop_goals, other = split_goals_in_prop metasenv subst open_goals in
- if prop_goals = [] then Some cand else None
- with
- | ProofEngineTypes.Fail s -> None
- | CicUnification.Uncertain s -> None
- ) None candidates
-;;
-
-let demodulate_theorem ~automation_cache uri =
- let eq_uri =
- match LibraryObjects.eq_URI () with
- | Some (uri) -> uri
- | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
- let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- let context,ty,bo =
- match obj with
- | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[]))
- | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem"))
- in
- if CicUtil.is_closed ty then
- raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction")));
- let initgoal = [], [], ty in
- (* compute the signature *)
- let signature =
- let ty_set = MetadataConstraints.constants_of ty in
- let hyp_set = MetadataQuery.signature_of_hypothesis context [] in
- let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in
- MetadataQuery.close_with_types set [] context
- in
- (* retrieve equations from the universe universe *)
- (* XXX automation_cache *)
- let universe = automation_cache.AutomationCache.univ in
- let equations =
- retrieve_equations true signature universe AutoCache.cache_empty context []
- in
- debug_print
- (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
- let eqs_and_types =
- HExtlib.filter_map
- (fun t ->
- let ty,_ =
- CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph
- in
- (* retrieve_equations could also return flexible terms *)
- if is_an_equality ty then Some(t,ty)
- else
- try
- let ty' = unfold context ty in
- if is_an_equality ty' then Some(t,ty') else None
- with ProofEngineTypes.Fail _ -> None)
- equations
- in
- let bag = Equality.mk_equality_bag () in
-
- let bag, units, _, newmeta =
- partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types
- in
- let table =
- List.fold_left
- (fun tbl eq -> Indexing.index tbl eq)
- Indexing.empty units
- in
- let changed,(newproof,newmetasenv, newty) =
- Indexing.demod bag
- ([],context,CicUniv.oblivion_ugraph) table initgoal in
- if changed then
- begin
- let oldproof = Equality.Exact bo in
- let proofterm,_ =
- Equality.build_goal_proof (~contextualize:false) (~forward:true) bag
- eq_uri newproof oldproof ty [] context newmetasenv
- in
- if newmetasenv <> [] then
- raise (ProofEngineTypes.Fail (lazy ("metasenv not empty")))
- else
- begin
- assert_proof_is_valid proofterm newmetasenv context newty;
- match is_subsumed universe context newty with
- | Some t -> raise
- (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t)))
- | None -> close_type proofterm newty context
- end
- end
- else (* if newty = ty then *)
- raise (ProofEngineTypes.Fail (lazy "no progress"))
- (*else ProofEngineTypes.apply_tactic
- (ReductionTactics.simpl_tac
- ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
-;;
-
-
-(* NEW DEMODULATE *)
-let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)=
- let universe, tables, cache =
- init_cache_and_tables
- ~dbd ~use_library:false ~use_context:true
- automation_cache univ (proof,goal)
- in
- let eq_uri =
- match LibraryObjects.eq_URI () with
- | Some (uri) -> uri
- | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
- let active, passive, bag = tables in
- let curi,metasenv,_subst,pbo,pty, attrs = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let initgoal = [], metasenv, ty in
- let equalities = (Saturation.list_of_passive passive) in
- (* we demodulate using both actives passives *)
- let env = metasenv,context,CicUniv.empty_ugraph in
- debug_print (lazy ("PASSIVES:" ^ string_of_int(List.length equalities)));
- List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
- equalities;
- let table =
- List.fold_left
- (fun tbl eq -> Indexing.index tbl eq)
- (snd active) equalities
- in
- let changed,(newproof,newmetasenv, newty) =
- (* Indexing.demodulation_goal bag *)
- Indexing.demod bag
- (metasenv,context,CicUniv.oblivion_ugraph) table initgoal
- in
- if changed then
- begin
- let maxm = CicMkImplicit.new_meta metasenv [] in
- let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
- let proofterm,_ =
- Equality.build_goal_proof (~contextualize:false) bag
- eq_uri newproof opengoal ty [] context metasenv
- in
- let metasenv = (maxm,context,newty)::metasenv in
- let proofterm, _, metasenv, _ =
- CicRefine.type_of_aux' metasenv context proofterm
- CicUniv.oblivion_ugraph
- in
- let extended_status =
- (curi,metasenv,_subst,pbo,pty, attrs),goal in
- let (status,newgoals) =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm)
- extended_status in
- (status,maxm::newgoals)
- end
- else (* if newty = ty then *)
- raise (ProofEngineTypes.Fail (lazy "no progress"))
- (*else ProofEngineTypes.apply_tactic
- (ReductionTactics.simpl_tac
- ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
-;;
-
-let demodulate_tac ~dbd ~params ~automation_cache =
- ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);;
-
-let demodulate_tac ~dbd ~params:(_,flags as params) ~automation_cache =
- let all = bool flags "all" false in
- if all then
- solve_rewrite_tac ~params ~automation_cache ()
- else
- demodulate_tac ~dbd ~params ~automation_cache
-;;
-
let pp_proofterm = Equality.pp_proofterm;;
let revision = "$Revision$";;
UriManager.uri ->
Cic.term * Cic.term
-val solve_rewrite_tac:
- params:auto_params ->
- automation_cache:AutomationCache.cache ->
- unit -> ProofEngineTypes.tactic
-
type auto_status =
Cic.context *
(* or list: goalno, goaltype, grey, depth, candidates: (goalno, c) *)
let cache_clean (univ,oldcache) =
univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache
;;
+let cache_reset_underinspection (u,c) =
+ u,List.filter (function (_,UnderInspection) -> false | _ -> true) c
+;;
val cache_add_success: cache -> cache_key -> Cic.term -> cache
val cache_add_underinspection: cache -> cache_key -> int -> cache
val cache_remove_underinspection: cache -> cache_key -> cache
+val cache_reset_underinspection: cache -> cache
val cache_empty: cache
val cache_print: Cic.context -> cache -> string
val cache_size: cache -> int
Tactics.auto ~dbd ~params:(univ, params') ~automation_cache]
| `Term just -> Tactics.apply just
| `SolveWith term ->
- Tactics.solve_rewrite ~automation_cache
- ~params:([term],["steps","1"; "use_context","false"]) ()
+ Tactics.demodulate ~automation_cache ~dbd
+ ~params:([term],
+ ["all","1";"steps","1"; "use_context","false"])
| `Proof ->
Tacticals.id_tac
in
;;
let we_proceed_by_induction_on t pat =
- let pattern = None, [], Some pat in
+(* let pattern = None, [], Some pat in *)
Tactics.elim_intros ~depth:0 (*~pattern*) t
;;
module DTI = DoubleTypeInference
module HEL = HExtlib
-let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
- let _rewrite_tac status =
+let rec rewrite ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status=
assert (wanted = None); (* this should be checked syntactically *)
let proof,goal = status in
- let curi, metasenv, _subst, pbo, pty, attrs = proof in
+ let curi, metasenv, subst, pbo, pty, attrs = proof in
let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
match hyps_pat with
he::(_::_ as tl) ->
- PET.apply_tactic
+ PET.apply_tactic
(T.then_
- (rewrite_tac ~direction
- ~pattern:(None,[he],None) equality)
- (rewrite_tac ~direction ~pattern:(None,tl,concl_pat)
- (S.lift 1 equality))
+ (PET.mk_tactic (rewrite ~direction
+ ~pattern:(None,[he],None) equality))
+ (PET.mk_tactic (rewrite ~direction
+ ~pattern:(None,tl,concl_pat) (S.lift 1 equality)))
) status
| [_] as hyps_pat when concl_pat <> None ->
- PET.apply_tactic
+ PET.apply_tactic
(T.then_
- (rewrite_tac ~direction
- ~pattern:(None,hyps_pat,None) equality)
- (rewrite_tac ~direction ~pattern:(None,[],concl_pat)
- (S.lift 1 equality))
+ (PET.mk_tactic (rewrite ~direction
+ ~pattern:(None,hyps_pat,None) equality))
+ (PET.mk_tactic (rewrite ~direction
+ ~pattern:(None,[],concl_pat) (S.lift 1 equality)))
) status
| _ ->
let arg,dir2,tac,concl_pat,gty =
| _::_ -> assert false
in
let gsort,_ =
- CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in
+ CicTypeChecker.type_of_aux'
+ metasenv ~subst context gty CicUniv.oblivion_ugraph
+ in
let if_right_to_left do_not_change a b =
match direction with
| `RightToLeft -> if do_not_change then a else b
| `LeftToRight -> if do_not_change then b else a
in
let ty_eq,ugraph =
- CicTypeChecker.type_of_aux' metasenv context equality
+ CicTypeChecker.type_of_aux' metasenv ~subst context equality
CicUniv.oblivion_ugraph in
let (ty_eq,metasenv',arguments,fresh_meta) =
TermUtil.saturate_term
(* now we always do as if direction was `LeftToRight *)
let fresh_name =
FreshNamesGenerator.mk_fresh_name
- ~subst:[] metasenv' context C.Anonymous ~typ:ty in
+ ~subst metasenv' context C.Anonymous ~typ:ty in
let lifted_t1 = S.lift 1 t1x in
let lifted_gty = S.lift 1 gty in
let lifted_conjecture =
in
let subst,metasenv',ugraph,_,selected_terms_with_context =
ProofEngineHelpers.select
- ~metasenv:metasenv' ~ugraph ~conjecture:lifted_conjecture
+ ~metasenv:metasenv' ~subst ~ugraph ~conjecture:lifted_conjecture
~pattern:lifted_pattern in
let metasenv' = CicMetaSubst.apply_subst_metasenv subst metasenv' in
let what,with_what =
let metasenv',arg,newtyp =
match arg with
None ->
+ let fresh_meta = CicMkImplicit.new_meta metasenv' subst in
let gty' = S.subst t2 abstr_gty in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
in
try
let (proof',goals) =
- PET.apply_tactic
- (tac ~term:exact_proof newtyp) ((curi,metasenv',_subst,pbo,pty, attrs),goal)
+ PET.apply_tactic (tac ~term:exact_proof newtyp)
+ ((curi,metasenv',subst,pbo,pty, attrs),goal)
in
let goals =
goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
TC.TypeCheckerFailure m ->
let msg = lazy ("rewrite: "^ Lazy.force m) in
raise (PET.Fail msg)
- in
- PET.mk_tactic _rewrite_tac
+;;
let rewrite_tac ~direction ~pattern equality names =
let _, hyps_pat, _ = pattern in
let froms = List.map fst hyps_pat in
- let start = rewrite_tac ~direction ~pattern equality in
+ let start = PET.mk_tactic (rewrite ~direction ~pattern equality) in
let continuation = PESR.rename ~froms ~tos:names in
if names = [] then start else T.then_ ~start ~continuation
+;;
let rewrite_simpl_tac ~direction ~pattern equality names =
T.then_
(ReductionTactics.simpl_tac
~pattern:(ProofEngineTypes.conclusion_pattern None))
-
let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status =
let _wanted, hyps_pat, concl_pat = pattern in
let (proof, goal) = status in
- let uri,metasenv,_subst,pbo,pty, attrs = proof in
+ let uri,metasenv,subst,pbo,pty, attrs = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
assert (hyps_pat = []); (*CSC: not implemented yet *)
let eq_URI =
in
let context_len = List.length context in
let subst,metasenv,u,_,selected_terms_with_context =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
+ ProofEngineHelpers.select ~subst ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
let with_what, metasenv, u = with_what context metasenv u in
let with_what = CicMetaSubst.apply_subst subst with_what in
let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in
let pty = CicMetaSubst.apply_subst subst pty in
- let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
+ let status = (uri,metasenv,subst,pbo,pty, attrs),goal in
let ty_of_with_what,u =
CicTypeChecker.type_of_aux'
- metasenv context with_what CicUniv.oblivion_ugraph in
+ metasenv ~subst context with_what CicUniv.oblivion_ugraph in
let whats =
match selected_terms_with_context with
[] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected"))
raise (ProofEngineTypes.Fail
(lazy "Replace: one of the selected terms is not closed")) in
let ty_of_t_in_context,u = (* TASSI: FIXME *)
- CicTypeChecker.type_of_aux' metasenv context t_in_context
+ CicTypeChecker.type_of_aux' metasenv ~subst context t_in_context
CicUniv.oblivion_ugraph in
- let b,u = CicReduction.are_convertible ~metasenv context
+ let b,u = CicReduction.are_convertible ~metasenv ~subst context
ty_of_with_what ty_of_t_in_context u in
if b then
let concl_pat_for_t = ProofEngineHelpers.pattern_of ~term:ty [t] in
~continuations:[
T.then_
~start:(
- rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1) [])
+ rewrite_tac
+ ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1) [])
~continuation:(
T.then_
~start:(
ProofEngineTypes.mk_tactic
(function ((proof,goal) as status) ->
- let _,metasenv,_subst,_,_, _ = proof in
+ let _,metasenv,_,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let hyps =
try
let symmetry_tac =
let symmetry_tac (proof, goal) =
- let (_,metasenv,_subst,_,_, _) = proof in
+ let (_,metasenv,_,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
when LibraryObjects.is_eq_URI uri ->
ProofEngineTypes.apply_tactic
(PrimitiveTactics.apply_tac
- ~term: (C.Const (LibraryObjects.sym_eq_URI uri, [])))
+ ~term:(C.Const (LibraryObjects.sym_eq_URI uri, [])))
(proof,goal)
| _ -> raise (ProofEngineTypes.Fail (lazy "Symmetry failed"))
let transitivity_tac ~term =
let transitivity_tac ~term status =
let (proof, goal) = status in
- let (_,metasenv,_subst,_,_, _) = proof in
+ let (_,metasenv,_,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
let fix_metas_goal (id_to_eq,newmeta) goal =
let (proof, menv, ty) = goal in
- let to_be_relocated =
- HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty))
- in
+ let to_be_relocated = List.map (fun i ,_,_ -> i) menv in
let subst, menv, newmeta = relocate newmeta menv to_be_relocated in
let ty = Subst.apply_subst subst ty in
let proof =
;;
let unification_all x y z =
- prerr_endline "unification_all"; subsumption_aux_all true x y z
+ subsumption_aux_all true x y z
;;
let rec demodulation_aux bag ?from ?(typecheck=false)
| None -> do_right ()
;;
-type next = L | R
-type solved = Yes of Equality.goal | No of Equality.goal list
-
(* returns all the 1 step demodulations *)
module C = Cic;;
module S = CicSubstitution;;
let termty, ugraph = C.Implicit None, ugraph in
let res =
find_all_matches
- metasenv context ugraph lift_amount term termty candidates
+ ~unif_fun:Founif.matching
+ metasenv context ugraph lift_amount term termty candidates
in
match term with
| C.Appl l ->
(res, [], List.map (S.lift 1) l) l
in
res
- | C.Prod (nn, s, t)
- | C.Lambda (nn, s, t) ->
- let context = (Some (nn, C.Decl s))::context in
- let mk s t =
- match term with
- | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
- in
- res @
- List.map
- (fun (rel, subst, m, ug, c) ->
- mk (S.lift 1 s) rel, subst, m, ug, c)
- (demodulation_all_aux
- metasenv context ugraph table (lift_amount+1) t)
- (* we could demodulate also in s, but then t may be badly
- * typed... *)
| t -> res
;;
-let solve_demodulating bag env table initgoal steps =
+let demod_all steps bag env table goal =
let _, context, ugraph = env in
- let solved goal res side =
- let newg = build_newgoal bag context goal side Equality.Demodulation res in
- match newg with
- | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right])
- when LibraryObjects.is_eq_URI uri ->
- (try
- let _ =
- Founif.unification [] m context left right CicUniv.empty_ugraph
- in
- Yes newg
- with CicUnification.UnificationFailure _ -> No [newg])
- | _ -> No [newg]
+ let is_visited l (_,_,t) =
+ List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
in
- let solved goal res_list side =
- let newg = List.map (fun x -> solved goal x side) res_list in
- try
- List.find (function Yes _ -> true | _ -> false) newg
- with Not_found ->
- No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
+ let rec aux steps visited bag = function
+ | _ when steps = 0 -> visited, bag, []
+ | [] -> visited, bag, []
+ | goal :: rest when is_visited visited goal -> aux steps visited bag rest
+ | goal :: rest ->
+ let visited = goal :: visited in
+ let _,menv,t = goal in
+ let res = demodulation_all_aux menv context ugraph table 0 t in
+ let steps = if res = [] then steps-1 else steps in
+ let new_goals =
+ List.map (build_newg bag context goal Equality.Demodulation) res
+ in
+ (* we need this cause an equation E like
+ F ?x => F ?y
+ can add a meta for y in a goal without instantiating it
+ P (F true) ----> P (F ?y)
+ and this may cause duplicated in metasenvs
+ demodulating again with E
+ *)
+ let bag, new_goals =
+ List.fold_right
+ (fun g (bag,acc) ->
+ let bag, g = Equality.fix_metas_goal bag g in
+ bag, g::acc)
+ new_goals (bag,[])
+ in
+ let visited, bag, res = aux steps visited bag (new_goals @ rest) in
+ visited, bag, goal :: res
in
- let rec first f acc l =
- match l with
- | [] -> acc,None
- | x::tl ->
- match f acc x with
- | acc,None -> first f acc tl
- | acc,Some x as ok -> ok
+ aux steps [] bag [goal]
+;;
+
+
+let solve_demodulating bag env table initgoal steps =
+ let proof,menv,eq,ty,left,right = open_goal initgoal in
+ let uri =
+ match eq with
+ | Cic.MutInd (u,_,_) -> u
+ | _ -> assert false
in
- let rec aux steps next visited goal =
- if steps = 0 then visited, None else
- let goalproof,menv,_,_,left,right = open_goal goal in
- if (List.mem (left,right,next) visited || List.mem (right,left,next) visited)
- then visited, None else
- let do_step t =
- demodulation_all_aux menv context ugraph table 0 t
+ let _, context, ugraph = env in
+ let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
+ let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
+ let is_solved left right ml mr =
+ let m = ml @ (List.filter
+ (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)
in
- let visited = (left,right,next) :: visited in
- match next with
- | L ->
- (match do_step left with
- | _::_ as res ->
- (match solved goal res Utils.Right with
- | No newgoals ->
- (match first (aux (steps - 1) L) visited newgoals with
- | _,Some g as success -> success
- | visited,None -> aux steps R visited goal)
- | Yes newgoal -> visited, Some newgoal)
- | [] -> aux steps R visited goal)
- | R ->
- (match do_step right with
- | _::_ as res ->
- (match solved goal res Utils.Left with
- | No newgoals ->
- (match first (aux (steps - 1) L) visited newgoals with
- | visited, Some g as success -> success
- | visited, None as failure -> failure)
- | Yes newgoal -> visited, Some newgoal)
- | [] -> visited, None)
+ try
+ let s,_,_ =
+ Founif.unification [] m context left right CicUniv.empty_ugraph in
+ Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
+ with CicUnification.UnificationFailure _ ->
+ let solutions =
+ unification_all env table (Equality.mk_tmp_equality
+ (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
+ in
+ if solutions = [] then None
+ else
+ let s, e, swapped = List.hd solutions in
+ let _,p,(ty,l,r,_),me,id = Equality.open_equality e in
+ let bag, p =
+ if swapped then Equality.symmetric bag ty l id uri me else bag, p
+ in
+ Some (bag, m,s, p)
in
- let _, res = aux steps L [] initgoal in
- res
+ let newgoal =
+ HExtlib.list_findopt
+ (fun (pr,mr,r) _ ->
+ try
+ let pl,ml,l,bag,m,s,p =
+ match
+ HExtlib.list_findopt (fun (pl,ml,l) _ ->
+ match is_solved l r ml mr with
+ | None -> None
+ | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
+ ) l_demod
+ with Some x -> x | _ -> raise Not_found
+ in
+ let pl =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pl
+ in
+ let pr =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pr
+ in
+ Some (bag,pr@pl@proof,m,s,p)
+ with Not_found -> None)
+ r_demod
+ in
+ newgoal
;;
-let get_stats () = "" ;;
+
+
Index.t ->
Equality.goal ->
int ->
- Equality.goal option
+ (Equality.equality_bag * Equality.goal_proof * Cic.metasenv *
+ Subst.substitution * Equality.proof) option
-
- (** profiling *)
-val get_stats: unit -> string
bag, p
in
bag, Some (goalproof, p, id, subst, cicmenv)
- | None -> bag, None)
+ | None ->
+ bag, None)
| _ -> bag, None
;;
| [] -> bag, (active_goals, [])
| hd::tl ->
let changed, selected = simplify_goal bag env hd active in
- let (_,_,t1) = selected in
+ let (_,m1,t1) = selected in
let already_in =
List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
active_goals
in
subst,newmetasenv',t
-let rec count_prods context ty =
- match CicReduction.whd context ty with
- Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+let rec count_prods subst context ty =
+ match CicReduction.whd ~subst context ty with
+ Cic.Prod (n,s,t) -> 1 + count_prods subst (Some (n,Cic.Decl s)::context) t
| _ -> 0
-let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
+let apply_with_subst ~term ~maxmeta (proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
- let (_,metasenv,_subst,_,_, _) = proof in
+ let (_,metasenv,subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
in
let metasenv' = metasenv@newmetasenvfragment in
let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
+ CicTypeChecker.type_of_aux'
+ metasenv' ~subst context term' CicUniv.oblivion_ugraph
in
let termty =
CicSubstitution.subst_vars exp_named_subst_diff termty in
- let goal_arity = count_prods context ty in
+ let goal_arity = count_prods subst context ty in
let subst,newmetasenv',t =
let rec add_one_argument n =
try
newmetasenv''
in
let subst = ((metano,(context,bo',ty))::subst) in
+ let newproof =
+ let u,m,_,p,t,l = newproof in
+ u,m,subst,p,t,l
+ in
subst,
(newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
(* ALB *)
let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
try
-(* apply_tac_verbose ~term status *)
- apply_with_subst ~term ~subst ~maxmeta status
- (* TODO cacciare anche altre eccezioni? *)
+ let status =
+ if subst <> [] then
+ let (u,m,_,p,t,l), g = status in (u,m,subst,p,t,l), g
+ else status
+ in
+ apply_with_subst ~term ~maxmeta status
with
| CicUnification.UnificationFailure msg
| CicTypeChecker.TypeCheckerFailure msg -> raise (PET.Fail msg)
if n <= 0 then [] else f n :: args_init (pred n) f
let mk_predicate_for_elim
- ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no =
+ ~context ~metasenv ~subst ~ugraph ~goal ~arg ~using ~cpattern ~args_no
+=
let instantiated_eliminator =
let f n = if n = 1 then arg else C.Implicit None in
C.Appl (using :: args_init args_no f)
| _ -> assert false
in
(* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *)
- let rec mk_pred metasenv context' pred arg' cpattern' = function
- | [] -> metasenv, pred, arg'
+ let rec mk_pred metasenv subst context' pred arg' cpattern' = function
+ | [] -> metasenv, subst, pred, arg'
| arg :: tail ->
(* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
- let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in
- let argty = CicReduction.whd context argty in
+ let argty, _ = TC.type_of_aux' metasenv ~subst context arg ugraph in
+ let argty = CicReduction.whd ~subst context argty in
let fresh_name =
FreshNamesGenerator.mk_fresh_name
- ~subst:[] metasenv context' C.Anonymous ~typ:argty in
+ ~subst metasenv context' C.Anonymous ~typ:argty in
let hyp = Some (fresh_name, C.Decl argty) in
let lazy_term c m u =
let distance = List.length c - List.length context in
S.lift distance arg, m, u in
let pattern = Some lazy_term, [], Some cpattern' in
let subst, metasenv, _ugraph, _conjecture, selected_terms =
- ProofEngineHelpers.select ~metasenv ~ugraph
+ ProofEngineHelpers.select ~subst ~metasenv ~ugraph
~conjecture:(0, context, pred) ~pattern in
let metasenv = MS.apply_subst_metasenv subst metasenv in
let map (_context_of_t, t) l = t :: l in
let pred = MS.apply_subst subst pred in
let pred = C.Lambda (fresh_name, argty, pred) in
let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in
- mk_pred metasenv (hyp :: context') pred arg' cpattern' tail
+ mk_pred metasenv subst (hyp :: context') pred arg' cpattern' tail
in
- let metasenv, pred, arg =
- mk_pred metasenv context goal arg cpattern (List.rev actual_args)
+ let metasenv, subst, pred, arg =
+ mk_pred metasenv subst context goal arg cpattern (List.rev actual_args)
in
HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args));
- metasenv, pred, arg, actual_args
+ metasenv, subst, pred, arg, actual_args
let beta_after_elim_tac upto predicate =
let beta_after_elim_tac status =
let (proof, goal) = status in
let module C = Cic in
let module T = Tacticals in
- let uri,metasenv,_subst,pbo,pty, attrs = proof in
+ let uri,metasenv,subst,pbo,pty, attrs = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let subst,metasenv,u,selected_hyps,terms_with_context =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
+ ProofEngineHelpers.select ~metasenv ~subst ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern in
let context = CicMetaSubst.apply_subst_context subst context in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
context_of_t, t context_of_t metasenv u
| (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u)
in
- let t,subst,metasenv' =
+ let t,e_subst,metasenv' =
try
CicMetaSubst.delift_rels [] metasenv
(List.length context_of_t - List.length context) t
in
(*CSC: I am not sure about the following two assertions;
maybe I need to propagate the new subst and metasenv *)
- assert (subst = []);
+ assert (e_subst = []);
assert (metasenv' = metasenv);
let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in
u,typ,t,metasenv
else
u1
) u terms_with_context) ;
- let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in
+ let status = (uri,metasenv',subst,pbo,pty, attrs),goal in
let proof,goals =
PET.apply_tactic
(T.thens
T.id_tac])
status
in
- let _,metasenv'',_subst,_,_, _ = proof in
+ let _,metasenv'',_,_,_, _ = proof in
(* CSC: the following is just a bad approximation since a meta
can be closed and then re-opened! *)
(proof,
let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
let elim_tac pattern (proof, goal) =
let ugraph = CicUniv.oblivion_ugraph in
- let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
+ let curi, metasenv, subst, proofbo, proofty, attrs = proof in
let conjecture = CicUtil.lookup_meta goal metasenv in
let metano, context, ty = conjecture in
let pattern = pattern_after_generalize_pattern_tac pattern in
match pattern with
| None, [], Some cpattern -> cpattern
| _ -> raise (PET.Fail (lazy "not implemented")) in
- let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in
- let termty = CicReduction.whd context termty in
+ let termty,_ugraph = TC.type_of_aux' metasenv ~subst context term ugraph in
+ let termty = CicReduction.whd ~subst context termty in
let termty, metasenv', arguments, _fresh_meta =
TermUtil.saturate_term
(ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
name
| _ -> assert false
in
- let ty_ty,_ugraph = TC.type_of_aux' metasenv' context ty ugraph in
+ let ty_ty,_ugraph = TC.type_of_aux' metasenv' ~subst context ty ugraph in
let ext =
match ty_ty with
C.Sort C.Prop -> "_ind"
| Some t -> t
in
let ety, _ugraph =
- TC.type_of_aux' metasenv' context eliminator_ref ugraph in
+ TC.type_of_aux' metasenv' ~subst context eliminator_ref ugraph in
(* FG: ADDED PART ***********************************************************)
(* FG: we can not assume eliminator is the default eliminator ***************)
let splits, args_no = PEH.split_with_whd (context, ety) in
| _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i
| _ -> raise NotAnEliminator
in
- let metasenv', pred, term, actual_args = match pattern with
+ let metasenv', subst, pred, term, actual_args = match pattern with
| None, [], Some (C.Implicit (Some `Hole)) ->
- metasenv', C.Implicit None, term, []
+ metasenv', subst, C.Implicit None, term, []
| _ ->
mk_predicate_for_elim
~args_no ~context ~ugraph ~cpattern
- ~metasenv:metasenv' ~arg:term ~using:eliminator_ref ~goal:ty
+ ~metasenv:metasenv' ~subst ~arg:term ~using:eliminator_ref ~goal:ty
in
(* FG: END OF ADDED PART ****************************************************)
let term_to_refine =
in
C.Appl (eliminator_ref :: args_init args_no f)
in
- let refined_term,_refined_termty,metasenv'',_ugraph =
- CicRefine.type_of_aux' metasenv' context term_to_refine ugraph
+ let refined_term,_refined_termty,metasenv'',subst,_ugraph =
+ CicRefine.type_of metasenv' subst context term_to_refine ugraph
in
let new_goals =
ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
- let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
+ let proof' = curi,metasenv'',subst,proofbo,proofty, attrs in
let proof'', new_goals' =
PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
in
(* The apply_tactic can have closed some of the new_goals *)
let patched_new_goals =
- let (_,metasenv''',_subst,_,_, _) = proof'' in
+ let (_,metasenv''',_,_,_, _) = proof'' in
List.filter
(function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
new_goals @ new_goals'
ProofEngineTypes.lazy_pattern ->
ProofEngineTypes.tactic
-(* ALB, needed by the new paramodulation... *)
-val apply_with_subst:
- term:Cic.term -> ?subst:Cic.substitution -> ?maxmeta:int -> ProofEngineTypes.proof * int ->
- Cic.substitution * (ProofEngineTypes.proof * int list) * int
-
(* not a real tactic *)
val apply_tac_verbose :
term:Cic.term ->
ProofEngineTypes.proof * int ->
(Cic.term -> Cic.term) * (ProofEngineTypes.proof * int list)
+(* the proof status has a subst now, and apply_tac honors it *)
val apply_tac:
term: Cic.term -> ProofEngineTypes.tactic
val applyP_tac: (* apply for procedural reconstruction *)
(* FG *)
val mk_predicate_for_elim:
- context:Cic.context -> metasenv:Cic.metasenv ->
+ context:Cic.context -> metasenv:Cic.metasenv -> subst:Cic.substitution ->
ugraph:CicUniv.universe_graph -> goal:Cic.term ->
arg:Cic.term -> using:Cic.term -> cpattern:Cic.term -> args_no:int ->
- Cic.metasenv * Cic.term * Cic.term * Cic.term list
+ Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.term list
exception Bad_pattern of string Lazy.t
-let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) =
- CicMkImplicit.new_meta metasenv []
+let new_meta_of_proof ~proof:(_, metasenv, subst, _, _, _) =
+ CicMkImplicit.new_meta metasenv subst
let subst_meta_in_proof proof meta term newmetasenv =
let uri,metasenv,initial_subst,bo,ty, attrs = proof in
in
find subst metasenv ugraph context wanted t
-let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
+let select_in_term
+ ~metasenv ~subst ~context ~ugraph ~term ~pattern:(wanted,where)
+=
let add_ctx context name entry = (Some (name, entry)) :: context in
let map2 error_msg f l1 l2 =
try
| Some where -> aux context where term
in
match wanted with
- None -> [],metasenv,ugraph,roots
+ None -> subst,metasenv,ugraph,roots
| Some wanted ->
- let rec find_in_roots =
+ let rec find_in_roots subst =
function
- [] -> [],metasenv,ugraph,[]
+ [] -> subst,metasenv,ugraph,[]
| (context',where)::tl ->
- let subst,metasenv,ugraph,tl' = find_in_roots tl in
+ let subst,metasenv,ugraph,tl' = find_in_roots subst tl in
let subst,metasenv,ugraph,found =
let wanted, metasenv, ugraph = wanted context' metasenv ugraph in
find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context'
in
subst,metasenv,ugraph,found @ tl'
in
- find_in_roots roots
+ find_in_roots subst roots
+;;
(** create a pattern from a term and a list of subterms.
* the pattern is granted to have a ? for every subterm that has no selected
*
* @raise Bad_pattern
* *)
- let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
+ let select ~metasenv ~subst ~ugraph ~conjecture:(_,context,ty)
~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
=
let what, hyp_patterns, goal_pattern = pattern in
aux [] context
in
let subst,metasenv,ugraph,ty_terms =
- select_in_term ~metasenv ~context ~ugraph ~term:ty
- ~pattern:(what,goal_pattern) in
+ select_in_term ~metasenv ~subst ~context ~ugraph ~term:ty
+ ~pattern:(what,goal_pattern)
+ in
let subst,metasenv,ugraph,context_terms =
let subst,metasenv,ugraph,res,_ =
(List.fold_right
subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
| Some pat ->
let subst,metasenv,ugraph,terms =
- select_in_term ~metasenv ~context ~ugraph ~term
+ select_in_term ~subst ~metasenv ~context ~ugraph ~term
~pattern:(what, Some pat)
in
subst,metasenv,ugraph,((Some (`Decl terms))::res),
(entry::context)
| Some pat ->
let subst,metasenv,ugraph,terms_bo =
- select_in_term ~metasenv ~context ~ugraph ~term:bo
+ select_in_term ~subst ~metasenv ~context ~ugraph ~term:bo
~pattern:(what, Some pat) in
let subst,metasenv,ugraph,terms_ty =
let subst,metasenv,ugraph,res =
- select_in_term ~metasenv ~context ~ugraph ~term:ty
+ select_in_term ~subst ~metasenv ~context ~ugraph ~term:ty
~pattern:(what, Some pat)
in
subst,metasenv,ugraph,res
subst,metasenv,ugraph,res
in
subst,metasenv,ugraph,context_terms, ty_terms
+;;
(** locate_in_term equality what where context
* [what] must match a subterm of [where] according to [equality]
* *)
val select:
metasenv:Cic.metasenv ->
+ subst:Cic.substitution ->
ugraph:CicUniv.universe_graph ->
conjecture:Cic.conjecture ->
pattern:ProofEngineTypes.lazy_pattern ->
(* Note: this code is almost identical to change_tac and
* it could be unified by making the change function a callback *)
let reduction_tac ~reduction ~pattern (proof,goal) =
- let curi,metasenv,_subst,pbo,pty, attrs = proof in
+ let curi,metasenv,subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
+ ProofEngineHelpers.select ~subst ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern
in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
| _ as t -> t
) metasenv
in
- (curi,metasenv',_subst,pbo,pty, attrs), [metano]
+ (curi,metasenv',subst,pbo,pty, attrs), [metano]
;;
let simpl_tac ~pattern =
term(s) to be replaced. *)
let change_tac ?(with_cast=false) ~pattern with_what =
let change_tac ~pattern ~with_what (proof, goal) =
- let curi,metasenv,_subst,pbo,pty, attrs = proof in
+ let curi,metasenv,subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
with_what context_of_t metasenv ugraph
in
let _,u =
- CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph
+ CicTypeChecker.type_of_aux'
+ metasenv ~subst context_of_t with_what ugraph
in
let b,_ =
- CicReduction.are_convertible ~metasenv context_of_t t with_what u
+ CicReduction.are_convertible
+ ~metasenv ~subst context_of_t t with_what u
in
if b then
((t, with_what) :: pairs), metasenv, ugraph
CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture
- ~pattern in
+ ProofEngineHelpers.select
+ ~metasenv ~subst ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern
+ in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
let context', metasenv, ugraph =
List.fold_right2
| _ as t -> t)
metasenv
in
- let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in
+ let proof,goal = (curi,metasenv',subst,pbo,pty, attrs), metano in
if with_cast then
let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in
let (newproof,_) =
proof,[goal]
in
mk_tactic (change_tac ~pattern ~with_what)
+;;
let fold_tac ~reduction ~term ~pattern =
let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
(change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
in
mk_tactic (fold_tac ~reduction ~term ~pattern)
+;;
let id_tac =
let id_tac (proof,goal) =
- let _, metasenv, _subst, _, _, _ = proof in
+ let _, metasenv, _, _, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
(proof,[goal])
in
let fail_tac =
let fail_tac (proof,goal) =
- let _, metasenv, _subst, _ , _, _ = proof in
+ let _, metasenv, _, _ , _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
raise (PET.Fail (lazy "fail tactical"))
in
let progress_tactic ~tactic =
let msg = lazy "Failed to progress" in
- let progress_tactic (((_,metasenv,_subst,_,_,_),g) as istatus) =
- let ((_,metasenv',_subst,_,_,_),opened) as ostatus =
+ let progress_tactic (((_,metasenv,_,_,_,_),g) as istatus) =
+ let ((_,metasenv',_,_,_,_),opened) as ostatus =
PET.apply_tactic tactic istatus
in
match opened with
let right = IntroductionTactics.right_tac
let ring = Ring.ring_tac
let simpl = ReductionTactics.simpl_tac
-let solve_rewrite = Auto.solve_rewrite_tac
let split = IntroductionTactics.split_tac
let symmetry = EqualityTactics.symmetry_tac
let transitivity = EqualityTactics.transitivity_tac
-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 16 11:28:06 CEST 2009 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 23 10:59:57 CEST 2009 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyP : term:Cic.term -> ProofEngineTypes.tactic
val right : ProofEngineTypes.tactic
val ring : ProofEngineTypes.tactic
val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
-val solve_rewrite :
- params:Auto.auto_params ->
- automation_cache:AutomationCache.cache -> unit -> ProofEngineTypes.tactic
val split : ProofEngineTypes.tactic
val symmetry : ProofEngineTypes.tactic
val transitivity : term:Cic.term -> ProofEngineTypes.tactic
let module R = CicReduction in
let module S = CicSubstitution in
let module PT = PrimitiveTactics in
- let _,metasenv,_subst,_,_, _ = proof in
+ let _,metasenv,_,_,_, _ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let rec find n = function
hd::tl ->
(*** lemmata on well-formedness ***)
-lemma fv_WFT : \forall T,x,G.(WFType G T) \to (in_list ? x (fv_type T)) \to
- (in_list ? x (fv_env G)).
+lemma fv_WFT : \forall T,x,G.(WFType G T) → x ∈ fv_type T → x ∈ fv_env G.
intros 4.elim H
[simplify in H2;elim (in_list_cons_case ? ? ? ? H2)
[rewrite > H3;assumption|elim (not_in_list_nil ? ? H3)]
|apply (SA_Arrow ? ? ? ? ? (H2 H5) (H4 H5))
|apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 ? H6)
[intro;apply H6;apply (fv_WFT ? ? ? (WFT_Forall ? ? ? H1 H3));
- simplify;autobatch
+ simplify;
+ autobatch;
|autobatch]]
qed.
]
qed.
+(*
notation > "hvbox(x ∈ l)"
non associative with precedence 30 for @{ 'inlist $x $l }.
notation < "hvbox(x \nbsp ∈ \nbsp l)"
non associative with precedence 30 for @{ 'inlist $x $l }.
-interpretation "item in list" 'inlist x l =
- (cic:/matita/list/in/in_list.ind#xpointer(1/1) _ x l).
+*)
+interpretation "item in list" 'mem x l = (in_list _ x l).
lemma max_case : \forall m,n.(max m n) = match (leb m n) with
[ true \Rightarrow n
]
|generalize in match n4.
elim n2
- [cases n6;simplify;autobatch
+ [cases n6;simplify;
+ [ exists; [2: autobatch;]
+ | exists; [2:autobatch;]
+ ]
|cases n7;simplify
- [autobatch
+ [exists;[2:autobatch]
|elim (H2 n9).
rewrite > H3.
simplify.
- autobatch
+ exists;[2:autobatch]
]]]]]
qed.
\ No newline at end of file
axiom Rtimes_x_R1 : ∀x.x * R1 = x.
axiom distr_Rtimes_Rplus_l : ∀x,y,z:R.x*(y+z) = x*y + x*z.
+pump 200.
+
lemma distr_Rtimes_Rplus_r : ∀x,y,z:R.(x+y)*z = x*z + y*z.
-intros;autobatch paramodulation;
+intros; demodulate all. (*autobatch paramodulation;*)
qed.
(* commutative field *)
qed. *)
lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
-intro;
+intro; demodulate all.
+(*
rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %);
rewrite < assoc_Rplus;
apply eq_f2;autobatch paramodulation;
+*)
qed.
lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x.
-intro.
+intro. demodulate all. (*
+auto paramodulation.
rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?);
apply eq_f2 [reflexivity]
rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?);
rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation;
+*)
qed.
lemma Ropp_inv : ∀x.x = Ropp (Ropp x).
|apply Rinv_Rtimes_l;assumption]
qed.
-lemma Ropp_R0 : R0 = - R0.
-rewrite < eq_Rtimes_Ropp_R1_Ropp;autobatch paramodulation;
+lemma Ropp_R0 : R0 = - R0. demodulate all. (*
+rewrite < eq_Rtimes_Ropp_R1_Ropp;autobatch paramodulation; *)
qed.
lemma distr_Ropp_Rplus : ∀x,y:R.-(x + y) = -x -y.
-intros;rewrite < eq_Rtimes_Ropp_R1_Ropp;
+intros; demodulate all; (*rewrite < eq_Rtimes_Ropp_R1_Ropp;
rewrite > sym_Rtimes;rewrite > distr_Rtimes_Rplus_l;
-autobatch paramodulation;
+autobatch paramodulation;*)
qed.
lemma Ropp_Rtimes_l : ∀x,y:R.-(x*y) = -x*y.
-intros;rewrite < eq_Rtimes_Ropp_R1_Ropp;
-rewrite > sym_Rtimes;rewrite < assoc_Rtimes;autobatch paramodulation;
+intros; demodulate all; (*rewrite < eq_Rtimes_Ropp_R1_Ropp;
+rewrite > sym_Rtimes;rewrite < assoc_Rtimes;autobatch paramodulation;*)
qed.
lemma Ropp_Rtimes_r : ∀x,y:R.-(x*y) = x*-y.
-intros;rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (???%);
-autobatch;
+intros; demodulate all; (*rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (???%);
+autobatch;*)
qed.
(* less than *)
lemma pos_z_to_le_Rtimes_Rtimes_to_lt : ∀x,y,z.R0 < z → z*x ≤ z*y → x ≤ y.
intros;cases H1
[left;autobatch
-|right;rewrite < Rtimes_x_R1;rewrite < Rtimes_x_R1 in ⊢ (???%);
+|right; rewrite < Rtimes_x_R1;rewrite < Rtimes_x_R1 in ⊢ (???%);
rewrite < sym_Rtimes;rewrite < sym_Rtimes in ⊢ (???%);
rewrite < (Rinv_Rtimes_l z)
- [rewrite < sym_Rtimes in ⊢ (??(?%?)?);rewrite < sym_Rtimes in ⊢ (???(?%?));
- autobatch paramodulation
+ [demodulate all; (*rewrite < sym_Rtimes in ⊢ (??(?%?)?);rewrite < sym_Rtimes in ⊢ (???(?%?));
+ autobatch paramodulation*)
|intro;rewrite > H3 in H;apply (irrefl_Rlt R0);assumption]]
qed.
rewrite > Ropp_inv in ⊢ (??%);
apply Rlt_to_Rlt_Ropp_Ropp;apply (pos_z_to_lt_Rtimes_Rtimes_to_lt ?? (-z))
[rewrite > Ropp_R0;autobatch
-|rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?(??%)?);
+|applyS H1; (*
+ rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?(??%)?);
rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (??(??%));
do 2 rewrite < assoc_Rtimes;
rewrite > eq_Rtimes_Ropp_R1_Ropp;
rewrite > eq_Rtimes_Ropp_R1_Ropp;
rewrite < Ropp_inv;
rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
- assumption]
+ assumption*)]
qed.
lemma lt_R0_Rinv : ∀x.R0 < x → R0 < Rinv x.
lemma lt_Rinv : ∀x,y.R0 < x → x < y → Rinv y < Rinv x.
intros;
lapply (Rlt_times_l ? ? (Rinv x * Rinv y) H1)
-[rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;
+[ lapply (Rinv_Rtimes_l x);[2: intro; destruct H2; autobatch;]
+ lapply (Rinv_Rtimes_l y);[2: intro; destruct H2; autobatch;]
+ cut ((x \sup -1/y*x<x \sup -1/y*y) = (y^-1 < x ^-1));[2:
+ demodulate all;]
+ rewrite < Hcut; assumption;
+ (*
+ rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;
rewrite > assoc_Rtimes in Hletin:(??%);
rewrite > sym_Rtimes in Hletin:(??(??%));
rewrite > Rinv_Rtimes_l in Hletin
[rewrite > Rinv_Rtimes_l in Hletin
- [rewrite > Rtimes_x_R1 in Hletin;rewrite > sym_Rtimes in Hletin;
- rewrite > Rtimes_x_R1 in Hletin;assumption
+ [applyS Hletin;(*rewrite > Rtimes_x_R1 in Hletin;rewrite > sym_Rtimes in Hletin;
+ rewrite > Rtimes_x_R1 in Hletin;assumption*)
|intro;rewrite > H2 in H1;apply (asym_Rlt ? ? H H1)]
- |intro;rewrite > H2 in H;apply (irrefl_Rlt ? H)]
+ |intro;rewrite > H2 in H;apply (irrefl_Rlt ? H)]*)
|apply pos_times_pos_pos;apply lt_R0_Rinv;autobatch]
qed.
lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
-intros;rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
+intros; lapply (Rlt_plus_l ?? (-b) H); applyS Hletin;
+(*
+rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
rewrite < assoc_Rplus;
rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
apply Rlt_plus_l;assumption;
+*)
qed.
lemma Rlt_plus_r_to_l : ∀a,b,c.a < b + c → a - c < b.
-intros;rewrite > Ropp_inv;rewrite > Ropp_inv in ⊢ (??%);
+intros;
+rewrite > Ropp_inv;rewrite > Ropp_inv in ⊢ (??%);
apply Rlt_to_Rlt_Ropp_Ropp;rewrite > distr_Ropp_Rplus;
apply Rlt_plus_l_to_r;rewrite < distr_Ropp_Rplus;apply Rlt_to_Rlt_Ropp_Ropp;
assumption;
rewrite < sym_Rplus;apply Rle_minus_r_to_l;
apply (pos_z_to_le_Rtimes_Rtimes_to_lt ? ? (n*Rexp_nat a (n-1)))
[apply pos_times_pos_pos
- [lapply (nat_lt_to_R_lt ?? H1);autobatch
+ [apply (nat_lt_to_R_lt ?? H1);
|elim daemon]
|rewrite > Rtimes_x_R0;do 2 rewrite > distr_Rtimes_Rplus_l;
rewrite > sym_Rtimes in ⊢ (? ? (? (? ? (? ? (? %))) ?));
rewrite < distr_Rtimes_Rplus_l;
apply (trans_Rle ? (Rexp_nat a n - Rexp_nat y n))
[apply Rle_plus_l;left;autobatch
- |rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
+ | cut (∀x,y.(S x ≤ y) = (x < y));[2: intros; reflexivity]
+ applyS Rexp_nat_tech;
+ [ unfold lt; change in H1 with (O < n);
+ autobatch; (*applyS H1;*)
+ | assumption;
+ | elim daemon; ]]
+ (*
+ rewrite > assoc_Rtimes;rewrite > sym_Rtimes in ⊢ (??(??%));
rewrite < assoc_Rtimes;apply Rexp_nat_tech
[autobatch
|assumption
- |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]
+ |(* by transitivity y^n < x < a^n and injectivity *) elim daemon]]*)
|intro;apply (irrefl_Rlt (n*Rexp_nat a (n-1)));
rewrite > H11 in ⊢ (?%?);apply pos_times_pos_pos
- [lapply (nat_lt_to_R_lt ?? H1);autobatch
+ [apply (nat_lt_to_R_lt ?? H1);
|elim daemon]]]]
|elim (R_archimedean R1 ((x-Rexp_nat a n)/(n*Rexp_nat (a+1) (n-1))))
[|autobatch]
assumption
|apply lt_R0_Rinv;apply pos_times_pos_pos
[apply pos_times_pos_pos
- [lapply (nat_lt_to_R_lt ?? H1);autobatch
+ [apply (nat_lt_to_R_lt ?? H1);
|elim daemon]
|apply (trans_Rlt ???? H8);apply pos_times_pos_pos
[apply Rlt_plus_l_to_r;rewrite > sym_Rplus;rewrite > Rplus_x_R0;
assumption
|apply lt_R0_Rinv;apply pos_times_pos_pos
- [lapply (nat_lt_to_R_lt ?? H1);autobatch
+ [apply (nat_lt_to_R_lt ?? H1);
|elim daemon]]]]]
|split
[(* show that h > R0, also useful in previous parts of the proof *)
lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? =
root (m*n) x ? H1.
[cases (root_sound n x H H1);assumption
-|autobatch
+| change in match O with (O*O); apply lt_times; assumption;
+ (* autobatch paramodulation; non fa narrowing, non fa deep subsumption... *)
|intros;lapply (Rexp_nat_Rexp_nat_Rtimes (root m (root n x H H1) H2 ?) m n)
[cases (root_sound n x H H1);assumption
|cases (root_sound m (root n x H H1))
unfold member_of_subgroup;
elim H2;
apply (ex_intro ? ? (x'·a \sup -1));
-rewrite > f_morph;
+rewrite > f_morph;
apply (eq_op_x_y_op_z_y_to_eq ? (a \sub H));
rewrite > (op_associative ? G);
rewrite < H3;
lemma prove_reflect : ∀P:Prop.∀b:bool.
(b = true → P) → (b = false → ¬P) → reflect P b.
-intros 2 (P b); cases b; intros; [left|right] autobatch.
+intros 2 (P b); cases b; intros; [left|right] [autobatch.|autobatch;]
qed.
(* ### standard connectives/relations with reflection predicate ### *)
lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
intros (n m); apply bool_to_eq; split; intros (H);
-[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch type]
+[1:cases (b2pT ? ? (orbP ? ?) H); [2: (*autobatch type;*) apply lebW; assumption; ]
rewrite > (eqb_true_to_eq ? ? H1); autobatch
|2:cases (b2pT ? ? (lebP ? ?) H);
[ elim n; [reflexivity|assumption]
theorem cantor: ∀a:axs. ¬ (Z ⊆ S' a ∧ S' a ⊆ Z).
intros 2; cases H; clear H;
cut (a ◃ S' a);
- [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); autobatch]]
+ [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); apply iter; autobatch]]
cut (a ◃ emptyset);
[2: apply transitivity; [apply (S' a)]
[ assumption
simplify in H4 ⊢ %;
apply H1;
[ apply (C ? a1 j);
- | autobatch;
+ | autobatch;
| assumption;
| assumption]]
qed.
(D[X \sup (1+m)] = (1+m) · X \sup m).
we need to prove
(m · (X \sup (1+ pred m)) = m · X \sup m) (Ppred).
+ lapply depth=0 le_n;
we proved (0 < m ∨ 0=m) (cases).
we proceed by induction on cases
to prove (m · (X \sup (1+ pred m)) = m · X \sup m).
qed.
theorem iff_trans: \forall A,B,C. A \liff B \to B \liff C \to A \liff C.
- intros. elim H. elim H1. apply iff_intro;intros;autobatch.
+ intros. elim H. elim H1. apply iff_intro;intros;autobatch depth=3.
qed.
elim H1;
split;
intro;
- autobatch.
+ autobatch depth=3.
qed.
rewrite < sym_times.
rewrite > distr_times_minus.
rewrite > plus_minus.
-lapply(plus_to_minus ??? H3); demodulate. reflexivity.
+lapply(plus_to_minus ??? H3); demodulate all.
(*
rewrite > sym_times.
rewrite < H5.
[ apply (trans_lt ? (S O));
[ unfold lt; apply le_n;
| apply lt_SO_smallest_factor; assumption; ]
- | letin x \def le.autobatch.
- (*
- apply divides_smallest_factor_n;
- apply (trans_lt ? (S O));
- [ unfold lt; apply le_n;
- | assumption; ] *) ] ]
- | autobatch.
+ | apply divides_smallest_factor_n;
+ autobatch; ] ]
+ | apply prime_to_nth_prime;
+ autobatch.
(*
apply prime_to_nth_prime;
apply prime_smallest_factor_n;
assumption.unfold Not.
intro.
cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
- [unfold Not in Hcut1.autobatch.
+ [ apply Hcut1; autobatch depth=2;
(*
apply Hcut1.apply divides_to_mod_O;
[ apply lt_O_nth_prime_n.
| assumption.
]
*)
- |letin z \def le.
- cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n)));
- [2: rewrite < H1.assumption.|letin x \def le.autobatch width = 4 depth = 2]
- (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
- ].
-(*
- apply (p_ord_aux_to_not_mod_O n n ? q r);
+ | unfold p_ord in H2; lapply depth=0 le_n; autobatch width = 4 depth = 2;
+ (*apply (p_ord_aux_to_not_mod_O n n ? q r);
[ apply lt_SO_nth_prime_n.
| assumption.
| apply le_n.
| rewrite < H1.assumption.
- ]
+ ]*)
].
-*)
+
apply (le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n)).
apply divides_to_max_prime_factor.
assumption.assumption.
[(* first case *)
rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
+ elim H1. autobatch;
+ (*
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
- elim H1.
- pump 39.
- applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
- (*
+ applyS (witness n ? ? (refl_eq ? ?)).
rewrite < (sym_times n).rewrite < assoc_times.
rewrite > (sym_times q).rewrite > assoc_times.
rewrite < (assoc_times a1).rewrite < (sym_times n).
|(* second case *)
rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
+ elim H1. autobatch;
+ (*
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
- elim H1.rewrite > H6.
- applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
- (*
+ rewrite > H6.
+ applyS (witness n ? ? (refl_eq ? ?)).
rewrite < sym_times.rewrite > assoc_times.
rewrite < (assoc_times q).
rewrite < (sym_times n).
rewrite > H4 in H2.
elim (divides_times_to_divides ? ? ? H H2)
[apply False_ind.apply H1.assumption
- |elim H5.
+ |elim H5.
apply (witness ? ? n2).
rewrite > sym_times in ⊢ (? ? ? (? % ?)).
rewrite > assoc_times.
rewrite > H8
[ reflexivity
| assumption
- | autobatch
+ | apply andb_true_true; [2: apply H12]
]
| apply eqb_false_to_not_eq.
generalize in match H14.
rewrite < exp_plus_times.
apply eq_f.
rewrite > sym_plus.
- apply plus_minus_m_m.
- autobatch
+ apply plus_minus_m_m.
+ autobatch;
]
]
|intros.
[apply le_S_S_to_le.
change with ((i/S m) < S n).
apply (lt_times_to_lt_l m).
- apply (le_to_lt_to_lt ? i)
- [autobatch|assumption]
+ apply (le_to_lt_to_lt ? i);[2:assumption]
+ apply eq_plus_to_le;[2:autobatch]
|apply le_exp
[assumption
|apply le_S_S_to_le.
apply le_S.
assumption
]
- |apply H2[autobatch|apply le_n]
+ |apply H2[autobatch |apply le_n]
]
]
]
apply lt_to_not_eq.
apply (le_to_lt_to_lt ? m)
[apply (trans_le ? (m-k))
- [assumption|autobatch]
+ [assumption| autobatch]
|apply le_S.apply le_n
]
]
|apply not_eq_to_eqb_false.
apply lt_to_not_eq.
- unfold.autobatch
+ unfold. autobatch;
]
]
|apply le_S_S_to_le.assumption
]
|apply sym_eq.
apply plus_to_minus.
- autobatch.
+ autobatch;
]
|intros.
cut ((S n1) \neq k1)
apply nat_elim2
[intros.apply False_ind.apply (not_le_Sn_O ? H)
|intros.rewrite < minus_n_O.
- autobatch
+ change in H1 with (n<n1);
+ apply lt_minus_m; autobatch depth=2;
|intros.
generalize in match H2.
apply (nat_case n1)
rewrite > eq_minus_S_pred.
apply lt_pred
[unfold lt.apply le_plus_to_minus_r.applyS H1
- |apply H[autobatch|assumption]
+ |apply H[autobatch depth=2|assumption]
]
]
qed.
theorem lt_O_minus_to_lt: \forall a,b:nat.
O \lt b-a \to a \lt b.
-intros.
+intros. applyS (lt_minus_to_plus O a b). assumption;
+(*
rewrite > (plus_n_O a).
rewrite > (sym_plus a O).
apply (lt_minus_to_plus O a b).
assumption.
+*)
qed.
theorem lt_minus_to_lt_plus:
\forall n,m,p. n - m < p \to n < m + p.
intros 2.
apply (nat_elim2 ? ? ? ? n m)
- [simplify.intros.autobatch.
+ [simplify.intros.
+ lapply depth=0 le_n; autobatch;
|intros 2.rewrite < minus_n_O.
intro.assumption
|intros.
intros.
apply sym_eq.
apply plus_to_minus.
-autobatch.
+autobatch;
qed.
theorem distributive_times_minus: distributive nat times minus.
theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
p+(n-m) = n-(m-p).
-intros.
+intros.
apply sym_eq.
apply plus_to_minus.
rewrite < assoc_plus.
+
(**************************************************************************)
(* __ *)
(* ||M|| *)
intros.elim n.
simplify.reflexivity.
simplify.
-demodulate all steps=3.
+demodulate all.
(*
apply eq_f.rewrite < H.
transitivity ((n1+m)+n1*m).symmetry.apply assoc_plus.
intros.elim x.
simplify.reflexivity.
simplify.
-demodulate all steps=16.
+demodulate all.
(*
rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z).
intros.
elim x. simplify.apply refl_eq.
simplify.
-demodulate all steps=4.
+demodulate all.
(*
rewrite < sym_times.
rewrite > distr_times_plus.
projects / helm.git / commitdiff