=
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
let add_list_to_tables metasenv subst automation_cache ct =
- let _,_,bag = automation_cache.AutomationCache.tables in
- let maxmeta = Equality.maxmeta bag in
- 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,maxmeta) ct
+ List.fold_left
+ (fun automation_cache (t,_) ->
+ AutomationCache.add_term_to_active automation_cache
+ metasenv subst context t None)
+ automation_cache ct
in
if restricted_univ = [] then
let ct =
in
let cache = AutoCache.cache_empty in
let cache = cache_add_list cache context (ct@lt) in
- let automation_cache, _ = add_list_to_tables metasenv subst automation_cache ct
+ let automation_cache =
+ add_list_to_tables metasenv subst automation_cache ct
in
- (* AutomationCache.pp_cache automation_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 as orig,acc, sacc, maxmeta) t ->
- let ty, _ =
- CicTypeChecker.type_of_aux'
- metasenv ~subst:[] context t CicUniv.oblivion_ugraph
- in
- let head, metasenv, args, maxmeta =
- TermUtil.saturate_term maxmeta metasenv context ty 0
- in
- 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
+ let t_ty =
+ List.map
+ (fun t ->
+ let ty, _ = CicTypeChecker.type_of_aux'
+ metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+ in
+ t, ty)
+ restricted_univ
in
(* let automation_cache = AutomationCache.empty () in *)
let automation_cache =
{ automation_cache with AutomationCache.univ = universe }
in
let ct =
- if use_context then find_context_theorems context metasenv else []
- in
- let automation_cache, _ = add_list_to_tables metasenv subst automation_cache ct
+ if use_context then find_context_theorems context metasenv else t_ty
in
- (* proviamo a tenere tutte le equazioni
let automation_cache =
- List.fold_left
- (fun c (t,ty) ->
- AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
- automation_cache s_t_ty
- in *)
+ add_list_to_tables metasenv subst automation_cache ct
+ in
(* AutomationCache.pp_cache automation_cache; *)
automation_cache.AutomationCache.univ,
automation_cache.AutomationCache.tables,
- (* cache_add_list cache_empty context t_ty *)
cache_empty
;;
- (*
-(* let signature = MetadataQuery.signature_of metasenv goal in *)
-(* let newmeta = CicMkImplicit.new_meta metasenv [] in *)
- let equations =
- retrieve_equations dont_filter (* true *) signature universe cache context metasenv
- 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'
- metasenv 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 units, other_equalities, newmeta =
- partition_unit_equalities context metasenv newmeta bag eqs_and_types
- in
- (* SIMPLIFICATION STEP
- let equalities =
- let env = (metasenv, context, CicUniv.oblivion_ugraph) in
- let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
- Saturation.simplify_equalities bag eq_uri env units
- in
- *)
- let passive = Saturation.make_passive units in
- let no = List.length units in
- let active = Saturation.make_active [] in
- let active,passive,newmeta =
- if paramod then active,passive,newmeta
- else
- Saturation.pump_actives
- context bag newmeta active passive (no+1) infinity
- in
- (active,passive,bag),cache,newmeta
-*)
-let fill_hypothesis context metasenv term tables (universe:Universe.universe) cache auto fast =
+let fill_hypothesis context metasenv subst term tables (universe:Universe.universe) cache auto fast =
let actives, passives, bag = tables in
let bag, head, metasenv, args =
- Equality.saturate_term bag metasenv context term
+ Equality.saturate_term bag metasenv subst context term
in
let tables = actives, passives, bag in
let propositional_args =
results,cache,tables
;;
-let build_equalities auto context metasenv tables universe cache equations =
+let build_equalities auto context metasenv subst tables universe cache equations =
List.fold_left
(fun (tables,facts,cache) (t,ty) ->
(* in any case we add the equation to the cache *)
let cache = AutoCache.cache_add_list cache context [(t,ty)] in
try
let saturated, cache, tables =
- fill_hypothesis context metasenv ty tables universe cache auto true
+ fill_hypothesis context metasenv subst ty tables universe cache auto true
in
let eqs, tables =
List.fold_left
let close_more tables context status auto universe cache =
let proof, goalno = status in
- let _, metasenv,_subst,_,_, _ = proof in
+ let _, metasenv,subst,_,_, _ = proof in
let signature = MetadataQuery.signature_of metasenv goalno in
let equations =
retrieve_equations false signature universe cache context metasenv
if is_an_equality ty then Some(t,ty) else None)
equations in
let tables, units, cache =
- build_equalities auto context metasenv tables universe cache eqs_and_types
+ build_equalities auto context metasenv subst tables universe cache eqs_and_types
in
let active,passive,bag = tables in
let passive = Saturation.add_to_passive units passive in
let module C = Cic in
let module S = CicSubstitution in
let module T = CicTypeChecker in
- let _,metasenv,_subst,_,_, _ = proof in
+ let _,metasenv,subst,_,_, _ = proof in
(* if use_auto is true, we try to close the hypothesis of equational
statements using auto; a naif, and probably wrong approach *)
let rec aux tables cache index = function
(try
let term = S.lift index term in
let saturated, cache, tables =
- fill_hypothesis context metasenv term
+ fill_hypothesis context metasenv subst term
tables universe cache default_auto false
in
let actives, passives, bag = tables in
automation_cache univ (proof'''',newmeta)
in
match
- Saturation.given_clause bag (proof'''',newmeta) active passive
- 1 0 infinity
+ Saturation.solve_narrowing bag (proof'''',newmeta) active passive
+ 1 (*0 infinity*)
with
| None, active, passive, bag ->
raise (ProofEngineTypes.Fail (lazy ("paramod fails")))
1,0,flags.timeout
in
match
- Saturation.given_clause bag status active passive
- goal_steps saturation_steps timeout
+ Saturation.solve_narrowing bag status active passive goal_steps
with
| None, active, passive, bag ->
[], (active,passive,bag), cache, flags
~subst metasenv context t CicUniv.oblivion_ugraph
in
let bag, head, metasenv, args =
- Equality.saturate_term bag metasenv context ty
+ Equality.saturate_term bag metasenv subst context ty
in
let mes = CicUtil.metas_of_term (Cic.Appl (head::t::args)) in
let t = if args = [] then t else Cic.Appl (t:: args) in
function
`Auto (l,params) ->
Tactics.auto ~dbd
- ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~automation_cache
+ ~params:(l,("skip_trie_filtering","1")::(*("skip_context","1")::*)params) ~automation_cache
| `Term t -> Tactics.apply t
;;
ignore(Unix.system "gv /tmp/matita_paramod.eps");
;;
-let saturate_term (id_to_eq, maxmeta) metasenv context term =
+let saturate_term (id_to_eq, maxmeta) metasenv subst context term =
+ let maxmeta = max maxmeta (CicMkImplicit.new_meta metasenv subst) in
let head, metasenv, args, newmeta =
TermUtil.saturate_term maxmeta metasenv context term 0
in
val term_of_equality: UriManager.uri -> equality -> Cic.term
val term_is_equality: Cic.term -> bool
-val saturate_term : equality_bag -> Cic.metasenv -> Cic.context -> Cic.term ->
+val saturate_term :
+ equality_bag -> Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.term ->
equality_bag * Cic.term * Cic.metasenv * Cic.term list
val push_maxmeta : equality_bag -> int -> equality_bag
(* returns all the 1 step demodulations *)
module C = Cic;;
module S = CicSubstitution;;
+
let rec demodulation_all_aux
metasenv context ugraph table lift_amount term
=
in
match term with
| C.Appl l ->
- let res, _, _ =
+ let res, _, _, _ =
List.fold_left
- (fun (res,l,r) t ->
- res @
- List.map
- (fun (rel, s, m, ug, c) ->
- (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
- (demodulation_all_aux
- metasenv context ugraph table lift_amount t),
- l@[List.hd r], List.tl r)
- (res, [], List.map (S.lift 1) l) l
+ (fun (res,b,l,r) t ->
+ if not b then res,b,l,r
+ else
+ let demods_for_t =
+ demodulation_all_aux
+ metasenv context ugraph table lift_amount t
+ in
+ let b = demods_for_t = [] in
+ res @
+ List.map
+ (fun (rel, s, m, ug, c) ->
+ (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+ demods_for_t, b, l@[List.hd r], List.tl r)
+ (res, true, [], List.map (S.lift 1) l) l
in
res
| t -> res
let is_visited l (_,_,t) =
List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
in
- 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
+ let rec aux steps visited nf bag = function
+ | _ when steps = 0 -> visited, bag, nf
+ | [] -> visited, bag, nf
+ | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest
| goal :: rest ->
let visited = goal :: visited in
let _,menv,t = goal in
let new_goals =
List.map (build_newg bag context goal Equality.Demodulation) res
in
- let visited, bag, res = aux steps visited bag (new_goals @ rest) in
- visited, bag, goal :: res
+ let nf = if new_goals = [] then goal :: nf else nf in
+ aux steps visited nf bag (new_goals @ rest)
in
- aux steps [] bag [goal]
+ aux steps [] [] bag [goal]
;;
+let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) =
+ let proof,m,eq,ty,left,right = open_goal goal 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
+ (pr@pl@proof, m, Cic.Appl [eq;ty;l;r])
+;;
+
+let demodulation_all_goal bag env table goal maxnf =
+ let proof,menv,eq,ty,left,right = open_goal goal in
+ let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
+ let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
+ let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
+ let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
+ List.fold_left
+ (fun acc (_,_,l as ld) ->
+ List.fold_left
+ (fun acc (_,_,r as rd) ->
+ combine_demodulation_proofs bag env goal ld rd :: acc)
+ acc r_demod)
+ [] l_demod
+;;
let solve_demodulating bag env table initgoal steps =
let proof,menv,eq,ty,left,right = open_goal initgoal in
Index.t ->
Equality.goal ->
bool * Equality.goal
+val demodulation_all_goal :
+ Equality.equality_bag ->
+ Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Index.t ->
+ Equality.goal -> int ->
+ Equality.goal list
val demodulation_theorem :
Equality.equality_bag ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
pos
in
pos_head @ pos_list @ pos_tail, add pos_set pos,
- List.fold_left Indexing.index pos_table new_pos
+ List.fold_left Indexing.index pos_table pos
;;
(* TODO *)
(fun bag -> check_if_goal_is_subsumed bag env (snd active));
(fun bag -> check_if_goal_is_subsumed bag env (last passive))
])
-(* provare active and passive?*)
(bag,None) (active_goals @ passive_goals)
;;
Some (subst, proof,gl),a,p, b
;;
+let solve_narrowing bag status active passive goal_steps =
+ let proof, goalno = status in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+ let cleaned_goal = Utils.remove_local_context type_of_goal in
+ let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in
+ let canonical_menv,other_menv =
+ List.partition (fun (_,c,_) -> c = context) metasenv in
+ let canonical_menv =
+ List.map
+ (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv
+ in
+ let metasenv' =
+ List.filter
+ (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal)
+ canonical_menv
+ in
+ let goal = [], metasenv', cleaned_goal in
+ let env = metasenv,context,CicUniv.empty_ugraph in
+ let goals =
+ let table = List.fold_left Indexing.index (last passive) (fst active) in
+ goal :: Indexing.demodulation_all_goal bag env table goal 4
+ in
+ let rec aux newactives newpassives bag = function
+ | [] -> bag, (newactives, newpassives)
+ | hd::tl ->
+ let selected = hd in
+ let (_,m1,t1) = selected in
+ let already_in =
+ List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
+ newactives
+ in
+ if already_in then
+ aux newactives newpassives bag tl
+ else
+ let bag, newpassives =
+ if Utils.metas_of_term t1 = [] then
+ bag, newpassives
+ else
+ let bag, new' =
+ Indexing.superposition_left bag env (snd active) selected
+ in
+ let new' =
+ List.map
+ (fun x -> let b, x = simplify_goal bag env x active in x)
+ new'
+ in
+ bag, newpassives @ new'
+ in
+ aux (selected::newactives) newpassives bag tl
+ in
+ let rec do_n bag ag pg = function
+ | 0 -> None, active, passive, bag
+ | n ->
+ let bag, (ag, pg) = aux [] [] bag (ag @ pg) in
+ match check_if_goals_set_is_solved bag env active passive (ag,pg) with
+ | bag, None -> do_n bag ag pg (n-1)
+ | bag, Some (gproof,newproof,subsumption_id,subsumption_subst,pmenv)->
+ let subst, proof, gl =
+ build_proof bag
+ status gproof newproof subsumption_id subsumption_subst pmenv
+ in
+ let uri,metasenv,subst,meta_proof,term_to_prove,attrs = proof in
+ let proof =
+ uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs
+ in
+ Some (subst, proof,gl),active,passive, bag
+ in
+ do_n bag [] goals goal_steps
+;;
+
let add_to_passive eql passives =
add_to_passive passives eql eql
ProofEngineTypes.goal list) option *
active_table * passive_table * Equality.equality_bag
+val solve_narrowing:
+ Equality.equality_bag ->
+ ProofEngineTypes.status ->
+ active_table ->
+ passive_table ->
+ int ->
+ (Cic.substitution *
+ ProofEngineTypes.proof *
+ ProofEngineTypes.goal list) option *
+ active_table * passive_table * Equality.equality_bag
theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
=defactorize_aux g m*defactorize_aux h m.
intro.elim g
- [elim h;simplify;autobatch
+ [elim h;simplify;autobatch;
|elim h
[simplify;autobatch
|simplify.rewrite > (H n3 (S m)).autobatch
qed.
lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
-intros; autobatch depth=4;
+intros;
+autobatch by H, (Rlt_plus_l (-b) (a+b) c);
(*
rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
rewrite < assoc_Rplus;
rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
-apply Rlt_plus_l;assumption;
+apply (Rlt_plus_l (-b) (a+b) c);assumption;
*)
qed.
* lemma `min_max` : `∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v`
* lemma `max_min` : `∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v`
* lemma `equiv_rewrite` : `∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3`
+* lemma `equiv_sym` : `∀F1,F2. F1 ≡ F2 → F2 ≡ F1`
DOCEND*)
notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed.
+lemma equiv_sym : ∀a,b.a ≡ b → b ≡ a. intros 4;symmetry;apply H;qed.
(* Esercizio 3
===========
the thesis becomes (dualize F1 ≡ dualize F2).
by (*BEGIN*)negate_fun(*END*), H we proved (negate F1 ≡ negate F2) (H1).
by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H1 we proved (FNot (dualize F1) ≡ negate F2) (H2).
- by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2 we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
+ by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2, equiv_sym we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
by (*BEGIN*)not_inj(*END*), H3 we proved (dualize F1 ≡ dualize F2) (H4).
by H4 done.
qed.
[elim Hcut1.elim H3.elim H4
[rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
- elim H1. autobatch by witness, divides_minus.
+ elim H1.
+ autobatch by witness;
(*
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
|(* second case *)
rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
- elim H1. autobatch by witness, divides_minus.
+ elim H1. autobatch by witness;
(*
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
elim (divides_times_to_divides ? ? ? H H2)
[apply False_ind.apply H1.assumption
|elim H5.
- (* applyS (witness ? ? n2 (refl_eq ? ?)).*)
+ autobatch by transitive_divides, H5, reflexive_divides,divides_times.
+ (*
apply (witness ? ? n2).
rewrite > sym_times in ⊢ (? ? ? (? % ?)).
rewrite > assoc_times.
- rewrite < H6.assumption
+ autobatch.
+ (*rewrite < H6.assumption*)
+ *)
]
qed.
\ No newline at end of file
apply (lt_to_not_eq O ? H).
rewrite > H7.
rewrite < H10.
- autobatch
+ autobatch;assumption;
]
|elim c
[rewrite > sym_gcd.
projects / helm.git / commitdiff