Declarative tactics for rewriting steps, elimination of the existential

[helm.git] / components / tactics / declarative.ml

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 1604d92d8029af62abb68fb4f79b0121bd97311a..3a24b0d5fd737624da42532c8d4bba173b998f51 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -34,16 +34,18 @@ let assume id t =
 ;;
 
 let suppose t id ty =
+(*BUG: ty not used *)
  Tacticals.then_
    ~start:
        (Tactics.intros ~howmany:1
              ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
    ~continuation:
-           (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)  
-             (fun _ metasenv ugraph -> t,metasenv,ugraph))
+            (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)  
+              (fun _ metasenv ugraph -> t,metasenv,ugraph))
 ;;
 
 let by_term_we_proved t ty id ty' =
+(*BUG: ty' not used *)
  match t with
     None -> assert false
   | Some t ->
@@ -63,6 +65,7 @@ let bydone t =
 ;;
 
 let we_need_to_prove t id ty =
+(*BUG: ty not used *)
  let aux status =
   let proof,goals =
    ProofEngineTypes.apply_tactic
@@ -80,10 +83,98 @@ let we_need_to_prove t id ty =
   ProofEngineTypes.mk_tactic aux
 ;;
 
-let prova _ = assert false
-;;
-let bywehave _ = assert false
+let existselim t id1 t1 id2 t2 =
+(*BUG: t1 and t2 not used *)
+(*PARSING BUG: t2 is parsed in the current context, but it may
+  have occurrences of id1 in it *)
+ Tactics.elim_intros t
+  ~mk_fresh_name_callback:
+    (let i = ref 0 in
+      fun _ _ _  ~typ ->
+       incr i;
+       if !i = 1 then Cic.Name id1 else Cic.Name id2)
+
+let andelim = existselim;;
+
+let rewritingstep lhs rhs just conclude =
+ let aux ((proof,goal) as status) =
+  let (curi,metasenv,proofbo,proofty) = proof in
+  let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let eq,trans =
+   match LibraryObjects.eq_URI () with
+      None -> assert false (*TODO*)
+    | Some uri ->
+      Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
+  in
+  let ty,_ =
+   CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
+  let just =
+   match just with
+      None -> assert false (*TOOD*)
+    | Some just -> just
+  in
+   match lhs with
+      None ->
+       let plhs,prhs =
+        match 
+         fst
+          (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1)
+            CicUniv.empty_ugraph)
+        with
+           Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
+         | _ -> assert false in
+       let last_hyp_name =
+        match context with
+           (Some (Cic.Name id,_))::_ -> id
+         | _ -> assert false
+       in
+        (match conclude with
+            None ->
+             ProofEngineTypes.apply_tactic
+              (Tacticals.thens
+                ~start:(Tactics.apply ~term:trans)
+                ~continuations:
+                  [ Tactics.apply prhs ;
+                    Tactics.apply (Cic.Rel 1) ;
+                    Tactics.apply just]) status
+          | Some name ->
+             let mk_fresh_name_callback =
+             fun metasenv context _ ~typ ->
+               FreshNamesGenerator.mk_fresh_name ~subst:[]
+                metasenv context name ~typ
+            in
+              ProofEngineTypes.apply_tactic
+               (Tacticals.thens
+                 ~start:(Tactics.cut ~mk_fresh_name_callback
+                 (Cic.Appl [eq ; ty ; plhs ; rhs]))
+                 ~continuations:
+                   [ Tactics.clear ~hyps:[last_hyp_name] ;
+                     Tacticals.thens
+                      ~start:(Tactics.apply ~term:trans)
+                      ~continuations:
+                        [ Tactics.apply prhs ;
+                          Tactics.apply (Cic.Rel 1) ;
+                          Tactics.apply just]
+                   ]) status)
+    | Some lhs ->
+       match conclude with
+          None -> ProofEngineTypes.apply_tactic (Tactics.apply just) status
+        | Some name ->
+            let mk_fresh_name_callback =
+            fun metasenv context _ ~typ ->
+              FreshNamesGenerator.mk_fresh_name ~subst:[]
+               metasenv context name ~typ
+           in
+             ProofEngineTypes.apply_tactic
+              (Tacticals.thens
+                ~start:
+                  (Tactics.cut ~mk_fresh_name_callback
+                    (Cic.Appl [eq ; ty ; lhs ; rhs]))
+                ~continuations:[ Tacticals.id_tac ; Tactics.apply just ]) status
+ in
+  ProofEngineTypes.mk_tactic aux
 ;;
+
 let case _ = assert false
 ;;
 let thesisbecomes _ = assert false
@@ -92,4 +183,3 @@ let byinduction _ = assert false
 ;;
 let we_proceed_by_induction_on _ = assert false
 ;;
-let let1 _ = assert false