]> matita.cs.unibo.it Git - helm.git/commitdiff
Hypotheses patterns for elim implemented. No more need to generalize in advance.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 8 Jun 2008 13:44:20 +0000 (13:44 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 8 Jun 2008 13:44:20 +0000 (13:44 +0000)
helm/software/components/tactics/compose.ml
helm/software/components/tactics/equalityTactics.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/primitiveTactics.mli
helm/software/components/tactics/proofEngineHelpers.ml
helm/software/components/tactics/proofEngineHelpers.mli
helm/software/components/tactics/tactics.ml
helm/software/components/tactics/tactics.mli
helm/software/components/tactics/variousTactics.ml
helm/software/components/tactics/variousTactics.mli
helm/software/matita/tests/elim_pattern.ma [new file with mode: 0644]

index 6bc3dd0fa2160dac8117a9d64f52f94f4a1870b2..e009010a7648980a9d979df0bd65b7edc781adc4 100644 (file)
@@ -125,7 +125,7 @@ let compose_core t2 t1 (proof, goal) =
         in
         let proof, gl = 
           ProofEngineTypes.apply_tactic
-            (VariousTactics.generalize_tac (Some (lazy_of t), [], None))
+            (PrimitiveTactics.generalize_tac (Some (lazy_of t), [], None))
             (proof,goal)
         in
         assert(List.length gl = 1);
index 47f422f52dbbd0c3801784314334dc0b83cc9822..82c339ae2b3d13381b6f1fee090eb1721f190fb9 100644 (file)
@@ -70,15 +70,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
    match hyps_pat with
       [] -> None,true,(fun ~term _ -> P.exact_tac term),concl_pat,gty
     | [name,pat] ->
-      let rec find_hyp n =
-       function
-          [] -> assert false
-        | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
-           Cic.Rel n, S.lift n ty
-        | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
-        | _::tl -> find_hyp (n+1) tl
-      in
-       let arg,gty = find_hyp 1 context in
+       let arg,gty = ProofEngineHelpers.find_hyp name context in
        let dummy = "dummy" in
         Some arg,false,
          (fun ~term typ ->
index 3822b7eac075fd825a98b79b1383a5880dab1535..7014a59417ceb21743aaa073ef17526a74528df3 100644 (file)
@@ -514,20 +514,17 @@ let mk_predicate_for_elim
 (* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
         let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in
          let argty = CicReduction.whd context argty in         
-              let fresh_name = 
+         let fresh_name = 
             FreshNamesGenerator.mk_fresh_name 
-            ~subst:[] metasenv context' C.Anonymous ~typ:argty
-         in
+            ~subst:[] metasenv context' C.Anonymous ~typ:argty in
         let hyp = Some (fresh_name, C.Decl argty) in
          let lazy_term c m u =  
-            let distance  = List.length c - List.length context in
-            S.lift distance arg, m, u
-         in
+          let distance  = List.length c - List.length context in
+           S.lift distance arg, m, u in
          let pattern = Some lazy_term, [], Some cpattern' in
          let subst, metasenv, _ugraph, _conjecture, selected_terms =
-            ProofEngineHelpers.select
-            ~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern
-         in
+          ProofEngineHelpers.select ~metasenv ~ugraph
+           ~conjecture:(0, context, pred) ~pattern in
          let metasenv = MS.apply_subst_metasenv subst metasenv in  
          let map (_context_of_t, t) l = t :: l in
          let what = List.fold_right map selected_terms [] in
@@ -607,17 +604,184 @@ let beta_after_elim_tac upto predicate =
       PET.apply_tactic tactic status
    in
    PET.mk_tactic beta_after_elim_tac
-   
+
+(* ANCORA DA DEBUGGARE *)
+
+exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;;
+exception TheSelectedTermsMustLiveInTheGoalContext
+exception AllSelectedTermsMustBeConvertible;;
+exception GeneralizationInHypothesesNotImplementedYet;;
+
+let generalize_tac 
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ pattern
+ =
+  let module PET = ProofEngineTypes in
+  let generalize_tac mk_fresh_name_callback
+       ~pattern:(term,hyps_pat,concl_pat) status
+  =
+   if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet;
+   let (proof, goal) = status in
+   let module C = Cic in
+   let module T = Tacticals in
+    let uri,metasenv,_subst,pbo,pty, attrs = proof in
+    let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
+    let subst,metasenv,u,selected_hyps,terms_with_context =
+     ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
+      ~conjecture ~pattern in
+    let context = CicMetaSubst.apply_subst_context subst context in
+    let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+    let pbo = CicMetaSubst.apply_subst subst pbo in
+    let pty = CicMetaSubst.apply_subst subst pty in
+    let term =
+     match term with
+        None -> None
+      | Some term ->
+          Some (fun context metasenv ugraph -> 
+                  let term, metasenv, ugraph = term context metasenv ugraph in
+                   CicMetaSubst.apply_subst subst term,
+                    CicMetaSubst.apply_subst_metasenv subst metasenv,
+                    ugraph)
+    in
+    let u,typ,term, metasenv' =
+     let context_of_t, (t, metasenv, u) =
+      match terms_with_context, term with
+         [], None ->
+          raise
+           UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
+       | [], Some t -> context, t context metasenv u
+       | (context_of_t, _)::_, Some t -> 
+           context_of_t, t context_of_t metasenv u
+       | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u)
+     in
+      let t,subst,metasenv' =
+       try
+        CicMetaSubst.delift_rels [] metasenv
+         (List.length context_of_t - List.length context) t
+       with
+        CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+         raise TheSelectedTermsMustLiveInTheGoalContext
+      in
+       (*CSC: I am not sure about the following two assertions;
+         maybe I need to propagate the new subst and metasenv *)
+       assert (subst = []);
+       assert (metasenv' = metasenv);
+       let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in
+        u,typ,t,metasenv
+    in
+    (* We need to check:
+        1. whether they live in the context of the goal;
+           if they do they are also well-typed since they are closed subterms
+           of a well-typed term in the well-typed context of the well-typed
+           term
+        2. whether they are convertible
+    *)
+    ignore (
+     List.fold_left
+      (fun u (context_of_t,t) ->
+        (* 1 *)
+        let t,subst,metasenv'' =
+         try
+          CicMetaSubst.delift_rels [] metasenv'
+           (List.length context_of_t - List.length context) t
+         with
+          CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+           raise TheSelectedTermsMustLiveInTheGoalContext in
+        (*CSC: I am not sure about the following two assertions;
+          maybe I need to propagate the new subst and metasenv *)
+        assert (subst = []);
+        assert (metasenv'' = metasenv');
+        (* 2 *)
+        let b,u1 = CicReduction.are_convertible ~subst context term t u in 
+         if not b then 
+          raise AllSelectedTermsMustBeConvertible
+         else
+          u1
+      ) u terms_with_context) ;
+    let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in
+    let proof,goals =
+     PET.apply_tactic 
+      (T.thens 
+        ~start:
+          (cut_tac 
+           (C.Prod(
+             (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), 
+             typ,
+             (ProofEngineReduction.replace_lifting_csc 1
+               ~equality:(==) 
+               ~what:(List.map snd terms_with_context)
+               ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context)
+               ~where:ty)
+           )))
+        ~continuations:
+          [(apply_tac ~term:(C.Appl [C.Rel 1; CicSubstitution.lift 1 term])) ;
+            T.id_tac])
+        status
+    in
+     let _,metasenv'',_subst,_,_, _ = proof in
+      (* CSC: the following is just a bad approximation since a meta
+         can be closed and then re-opened! *)
+      (proof,
+        goals @
+         (List.filter
+           (fun j -> List.exists (fun (i,_,_) -> i = j) metasenv'')
+           (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
+             ~newmetasenv:metasenv')))
+ in
+  PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
+;;
+
+let generalize_pattern_tac pattern =
+ let generalize_pattern_tac (proof,goal) =
+   let _,metasenv,_,_,_,_ = proof in
+   let conjecture = CicUtil.lookup_meta goal metasenv in
+   let _,context,_ = conjecture in 
+   let generalize_hyps =
+    let _,hpatterns,_ = ProofEngineHelpers.sort_pattern_hyps context pattern in
+     List.map fst hpatterns in
+   let ids_and_patterns =
+    List.map
+     (fun id ->
+       let rel,_ = ProofEngineHelpers.find_hyp id context in
+        id,(Some (PET.const_lazy_term rel), [], None)
+     ) generalize_hyps in
+   let tactics =
+    List.map
+     (function (id,pattern) ->
+       Tacticals.then_ ~start:(generalize_tac pattern)
+        ~continuation:(Tacticals.try_tactic
+          (ProofEngineStructuralRules.clear [id]))
+     ) ids_and_patterns
+   in
+    PET.apply_tactic (Tacticals.seq tactics) (proof,goal)
+ in
+  PET.mk_tactic (generalize_pattern_tac)
+;;
+
+let pattern_after_generalize_pattern_tac (tp, hpatterns, cpattern) =
+ let cpattern =
+  match cpattern with
+     None -> ProofEngineTypes.hole
+   | Some t -> t
+ in
+ let cpattern =
+  List.fold_left
+   (fun t (_,ty) -> Cic.Prod (Cic.Anonymous, ty, t)) cpattern hpatterns
+ in
+  tp, [], Some cpattern
+;;
+
 let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = 
- let elim_tac (proof, goal) =
-   let cpattern = match pattern with 
-      | None, [], Some cpattern -> cpattern
-      | _                       -> raise (PET.Fail (lazy "not implemented"))
-   in    
+ let elim_tac pattern (proof, goal) =
    let ugraph = CicUniv.oblivion_ugraph in
    let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
    let conjecture = CicUtil.lookup_meta goal metasenv in
    let metano, context, ty = conjecture in 
+   let pattern = pattern_after_generalize_pattern_tac pattern in
+   let cpattern =
+    match pattern with 
+      | None, [], Some cpattern -> cpattern
+      | _ -> raise (PET.Fail (lazy "not implemented")) in    
     let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in
     let termty = CicReduction.whd context termty in
     let termty, metasenv', arguments, _fresh_meta =
@@ -710,7 +874,16 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
          (T.then_ ~start:(PET.mk_tactic (fun _ -> res)) ~continuation)
          dummy_status
    in
-   PET.mk_tactic elim_tac
+   let reorder_pattern ((proof, goal) as status) =
+     let _,metasenv,_,_,_,_ = proof in
+     let conjecture = CicUtil.lookup_meta goal metasenv in
+     let _,context,_ = conjecture in
+     let pattern = ProofEngineHelpers.sort_pattern_hyps context pattern in
+      PET.apply_tactic
+       (Tacticals.then_ ~start:(generalize_pattern_tac pattern)
+         ~continuation:(PET.mk_tactic (elim_tac pattern))) status
+   in
+    PET.mk_tactic reorder_pattern
 ;;
 
 let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
index 492fbf601c8d53c2edb4061a13e733e72798fd80..95ba654f50815965c1925d7a5dce63a05c043861 100644 (file)
@@ -42,6 +42,15 @@ val classify_metas :
   (Cic.term * Cic.context * Cic.term) list *
   (Cic.term * Cic.context * Cic.term) list
 
+(* Not primitive, but useful for elim *)
+
+exception AllSelectedTermsMustBeConvertible;;
+
+val generalize_tac:
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ ProofEngineTypes.lazy_pattern ->
+   ProofEngineTypes.tactic
+
 (* ALB, needed by the new paramodulation... *)
 val apply_with_subst:
   term:Cic.term -> ?subst:Cic.substitution -> ?maxmeta:int -> ProofEngineTypes.proof * int ->
index 7d223a4437b4d9fe232032315b9ec8c933a17a6a..e45c13257d54003e2dbee36171e84463417127e1 100644 (file)
@@ -640,6 +640,32 @@ let lookup_type metasenv context hyp =
    in
    aux 1 context
 
+let find_hyp name =
+ let rec find_hyp n =
+  function
+     [] -> assert false
+   | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
+      Cic.Rel n, CicSubstitution.lift n ty
+   | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
+   | _::tl -> find_hyp (n+1) tl
+ in
+  find_hyp 1
+;;
+
+(* sort pattern hypotheses from the smallest to the highest Rel *)
+let sort_pattern_hyps context (t,hpatterns,cpattern) =
+ let hpatterns =
+  List.sort
+   (fun (id1,_) (id2,_) ->
+     let t1,_ = find_hyp id1 context in
+     let t2,_ = find_hyp id2 context in
+     match t1,t2 with
+        Cic.Rel n1, Cic.Rel n2 -> compare n1 n2
+      | _,_ -> assert false) hpatterns
+ in
+  t,hpatterns,cpattern
+;;
+
 (* FG: **********************************************************************)
 
 let get_name context index =
index a51213f9377635aa5a4d8dacde53eedb9976f67c..71486050195dcd55b95961c3c2545e1d304d971f 100644 (file)
@@ -109,6 +109,13 @@ val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
 (* orders a metasenv w.r.t. dependency among metas *)
 val sort_metasenv: Cic.metasenv -> Cic.metasenv
 
+(* finds an hypothesis by name in the context *)
+val find_hyp: string -> Cic.context -> Cic.term * Cic.term
+
+(* sort pattern hypotheses from the smallest to the highest Rel *)
+val sort_pattern_hyps:
+ Cic.context -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.lazy_pattern
+
 
 (* FG: some helper functions ************************************************)
 
index b941a8752a3b1d9c36b340717d054ec09ac87bd4..832469ae69b4a0a1329393a15b00c8b2f588df96 100644 (file)
@@ -49,7 +49,7 @@ let fail = Tacticals.fail_tac
 let fold = ReductionTactics.fold_tac
 let fourier = FourierR.fourier_tac
 let fwd_simpl = FwdSimplTactic.fwd_simpl_tac
-let generalize = VariousTactics.generalize_tac
+let generalize = PrimitiveTactics.generalize_tac
 let id = Tacticals.id_tac
 let intros = PrimitiveTactics.intros_tac
 let inversion = Inversion.inversion_tac
index 3c27f52f41a891f0dc70ebb10bee158b986071f5..c75f183e45a48821c7d6b9067a8227be21d85b67 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Mar 20 16:36:00 CET 2008 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Sat Jun  7 20:09:50 CEST 2008 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
index 28dc4575d6f9e7ac56ac78ad3e5526883cb55725..4652899f038fea8a568b5c624426baac01e0362c 100644 (file)
@@ -56,130 +56,3 @@ let assumption_tac =
  in
   PET.mk_tactic assumption_tac
 ;;
-
-(* ANCORA DA DEBUGGARE *)
-
-exception UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly;;
-exception TheSelectedTermsMustLiveInTheGoalContext
-exception AllSelectedTermsMustBeConvertible;;
-exception GeneralizationInHypothesesNotImplementedYet;;
-
-let generalize_tac 
- ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- pattern
- =
-  let module PET = ProofEngineTypes in
-  let generalize_tac mk_fresh_name_callback
-       ~pattern:(term,hyps_pat,concl_pat) status
-  =
-   if hyps_pat <> [] then raise GeneralizationInHypothesesNotImplementedYet;
-   let (proof, goal) = status in
-   let module C = Cic in
-   let module P = PrimitiveTactics in
-   let module T = Tacticals in
-    let uri,metasenv,_subst,pbo,pty, attrs = proof in
-    let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
-    let subst,metasenv,u,selected_hyps,terms_with_context =
-     ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
-      ~conjecture ~pattern in
-    let context = CicMetaSubst.apply_subst_context subst context in
-    let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-    let pbo = CicMetaSubst.apply_subst subst pbo in
-    let pty = CicMetaSubst.apply_subst subst pty in
-    let term =
-     match term with
-        None -> None
-      | Some term ->
-          Some (fun context metasenv ugraph -> 
-                  let term, metasenv, ugraph = term context metasenv ugraph in
-                   CicMetaSubst.apply_subst subst term,
-                    CicMetaSubst.apply_subst_metasenv subst metasenv,
-                    ugraph)
-    in
-    let u,typ,term, metasenv' =
-     let context_of_t, (t, metasenv, u) =
-      match terms_with_context, term with
-         [], None ->
-          raise
-           UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
-       | [], Some t -> context, t context metasenv u
-       | (context_of_t, _)::_, Some t -> 
-           context_of_t, t context_of_t metasenv u
-       | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u)
-     in
-      let t,subst,metasenv' =
-       try
-        CicMetaSubst.delift_rels [] metasenv
-         (List.length context_of_t - List.length context) t
-       with
-        CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-         raise TheSelectedTermsMustLiveInTheGoalContext
-      in
-       (*CSC: I am not sure about the following two assertions;
-         maybe I need to propagate the new subst and metasenv *)
-       assert (subst = []);
-       assert (metasenv' = metasenv);
-       let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in
-        u,typ,t,metasenv
-    in
-    (* We need to check:
-        1. whether they live in the context of the goal;
-           if they do they are also well-typed since they are closed subterms
-           of a well-typed term in the well-typed context of the well-typed
-           term
-        2. whether they are convertible
-    *)
-    ignore (
-     List.fold_left
-      (fun u (context_of_t,t) ->
-        (* 1 *)
-        let t,subst,metasenv'' =
-         try
-          CicMetaSubst.delift_rels [] metasenv'
-           (List.length context_of_t - List.length context) t
-         with
-          CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-           raise TheSelectedTermsMustLiveInTheGoalContext in
-        (*CSC: I am not sure about the following two assertions;
-          maybe I need to propagate the new subst and metasenv *)
-        assert (subst = []);
-        assert (metasenv'' = metasenv');
-        (* 2 *)
-        let b,u1 = CicReduction.are_convertible ~subst context term t u in 
-         if not b then 
-          raise AllSelectedTermsMustBeConvertible
-         else
-          u1
-      ) u terms_with_context) ;
-    let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in
-    let proof,goals =
-     PET.apply_tactic 
-      (T.thens 
-        ~start:
-          (P.cut_tac 
-           (C.Prod(
-             (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), 
-             typ,
-             (ProofEngineReduction.replace_lifting_csc 1
-               ~equality:(==) 
-               ~what:(List.map snd terms_with_context)
-               ~with_what:(List.map (function _ -> C.Rel 1) terms_with_context)
-               ~where:ty)
-           )))
-        ~continuations:
-          [(P.apply_tac ~term:(C.Appl [C.Rel 1; CicSubstitution.lift 1 term])) ;
-            T.id_tac])
-        status
-    in
-     let _,metasenv'',_subst,_,_, _ = proof in
-      (* CSC: the following is just a bad approximation since a meta
-         can be closed and then re-opened! *)
-      (proof,
-        goals @
-         (List.filter
-           (fun j -> List.exists (fun (i,_,_) -> i = j) metasenv'')
-           (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
-             ~newmetasenv:metasenv')))
- in
-  PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern)
-;;
index 35576326eb2dbc2f6ffa1e0f4b7adb6744908acc..3ce6c47e8a400b95118a10d687161a58ad81edcc 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-exception AllSelectedTermsMustBeConvertible;;
-
 val assumption_tac: ProofEngineTypes.tactic
-
-val generalize_tac:
- ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ProofEngineTypes.lazy_pattern ->
-   ProofEngineTypes.tactic
-
diff --git a/helm/software/matita/tests/elim_pattern.ma b/helm/software/matita/tests/elim_pattern.ma
new file mode 100644 (file)
index 0000000..688e1d4
--- /dev/null
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "nat/plus.ma".
+
+alias num (instance 0) = "natural number".
+lemma ex1: ∀n:nat. n ≠ n+0 → n = O+O → (∀n1.¬¬(n≠n1+O)) → False.
+ intros (n U V K);
+ elim n in U:(? (? ? ? %)) ⊢ %;
+  [ apply (H V)
+  | apply (K ? H)]
+qed.
\ No newline at end of file