From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 25 Feb 2007 16:28:38 +0000 (+0000)
Subject: RELATIONAL: new undecomposable definition of NLE
X-Git-Tag: make_still_working~6444
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00e0c1d5cff8d5b5588185e1a70352a2e7a1a8e9;p=helm.git

RELATIONAL: new undecomposable definition of NLE
Procedural: some refactoring
decompose tactic: only types of sort Prop are decomposed now
---

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 <command>H</command> 
 	     of type <command>T</command> in the current context
 	     where <command>T</command> is a non-recursive inductive type
-	     withour right parameters, the tactic runs
+	     of sort Prop without right parameters, the tactic runs
 	     <command> 
 	      elim H as H<subscript>1</subscript> ... H<subscript>m</subscript>
 	     </command>, clears <command>H</command>  and runs itself