From 25564c06c570e5ab9be455904c0b381842f8d4c4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 May 2009 14:26:06 +0000 Subject: [PATCH] apply and auto.equational_case call saturation.solve_narrowing that performs goal inference and demodulation --- helm/software/components/tactics/auto.ml | 141 ++++-------------- .../components/tactics/automationCache.ml | 2 +- .../components/tactics/declarative.ml | 2 +- .../tactics/paramodulation/equality.ml | 3 +- .../tactics/paramodulation/equality.mli | 3 +- .../tactics/paramodulation/indexing.ml | 85 ++++++++--- .../tactics/paramodulation/indexing.mli | 6 + .../tactics/paramodulation/saturation.ml | 74 ++++++++- .../tactics/paramodulation/saturation.mli | 10 ++ .../matita/library/Q/nat_fact/times.ma | 2 +- helm/software/matita/library/R/r.ma | 5 +- .../library/didactic/exercises/duality.ma | 4 +- helm/software/matita/library/nat/gcd.ma | 12 +- helm/software/matita/library/nat/ord.ma | 2 +- 14 files changed, 208 insertions(+), 143 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 15b2d848b..53120a44d 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -368,32 +368,12 @@ let init_cache_and_tables = 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 = @@ -406,29 +386,22 @@ let init_cache_and_tables 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 = @@ -439,74 +412,21 @@ let init_cache_and_tables { 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 = @@ -568,14 +488,14 @@ let fill_hypothesis context metasenv term tables (universe:Universe.universe) ca 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 @@ -598,7 +518,7 @@ let build_equalities auto context metasenv tables universe cache equations = 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 @@ -613,7 +533,7 @@ let close_more tables context status auto universe cache = 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 @@ -629,7 +549,7 @@ let find_context_equalities dbd tables context proof (universe:Universe.universe 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 @@ -644,7 +564,7 @@ let find_context_equalities dbd tables context proof (universe:Universe.universe (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 @@ -1115,8 +1035,8 @@ let apply_smart_aux 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"))) @@ -1619,8 +1539,7 @@ let equational_case 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 diff --git a/helm/software/components/tactics/automationCache.ml b/helm/software/components/tactics/automationCache.ml index 7d8e7d129..34bb3efdf 100644 --- a/helm/software/components/tactics/automationCache.ml +++ b/helm/software/components/tactics/automationCache.ml @@ -67,7 +67,7 @@ let add_term_to_active cache metasenv subst context t ty_opt = ~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 diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index 428e858c5..139dcb1f8 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -29,7 +29,7 @@ let mk_just ~dbd ~automation_cache = 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 ;; diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 5888019e4..cb12f7a77 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -1365,7 +1365,8 @@ let draw_proof bag names goal_proof proof id = 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 diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli index b4aa66d29..d60164689 100644 --- a/helm/software/components/tactics/paramodulation/equality.mli +++ b/helm/software/components/tactics/paramodulation/equality.mli @@ -123,7 +123,8 @@ val equality_of_term: 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 diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index b759427e3..cf4bcd555 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -1249,6 +1249,7 @@ let rec demodulation_goal bag env table goal = (* returns all the 1 step demodulations *) module C = Cic;; module S = CicSubstitution;; + let rec demodulation_all_aux metasenv context ugraph table lift_amount term = @@ -1266,17 +1267,22 @@ let rec demodulation_all_aux 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 @@ -1287,10 +1293,10 @@ let demod_all steps bag env table goal = 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 @@ -1299,12 +1305,57 @@ let demod_all steps bag env table goal = 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 diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index 8370d9da3..e36cfba49 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -94,6 +94,12 @@ val demodulation_goal : 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 -> diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 96b4d515b..be3d21aa1 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -298,7 +298,7 @@ let add_to_passive passive new_pos preferred = 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 *) @@ -902,7 +902,6 @@ let check_if_goals_set_is_solved bag env active passive goals = (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) ;; @@ -1654,6 +1653,77 @@ let given_clause 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 diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli index 71764cddd..d890a719d 100644 --- a/helm/software/components/tactics/paramodulation/saturation.mli +++ b/helm/software/components/tactics/paramodulation/saturation.mli @@ -74,3 +74,13 @@ val given_clause: 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 diff --git a/helm/software/matita/library/Q/nat_fact/times.ma b/helm/software/matita/library/Q/nat_fact/times.ma index 43c213c9b..88e2602b8 100644 --- a/helm/software/matita/library/Q/nat_fact/times.ma +++ b/helm/software/matita/library/Q/nat_fact/times.ma @@ -30,7 +30,7 @@ let rec times_f h g \def 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 diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma index 9e7ba97f5..f2bca131f 100644 --- a/helm/software/matita/library/R/r.ma +++ b/helm/software/matita/library/R/r.ma @@ -362,12 +362,13 @@ lapply (Rlt_times_l (Rinv x * Rinv y) ? ? H1) 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. diff --git a/helm/software/matita/library/didactic/exercises/duality.ma b/helm/software/matita/library/didactic/exercises/duality.ma index 28e254f94..2862883c5 100644 --- a/helm/software/matita/library/didactic/exercises/duality.ma +++ b/helm/software/matita/library/didactic/exercises/duality.ma @@ -164,6 +164,7 @@ sono necessari i seguenti lemmi: * 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*) @@ -221,6 +222,7 @@ notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associat 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 =========== @@ -625,7 +627,7 @@ theorem duality: ∀F1,F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2. 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. diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma index aa512566e..dcdbc7b7a 100644 --- a/helm/software/matita/library/nat/gcd.ma +++ b/helm/software/matita/library/nat/gcd.ma @@ -757,7 +757,8 @@ cut (n \divides p \lor n \ndivides p) [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). @@ -772,7 +773,7 @@ cut (n \divides p \lor n \ndivides p) |(* 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). @@ -921,10 +922,13 @@ rewrite > H4 in H2. 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 diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index cd53cc056..7dd4fb362 100644 --- a/helm/software/matita/library/nat/ord.ma +++ b/helm/software/matita/library/nat/ord.ma @@ -299,7 +299,7 @@ cut (S O < p) apply (lt_to_not_eq O ? H). rewrite > H7. rewrite < H10. - autobatch + autobatch;assumption; ] |elim c [rewrite > sym_gcd. -- 2.39.2