From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
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 @@
     <keyword>injection</keyword>
     <keyword>intro</keyword>
     <keyword>intros</keyword>
+    <keyword>lapply</keyword>
     <keyword>left</keyword>
     <keyword>letin</keyword>
     <keyword>normalize</keyword>
@@ -94,6 +95,7 @@
     <keyword>symmetry</keyword>
     <keyword>simplify</keyword>
     <keyword>split</keyword>
+    <keyword>to</keyword>
     <keyword>transitivity</keyword>
     <keyword>whd</keyword>
   </keyword-list>
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 =