From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 28 Jun 2005 17:23:03 +0000 (+0000)
Subject: lapply improved
X-Git-Tag: INDEXING_NO_PROOFS~19
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=51380ce8eb393283476497f498d58546bceb5010;p=helm.git

lapply improved
---

diff --git a/helm/Makefile b/helm/Makefile
index ffab1984d..5cb7556b6 100644
--- a/helm/Makefile
+++ b/helm/Makefile
@@ -1,4 +1,5 @@
-DIRS = ocaml gTopLevel searchEngine mathql_test hxp
+DIRS = ocaml matita 
+# gTopLevel searchEngine mathql_test hxp
 
 DIRS_BYTE = $(patsubst %,%.byte,$(DIRS))
 DIRS_OPT = $(patsubst %,%.opt,$(DIRS))
diff --git a/helm/mathql_db_map.txt b/helm/mathql_db_map.txt
index a7e99985c..c58d843d2 100644
--- a/helm/mathql_db_map.txt
+++ b/helm/mathql_db_map.txt
@@ -19,6 +19,8 @@ backPointer source       <- backPointer h:occurrence
 backPointer h_occurrence <- 
 backPointer h_position   <- backPointer h:position
 backPointer h_depth      <- backPointer h:depth
+no_inconcl_aux source    <- 
+no_inconcl_aux no        <- no_inconcl 
 
 backPointer -> refObj
             ->
diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma
index 88e577f13..a28afef87 100644
--- a/helm/matita/tests/fguidi.ma
+++ b/helm/matita/tests/fguidi.ma
@@ -89,9 +89,17 @@ theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)).
 intros. auto.
 qed.
 
+(* teorema di prova che non compila per via del let *)
+theorem le_gen_S_x_2: \forall m,x. (le (S m) x) \to let k \def (S O) in
+                      (\exists n. x = (S n) \land (le m n) \land k = k).
+intros.
+lapply le_gen_S_x to H using H0. elim H0. elim H1.
+exists. exact x1. auto.
+qed.
+
 (* 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 to H. elim Hcut1. elim H1. 
-lapply eq_gen_S_S to H2. rewrite left Hcut3. assumption.
+lapply le_gen_S_x_2 to H using H0. elim H0. elim H1. 
+lapply eq_gen_S_S to H2 using H4. rewrite left H4. assumption.
 qed.
\ No newline at end of file
diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index fb9c04817..5160ea929 100644
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -38,25 +38,69 @@ let error msg = raise (PET.Fail msg)
 
 (* lapply *******************************************************************)
 
+let strip_dependent_prods metasenv context t =
+   let irl = MI.identity_relocation_list_for_metavariable context in
+   let rec aux metasenv p xcontext = function
+      | Cic.Prod (name, t1, t2) when not (TC.does_not_occur xcontext 0 1 t2) ->  
+         let index = MI.new_meta metasenv [] in
+         let metasenv = [index, context, t1] @ metasenv in
+         let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, irl) in    
+	 aux metasenv (succ p) (e :: xcontext) (S.subst s t2)
+      | Cic.Prod (name, t1, t2) -> metasenv, p, Some t1, (S.subst (Cic.Rel 1) t2)
+      | t                       -> metasenv, p, None, t 
+   in
+   aux metasenv 0 context t
+
+let skip_metas p =
+   let rec aux conts p =
+      if p <= 0 then conts else aux (T.id_tac :: conts) (pred p) 
+   in
+   aux [] p
+   
+let get_conclusion context t =
+   let rec aux p context = function 
+      | Cic.Prod (name, t1, t2)  -> 
+         aux (succ p) (Some (name, Cic.Decl t1) :: context) t2
+      | Cic.LetIn (name, u1, t2) -> 
+         aux (succ p) (Some (name, Cic.Def (u1, None)) :: context) t2
+     | Cic.Cast (t2, t1)         -> aux p context t2
+     | t                         -> p, context, t
+   in aux 0 context t
+
+let get_conclusion_dependences context t =
+   let p, context, conclusion = get_conclusion context t in
+   let rec aux l q = 
+      if q <= 0 then l else 
+      let b = TC.does_not_occur context (pred q) q conclusion in
+      aux (b :: l) (pred q)
+   in
+   aux [] p
+
+let solve_independents ?with_what deps =
+  let rec aux p conts = function
+     | []          -> p, conts
+     | true :: tl  -> 
+        let cont = PT.apply_tac ~term:(Cic.Rel (succ p)) in
+	aux (succ p) (cont :: conts) tl
+     | false :: tl -> aux (succ p) conts tl
+   in 
+   let p, conts = aux 0 [] deps in
+   match with_what with
+      | None   -> conts
+      | Some t -> PT.apply_tac ~term:(S.lift p t) :: conts
+	 
 let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
                (* ?(substs = []) *) ?to_what what =
    let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in
