decompose: delta-expansion of the type to eliminate now works fine

diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml
index 5bcdb5b8a22d315155bd9407b93af43bdcf70218..e74886e95e1146235ef0114fd3b350d4360a5e13 100644 (file)
--- a/helm/software/components/tactics/eliminationTactics.ml
+++ b/helm/software/components/tactics/eliminationTactics.ml
@@ -53,10 +53,6 @@ let split c t =
 
 (****************************************************************************)
 
-type type_class = Other
-                | Ind
-               | Con of C.lazy_term
-
 let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None 
 
 let get_inductive_def uri =
@@ -73,32 +69,35 @@ let is_not_recursive uri tyno tys =
       let premises, _ = split [] ty in
       List.fold_left map mutinds (List.tl premises)
    in
+   let msg = "recursiveness check non implemented for mutually inductive types" in
+   if List.length tys > 1 then raise (PET.Fail (lazy msg)) else
    let _, _, _, constructors = List.nth tys tyno in
    let mutinds = List.fold_left map I.S.empty constructors in
    I.S.is_empty mutinds
 
-let rec check_type sorts metasenv context = function 
-   | C.MutInd (uri, tyno, _) as t -> 
-      let lpsno, tys = get_inductive_def uri in
-      let _, inductive, arity, _ = List.nth tys tyno in
-      let _, psno = split [] arity in
-      let not_relation = (lpsno = psno) in
-      let not_recursive = is_not_recursive uri tyno tys in
-      let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
-      let sort = match split context ty_ty with
-         | C.Sort sort ::_ , _ -> CicPp.ppsort sort
-        | C.Meta _ :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
-        | _                   -> assert false
-      in
-      let right_sort = List.mem sort sorts in
-      if not_relation && inductive && not_recursive && right_sort then 
-      (HLog.warn (Printf.sprintf "Decomposing %s %u %b %u %u %b" (UriManager.string_of_uri uri) (succ tyno) inductive lpsno psno not_recursive);
-      Ind) 
-      else Other 
-(*   | C.Const (uri, _) as t     -> 
-      if List.mem (uri, None) types then Con (PET.const_lazy_term t) else Other
-*)   | C.Appl (hd :: tl)         -> check_type sorts metasenv context hd
-   | _                         -> Other
+let rec check_type sorts metasenv context t = 
+   match R.whd ~delta:true context t with
+      | C.MutInd (uri, tyno, _) as t -> 
+         let lpsno, tys = get_inductive_def uri in
+         let _, inductive, arity, _ = List.nth tys tyno in
+         let _, psno = split [] arity in
+         let not_relation = (lpsno = psno) in
+         let not_recursive = is_not_recursive uri tyno tys in
+         let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
+         let sort = match split context ty_ty with
+            | C.Sort sort ::_ , _ -> CicPp.ppsort sort
+           | C.Meta _ :: _, _    -> CicPp.ppsort (C.Type (Un.fresh ()))
+           | _                   -> assert false
+         in
+         let right_sort = List.mem sort sorts in
+         if not_relation && inductive && not_recursive && right_sort then
+        begin
+            HLog.warn (Printf.sprintf "Decomposing %s %u" (UriManager.string_of_uri uri) (succ tyno));
+            true 
+         end
+        else false 
+      | C.Appl (hd :: tl)         -> check_type sorts metasenv context hd
+      | _                         -> false
 
 (* unexported tactics *******************************************************)
 
@@ -128,11 +127,11 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
       let _, metasenv, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = H.lookup_type metasenv context what in
-      let tac = match check_type sorts metasenv context (S.lift index ty) with 
-         | Ind   -> T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
-                           ~continuation:(PESR.clear [what])
-         | Con t -> RT.unfold_tac (Some t) ~pattern:(premise_pattern what)
-        | Other -> 
+      let tac = 
+         if check_type sorts metasenv context (S.lift index ty) then 
+            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
+                   ~continuation:(PESR.clear [what])
+        else 
            let msg = "unexported elim_clear: not an decomposable type" in
            raise (PET.Fail (lazy msg))
       in
@@ -169,7 +168,7 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s)))
 
 (* roba seria ------------------------------------------------------------- *)
 
-let decompose_tac ?(sorts=[CicPp.ppsort C.Prop]) 
+let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp]) 
                   ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
    let decompose_tac status =
       let (proof, goal) = status in

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 193a0e3310f489c1c587955cc1a3210deed2f4a3..e03dece5bc1bd8ea612d0b4fdfe4153b66d9d899 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -519,10 +519,10 @@
           <term>Action:</term>
           <listitem>
             <para>
-            For each each premise <command>H</command> 
-            of type <command>T</command> in the current context
-            where <command>T</command> is a non-recursive inductive type
-            of sort Prop without right parameters, the tactic runs
+            For each each premise <command>H</command> of type 
+            <command>T</command> in the current context where
+            <command>T</command> is a non-recursive inductive type without
+            right parameters and of sort Prop or CProp, the tactic runs
             <command> 
              elim H as H<subscript>1</subscript> ... H<subscript>m</subscript>
             </command>, clears <command>H</command>  and runs itself

diff --git a/helm/software/matita/help/C/tactics_quickref.xml b/helm/software/matita/help/C/tactics_quickref.xml
index 47e237e86c08b960bdaf2a183f3e59423c0ca82a..70d42ac2b59891d92a7614952cde0d91706a6856 100644 (file)
--- a/helm/software/matita/help/C/tactics_quickref.xml
+++ b/helm/software/matita/help/C/tactics_quickref.xml
@@ -81,10 +81,6 @@
         <entry>|</entry>
         <entry>
             <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
-            [<emphasis role="bold">(</emphasis>
-            <emphasis><link linkend="grammar.id">id</link></emphasis>…
-            <emphasis role="bold">)</emphasis>]
-            [<emphasis><link linkend="grammar.id">id</link></emphasis>] 
             [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
            </entry>
       </row>

diff --git a/helm/software/matita/tests/decompose.ma b/helm/software/matita/tests/decompose.ma
index 815fcf66c7d57faa6e71d38bf4ccbb71ba6fd9c7..2ba58c158c3adf50edd95475d6330272d3cb87b3 100644 (file)
--- a/helm/software/matita/tests/decompose.ma
+++ b/helm/software/matita/tests/decompose.ma
@@ -13,14 +13,17 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/decompose".
-include "../legacy/coq.ma".
-alias symbol "and" (instance 0) = "Coq's logical and".
-alias symbol "or" (instance 0) = "Coq's logical or".
-
 
+include "logic/connectives.ma".
 
 theorem stupid: 
   \forall a,b,c:Prop.
   (a \land c \lor b \land c) \to (c \land (b \lor a)).
   intros.decompose.split.assumption.right.assumption.
   split.assumption.left.assumption.qed.
+
+definition MyFalse \def False.
+
+theorem ex_falso_quodlibet: \forall (P:Prop). MyFalse \to P.
+ intros. decompose.
+qed.