From 1f974ca07c502d85c9a3760aaaf633bae3c84fb6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 26 Feb 2007 13:36:43 +0000 Subject: [PATCH] decompose: delta-expansion of the type to eliminate now works fine --- .../components/tactics/eliminationTactics.ml | 63 +++++++++---------- helm/software/matita/help/C/sec_tactics.xml | 8 +-- .../matita/help/C/tactics_quickref.xml | 4 -- helm/software/matita/tests/decompose.ma | 11 ++-- 4 files changed, 42 insertions(+), 44 deletions(-) diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index 5bcdb5b8a..e74886e95 100644 --- 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 193a0e331..e03dece5b 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -519,10 +519,10 @@ Action: - For each each premise H - of type T in the current context - where T is a non-recursive inductive type - of sort Prop without right parameters, the tactic runs + For each each premise H of type + T in the current context where + T is a non-recursive inductive type without + right parameters and of sort Prop or CProp, the tactic runs elim H as H1 ... Hm , clears H and runs itself diff --git a/helm/software/matita/help/C/tactics_quickref.xml b/helm/software/matita/help/C/tactics_quickref.xml index 47e237e86..70d42ac2b 100644 --- a/helm/software/matita/help/C/tactics_quickref.xml +++ b/helm/software/matita/help/C/tactics_quickref.xml @@ -81,10 +81,6 @@ | decompose - [( - id… - )] - [id] [as id…] diff --git a/helm/software/matita/tests/decompose.ma b/helm/software/matita/tests/decompose.ma index 815fcf66c..2ba58c158 100644 --- 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. -- 2.39.2