lapply improved

diff --git a/helm/Makefile b/helm/Makefile
index ffab1984d244a6642fe7f82fe0f48bdb089b4592..5cb7556b6967997866bdf9ce1d28abb944129bd2 100644 (file)
--- 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 a7e99985c644aa7de90244f4cd9b08e5cafae24c..c58d843d29163b52d03e7cdf117f7e0dc669ec5f 100644 (file)
--- 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 88e577f13bdc7691a274812cfbeb245559b92713..a28afef8773e9b942410a03c5d846b9a3171758b 100644 (file)
--- 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 fb9c0481796953d8e402eb5214510457dfa9d4b0..5160ea929c678e967d7abd872828546c0f2eb5f7 100644 (file)
--- 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