From 00e0c1d5cff8d5b5588185e1a70352a2e7a1a8e9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 25 Feb 2007 16:28:38 +0000 Subject: [PATCH] RELATIONAL: new undecomposable definition of NLE Procedural: some refactoring decompose tactic: only types of sort Prop are decomposed now --- .../acic_procedural/acic2Procedural.ml | 9 +- .../acic_procedural/proceduralClassify.ml | 71 ++--------- .../acic_procedural/proceduralClassify.mli | 8 +- helm/software/components/cic/.depend | 2 + helm/software/components/cic/.depend.opt | 2 + helm/software/components/cic/Makefile | 5 +- helm/software/components/cic/cicInspect.ml | 111 ++++++++++++++++++ helm/software/components/cic/cicInspect.mli | 32 +++++ .../components/tactics/eliminationTactics.ml | 56 ++++++--- .../components/tactics/eliminationTactics.mli | 1 + helm/software/components/tactics/tactics.mli | 3 +- .../matita/contribs/RELATIONAL/NLE/defs.ma | 6 +- .../matita/contribs/RELATIONAL/NLE/inv.ma | 32 ++--- .../matita/contribs/RELATIONAL/NLE/nplus.ma | 4 + .../matita/contribs/RELATIONAL/NLE/props.ma | 59 +--------- helm/software/matita/help/C/sec_tactics.xml | 2 +- 16 files changed, 244 insertions(+), 159 deletions(-) create mode 100644 helm/software/components/cic/cicInspect.ml create mode 100644 helm/software/components/cic/cicInspect.mli diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 22936c1a4..42214b57b 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -24,6 +24,7 @@ *) module C = Cic +module I = CicInspect module D = Deannotate module DTI = DoubleTypeInference module TC = CicTypeChecker @@ -286,13 +287,13 @@ and mk_proof st = function let decurry = List.length classes - List.length tl in if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else - let synth = Cl.S.singleton 0 in + let synth = I.S.singleton 0 in let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in match rc with | Some (i, j) when i > 1 && i <= List.length classes -> let classes, tl, _, what = split2_last classes tl in let script, what = mk_atomic st dtext what in - let synth = Cl.S.add 1 synth in + let synth = I.S.add 1 synth in let qs = mk_bkd_proofs (next st) synth classes tl in if is_rewrite_right hd then List.rev script @ convert st t @ @@ -330,8 +331,8 @@ and mk_bkd_proofs st synth classes ts = try let _, dtext = test_depth st in let aux inv v = - if Cl.overlaps synth inv then None else - if Cl.S.is_empty inv then Some (mk_proof st v) else + if I.overlaps synth inv then None else + if I.S.is_empty inv then Some (mk_proof st v) else Some [T.Apply (v, dtext ^ "dependent")] in T.list_map2_filter aux classes ts diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml index 4cfd47e5a..6fd8a5e60 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.ml +++ b/helm/software/components/acic_procedural/proceduralClassify.ml @@ -26,19 +26,15 @@ module C = Cic module R = CicReduction module D = Deannotate -module Int = struct - type t = int - let compare = compare -end -module S = Set.Make (Int) +module I = CicInspect type conclusion = (int * int) option (* debugging ****************************************************************) let string_of_entry inverse = - if S.mem 0 inverse then "C" else - if S.is_empty inverse then "I" else "P" + if I.S.mem 0 inverse then "C" else + if I.S.is_empty inverse then "I" else "P" let to_string (classes, rc) = let linearize = String.concat " " (List.map string_of_entry classes) in @@ -49,7 +45,7 @@ let to_string (classes, rc) = let out_table b = let map i (_, inverse) = let map i tl = Printf.sprintf "%2u" i :: tl in - let iset = String.concat " " (S.fold map inverse []) in + let iset = String.concat " " (I.S.fold map inverse []) in Printf.eprintf "%2u|%s\n" i iset in Array.iteri map b; @@ -59,47 +55,6 @@ let out_table b = let id x = x -let rec list_fold_left g map = function - | [] -> g - | hd :: tl -> map (list_fold_left g map tl) hd - -let get_rels h t = - let rec aux d g = function - | C.Sort _ - | C.Implicit _ -> g - | C.Rel i -> - if i < d then g else fun a -> g (S.add (i - d + h + 1) a) - | C.Appl ss -> list_fold_left g (aux d) ss - | C.Const (_, ss) - | C.MutInd (_, _, ss) - | C.MutConstruct (_, _, _, ss) - | C.Var (_, ss) -> - let map g (_, t) = aux d g t in - list_fold_left g map ss - | C.Meta (_, ss) -> - let map g = function - | None -> g - | Some t -> aux d g t - in - list_fold_left g map ss - | C.Cast (t1, t2) -> aux d (aux d g t2) t1 - | C.LetIn (_, t1, t2) - | C.Lambda (_, t1, t2) - | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1 - | C.MutCase (_, _, t1, t2, ss) -> - aux d (aux d (list_fold_left g (aux d) ss) t2) t1 - | C.Fix (_, ss) -> - let k = List.length ss in - let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in - list_fold_left g map ss - | C.CoFix (_, ss) -> - let k = List.length ss in - let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in - list_fold_left g map ss - in - let g a = a in - aux 1 g t S.empty - let split c t = let add s v c = Some (s, C.Decl v) :: c in let rec aux whd a n c = function @@ -118,32 +73,28 @@ let classify c t = try let vs, h = split c t in let rc = classify_conclusion (List.hd vs) in - let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in + let map (b, h) v = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in let l, h = List.fold_left map ([], 0) vs in let b = Array.of_list (List.rev l) in let mk_closure b h = - let map j = if j < h then S.union (fst b.(j)) else id in + let map j = if j < h then I.S.union (fst b.(j)) else id in for i = pred h downto 0 do let direct, unused = b.(i) in - b.(i) <- S.fold map direct direct, unused + b.(i) <- I.S.fold map direct direct, unused done; b in let b = mk_closure b h in let rec mk_inverse i direct = - if S.is_empty direct then () else - let j = S.choose direct in + if I.S.is_empty direct then () else + let j = I.S.choose direct in if j < h then let unused, inverse = b.(j) in - b.(j) <- unused, S.add i inverse + b.(j) <- unused, I.S.add i inverse else (); - mk_inverse i (S.remove j direct) + mk_inverse i (I.S.remove j direct) in let map i (direct, _) = mk_inverse i direct in Array.iteri map b; (* out_table b; *) List.rev_map snd (List.tl (Array.to_list b)), rc with Invalid_argument _ -> failwith "Classify.classify" - -let overlaps s1 s2 = - let predicate x = S.mem x s1 in - S.exists predicate s2 diff --git a/helm/software/components/acic_procedural/proceduralClassify.mli b/helm/software/components/acic_procedural/proceduralClassify.mli index 79a8f4d9f..35c07ab47 100644 --- a/helm/software/components/acic_procedural/proceduralClassify.mli +++ b/helm/software/components/acic_procedural/proceduralClassify.mli @@ -23,14 +23,10 @@ * http://cs.unibo.it/helm/. *) -module S : Set.S with type elt = int - type conclusion = (int * int) option -val classify: Cic.context -> Cic.term -> S.t list * conclusion - -val to_string: S.t list * conclusion -> string +val classify: Cic.context -> Cic.term -> CicInspect.S.t list * conclusion -val overlaps: S.t -> S.t -> bool +val to_string: CicInspect.S.t list * conclusion -> string val split: Cic.context -> Cic.term -> Cic.term list * int diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend index 7829317ad..0d1e0cafc 100644 --- a/helm/software/components/cic/.depend +++ b/helm/software/components/cic/.depend @@ -25,3 +25,5 @@ discrimination_tree.cmo: cicUtil.cmi cic.cmo discrimination_tree.cmi discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi path_indexing.cmo: cic.cmo path_indexing.cmi path_indexing.cmx: cic.cmx path_indexing.cmi +cicInspect.cmo: cic.cmo cicInspect.cmi +cicInspect.cmx: cic.cmx cicInspect.cmi diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt index 44b016d1c..94eaa78b8 100644 --- a/helm/software/components/cic/.depend.opt +++ b/helm/software/components/cic/.depend.opt @@ -25,3 +25,5 @@ discrimination_tree.cmo: cicUtil.cmi cic.cmx discrimination_tree.cmi discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi path_indexing.cmo: cic.cmx path_indexing.cmi path_indexing.cmx: cic.cmx path_indexing.cmi +cicInspect.cmo: cic.cmx cicInspect.cmi +cicInspect.cmx: cic.cmx cicInspect.cmi diff --git a/helm/software/components/cic/Makefile b/helm/software/components/cic/Makefile index f3d9df425..67979211b 100644 --- a/helm/software/components/cic/Makefile +++ b/helm/software/components/cic/Makefile @@ -8,9 +8,10 @@ INTERFACE_FILES = \ cicParser.mli \ cicUtil.mli \ helmLibraryObjects.mli \ - libraryObjects.mli \ + libraryObjects.mli \ discrimination_tree.mli \ - path_indexing.mli + path_indexing.mli \ + cicInspect.mli IMPLEMENTATION_FILES = \ cic.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi diff --git a/helm/software/components/cic/cicInspect.ml b/helm/software/components/cic/cicInspect.ml new file mode 100644 index 000000000..3d5d65d59 --- /dev/null +++ b/helm/software/components/cic/cicInspect.ml @@ -0,0 +1,111 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module UM = UriManager +module C = Cic + +module Int = struct + type t = int + let compare = compare +end +module S = Set.Make (Int) + +let overlaps s1 s2 = + let predicate x = S.mem x s1 in + S.exists predicate s2 + +let get_rels_from_premise h t = + let rec aux d g = function + | C.Sort _ + | C.Implicit _ -> g + | C.Rel i -> + if i < d then g else fun a -> g (S.add (i - d + h + 1) a) + | C.Appl ss -> List.fold_left (aux d) g ss + | C.Const (_, ss) + | C.MutInd (_, _, ss) + | C.MutConstruct (_, _, _, ss) + | C.Var (_, ss) -> + let map g (_, t) = aux d g t in + List.fold_left map g ss + | C.Meta (_, ss) -> + let map g = function + | None -> g + | Some t -> aux d g t + in + List.fold_left map g ss + | C.Cast (t1, t2) -> aux d (aux d g t2) t1 + | C.LetIn (_, t1, t2) + | C.Lambda (_, t1, t2) + | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1 + | C.MutCase (_, _, t1, t2, ss) -> + aux d (aux d (List.fold_left (aux d) g ss) t2) t1 + | C.Fix (_, ss) -> + let k = List.length ss in + let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in + List.fold_left map g ss + | C.CoFix (_, ss) -> + let k = List.length ss in + let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in + List.fold_left map g ss + in + let g a = a in + aux 1 g t S.empty + +let get_mutinds_of_uri u t = + let rec aux g = function + | C.Sort _ + | C.Implicit _ + | C.Rel _ -> g + | C.Appl ss -> List.fold_left aux g ss + | C.Const (_, ss) + | C.MutConstruct (_, _, _, ss) + | C.Var (_, ss) -> + let map g (_, t) = aux g t in + List.fold_left map g ss + | C.MutInd (uri, tyno, ss) -> + let map g (_, t) = aux g t in + let g = List.fold_left map g ss in + if UM.eq u uri then fun a -> g (S.add tyno a) else g + | C.Meta (_, ss) -> + let map g = function + | None -> g + | Some t -> aux g t + in + List.fold_left map g ss + | C.Cast (t1, t2) -> aux (aux g t2) t1 + | C.LetIn (_, t1, t2) + | C.Lambda (_, t1, t2) + | C.Prod (_, t1, t2) -> aux (aux g t2) t1 + | C.MutCase (_, _, t1, t2, ss) -> + aux (aux (List.fold_left aux g ss) t2) t1 + | C.Fix (_, ss) -> + let map g (_, _, t1, t2) = aux (aux g t2) t1 in + List.fold_left map g ss + | C.CoFix (_, ss) -> + let map g (_, t1, t2) = aux (aux g t2) t1 in + List.fold_left map g ss + in + let g a = a in + aux g t S.empty diff --git a/helm/software/components/cic/cicInspect.mli b/helm/software/components/cic/cicInspect.mli new file mode 100644 index 000000000..c4bcd8aaf --- /dev/null +++ b/helm/software/components/cic/cicInspect.mli @@ -0,0 +1,32 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module S: Set.S with type elt = int + +val overlaps: S.t -> S.t -> bool + +val get_rels_from_premise: int -> Cic.term -> S.t + +val get_mutinds_of_uri: UriManager.uri -> Cic.term -> S.t diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index c98f020d7..5bcdb5b8a 100644 --- a/helm/software/components/tactics/eliminationTactics.ml +++ b/helm/software/components/tactics/eliminationTactics.ml @@ -26,9 +26,12 @@ (* $Id$ *) module C = Cic +module I = CicInspect +module S = CicSubstitution +module TC = CicTypeChecker module P = PrimitiveTactics module T = Tacticals -module S = ProofEngineStructuralRules +module PESR = ProofEngineStructuralRules module F = FreshNamesGenerator module PET = ProofEngineTypes module H = ProofEngineHelpers @@ -56,21 +59,45 @@ type type_class = Other let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None -let get_inductive_type uri tyno = +let get_inductive_def uri = match E.get_obj Un.empty_ugraph uri with | C.InductiveDefinition (tys, _, lpsno, _), _ -> - let _, inductive, arity, _ = List.nth tys tyno in - lpsno, inductive, arity + lpsno, tys | _ -> assert false -let rec check_type = function - | C.MutInd (uri, tyno, _) -> - let lpsno, inductive, arity = get_inductive_type uri tyno in +let is_not_recursive uri tyno tys = + let map mutinds (_, ty) = +(* FG: we can do much better here *) + let map mutinds t = I.S.union mutinds (I.get_mutinds_of_uri uri t) in +(**********************************) + let premises, _ = split [] ty in + List.fold_left map mutinds (List.tl premises) + in + 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 - if lpsno <> psno && inductive then Other else Ind + 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 hd +*) | C.Appl (hd :: tl) -> check_type sorts metasenv context hd | _ -> Other (* unexported tactics *******************************************************) @@ -95,15 +122,15 @@ let rec scan_tac ~old_context_length ~index ~tactic = in PET.mk_tactic scan_tac -let elim_clear_unfold_tac ~mk_fresh_name_callback ~what = +let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what = let elim_clear_unfold_tac status = let (proof, goal) = status in 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 ty with + 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:(S.clear [what]) + ~continuation:(PESR.clear [what]) | Con t -> RT.unfold_tac (Some t) ~pattern:(premise_pattern what) | Other -> let msg = "unexported elim_clear: not an decomposable type" in @@ -142,12 +169,13 @@ let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s))) (* roba seria ------------------------------------------------------------- *) -let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () = +let decompose_tac ?(sorts=[CicPp.ppsort C.Prop]) + ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () = let decompose_tac status = let (proof, goal) = status in let _, metasenv,_,_, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in - let tactic = elim_clear_unfold_tac ~mk_fresh_name_callback in + let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in let old_context_length = List.length context in let tac = scan_tac ~old_context_length ~index:old_context_length ~tactic in diff --git a/helm/software/components/tactics/eliminationTactics.mli b/helm/software/components/tactics/eliminationTactics.mli index 492566042..b203bee22 100644 --- a/helm/software/components/tactics/eliminationTactics.mli +++ b/helm/software/components/tactics/eliminationTactics.mli @@ -28,5 +28,6 @@ val elim_type_tac: ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic val decompose_tac: + ?sorts:string list -> ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index f0ac7adc8..47119060b 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Feb 21 14:36:23 CET 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Sun Feb 25 17:03:54 CET 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -24,6 +24,7 @@ val cut : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> ProofEngineTypes.tactic val decompose : + ?sorts:string list -> ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> ProofEngineTypes.tactic val demodulate : diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma b/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma index 146c274b3..18fc87b10 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma @@ -16,8 +16,10 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/defs". include "NPlus/defs.ma". -inductive NLE (q:Nat) (r:Nat): Prop \def - | nle_nplus: \forall p. (p + q == r) \to NLE q r. +inductive NLE: Nat \to Nat \to Prop \def + | nle_zero_1: \forall q. NLE zero q + | nle_succ_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q) +. (*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'greater or equal to'" 'geq y x= diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma index 67a18d820..bc878009c 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma @@ -14,41 +14,41 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/inv". -include "NPlus/inv.ma". include "NLE/defs.ma". theorem nle_inv_succ_1: \forall x,y. x < y \to \exists z. y = succ z \land x <= z. - intros. elim H. - lapply linear nplus_inv_succ_2 to H1. - decompose. subst. auto depth = 4. + intros. inversion H; clear H; intros; subst; + [ destruct H + | destruct H2. clear H2. subst. auto + ] qed. theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y. - intros. - lapply linear nle_inv_succ_1 to H. decompose. - destruct H1. clear H1. subst. - auto. + intros. inversion H; clear H; intros; subst; + [ destruct H + | destruct H2. destruct H3. clear H2 H3. subst. auto + ] qed. theorem nle_inv_succ_zero: \forall x. x < zero \to False. - intros. - lapply linear nle_inv_succ_1 to H. decompose. - destruct H1. + intros. inversion H; clear H; intros; subst; + [ destruct H + | destruct H3 + ] qed. theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero. - intros 1. elim x; clear x; intros; + intros. inversion H; clear H; intros; subst; [ auto - | lapply linear nle_inv_succ_zero to H1. decompose. + | destruct H3 ]. qed. theorem nle_inv_succ_2: \forall y,x. x <= succ y \to x = zero \lor \exists z. x = succ z \land z <= y. - intros 2; elim x; clear x; intros; + intros. inversion H; clear H; intros; subst; [ auto - | lapply linear nle_inv_succ_succ to H1. - auto depth = 4. + | destruct H3. clear H3. subst. auto depth = 4 ]. qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma b/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma index f469568d7..78ca2e569 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma @@ -16,6 +16,10 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/nplus". include "NLE/defs.ma". +theorem nle_nplus: \forall p, q, r. (p + q == r) \to q <= r. + intros. elim H; clear H q r; auto. +qed. + axiom nle_nplus_comp: \forall x1, x2, x3. (x1 + x2 == x3) \to \forall y1, y2, y3. (y1 + y2 == y3) \to x1 <= y1 \to x2 <= y2 \to x3 <= y3. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma index a6d0ca7a8..db1476309 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma @@ -14,65 +14,18 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/props". -include "NLE/inv.ma". - -theorem nle_zero_1: \forall q. zero <= q. - intros. auto. -qed. - -theorem nle_succ_succ: \forall p,q. p <= q \to succ p <= succ q. - intros. elim H. clear H. auto. -qed. - -theorem nle_ind: \forall P:(Nat \to Nat \to Prop). - (\forall n:Nat.P zero n) \to - (\forall n,n1:Nat. - n <= n1 \to P n n1 \to P (succ n) (succ n1) - ) \to - \forall n,n1:Nat. n <= n1 \to P n n1. - intros 4. elim n; clear n; - [ auto - | lapply linear nle_inv_succ_1 to H3. decompose; subst. - auto - ]. -qed. - -theorem nle_refl: \forall x. x <= x. - intros 1; elim x; clear x; intros; auto. -qed. +include "NLE/order.ma". theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y. - intros. elim H using nle_ind; clear H x y; auto. -qed. - -theorem nle_false: \forall x,y. x <= y \to y < x \to False. - intros 3; elim H using nle_ind; clear H x y; auto. -qed. - -theorem nle_trans: \forall x,y. x <= y \to - \forall z. y <= z \to x <= z. - intros 3. elim H using nle_ind; clear H x y; - [ auto - | lapply linear nle_inv_succ_1 to H3. decompose. subst. - auto - ]. -qed. - -theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y. - intros. elim H using nle_ind; clear H x y; - [ elim n; clear n; auto - | decompose; subst; auto - ]. + intros. elim H; clear H x y; auto. qed. -theorem nle_gt_or_le: \forall x,y. y > x \lor y <= x. +theorem nle_gt_or_le: \forall x, y. y > x \lor y <= x. intros 2; elim y; clear y; [ auto | decompose; - [ lapply linear nle_inv_succ_1 to H1. decompose. - subst. auto depth=4 - | lapply linear nle_lt_or_eq to H1; decompose; - subst; auto - ] + [ lapply linear nle_inv_succ_1 to H1 + | lapply linear nle_lt_or_eq to H1 + ]; decompose; subst; auto depth = 4 ]. qed. diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index cad04a53c..193a0e331 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -522,7 +522,7 @@ For each each premise H of type T in the current context where T is a non-recursive inductive type - withour right parameters, the tactic runs + of sort Prop without right parameters, the tactic runs elim H as H1 ... Hm , clears H and runs itself -- 2.39.2