From: Ferruccio Guidi Date: Sat, 25 Jun 2005 19:17:47 +0000 (+0000) Subject: first working (?) version of lapply X-Git-Tag: INDEXING_NO_PROOFS~63 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8c5a76439368f52a7df7c7b524c726b1f9d4eb39;p=helm.git first working (?) version of lapply --- diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang index d2015ee3e..d2b6280b7 100644 --- a/helm/matita/matita.lang +++ b/helm/matita/matita.lang @@ -82,6 +82,7 @@ injection intro intros + lapply left letin normalize @@ -94,6 +95,7 @@ symmetry simplify split + to transitivity whd diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 37143ea23..4373b9be7 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -79,9 +79,8 @@ let tactic_of_ast = function EqualityTactics.rewrite_back_tac ~where:pattern ~term:t () | TacticAst.FwdSimpl (_, term) -> Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ()) - | TacticAst.LApply (_, term) -> - let f (name, term) = Cic.Name name, term in - Tactics.lapply term + | TacticAst.LApply (_, to_what, what) -> + Tactics.lapply ?to_what what let eval_tactical status tac = let apply_tactic tactic = @@ -452,9 +451,13 @@ let disambiguate_tactic status = function | TacticAst.FwdSimpl (loc, term) -> let status, term = disambiguate_term status term in status, TacticAst.FwdSimpl (loc, term) - | TacticAst.LApply (loc, term) -> - let status, term = disambiguate_term status term in - status, TacticAst.LApply (loc, term) + | TacticAst.LApply (loc, Some to_what, what) -> + let status, to_what = disambiguate_term status to_what in + let status, what = disambiguate_term status what in + status, TacticAst.LApply (loc, Some to_what, what) + | TacticAst.LApply (loc, None, what) -> + let status, what = disambiguate_term status what in + status, TacticAst.LApply (loc, None, what) let rec disambiguate_tactical status = function | TacticAst.Tactic (loc, tactic) -> diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index 284a700e7..88e577f13 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -89,8 +89,9 @@ theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)). intros. auto. qed. -(* -theorem pippo: \forall m,n. (le (S m) (S n)) \to (le m n). +(* proof of le_gen_S_S with lapply *) +theorem le_gen_S_S_2: \forall m,n. (le (S m) (S n)) \to (le m n). intros. -lapply le_gen_S_x. -*) +lapply le_gen_S_x to H. elim Hcut1. elim H1. +lapply eq_gen_S_S to H2. rewrite left Hcut3. assumption. +qed. \ No newline at end of file diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index d75a7c5f8..fb9c04817 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -84,69 +84,6 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub in PET.mk_tactic lapply_tac - - - - - - - - -(* - let count_dependent_prods context t = - let rec aux context p = function - | Cic.Prod (name, t1, t2) -> - if TC.does_not_occur context 0 1 t2 then p else - let e = Some (name, Cic.Decl t1) in - aux (e :: context) (succ p) t2 - | t -> p - in - aux context 0 t - in - let rec pad_context p context add_context = - if List.length add_context >= p then add_context @ context - else pad_context p context (None :: add_context) - in - let strip_dependent_prods metasenv context p t = - let rec aux metasenv add_context q = function - | Cic.Prod (name, t1, t2) when q > 0 -> - let context_for_meta = pad_context p context add_context in - let metasenv, index = MI.mk_implicit metasenv [] context_for_meta in - let rs = MI.identity_relocation_list_for_metavariable context_for_meta in - let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, rs) in - aux metasenv (e :: add_context) (pred q) (S.subst s t2) - | t -> metasenv, add_context, t - in - aux metasenv [] p t - in - let mk_body bo = function - | Some (name, Cic.Decl t1) -> Cic.Lambda (name, t1, bo) - | _ -> failwith "mk_body" - in - let lapply_tac (proof, goal) = - let xuri, metasenv, u, t = proof in -(* preliminaries *) - let metano, context, ty = CicUtil.lookup_meta goal metasenv in - let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in - let p = count_dependent_prods context lemma in -(* stripping *) - let metasenv, add_context, holed_lemma = strip_dependent_prods metasenv context p lemma in - let proof = xuri, metasenv, u, t in - let newmeta = MI.new_meta metasenv [] in - let context = add_context @ context in - let irl = MI.identity_relocation_list_for_metavariable context in - let bo = List.fold_left mk_body (Cic.Meta (newmeta, irl)) add_context in - let ty = S.lift p ty in - let (xuri, metasenv, u, t), _ = - PEH.subst_meta_in_proof proof metano bo [newmeta, context, ty] - in - prerr_endline (CicPp.ppterm holed_lemma); -(* cut *) - let status = (xuri, metasenv, u, t), newmeta in - PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status - in - PET.mk_tactic lapply_tac -*) (* fwd **********************************************************************) let fwd_simpl_tac ~what ~dbd =