-   let apply_tac term = PT.apply_tac term in
-   let strip_dependent_prods metasenv context t =
-      let irl = MI.identity_relocation_list_for_metavariable context in
-      let rec aux metasenv p xcontext = function
-         | Cic.Prod (name, t1, t2) when not (TC.does_not_occur xcontext 0 1 t2) ->  
-            let index = MI.new_meta metasenv [] in
-            let metasenv = [index, context, t1] @ metasenv in
-            let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, irl) in    
-	    aux metasenv (succ p) (e :: xcontext) (S.subst s t2)
-         | Cic.Prod (name, t1, t2) -> metasenv, p, Some t1, t2
-         | t                       -> metasenv, p, None, t 
-      in
-      aux metasenv 0 context t
-   in
-   let rec mk_continuations p l =
-      if p <= 0 then l else mk_continuations (pred p) (T.id_tac :: l)
+   let intros_tac () = PT.intros_tac ~mk_fresh_name_callback () in
+   let solve_conclusion_tac ?with_what p deps = 
+      T.then_ ~start:(intros_tac ())
+	      ~continuation:(  
+         T.thens ~start:(PT.apply_tac what)
+	         ~continuations:( 
+	    skip_metas p @ solve_independents ?with_what deps 
+	 )
+      )
    in
    let lapply_tac (proof, goal) =
       let xuri, metasenv, u, t = proof in
@@ -64,21 +108,23 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
       match strip_dependent_prods metasenv context lemma with
          | metasenv, p, Some premise, conclusion ->
-	    let premise_tac = 
-	       match to_what with
-	          | None      -> T.id_tac 
-		  | Some term -> PT.apply_tac term 
+	    let deps = get_conclusion_dependences context conclusion in
+	    let inner_tac = match to_what with
+	       | None      -> 
+	          T.thens ~start:(cut_tac premise)
+		          ~continuations:[
+                     solve_conclusion_tac ~with_what:(Cic.Rel 1) p deps;
+	             T.id_tac
+	          ]
+	       | Some with_what -> 
+                  solve_conclusion_tac ~with_what p deps
+	    in	    
+	    let outer_tac =
+	       T.thens ~start:(cut_tac conclusion)
+	               ~continuations:[T.id_tac; inner_tac]
 	    in
 	    let status = (xuri, metasenv, u, t), goal in
-            let tac = T.thens ~start:(cut_tac premise)
-	                      ~continuations:[  
-		      T.thens ~start:(cut_tac conclusion)
-			      ~continuations:[ T.id_tac; 
-		      T.thens ~start:(PT.apply_tac what)
-		              ~continuations:(mk_continuations p [PT.apply_tac ~term:(Cic.Rel 1)])
-		                             ]; premise_tac ]
-	    in
-	    PET.apply_tactic tac status
+	    PET.apply_tactic outer_tac status
          | metasenv, p, None, conclusion         ->
 	    failwith "lapply_tac: not implemented"
    in