]> matita.cs.unibo.it Git - helm.git/commitdiff
new implementation of the destruct tactic,
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 6 Nov 2007 19:30:16 +0000 (19:30 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 6 Nov 2007 19:30:16 +0000 (19:30 +0000)
which includes the old subst tactic (now removed)

24 files changed:
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/.depend
helm/software/components/tactics/.depend.opt
helm/software/components/tactics/Makefile
helm/software/components/tactics/destructTactic.ml [new file with mode: 0644]
helm/software/components/tactics/destructTactic.mli [new file with mode: 0644]
helm/software/components/tactics/discriminationTactics.ml [deleted file]
helm/software/components/tactics/discriminationTactics.mli [deleted file]
helm/software/components/tactics/substTactic.ml [deleted file]
helm/software/components/tactics/substTactic.mli [deleted file]
helm/software/components/tactics/tactics.ml
helm/software/components/tactics/tactics.mli
helm/software/matita/library/Fsub/defn.ma
helm/software/matita/library/Fsub/part1a.ma
helm/software/matita/library/Fsub/part1a_inversion.ma
helm/software/matita/library/Fsub/util.ma
helm/software/matita/library/Z/z.ma
helm/software/matita/library/decidable_kit/fgraph.ma
helm/software/matita/library/decidable_kit/list_aux.ma
helm/software/matita/tests/destruct.ma

index a0bb2e4f95501a7018cf16520fcabafd32e79433..3e87ffba5a3b56573bcc5bfb4812c74dd8d354b7 100644 (file)
@@ -71,7 +71,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Cut of loc * 'ident option * 'term
   | Decompose of loc * 'ident option list
   | Demodulate of loc
-  | Destruct of loc * 'term
+  | Destruct of loc * 'term option
   | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern *
            'ident intros_spec
   | ElimType of loc * 'term * 'term option * 'ident intros_spec
@@ -96,7 +96,6 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Right of loc
   | Ring of loc
   | Split of loc
-  | Subst of loc
   | Symmetry of loc
   | Transitivity of loc * 'term
   (* Costruttori Aggiunti *)
index de7af826370d8c87acd36762cf9ac19c4475130c..eb1a18e5ad00d365ba23e3db088b620ece02ceab 100644 (file)
@@ -126,7 +126,8 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
       Printf.sprintf "decompose%s" 
       (pp_intros_specs "names " (None, names)) 
   | Demodulate _ -> "demodulate"
-  | Destruct (_, term) -> "destruct " ^ term_pp term
+  | Destruct (_, None) -> "destruct" 
+  | Destruct (_, Some term) -> "destruct " ^ term_pp term
   | Elim (_, what, using, pattern, specs) ->
       Printf.sprintf "elim %s%s %s%s" 
       (term_pp what)
@@ -177,7 +178,6 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   | Right _ -> "right"
   | Ring _ -> "ring"
   | Split _ -> "split"
-  | Subst _ -> "subst"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
   (* Tattiche Aggiunte *)
index f587d2defcaa207b53eb6c6afd075c1ea5ce967e..0d2fb682ed78b98ec293f6e26b6ce94353a7c1e2 100644 (file)
@@ -95,7 +95,7 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Demodulate _ -> 
       Tactics.demodulate 
        ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
-  | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
+  | GrafiteAst.Destruct (_,xterm) -> Tactics.destruct xterm
   | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
         ~pattern what
@@ -160,7 +160,6 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.Right _ -> Tactics.right
   | GrafiteAst.Ring _ -> Tactics.ring
   | GrafiteAst.Split _ -> Tactics.split
-  | GrafiteAst.Subst _ -> Tactics.subst
   | GrafiteAst.Symmetry _ -> Tactics.symmetry
   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
   (* Implementazioni Aggiunte *)
index d4ab241cbbc64cfe8638980b81e4e051dcf9e57f..2fe6b9aaee80949f0130b972cc8bae673ace256f 100644 (file)
@@ -216,9 +216,11 @@ let rec disambiguate_tactic
          metasenv,GrafiteAst.Decompose (loc, names)
     | GrafiteAst.Demodulate loc ->
         metasenv,GrafiteAst.Demodulate loc
-    | GrafiteAst.Destruct (loc,term) ->
+    | GrafiteAst.Destruct (loc, Some term) ->
         let metasenv,term = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.Destruct(loc,term)
+        metasenv,GrafiteAst.Destruct(loc, Some term)
+    | GrafiteAst.Destruct (loc, None) ->
+        metasenv,GrafiteAst.Destruct(loc,None)
     | GrafiteAst.Exact (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Exact (loc, cic)
@@ -294,8 +296,6 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Ring loc
     | GrafiteAst.Split loc ->
         metasenv,GrafiteAst.Split loc
-    | GrafiteAst.Subst loc ->
-        metasenv, GrafiteAst.Subst loc
     | GrafiteAst.Symmetry loc ->
         metasenv,GrafiteAst.Symmetry loc
     | GrafiteAst.Transitivity (loc, term) -> 
index 081055ce84d64ffea17c354bc635e4e091100775..83e9d10d879904456952cfacf10bb03f60becd69 100644 (file)
@@ -170,8 +170,8 @@ EXTEND
        let idents = match idents with None -> [] | Some idents -> idents in
        GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
-    | IDENT "destruct"; t = tactic_term ->
-        GrafiteAst.Destruct (loc, t)
+    | IDENT "destruct"; xt = OPT [ t = tactic_term -> t ] ->
+        GrafiteAst.Destruct (loc, xt)
     | IDENT "elim"; what = tactic_term; using = using; 
        pattern = OPT pattern_spec;
        (num, idents) = intros_spec ->
@@ -246,8 +246,6 @@ EXTEND
         GrafiteAst.Ring loc
     | IDENT "split" ->
         GrafiteAst.Split loc
-    | IDENT "subst" ->
-        GrafiteAst.Subst loc    
     | IDENT "symmetry" ->
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->
index 964011bfd1609a0355170ca53b1024c22970af70..579ab17ccecd73304de6c735f36fb04fe63d587d 100644 (file)
@@ -23,8 +23,7 @@ eliminationTactics.cmi: proofEngineTypes.cmi
 negationTactics.cmi: proofEngineTypes.cmi 
 equalityTactics.cmi: proofEngineTypes.cmi 
 auto.cmi: universe.cmi proofEngineTypes.cmi 
-discriminationTactics.cmi: proofEngineTypes.cmi 
-substTactic.cmi: proofEngineTypes.cmi 
+destructTactic.cmi: proofEngineTypes.cmi 
 inversion.cmi: proofEngineTypes.cmi 
 ring.cmi: proofEngineTypes.cmi 
 setoids.cmi: proofEngineTypes.cmi 
@@ -147,20 +146,14 @@ auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \
     proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
     metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \
     paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi 
-discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
-    proofEngineTypes.cmi proofEngineStructuralRules.cmi \
-    proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \
-    equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi 
-discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
-    proofEngineTypes.cmx proofEngineStructuralRules.cmx \
-    proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
-    equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi 
-substTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
-    proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \
-    discriminationTactics.cmi substTactic.cmi 
-substTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
-    proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \
-    discriminationTactics.cmx substTactic.cmi 
+destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
+    proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
+    primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \
+    eliminationTactics.cmi destructTactic.cmi 
+destructTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
+    proofEngineStructuralRules.cmx proofEngineHelpers.cmx \
+    primitiveTactics.cmx introductionTactics.cmx equalityTactics.cmx \
+    eliminationTactics.cmx destructTactic.cmi 
 inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
     equalityTactics.cmi inversion.cmi 
@@ -199,18 +192,18 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \
     statefulProofEngine.cmi 
 statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \
     statefulProofEngine.cmi 
-tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \
-    ring.cmi reductionTactics.cmi proofEngineStructuralRules.cmi \
-    primitiveTactics.cmi negationTactics.cmi inversion.cmi \
-    introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \
-    equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \
-    compose.cmi closeCoercionGraph.cmi auto.cmi tactics.cmi 
-tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \
-    ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \
-    primitiveTactics.cmx negationTactics.cmx inversion.cmx \
-    introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
-    equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
-    compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi 
+tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi ring.cmi \
+    reductionTactics.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
+    negationTactics.cmi inversion.cmi introductionTactics.cmi \
+    fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \
+    eliminationTactics.cmi destructTactic.cmi compose.cmi \
+    closeCoercionGraph.cmi auto.cmi tactics.cmi 
+tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \
+    reductionTactics.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \
+    negationTactics.cmx inversion.cmx introductionTactics.cmx \
+    fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
+    eliminationTactics.cmx destructTactic.cmx compose.cmx \
+    closeCoercionGraph.cmx auto.cmx tactics.cmi 
 declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
 declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
index 964011bfd1609a0355170ca53b1024c22970af70..579ab17ccecd73304de6c735f36fb04fe63d587d 100644 (file)
@@ -23,8 +23,7 @@ eliminationTactics.cmi: proofEngineTypes.cmi
 negationTactics.cmi: proofEngineTypes.cmi 
 equalityTactics.cmi: proofEngineTypes.cmi 
 auto.cmi: universe.cmi proofEngineTypes.cmi 
-discriminationTactics.cmi: proofEngineTypes.cmi 
-substTactic.cmi: proofEngineTypes.cmi 
+destructTactic.cmi: proofEngineTypes.cmi 
 inversion.cmi: proofEngineTypes.cmi 
 ring.cmi: proofEngineTypes.cmi 
 setoids.cmi: proofEngineTypes.cmi 
@@ -147,20 +146,14 @@ auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \
     proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
     metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \
     paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi 
-discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
-    proofEngineTypes.cmi proofEngineStructuralRules.cmi \
-    proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \
-    equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi 
-discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
-    proofEngineTypes.cmx proofEngineStructuralRules.cmx \
-    proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
-    equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi 
-substTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
-    proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \
-    discriminationTactics.cmi substTactic.cmi 
-substTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
-    proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \
-    discriminationTactics.cmx substTactic.cmi 
+destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
+    proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
+    primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \
+    eliminationTactics.cmi destructTactic.cmi 
+destructTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
+    proofEngineStructuralRules.cmx proofEngineHelpers.cmx \
+    primitiveTactics.cmx introductionTactics.cmx equalityTactics.cmx \
+    eliminationTactics.cmx destructTactic.cmi 
 inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
     equalityTactics.cmi inversion.cmi 
@@ -199,18 +192,18 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \
     statefulProofEngine.cmi 
 statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \
     statefulProofEngine.cmi 
-tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \
-    ring.cmi reductionTactics.cmi proofEngineStructuralRules.cmi \
-    primitiveTactics.cmi negationTactics.cmi inversion.cmi \
-    introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \
-    equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \
-    compose.cmi closeCoercionGraph.cmi auto.cmi tactics.cmi 
-tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \
-    ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \
-    primitiveTactics.cmx negationTactics.cmx inversion.cmx \
-    introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
-    equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
-    compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi 
+tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi ring.cmi \
+    reductionTactics.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
+    negationTactics.cmi inversion.cmi introductionTactics.cmi \
+    fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \
+    eliminationTactics.cmi destructTactic.cmi compose.cmi \
+    closeCoercionGraph.cmi auto.cmi tactics.cmi 
+tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \
+    reductionTactics.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \
+    negationTactics.cmx inversion.cmx introductionTactics.cmx \
+    fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
+    eliminationTactics.cmx destructTactic.cmx compose.cmx \
+    closeCoercionGraph.cmx auto.cmx tactics.cmi 
 declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
 declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
index c4e020005e0a8ea4462aa678a88e08aa57062bab..9a6c6d4d04b40ec2e70757a44d504bea1694eef2 100644 (file)
@@ -22,7 +22,7 @@ INTERFACE_FILES = \
        introductionTactics.mli eliminationTactics.mli negationTactics.mli \
        equalityTactics.mli \
        auto.mli \
-       discriminationTactics.mli substTactic.mli \
+       destructTactic.mli \
         inversion.mli inversion_principle.mli ring.mli setoids.mli \
        fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \
        statefulProofEngine.mli tactics.mli declarative.mli
diff --git a/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml
new file mode 100644 (file)
index 0000000..bbfee80
--- /dev/null
@@ -0,0 +1,677 @@
+(* Copyright (C) 2002, 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/.
+ *)
+
+(* $Id$ *)
+
+module C = Cic
+module U = UriManager
+module P = PrimitiveTactics
+module T = Tacticals
+module CR = CicReduction 
+module PST = ProofEngineStructuralRules
+module PET = ProofEngineTypes
+module CTC = CicTypeChecker
+module CU = CicUniv
+module S = CicSubstitution
+module RT = ReductionTactics
+module PEH = ProofEngineHelpers
+module ET = EqualityTactics
+module DTI = DoubleTypeInference
+module FNG = FreshNamesGenerator
+
+let debug = true
+let debug_print = 
+  if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
+
+(* funzione generale di rilocazione dei riferimenti locali *)
+
+let relocate_term map t =
+   let rec map_xnss k xnss =
+      let imap (uri, t) = uri, map_term k t in
+      List.map imap xnss
+   and map_mss k mss =
+      let imap = function
+         | None   -> None
+         | Some t -> Some (map_term k t)
+      in
+      List.map imap mss
+   and map_fs len k fs = 
+      let imap (name, i, ty, bo) = name, i, map_term k ty, map_term (k + len) bo in
+      List.map imap fs
+   and map_cfs len k cfs = 
+      let imap (name, ty, bo) = name, map_term k ty, map_term (k + len) bo in
+      List.map imap cfs
+   and map_term k = function
+      | C.Rel m -> if m < k then C.Rel m else C.Rel (map (m - k))
+      | C.Sort _ as t -> t
+      | C.Implicit _ as t -> t
+      | C.Var (uri, xnss) -> C.Var (uri, map_xnss k xnss)
+      | C.Const (uri, xnss) -> C.Const (uri, map_xnss k xnss)
+      | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, map_xnss k xnss)
+      | C.MutConstruct (uri, tyno, consno, xnss) ->
+         C.MutConstruct (uri, tyno, consno, map_xnss k xnss)
+      | C.Meta (i, mss) -> C.Meta(i, map_mss k mss)
+      | C.Cast (te, ty) -> C.Cast (map_term k te, map_term k ty)
+      | C.Appl ts -> C.Appl (List.map (map_term k) ts)
+      | C.MutCase (sp, i, outty, t, pl) ->
+         C.MutCase (sp, i, map_term k outty, map_term k t, List.map (map_term k) pl)    
+      | C.Prod (n, s, t) -> C.Prod (n, map_term k s, map_term (succ k) t)
+      | C.Lambda (n, s, t) -> C.Lambda (n, map_term k s, map_term (succ k) t)
+      | C.LetIn (n, s, t) -> C.LetIn (n, map_term k s, map_term (succ k) t)
+      | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs)
+      | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs)
+   in
+   map_term 0 t
+
+let id n = n
+
+let after continuation aftermap beforemap = 
+   continuation ~map:(fun n -> aftermap (beforemap n))
+
+let after2 continuation aftermap beforemap ~map = 
+   continuation ~map:(fun n -> map (aftermap (beforemap n)))
+
+(* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
+diversi *)
+
+let discriminate_tac ~term =
+ let true_URI =
+  match LibraryObjects.true_URI () with
+     Some uri -> uri
+   | None -> raise (PET.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
+ let false_URI =
+  match LibraryObjects.false_URI () with
+     Some uri -> uri
+   | None -> raise (PET.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
+ let fail msg = raise (PET.Fail (lazy ("Discriminate: " ^ msg))) in
+ let find_discriminating_consno t1 t2 =
+   let rec aux t1 t2 =
+     match t1, t2 with
+     | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None
+     | C.Appl ((C.MutConstruct _ as constr1) :: args1),
+       C.Appl ((C.MutConstruct _ as constr2) :: args2)
+       when constr1 = constr2 ->
+         let rec aux_list l1 l2 =
+           match l1, l2 with
+           | [], [] -> None
+           | hd1 :: tl1, hd2 :: tl2 ->
+               (match aux hd1 hd2 with
+               | None -> aux_list tl1 tl2
+               | Some _ as res -> res)
+           | _ -> (* same constructor applied to a different number of args *)
+               assert false
+         in
+         aux_list args1 args2
+     | ((C.MutConstruct (_,_,consno1,subst1)),
+       (C.MutConstruct (_,_,consno2,subst2)))
+     | ((C.MutConstruct (_,_,consno1,subst1)),
+       (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
+     | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
+       (C.MutConstruct (_,_,consno2,subst2)))
+     | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
+       (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
+       when (consno1 <> consno2) || (subst1 <> subst2) ->
+         Some consno2
+     | _ -> fail "not a discriminable equality"
+   in
+   aux t1 t2
+ in
+ let mk_branches_and_outtype turi typeno consno context args =
+    (* a list of "True" except for the element in position consno which
+     * is "False" *)
+    match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+    | C.InductiveDefinition (ind_type_list,_,paramsno,_)  ->
+        let _,_,rty,constructor_list = List.nth ind_type_list typeno in 
+        let false_constr_id,_ = List.nth constructor_list (consno - 1) in
+        let branches =
+         List.map 
+           (fun (id,cty) ->
+             (* dubbio: e' corretto ridurre in questo context ??? *)
+             let red_ty = CR.whd context cty in
+             let rec aux t k =
+               match t with
+               | C.Prod (_,_,target) when (k <= paramsno) ->
+                   S.subst (List.nth args (k-1))
+                     (aux target (k+1))
+               | C.Prod (binder,source,target) when (k > paramsno) ->
+                   C.Lambda (binder, source, (aux target (k+1)))
+               | _ -> 
+                   if (id = false_constr_id)
+                   then (C.MutInd(false_URI,0,[]))
+                   else (C.MutInd(true_URI,0,[]))
+             in
+             (S.lift 1 (aux red_ty 1)))
+           constructor_list in
+        let outtype =
+         let seed = ref 0 in
+         let rec mk_lambdas rev_left_args =
+          function
+             0, args, C.Prod (_,so,ta) ->
+              C.Lambda
+               (C.Name (incr seed; "x" ^ string_of_int !seed),
+               so,
+               mk_lambdas rev_left_args (0,args,ta))
+           | 0, args, C.Sort _ ->
+              let rec mk_rels =
+               function
+                  0 -> []
+                | n -> C.Rel n :: mk_rels (n - 1) in
+              let argsno = List.length args in
+               C.Lambda
+                (C.Name "x",
+                 (if argsno + List.length rev_left_args > 0 then
+                   C.Appl
+                    (C.MutInd (turi, typeno, []) ::
+                     (List.map
+                      (S.lift (argsno + 1))
+                      (List.rev rev_left_args)) @
+                     mk_rels argsno)
+                  else
+                   C.MutInd (turi,typeno,[])),
+                 C.Sort C.Prop)
+           | 0, _, _ -> assert false (* seriously screwed up *)
+           | n, he::tl, C.Prod (_,_,ta) ->
+              mk_lambdas (he::rev_left_args)(n-1,tl,S.subst he ta)
+           | n,_,_ ->
+              assert false (* we should probably reduce in some context *)
+         in
+          mk_lambdas [] (paramsno, args, rty)
+        in
+         branches, outtype 
+    | _ -> assert false
+ in
+ let discriminate'_tac ~term status = 
+  let (proof, goal) = status in
+  let _,metasenv,_subst,_,_, _ = proof in
+  let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let termty,_ = 
+    CTC.type_of_aux' metasenv context term CU.empty_ugraph
+  in
+  match termty with
+   | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
+     when LibraryObjects.is_eq_URI equri ->
+      let turi,typeno,exp_named_subst,args = 
+        match tty with
+        | (C.MutInd (turi,typeno,exp_named_subst)) ->
+            turi,typeno,exp_named_subst,[]
+        | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) ->
+            turi,typeno,exp_named_subst,args
+        | _ -> fail "not a discriminable equality"
+      in
+      let consno =
+        match find_discriminating_consno t1 t2 with
+        | Some consno -> consno
+        | None -> fail "discriminating terms are structurally equal"
+      in
+      let branches,outtype =
+       mk_branches_and_outtype turi typeno consno context args
+      in
+      PET.apply_tactic
+       (T.then_
+         ~start:(EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
+         ~continuation:
+           (T.then_
+             ~start:
+               (RT.change_tac 
+                 ~pattern:(PET.conclusion_pattern None)
+                 (fun _ m u ->
+                   C.Appl [
+                     C.Lambda ( C.Name "x", tty,
+                       C.MutCase (turi, typeno, outtype, (C.Rel 1), branches));
+                     t2 ],
+                   m, u))
+             ~continuation:
+               (T.then_
+                 ~start:
+                   (ET.rewrite_simpl_tac
+                     ~direction:`RightToLeft
+                     ~pattern:(PET.conclusion_pattern None)
+                     term [])
+                 ~continuation:
+                   (IntroductionTactics.constructor_tac ~n:1)))) status
+    | _ -> fail "not an equality"
+  in
+  PET.mk_tactic (discriminate'_tac ~term)
+
+let exn_noneq = 
+  PET.Fail (lazy "Injection: not an equality")
+let exn_nothingtodo = 
+  PET.Fail (lazy "Nothing to do")
+let exn_discrnonind =
+  PET.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible")
+let exn_injwronggoal = 
+  PET.Fail (lazy "Injection: goal after cut is not correct")
+let exn_noneqind =
+  PET.Fail (lazy "Injection: not an equality over elements of an inductive type")
+
+let pp ctx t = 
+  let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in
+  CicPp.pp t names
+
+let clear_term first_time lterm =
+   let clear_term status =
+      let (proof, goal) = status in
+      let _,metasenv,_subst,_,_, _ = proof in
+      let _,context,_ = CicUtil.lookup_meta goal metasenv in
+      let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+      debug_print (lazy ("\nclear di: " ^ pp context term));
+      debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context)); 
+      let g () = if first_time then raise exn_nothingtodo else T.id_tac in
+      let tactic = match term with
+         | C.Rel n -> 
+           begin match List.nth context (pred n) with
+               | Some (C.Name id, _) -> 
+                 T.if_ ~fail:(g ()) ~start:(PST.clear ~hyps:[id]) ~continuation:T.id_tac
+              | _ -> assert false
+            end
+          | _      -> g ()
+      in
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic clear_term
+
+let simpl_in_term context = function
+   | Cic.Rel i ->
+      let name = match List.nth context (pred i) with
+         | Some (Cic.Name s, Cic.Def _) -> s
+         | Some (Cic.Name s, Cic.Decl _) -> s
+         | _ -> assert false
+      in
+      RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None)
+   | _ -> T.id_tac
+
+let mk_fresh_name metasenv context name typ =
+   let name = C.Name name in
+   match FNG.mk_fresh_name ~subst:[] metasenv context name ~typ with
+      | C.Name s    -> s
+      | C.Anonymous -> assert false
+
+let exists context = function
+   | C.Rel i -> List.nth context (pred i) <> None
+   | _       -> true
+
+let rec recur_on_child_tac name =
+   let recur_on_child status = 
+      let (proof, goal) = status in
+      let _, metasenv, _subst, _, _, _ = proof in
+      let _, context, _ = CicUtil.lookup_meta goal metasenv in
+      debug_print (lazy ("\nrecur_on_child su: " ^ name));
+      debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));      
+      let rec search_name i = function
+         | []                                      -> T.id_tac
+         | Some (Cic.Name n, _) :: _ when n = name -> 
+             destruct ~first_time:false ~term:(Cic.Rel i)
+        | _ :: tl -> search_name (succ i) tl
+      in
+      PET.apply_tactic (search_name 1 context) status  
+   in
+   PET.mk_tactic recur_on_child
+   
+and injection_tac ~lterm ~i ~continuation =
+ let give_name seed = function
+   | C.Name _ as name -> name
+   | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
+ in
+ let rec mk_rels = function | 0 -> [] | n -> C.Rel n :: (mk_rels (n - 1)) in
+ let injection_tac status =
+  let (proof, goal) = status in
+  (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma 
+   * differiscono (o potrebbero differire?) nell'i-esimo parametro 
+   * del costruttore *)
+  let _,metasenv,_subst,_,_, _ = proof in
+  let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+  let termty,_ =
+    CTC.type_of_aux' metasenv context term CU.empty_ugraph
+  in
+  debug_print (lazy ("\ninjection su : " ^ pp context termty)); 
+  match termty with (* an equality *)
+   | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
+    when LibraryObjects.is_eq_URI equri -> 
+      let turi,typeno,ens,params =
+        match tty with (* some inductive type *)
+        | C.MutInd (turi,typeno,ens) -> turi,typeno,ens,[]
+        | C.Appl (C.MutInd (turi,typeno,ens)::params) -> turi,typeno,ens,params
+        | _ -> raise exn_noneqind
+      in
+      let t1',t2',consno = (* sono i due sottotermini che differiscono *)
+        match t1,t2 with
+        | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1),
+          C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2)
+          when (uri1 = uri2) && (typeno1 = typeno2) && 
+               (consno1 = consno2) && (ens1 = ens2) -> 
+               (* controllo ridondante *)
+            List.nth applist1 (pred i),List.nth applist2 (pred i),consno2
+        | _ -> assert false
+      in
+      let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in
+      let patterns,outtype =
+        match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+        | C.InductiveDefinition (ind_type_list,_,paramsno,_)->
+           let left_params, right_params = HExtlib.split_nth paramsno params in
+           let _,_,_,constructor_list = List.nth ind_type_list typeno in
+           let i_constr_id,_ = List.nth constructor_list (consno - 1) in
+           let patterns =
+             let seed = ref 0 in
+             List.map
+               (function (id,cty) ->
+                 let reduced_cty = CR.whd context cty in
+                 let rec aux k = function
+                   | C.Prod (_,_,tgt) when k <= paramsno -> 
+                       let left = List.nth left_params (k-1) in
+                       aux (k+1) (S.subst left tgt)
+                   | C.Prod (binder,source,target) when k > paramsno ->
+                      let binder' = give_name seed binder in
+                      C.Lambda (binder',source,(aux (k+1) target))
+                   | _ ->
+                     let nr_param_constr = k - paramsno - 1 in
+                     if id = i_constr_id then C.Rel (k - i)
+                     else S.lift nr_param_constr t1' 
+                     (* + 1 per liftare anche il lambda aggiunto
+                      * esternamente al case *)
+                 in S.lift 1 (aux 1 reduced_cty))
+               constructor_list 
+           in
+           (* this code should be taken from cases_tac *)
+           let outtype =
+             let seed = ref 0 in
+             let rec to_lambdas te head =
+               match CR.whd context te with
+               | C.Prod (binder,so,ta) ->
+                   let binder' = give_name seed binder in
+                   C.Lambda (binder',so,to_lambdas ta head)
+               | _ -> head 
+             in
+             let rec skip_prods params te =
+               match params, CR.whd context te with
+               | [], _ -> te
+               | left::tl, C.Prod (_,_,ta) -> 
+                   skip_prods tl (S.subst left ta)
+               | _, _ -> assert false
+             in
+             let abstracted_tty =
+               let tty =
+                 List.fold_left (fun x y -> S.subst y x) tty left_params
+               in
+               (* non lift, ma subst coi left! *)
+               match S.lift 1 tty with
+               | C.MutInd _ as tty' -> tty'
+               | C.Appl l ->
+                   let keep,abstract = HExtlib.split_nth (paramsno +1) l in
+                   let keep = List.map (S.lift paramsno) keep in
+                   C.Appl (keep@mk_rels (List.length abstract))
+               | _ -> assert false
+             in
+             match ind_type_list with
+             | [] -> assert false
+             | (_,_,ty,_)::_ ->
+               (* this is in general wrong, do as in cases_tac *)
+               to_lambdas (skip_prods left_params ty)
+                 (C.Lambda 
+                   (C.Name "cased", abstracted_tty,
+                     (* here we should capture right parameters *)
+                     (* 1 for his Lambda, one for the Lambda outside the match
+                      * and then one for each to_lambda *)
+                     S.lift (2+List.length right_params) tty'))
+          in
+            patterns,outtype
+        | _ -> raise exn_discrnonind
+      in
+      let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in
+      let changed = 
+        C.Appl [ C.Lambda (C.Name "x", tty, 
+                  C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; t1]
+      in
+      (* check if cutted and changed are well typed and if t1' ~ changed *)
+      let go_on =
+        try
+          let _,g = CTC.type_of_aux' metasenv context  cutted
+            CU.empty_ugraph
+          in
+          let _,g = CTC.type_of_aux' metasenv context changed g in
+          fst (CR.are_convertible ~metasenv context  t1' changed g)
+        with
+        | CTC.TypeCheckerFailure _ -> false
+      in
+      if not go_on then begin
+        HLog.warn "destruct: injection failed";
+        PET.apply_tactic continuation status
+      end else
+        let fill_cut_tac term = 
+          let fill_cut status =
+               debug_print (lazy "riempio il cut"); 
+               let (proof, goal) = status in
+               let _,metasenv,_subst,_,_, _ = proof in
+               let _,context,gty = CicUtil.lookup_meta goal metasenv in
+               let gty = Unshare.unshare gty in
+               let new_t1' = match gty with 
+                  | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t
+                  | _ -> raise exn_injwronggoal
+               in
+               debug_print (lazy ("metto: " ^ pp context changed));
+               debug_print (lazy ("al posto di: " ^ pp context new_t1'));
+               debug_print (lazy ("nel goal: " ^ pp context gty));
+               debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
+               debug_print (lazy ("e poi rewrite con: "^pp context term));
+               let tac = T.seq ~tactics:[
+                 RT.change_tac
+                     ~pattern:(None, [], Some (PEH.pattern_of ~term:gty [new_t1']))
+                     (fun _ m u -> changed,m,u);
+                 ET.rewrite_simpl_tac
+                     ~direction:`LeftToRight
+                     ~pattern:(PET.conclusion_pattern None)
+                     term [];
+                  ET.reflexivity_tac   
+              ] in
+              PET.apply_tactic tac status
+          in
+          PET.mk_tactic fill_cut
+       in
+       debug_print (lazy ("CUT: " ^ pp context cutted));  
+       let name = mk_fresh_name metasenv context "Hcut" cutted in
+       let mk_fresh_name_callback = PEH.namer_of [Some name] in
+       debug_print (lazy ("figlio: " ^ name));
+       let tactic = 
+          T.thens ~start: (P.cut_tac ~mk_fresh_name_callback cutted)
+                   ~continuations:[
+                     T.seq ~tactics:[continuation; recur_on_child_tac name];
+                     fill_cut_tac term
+                  ]
+        in
+       PET.apply_tactic tactic status
+   | _ -> raise exn_noneq
+ in
+  PET.mk_tactic injection_tac
+
+and subst_tac ~lterm ~direction ~where ~continuation =
+   let subst_tac status =
+      let (proof, goal) = status in
+      let _,metasenv,_subst,_,_, _ = proof in
+      let _,context,_ = CicUtil.lookup_meta goal metasenv in
+      let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+      debug_print (lazy ("\nsubst " ^ (match direction with `LeftToRight -> "->" | `RightToLeft -> "<-") ^ " di: " ^ pp context term));
+      let tactic = match where with
+         | None      -> 
+           debug_print (lazy ("nella conclusione"));
+           let pattern = PET.conclusion_pattern None in
+            let tactic = ET.rewrite_tac ~direction ~pattern term [] in
+            T.then_ ~start:(T.try_tactic ~tactic) ~continuation
+        | Some name ->
+            debug_print (lazy ("nella premessa: " ^ name));
+           let pattern = None, [name, PET.hole], None in
+            let start = ET.rewrite_tac ~direction ~pattern term [] in
+            let ok_tactic = 
+              T.seq ~tactics:[continuation; recur_on_child_tac name]
+           in
+           debug_print (lazy ("figlio: " ^ name));
+           T.if_ ~start ~continuation:ok_tactic ~fail:continuation         
+      in 
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic subst_tac
+
+(* ~term vive nel contesto della tattica una volta ~mappato
+ * ~continuation riceve la mappa assoluta
+ *)
+and destruct ~first_time ~term =
+ let are_convertible hd1 hd2 metasenv context = 
+   fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
+ in
+ let destruct status = 
+  let (proof, goal) = status in
+  let _,metasenv,_subst, _,_, _ = proof in
+  let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  debug_print (lazy ("\ndestruct di: " ^ pp context term)); 
+  debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
+  let termty,_ = 
+    CTC.type_of_aux' metasenv context term CU.empty_ugraph
+  in
+  debug_print (lazy ("\ndestruct su: " ^ pp context termty)); 
+  let mk_lterm term c m ug =
+     let distance = List.length c - List.length context in
+     S.lift distance term, m, ug
+  in
+  let lterm = mk_lterm term in
+  let mk_subst_chain direction index with_what what =
+     let k = match term with C.Rel i -> i | _ -> -1 in
+     let rec traverse_context first_time j = function
+        | [] ->           
+          let continuation =
+             T.seq ~tactics:[
+                clear_term first_time lterm;
+                clear_term false (mk_lterm what);
+                clear_term false (mk_lterm with_what)
+             ]
+          in
+          subst_tac ~direction ~lterm ~where:None ~continuation
+        | Some (C.Name name, _) :: tl when j < index && j <> k ->
+          debug_print (lazy ("\nsubst programmata: cosa: " ^ string_of_int index ^ ", dove: " ^ string_of_int j));
+          subst_tac ~direction ~lterm ~where:(Some name) 
+                    ~continuation:(traverse_context false (succ j) tl)
+        | _ :: tl -> traverse_context first_time (succ j) tl
+     in
+     traverse_context first_time 1 context
+  in
+  let tac = match termty with
+    | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] 
+      when LibraryObjects.is_eq_URI equri ->
+          begin match t1,t2 with
+(* injection part *)
+           | C.MutConstruct _,
+              C.MutConstruct _
+              when t1 = t2 -> clear_term first_time lterm
+            | C.Appl (C.MutConstruct _ as mc1 :: applist1),
+              C.Appl (C.MutConstruct _ as mc2 :: applist2)
+              when mc1 = mc2 ->
+                let rec traverse_list first_time i l1 l2 = 
+                  match l1, l2 with
+                      | [], [] -> clear_term first_time lterm
+                      | hd1 :: tl1, hd2 :: tl2 -> 
+                        if are_convertible hd1 hd2 metasenv context then
+                           traverse_list first_time (succ i) tl1 tl2
+                        else
+                          injection_tac ~i ~lterm ~continuation:
+                             (traverse_list false (succ i) tl1 tl2)
+                      | _ -> assert false 
+                      (* i 2 termini hanno in testa lo stesso costruttore, 
+                       * ma applicato a un numero diverso di termini *)
+                in
+                  traverse_list first_time 1 applist1 applist2
+(* discriminate part *)
+           | C.MutConstruct (_,_,consno1,ens1),
+              C.MutConstruct (_,_,consno2,ens2)
+            | C.MutConstruct (_,_,consno1,ens1),
+              C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_)
+            | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_),
+              C.MutConstruct (_,_,consno2,ens2)
+            | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_),
+              C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_)
+              when (consno1 <> consno2) || (ens1 <> ens2) -> 
+                discriminate_tac ~term
+(* subst part *)
+            | C.Rel _, C.Rel _ when t1 = t2 ->
+               T.seq ~tactics:[
+                  clear_term first_time lterm;
+                  clear_term false (mk_lterm t1)
+               ]
+           | C.Rel i1, C.Rel i2 when i1 < i2 ->  
+              mk_subst_chain `LeftToRight i1 t2 t1
+           | C.Rel i1, C.Rel i2 when i1 > i2 ->
+              mk_subst_chain `RightToLeft i2 t1 t2
+           | C.Rel i1, _ when DTI.does_not_occur i1 t2 ->
+              mk_subst_chain `LeftToRight i1 t2 t1
+           | _, C.Rel i2 when DTI.does_not_occur i2 t1 ->
+              mk_subst_chain `RightToLeft i2 t1 t2
+(* else part *)
+           | _ when not first_time -> T.id_tac
+            | _ (* when first_time *) -> 
+               T.then_ ~start:(simpl_in_term context term)
+                       ~continuation:(destruct ~first_time:false ~term)
+           end
+     | _ when not first_time -> T.id_tac
+     | _ (* when first_time *) -> raise exn_nothingtodo
+  in  
+    PET.apply_tactic tac status
+ in 
+   PET.mk_tactic destruct
+
+let lazy_destruct_tac ~first_time ~lterm =
+   let lazy_destruct status =
+      let (proof, goal) = status in
+      let _,metasenv,_subst,_,_, _ = proof in
+      let _,context,_ = CicUtil.lookup_meta goal metasenv in
+      let term, _, _ = lterm context metasenv CU.empty_ugraph in
+      let tactic = 
+         if exists context term then destruct ~first_time ~term else T.id_tac
+      in
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic lazy_destruct
+
+(* destruct performs either injection or discriminate *)
+(* equivalent to Coq's "analyze equality"             *)
+let destruct_tac = function
+   | Some term -> destruct ~first_time:true ~term
+   | None      ->
+      let destruct_all status =
+         let (proof, goal) = status in
+         let _,metasenv,_subst,_,_, _ = proof in
+         let _,context,_ = CicUtil.lookup_meta goal metasenv in
+         let mk_lterm term c m ug =
+            let distance = List.length c - List.length context in
+            S.lift distance term, m, ug
+         in
+         let rec mk_tactics first_time i tacs = function
+           | []           -> List.rev tacs
+           | Some _ :: tl -> 
+              let lterm = mk_lterm (C.Rel i) in
+              let tacs = lazy_destruct_tac ~first_time ~lterm :: tacs in
+              mk_tactics false (succ i) tacs tl 
+          | _ :: tl       -> mk_tactics first_time (succ i) tacs tl
+        in
+        let tactics = mk_tactics false 1 [] context in
+        PET.apply_tactic (T.seq ~tactics) status
+      in
+      PET.mk_tactic destruct_all
diff --git a/helm/software/components/tactics/destructTactic.mli b/helm/software/components/tactics/destructTactic.mli
new file mode 100644 (file)
index 0000000..0ecccda
--- /dev/null
@@ -0,0 +1,30 @@
+(* Copyright (C) 2002, 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/.
+ *)
+
+(* Performs a recursive comparisons of the two sides of an equation
+   looking for constructors. If the two sides differ on two constructors,
+   it closes the current goal. If they differ by other two terms it introduces
+   an equality. *)
+val destruct_tac: Cic.term option -> ProofEngineTypes.tactic
diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
deleted file mode 100644 (file)
index 83f676e..0000000
+++ /dev/null
@@ -1,572 +0,0 @@
-(* Copyright (C) 2002, 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/.
- *)
-
-(* $Id$ *)
-
-module C = Cic
-module U = UriManager
-module P = PrimitiveTactics
-module T = Tacticals
-module CR = CicReduction 
-module PST = ProofEngineStructuralRules
-module PET = ProofEngineTypes
-module CTC = CicTypeChecker
-module CU = CicUniv
-module S = CicSubstitution
-module RT = ReductionTactics
-module PEH = ProofEngineHelpers
-module ET = EqualityTactics
-
-let debug = false
-let debug_print = 
-  if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
-
-(* funzione generale di rilocazione dei riferimenti locali *)
-
-let relocate_term map t =
-   let rec map_xnss k xnss =
-      let imap (uri, t) = uri, map_term k t in
-      List.map imap xnss
-   and map_mss k mss =
-      let imap = function
-         | None   -> None
-         | Some t -> Some (map_term k t)
-      in
-      List.map imap mss
-   and map_fs len k fs = 
-      let imap (name, i, ty, bo) = name, i, map_term k ty, map_term (k + len) bo in
-      List.map imap fs
-   and map_cfs len k cfs = 
-      let imap (name, ty, bo) = name, map_term k ty, map_term (k + len) bo in
-      List.map imap cfs
-   and map_term k = function
-      | C.Rel m -> if m < k then C.Rel m else C.Rel (map (m - k))
-      | C.Sort _ as t -> t
-      | C.Implicit _ as t -> t
-      | C.Var (uri, xnss) -> C.Var (uri, map_xnss k xnss)
-      | C.Const (uri, xnss) -> C.Const (uri, map_xnss k xnss)
-      | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, map_xnss k xnss)
-      | C.MutConstruct (uri, tyno, consno, xnss) ->
-         C.MutConstruct (uri, tyno, consno, map_xnss k xnss)
-      | C.Meta (i, mss) -> C.Meta(i, map_mss k mss)
-      | C.Cast (te, ty) -> C.Cast (map_term k te, map_term k ty)
-      | C.Appl ts -> C.Appl (List.map (map_term k) ts)
-      | C.MutCase (sp, i, outty, t, pl) ->
-         C.MutCase (sp, i, map_term k outty, map_term k t, List.map (map_term k) pl)    
-      | C.Prod (n, s, t) -> C.Prod (n, map_term k s, map_term (succ k) t)
-      | C.Lambda (n, s, t) -> C.Lambda (n, map_term k s, map_term (succ k) t)
-      | C.LetIn (n, s, t) -> C.LetIn (n, map_term k s, map_term (succ k) t)
-      | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs)
-      | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs)
-   in
-   map_term 0 t
-
-let id n = n
-
-let after continuation aftermap beforemap = 
-   continuation ~map:(fun n -> aftermap (beforemap n))
-
-let after2 continuation aftermap beforemap ~map = 
-   continuation ~map:(fun n -> map (aftermap (beforemap n)))
-
-(* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
-diversi *)
-
-let discriminate_tac ~term =
- let true_URI =
-  match LibraryObjects.true_URI () with
-     Some uri -> uri
-   | None -> raise (PET.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
- let false_URI =
-  match LibraryObjects.false_URI () with
-     Some uri -> uri
-   | None -> raise (PET.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
- let fail msg = raise (PET.Fail (lazy ("Discriminate: " ^ msg))) in
- let find_discriminating_consno t1 t2 =
-   let rec aux t1 t2 =
-     match t1, t2 with
-     | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None
-     | C.Appl ((C.MutConstruct _ as constr1) :: args1),
-       C.Appl ((C.MutConstruct _ as constr2) :: args2)
-       when constr1 = constr2 ->
-         let rec aux_list l1 l2 =
-           match l1, l2 with
-           | [], [] -> None
-           | hd1 :: tl1, hd2 :: tl2 ->
-               (match aux hd1 hd2 with
-               | None -> aux_list tl1 tl2
-               | Some _ as res -> res)
-           | _ -> (* same constructor applied to a different number of args *)
-               assert false
-         in
-         aux_list args1 args2
-     | ((C.MutConstruct (_,_,consno1,subst1)),
-       (C.MutConstruct (_,_,consno2,subst2)))
-     | ((C.MutConstruct (_,_,consno1,subst1)),
-       (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
-     | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
-       (C.MutConstruct (_,_,consno2,subst2)))
-     | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
-       (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
-       when (consno1 <> consno2) || (subst1 <> subst2) ->
-         Some consno2
-     | _ -> fail "not a discriminable equality"
-   in
-   aux t1 t2
- in
- let mk_branches_and_outtype turi typeno consno context args =
-    (* a list of "True" except for the element in position consno which
-     * is "False" *)
-    match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
-    | C.InductiveDefinition (ind_type_list,_,paramsno,_)  ->
-        let _,_,rty,constructor_list = List.nth ind_type_list typeno in 
-        let false_constr_id,_ = List.nth constructor_list (consno - 1) in
-        let branches =
-         List.map 
-           (fun (id,cty) ->
-             (* dubbio: e' corretto ridurre in questo context ??? *)
-             let red_ty = CR.whd context cty in
-             let rec aux t k =
-               match t with
-               | C.Prod (_,_,target) when (k <= paramsno) ->
-                   S.subst (List.nth args (k-1))
-                     (aux target (k+1))
-               | C.Prod (binder,source,target) when (k > paramsno) ->
-                   C.Lambda (binder, source, (aux target (k+1)))
-               | _ -> 
-                   if (id = false_constr_id)
-                   then (C.MutInd(false_URI,0,[]))
-                   else (C.MutInd(true_URI,0,[]))
-             in
-             (S.lift 1 (aux red_ty 1)))
-           constructor_list in
-        let outtype =
-         let seed = ref 0 in
-         let rec mk_lambdas rev_left_args =
-          function
-             0, args, C.Prod (_,so,ta) ->
-              C.Lambda
-               (C.Name (incr seed; "x" ^ string_of_int !seed),
-               so,
-               mk_lambdas rev_left_args (0,args,ta))
-           | 0, args, C.Sort _ ->
-              let rec mk_rels =
-               function
-                  0 -> []
-                | n -> C.Rel n :: mk_rels (n - 1) in
-              let argsno = List.length args in
-               C.Lambda
-                (C.Name "x",
-                 (if argsno + List.length rev_left_args > 0 then
-                   C.Appl
-                    (C.MutInd (turi, typeno, []) ::
-                     (List.map
-                      (S.lift (argsno + 1))
-                      (List.rev rev_left_args)) @
-                     mk_rels argsno)
-                  else
-                   C.MutInd (turi,typeno,[])),
-                 C.Sort C.Prop)
-           | 0, _, _ -> assert false (* seriously screwed up *)
-           | n, he::tl, C.Prod (_,_,ta) ->
-              mk_lambdas (he::rev_left_args)(n-1,tl,S.subst he ta)
-           | n,_,_ ->
-              assert false (* we should probably reduce in some context *)
-         in
-          mk_lambdas [] (paramsno, args, rty)
-        in
-         branches, outtype 
-    | _ -> assert false
- in
- let discriminate'_tac ~term status = 
-  let (proof, goal) = status in
-  let _,metasenv,_subst,_,_, _ = proof in
-  let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let termty,_ = 
-    CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph
-  in
-  match termty with
-   | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
-     when LibraryObjects.is_eq_URI equri ->
-      let turi,typeno,exp_named_subst,args = 
-        match tty with
-        | (C.MutInd (turi,typeno,exp_named_subst)) ->
-            turi,typeno,exp_named_subst,[]
-        | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) ->
-            turi,typeno,exp_named_subst,args
-        | _ -> fail "not a discriminable equality"
-      in
-      let consno =
-        match find_discriminating_consno t1 t2 with
-        | Some consno -> consno
-        | None -> fail "discriminating terms are structurally equal"
-      in
-      let branches,outtype =
-       mk_branches_and_outtype turi typeno consno context args
-      in
-      PET.apply_tactic
-       (T.then_
-         ~start:(EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
-         ~continuation:
-           (T.then_
-             ~start:
-               (RT.change_tac 
-                 ~pattern:(PET.conclusion_pattern None)
-                 (fun _ m u ->
-                   C.Appl [
-                     C.Lambda ( C.Name "x", tty,
-                       C.MutCase (turi, typeno, outtype, (C.Rel 1), branches));
-                     t2 ],
-                   m, u))
-             ~continuation:
-               (T.then_
-                 ~start:
-                   (ET.rewrite_simpl_tac
-                     ~direction:`RightToLeft
-                     ~pattern:(PET.conclusion_pattern None)
-                     term [])
-                 ~continuation:
-                   (IntroductionTactics.constructor_tac ~n:1)))) status
-    | _ -> fail "not an equality"
-  in
-  PET.mk_tactic (discriminate'_tac ~term)
-
-let exn_nonproj = 
-  PET.Fail (lazy "Injection: not a projectable equality")
-let exn_noneq = 
-  PET.Fail (lazy "Injection: not an equality")
-let exn_nothingtodo = 
-  PET.Fail (lazy "Nothing to do")
-let exn_discrnonind =
-  PET.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible")
-let exn_injwronggoal = 
-  PET.Fail (lazy "Injection: goal after cut is not correct")
-let exn_noneqind =
-  PET.Fail (lazy "Injection: not an equality over elements of an inductive type")
-
-let pp ctx t = 
-  let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in
-  CicPp.pp t names
-
-let clear_term first_time context term =
-   let g () = if first_time then raise exn_nothingtodo else T.id_tac in
-   match term with
-      | C.Rel n -> 
-         begin match List.nth context (pred n) with
-            | Some (C.Name id, _) -> PST.clear ~hyps:[id]
-           | _                   -> assert false
-         end
-       | _      -> g ()
-
-let simpl_in_term context = function
-   | Cic.Rel i ->
-      let name = match List.nth context (pred i) with
-         | Some (Cic.Name s, Cic.Def _) -> s
-         | Some (Cic.Name s, Cic.Decl _) -> s
-         | _ -> assert false
-      in
-      RT.simpl_tac ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None)
-   | _ -> raise exn_nonproj
-
-(* ~term vive nel contesto della tattica una volta ~mappato
- * ~continuation riceve la mappa assoluta
- *)
-let rec injection_tac ~map ~term ~i ~continuation =
- let give_name seed = function
-   | C.Name _ as name -> name
-   | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
- in
- let rec mk_rels = function | 0 -> [] | n -> C.Rel n :: (mk_rels (n - 1)) in
- let injection_tac status =
-  let (proof, goal) = status in
-  (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma 
-   * differiscono (o potrebbero differire?) nell'i-esimo parametro 
-   * del costruttore *)
-  let _,metasenv,_subst,_,_, _ = proof in
-  let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let term = relocate_term map term in
-  let termty,_ = 
-    CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph
-  in
-  debug_print (lazy ("\ninjection su : " ^ pp context termty)); 
-  match termty with (* an equality *)
-   | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
-    when LibraryObjects.is_eq_URI equri -> 
-      let turi,typeno,ens,params =
-        match tty with (* some inductive type *)
-        | C.MutInd (turi,typeno,ens) -> turi,typeno,ens,[]
-        | C.Appl (C.MutInd (turi,typeno,ens)::params) -> turi,typeno,ens,params
-        | _ -> raise exn_noneqind
-      in
-      let t1',t2',consno = (* sono i due sottotermini che differiscono *)
-        match t1,t2 with
-        | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1),
-          C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2)
-          when (uri1 = uri2) && (typeno1 = typeno2) && 
-               (consno1 = consno2) && (ens1 = ens2) -> 
-               (* controllo ridondante *)
-            List.nth applist1 (pred i),List.nth applist2 (pred i),consno2
-        | _ -> assert false
-      in
-      let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in
-      let patterns,outtype =
-        match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
-        | C.InductiveDefinition (ind_type_list,_,paramsno,_)->
-           let left_params, right_params = HExtlib.split_nth paramsno params in
-           let _,_,_,constructor_list = List.nth ind_type_list typeno in
-           let i_constr_id,_ = List.nth constructor_list (consno - 1) in
-           let patterns =
-             let seed = ref 0 in
-             List.map
-               (function (id,cty) ->
-                 let reduced_cty = CR.whd context cty in
-                 let rec aux k = function
-                   | C.Prod (_,_,tgt) when k <= paramsno -> 
-                       let left = List.nth left_params (k-1) in
-                       aux (k+1) (S.subst left tgt)
-                   | C.Prod (binder,source,target) when k > paramsno ->
-                      let binder' = give_name seed binder in
-                      C.Lambda (binder',source,(aux (k+1) target))
-                   | _ ->
-                     let nr_param_constr = k - paramsno - 1 in
-                     if id = i_constr_id then C.Rel (k - i)
-                     else S.lift nr_param_constr t1' 
-                     (* + 1 per liftare anche il lambda aggiunto
-                      * esternamente al case *)
-                 in S.lift 1 (aux 1 reduced_cty))
-               constructor_list 
-           in
-           (* this code should be taken from cases_tac *)
-           let outtype =
-             let seed = ref 0 in
-             let rec to_lambdas te head =
-               match CR.whd context te with
-               | C.Prod (binder,so,ta) ->
-                   let binder' = give_name seed binder in
-                   C.Lambda (binder',so,to_lambdas ta head)
-               | _ -> head 
-             in
-             let rec skip_prods params te =
-               match params, CR.whd context te with
-               | [], _ -> te
-               | left::tl, C.Prod (_,_,ta) -> 
-                   skip_prods tl (S.subst left ta)
-               | _, _ -> assert false
-             in
-             let abstracted_tty =
-               let tty =
-                 List.fold_left (fun x y -> S.subst y x) tty left_params
-               in
-               (* non lift, ma subst coi left! *)
-               match S.lift 1 tty with
-               | C.MutInd _ as tty' -> tty'
-               | C.Appl l ->
-                   let keep,abstract = HExtlib.split_nth (paramsno +1) l in
-                   let keep = List.map (S.lift paramsno) keep in
-                   C.Appl (keep@mk_rels (List.length abstract))
-               | _ -> assert false
-             in
-             match ind_type_list with
-             | [] -> assert false
-             | (_,_,ty,_)::_ ->
-               (* this is in general wrong, do as in cases_tac *)
-               to_lambdas (skip_prods left_params ty)
-                 (C.Lambda 
-                   (C.Name "cased", abstracted_tty,
-                     (* here we should capture right parameters *)
-                     (* 1 for his Lambda, one for the Lambda outside the match
-                      * and then one for each to_lambda *)
-                     S.lift (2+List.length right_params) tty'))
-          in
-            patterns,outtype
-        | _ -> raise exn_discrnonind
-      in
-      let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in
-      let changed = 
-        C.Appl [ C.Lambda (C.Name "x", tty, 
-                  C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; t1]
-      in
-      (* check if cutted and changed are well typed and if t1' ~ changed *)
-      let go_on =
-        try
-          let _,g = CTC.type_of_aux' metasenv context  cutted
-            CicUniv.empty_ugraph
-          in
-          let _,g = CTC.type_of_aux' metasenv context changed g in
-          fst (CR.are_convertible ~metasenv context  t1' changed g)
-        with
-        | CTC.TypeCheckerFailure _ -> false
-      in
-      if not go_on then 
-        PET.apply_tactic (continuation ~map) status
-      else
-        let tac term = 
-          let tac status =
-               debug_print (lazy "riempio il cut"); 
-               let (proof, goal) = status in
-               let _,metasenv,_subst,_,_, _ = proof in
-               let _,context,gty = CicUtil.lookup_meta goal metasenv in
-               let gty = Unshare.unshare gty in
-               let new_t1' = match gty with 
-                  | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t
-                  | _ -> raise exn_injwronggoal
-               in
-               debug_print (lazy ("metto: " ^ pp context changed));
-               debug_print (lazy ("al posto di: " ^ pp context new_t1'));
-               debug_print (lazy ("nel goal: " ^ pp context gty));
-               debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
-               debug_print (lazy ("e poi rewrite con: "^pp context term));
-               let tac = T.seq ~tactics:[
-                 RT.change_tac
-                     ~pattern:(None, [], Some (PEH.pattern_of ~term:gty [new_t1']))
-                     (fun _ m u -> changed,m,u);
-                 ET.rewrite_simpl_tac
-                     ~direction:`LeftToRight
-                     ~pattern:(PET.conclusion_pattern None)
-                     term [];
-                  ET.reflexivity_tac   
-              ] in
-              PET.apply_tactic tac status
-          in
-          PET.mk_tactic tac
-       in
-       debug_print (lazy ("CUT: " ^ pp context cutted));  
-       PET.apply_tactic   
-          (T.thens ~start: (P.cut_tac cutted)
-                   ~continuations:[
-                     (destruct ~first_time:false ~term:(C.Rel 1) ~map:id 
-                                ~continuation:(after2 continuation succ map) 
-                     );  
-                     tac term] 
-         ) status
-   | _ -> raise exn_noneq
- in
-  PET.mk_tactic injection_tac
-
-(* ~term vive nel contesto della tattica una volta ~mappato
- * ~continuation riceve la mappa assoluta
- *)
-and subst_tac ~map ~term ~direction ~where ~continuation =
-   let fail_tactic = continuation ~map in
-   let subst_tac status =
-      let term = relocate_term map term in
-      let tactic = match where with
-         | None      -> 
-           let pattern = PET.conclusion_pattern None in
-            let tactic = ET.rewrite_tac ~direction ~pattern term [] in
-            T.then_ ~start:(T.try_tactic ~tactic)
-                   ~continuation:fail_tactic
-        | Some name ->   
-            let pattern = None, [name, PET.hole], None in
-            let start = ET.rewrite_tac ~direction ~pattern term [] in
-            let continuation =
-              destruct ~first_time:false ~term:(C.Rel 1) ~map:id 
-                       ~continuation:(after2 continuation succ map)
-           in
-           T.if_ ~start ~continuation ~fail:fail_tactic
-      in 
-      PET.apply_tactic tactic status
-   in
-   PET.mk_tactic subst_tac
-
-(* ~term vive nel contesto della tattica una volta ~mappato
- * ~continuation riceve la mappa assoluta
- *)
-and destruct ~first_time ~map ~term ~continuation =
- let are_convertible hd1 hd2 metasenv context = 
-   fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
- in
- let destruct status = 
-  let (proof, goal) = status in
-  let _,metasenv,_subst, _,_, _ = proof in
-  let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let term = relocate_term map term in
-  debug_print (lazy ("\nqnify di: " ^ pp context term)); 
-  debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
-  let termty,_ = 
-    CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph
-  in
-  debug_print (lazy ("\nqnify su: " ^ pp context termty)); 
-  let tac = match termty with
-    | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] 
-      when LibraryObjects.is_eq_URI equri -> begin
-       match (CR.whd ~delta:true context tty) with
-        | C.MutInd _
-        | C.Appl (C.MutInd _ :: _) -> 
-          begin match t1,t2 with
-            | C.MutConstruct _,
-              C.MutConstruct _
-              when t1 = t2 ->
-               T.then_ ~start:(clear_term first_time context term)
-                        ~continuation:(continuation ~map)
-            | C.Appl (C.MutConstruct _ as mc1 :: applist1),
-              C.Appl (C.MutConstruct _ as mc2 :: applist2)
-              when mc1 = mc2 ->
-                let rec traverse_list first_time i l1 l2 = 
-                  match l1, l2 with
-                      | [], [] ->
-                        fun ~map:aftermap ->
-                           T.then_ ~start:(clear_term first_time context term)
-                                    ~continuation:(after continuation aftermap map)
-                      | hd1 :: tl1, hd2 :: tl2 -> 
-                        if are_convertible hd1 hd2 metasenv context then
-                           traverse_list first_time (succ i) tl1 tl2
-                        else
-                          injection_tac ~i ~term ~continuation:
-                             (traverse_list false (succ i) tl1 tl2)
-                      | _ -> assert false 
-                      (* i 2 termini hanno in testa lo stesso costruttore, 
-                       * ma applicato a un numero diverso di termini *)
-                in
-                  traverse_list first_time 1 applist1 applist2 ~map:id
-            | C.MutConstruct (_,_,consno1,ens1),
-              C.MutConstruct (_,_,consno2,ens2)
-            | C.MutConstruct (_,_,consno1,ens1),
-              C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_)
-            | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_),
-              C.MutConstruct (_,_,consno2,ens2)
-            | C.Appl ((C.MutConstruct (_,_,consno1,ens1))::_),
-              C.Appl ((C.MutConstruct (_,_,consno2,ens2))::_)
-              when (consno1 <> consno2) || (ens1 <> ens2) -> 
-                discriminate_tac ~term
-            | _ when not first_time -> continuation ~map
-            | _ (* when first_time *) -> 
-               T.then_ ~start:(simpl_in_term context term)
-                       ~continuation:(destruct ~first_time:false ~term ~map ~continuation)
-           end
-        | _ when not first_time -> continuation ~map
-        | _ (* when first_time *) -> raise exn_nonproj
-        end 
-    | _ -> raise exn_nonproj
-  in  
-    PET.apply_tactic tac status
- in 
-   PET.mk_tactic destruct
-
-(* destruct performs either injection or discriminate *)
-(* equivalent to Coq's "analyze equality"             *)
-let destruct_tac =
- destruct
-  ~first_time:true ~map:id ~continuation:(fun ~map -> T.id_tac)
diff --git a/helm/software/components/tactics/discriminationTactics.mli b/helm/software/components/tactics/discriminationTactics.mli
deleted file mode 100644 (file)
index 3a74e3d..0000000
+++ /dev/null
@@ -1,30 +0,0 @@
-(* Copyright (C) 2002, 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/.
- *)
-
-(* Performs a recursive comparisons of the two sides of an equation
-   looking for constructors. If the two sides differ on two constructors,
-   it closes the current goal. If they differ by other two terms it introduces
-   an equality. *)
-val destruct_tac: term:Cic.term -> ProofEngineTypes.tactic
diff --git a/helm/software/components/tactics/substTactic.ml b/helm/software/components/tactics/substTactic.ml
deleted file mode 100644 (file)
index feff68f..0000000
+++ /dev/null
@@ -1,164 +0,0 @@
-(* Copyright (C) 2002, 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 C    = Cic
-module DT   = DiscriminationTactics
-module DTI  = DoubleTypeInference
-module ET   = EqualityTactics
-module HEL  = HExtlib
-module LO   = LibraryObjects
-module PEH  = ProofEngineHelpers
-module PESR = ProofEngineStructuralRules
-module PET  = ProofEngineTypes
-module RT   = ReductionTactics
-module S    = CicSubstitution
-module T    = Tacticals
-module TC   = CicTypeChecker
-
-let lift_rewrite_tac ~context ~direction ~pattern equality =
-   let lift_rewrite_tac status =
-      let (proof, goal) = status in
-      let (_, metasenv, _subst, _, _, _) = proof in
-      let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
-      let n = List.length new_context - List.length context in
-      let equality = S.lift n equality in
-      PET.apply_tactic (ET.rewrite_tac ~direction ~pattern equality []) status
-   in
-   PET.mk_tactic lift_rewrite_tac
-
-let lift_destruct_tac ~context ~what =
-   let lift_destruct_tac status =
-      let (proof, goal) = status in
-      let (_, metasenv, _subst, _, _, _) = proof in
-      let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
-      let n = List.length new_context - List.length context in
-      let what = S.lift n what in
-      PET.apply_tactic (DT.destruct_tac ~term:what) status
-   in
-   PET.mk_tactic lift_destruct_tac
-      
-let msg0 = lazy "Subst: not found in context"
-let msg1 = lazy "Subst: not an erasable equation"
-let msg2 = lazy "Subst: recursive equation" 
-let msg3 = lazy "Subst: no progress" 
-
-let rec subst_tac ~try_tactic ~hyp =
-   let hole = C.Implicit (Some `Hole) in
-   let meta = C.Implicit None in
-   let rec ind = function
-      | C.MutInd _       -> true
-      | C.Appl (t :: tl) -> ind t
-      | _                -> false
-   in
-   let rec constr = function
-      | C.MutConstruct _ -> true
-      | C.Appl (t :: tl) -> constr t
-      | _                -> false
-   in
-   let subst_tac status =
-      let (proof, goal) = status in
-      let (_, metasenv, _subst, _, _, _) = proof in
-      let _, context, _ = CicUtil.lookup_meta goal metasenv in
-      let what = match PEH.get_rel context hyp with
-         | Some t -> t
-        | None   -> raise (PET.Fail msg0)
-      in
-      let ty, _ = TC.type_of_aux' metasenv context what CicUniv.empty_ugraph in
-      let subst_g direction i t =
-         let rewrite pattern =
-            let tactic = lift_rewrite_tac ~context ~direction ~pattern what in
-           try_tactic ~tactic
-         in
-         let var = match PEH.get_name context i with
-            | Some name -> name
-           | None      -> raise (PET.Fail msg0)        
-         in
-         if DTI.does_not_occur i t then () else raise (PET.Fail msg2);
-         let map self = function
-            | Some (C.Name s, _) when s <> self -> 
-               Some (rewrite (None, [(s, hole)], None))
-            | _                                 -> None
-         in
-         let rew_hips = HEL.list_rev_map_filter (map hyp) context in
-         let rew_concl = rewrite (None, [], Some hole) in
-         let clear = PESR.clear ~hyps:[hyp; var] in
-         List.rev_append (rew_concl :: rew_hips) [clear]
-      in
-      let destruct_g () =
-         [lift_destruct_tac ~context ~what; PESR.clear ~hyps:[hyp]]
-      in
-      let whd_g () =
-         let whd_pattern = C.Appl [meta; hole; hole; hole] in
-        let pattern = None, [hyp, whd_pattern], None in
-        [RT.whd_tac ~pattern; subst_tac ~try_tactic ~hyp]
-      in
-      let tactics = match ty with
-         | (C.Appl [(C.MutInd (uri, 0, [])); _; C.Rel i; t]) 
-           when LO.is_eq_URI uri -> subst_g `LeftToRight i t
-         | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i]) 
-           when LO.is_eq_URI uri -> subst_g `RightToLeft i t
-        | (C.Appl [(C.MutInd (uri, 0, [])); t; t1; t2]) 
-           when LO.is_eq_URI uri && ind t && constr t1 && constr t2 -> destruct_g ()
-        | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2])
-           when LO.is_eq_URI uri -> whd_g ()    
-        | _ -> raise (PET.Fail msg1)
-      in
-      PET.apply_tactic (T.seq ~tactics) status
-   in
-   PET.mk_tactic subst_tac
-
-let subst_tac =
-   let subst_tac status =
-      let progress = ref false in
-      let try_tactic ~tactic =
-         let try_tactic status =
-            try 
-              let result = PET.apply_tactic tactic status in
-              progress := true; result
-           with
-               | PET.Fail _ -> PET.apply_tactic T.id_tac status
-         in
-         PET.mk_tactic try_tactic
-      in
-      let subst hyp = try_tactic ~tactic:(subst_tac ~try_tactic ~hyp) in
-      let map = function
-         | Some (C.Name s, _) -> Some (subst s)
-         | _                  -> None
-      in
-      let (proof, goal) = status in
-      let (_, metasenv, _subst, _, _, _) = proof in
-      let _, context, _ = CicUtil.lookup_meta goal metasenv in
-      let tactics = HEL.list_rev_map_filter map context in
-      let result = PET.apply_tactic (T.seq ~tactics) status in
-      if !progress then result else raise (PET.Fail msg3)
-   in
-   PET.mk_tactic subst_tac
-
-   let try_tac tactic = T.try_tactic ~tactic 
-   let then_tac start continuation = T.then_ ~start ~continuation 
-
-let subst_tac = 
-   let tactic = T.repeat_tactic ~tactic:subst_tac in
-   T.try_tactic ~tactic 
diff --git a/helm/software/components/tactics/substTactic.mli b/helm/software/components/tactics/substTactic.mli
deleted file mode 100644 (file)
index cce9d0f..0000000
+++ /dev/null
@@ -1,27 +0,0 @@
-(* Copyright (C) 2002, 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/.
- *)
-
-(* rewrites and clears all simple equalities in the context *)
-val subst_tac: ProofEngineTypes.tactic
index 67a607d1acf16087a7caa65a57ad67bafa88d79d..aa2e2bf4fc3dab3221f0b4651a575d777820ce64 100644 (file)
@@ -39,7 +39,7 @@ let contradiction = NegationTactics.contradiction_tac
 let cut = PrimitiveTactics.cut_tac
 let decompose = EliminationTactics.decompose_tac
 let demodulate = Auto.demodulate_tac
-let destruct = DiscriminationTactics.destruct_tac
+let destruct = DestructTactic.destruct_tac
 let elim_intros = PrimitiveTactics.elim_intros_tac
 let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac
 let elim_type = EliminationTactics.elim_type_tac
@@ -67,7 +67,6 @@ let ring = Ring.ring_tac
 let simpl = ReductionTactics.simpl_tac
 let solve_rewrite = Auto.solve_rewrite_tac
 let split = IntroductionTactics.split_tac
-let subst = SubstTactic.subst_tac
 let symmetry = EqualityTactics.symmetry_tac
 let transitivity = EqualityTactics.transitivity_tac
 let unfold = ReductionTactics.unfold_tac
index fb62b85fc32f680371dec8b1df5d03d6894c8ccf..a58752461695fd96769104904d95513be939a09b 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jul  6 11:03:35 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Nov  6 16:23:06 CET 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -32,7 +32,7 @@ val decompose :
   unit -> ProofEngineTypes.tactic
 val demodulate :
   dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
-val destruct : term:Cic.term -> ProofEngineTypes.tactic
+val destruct : Cic.term option -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int ->
@@ -98,7 +98,6 @@ val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val solve_rewrite :
   universe:Universe.universe -> ?steps:int -> unit -> ProofEngineTypes.tactic
 val split : ProofEngineTypes.tactic
-val subst : ProofEngineTypes.tactic
 val symmetry : ProofEngineTypes.tactic
 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
 val unfold :
index 177edbb4575441575330b299d0e573417c8f0d16..2a5367834890b395b980fd2de1e6af23989b8ca1 100644 (file)
@@ -224,7 +224,7 @@ lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
             (in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))).
 intros 10;elim H
   [simplify in H1;elim (in_cons_case ? ? ? ? H1)
-     [destruct H3;elim (H2 Hcut1)
+     [destruct H3;elim (H2);reflexivity
      |simplify;apply (in_Skip ? ? ? ? H3);]
   |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2)
      [rewrite > H4;apply in_Base
@@ -323,18 +323,16 @@ lemma WFE_Typ_subst : \forall H,x,B,C,T,U,G.
 intros 7;elim H 0
   [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1;intros
      [lapply (nil_cons ? G (mk_bound B x T));elim (Hletin H4)
-     |destruct H8;rewrite < Hcut2 in H6;rewrite < Hcut in H4;
-      rewrite < Hcut in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)]
+     |destruct H8;apply (WFE_cons ? ? ? ? H4 H6 H2)]
   |intros;simplify;generalize in match H2;elim t;simplify in H4;
    inversion H4;intros
      [destruct H5
      |destruct H9;apply WFE_cons
-        [rewrite < Hcut in H5;apply (H1 H5 H3)
-        |rewrite < (fv_env_extends ? x B C T U);rewrite > Hcut;rewrite > Hcut2;
-         assumption
-        |rewrite < Hcut3 in H8;rewrite > Hcut1;apply (WFT_env_incl ? ? H8);
+        [apply (H1 H5 H3)
+        |rewrite < (fv_env_extends ? x B C T U); assumption
+        |apply (WFT_env_incl ? ? H8);
          rewrite < (fv_env_extends ? x B C T U);unfold;intros;
-         rewrite > Hcut;assumption]]]
+         assumption]]]
 qed.
 
 lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to
@@ -343,13 +341,13 @@ lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to
 intros 6;elim H
   [lapply (in_list_nil ? ? H1);elim Hletin
   |elim (in_cons_case ? ? ? ? H6)
-     [destruct H7;subst;elim (in_cons_case ? ? ? ? H5)
-        [destruct H7;assumption
-        |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? b);
+     [destruct H7;destruct;elim (in_cons_case ? ? ? ? H5)
+        [destruct H7;reflexivity
+        |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B);
          apply (ex_intro ? ? T);assumption]
      |elim (in_cons_case ? ? ? ? H5)
         [destruct H8;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B);
-         apply (ex_intro ? ? U);rewrite < Hcut1;assumption
+         apply (ex_intro ? ? U);assumption
         |apply (H2 H8 H7)]]]
 qed.
 
@@ -360,8 +358,8 @@ lemma WFT_to_incl: ∀G,T,U.
 intros.elim (fresh_name ((fv_type U)@(fv_env G))).lapply(H a)
   [unfold;intros;lapply (fv_WFT ? x ? Hletin)
      [simplify in Hletin1;inversion Hletin1;intros
-        [destruct H4;elim H1;rewrite > Hcut;rewrite < H3.autobatch
-        |destruct H6;rewrite > Hcut1;assumption]
+        [destruct H4;elim H1;autobatch
+        |destruct H6;assumption]
      |apply in_FV_subst;assumption]
   |*:intro;apply H1;autobatch]
 qed.
index 48543ce18dd07ae6f6c1c65816de48e3f960791d..8558725cc883569783da832862df8b0d1ed8e969 100644 (file)
@@ -43,8 +43,8 @@ intros 4;elim H
      [unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9)
      |apply (WFE_cons ? ? ? ? H6 H8);autobatch
      |unfold;intros;inversion H9;intros
-        [destruct H11;rewrite > Hcut;apply in_Base
-        |destruct H13;rewrite < Hcut1 in H10;apply in_Skip;apply (H7 ? H10)]]]
+        [destruct H11;apply in_Base
+        |destruct H13;apply in_Skip;apply (H7 ? H10)]]]
 qed.
 
 theorem narrowing:∀X,G,G1,U,P,M,N.
@@ -87,15 +87,15 @@ intros 3;elim H;clear H; try autobatch;
   |generalize in match H7;generalize in match H4;generalize in match H2;
    generalize in match H5;clear H7 H4 H2 H5;
    generalize in match (refl_eq ? (Arrow t t1));
-   elim H6 in ⊢ (? ? ? %→%); clear H6; intros; subst;
+   elim H6 in ⊢ (? ? ? %→%); clear H6; intros; destruct;
     [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? ? H8 H9);autobatch
-    |inversion H11;intros; subst; autobatch depth=4 width=4 size=9;
+    |inversion H11;intros; destruct; autobatch depth=4 width=4 size=9;
     ]
   |generalize in match H7;generalize in match H4;generalize in match H2;
    generalize in match H5;clear H7 H4 H2 H5;
-   generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);subst
+   generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);destruct;
      [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? H7 H8 H9 H10);reflexivity
-     |inversion H11;intros;subst
+     |inversion H11;intros;destruct;
         [apply SA_Top
            [autobatch
               |apply WFT_Forall
@@ -108,7 +108,7 @@ intros 3;elim H;clear H; try autobatch;
                  |intro;apply H15;apply H8;apply (WFT_to_incl ? ? ? H3);
                   assumption
                  |simplify;autobatch
-                 |apply (narrowing X (mk_bound true X t::l2) 
+                 |apply (narrowing X (mk_bound true X t::l1)
                          ? ? ? ? ? H7 ? ? [])
                     [intros;apply H9
                        [unfold;intros;lapply (H8 ? H17);rewrite > fv_append;
index 463ceca958521b08572ad82c6bd64e621aa916af..f96e07679c4b4be9a406cc8a0ec936d4f3f5c6cf 100644 (file)
@@ -43,8 +43,8 @@ intros 4;elim H
      [unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9)
      |apply (WFE_cons ? ? ? ? H6 H8);autobatch
      |unfold;intros;inversion H9;intros
-        [destruct H11;rewrite > Hcut;apply in_Base
-        |destruct H13;rewrite < Hcut1 in H10;apply in_Skip;apply (H7 ? H10)]]]
+        [destruct H11;apply in_Base
+        |destruct H13;apply in_Skip;apply (H7 ? H10)]]]
 qed.
 
 theorem narrowing:∀X,G,G1,U,P,M,N.
@@ -95,10 +95,10 @@ lemma JSubtype_Arrow_inv:
  elim H2 in ⊢ (? ? ? % → ? ? ? % → %);
   [1,2: destruct H6
   |5: destruct H8
-  | lapply (H5 H6 H7); subst; clear H5;
+  | lapply (H5 H6 H7); destruct; clear H5;
     apply H;
     assumption
-  | subst;
+  | destruct;
     clear H4 H6;
     apply H1;
     assumption
@@ -111,13 +111,13 @@ intros 3;elim H;clear H; try autobatch;
   [rewrite > (JSubtype_Top ? ? H3);autobatch
   |apply (JSubtype_Arrow_inv ? ? ? ? ? ? ? H6); intros;
     [ autobatch
-    | inversion H7;intros; subst; autobatch depth=4 width=4 size=9
+    | inversion H7;intros; destruct; autobatch depth=4 width=4 size=9
     ]
   |generalize in match H7;generalize in match H4;generalize in match H2;
    generalize in match H5;clear H7 H4 H2 H5;
-   generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);subst
+   generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);destruct;
      [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? H7 H8 H9 H10);reflexivity
-     |inversion H11;intros;subst
+     |inversion H11;intros;destruct;
         [apply SA_Top
            [autobatch
               |apply WFT_Forall
@@ -130,7 +130,7 @@ intros 3;elim H;clear H; try autobatch;
                  |intro;apply H15;apply H8;apply (WFT_to_incl ? ? ? H3);
                   assumption
                  |simplify;autobatch
-                 |apply (narrowing X (mk_bound true X t::l2
+                 |apply (narrowing X (mk_bound true X t::l1
                          ? ? ? ? ? H7 ? ? [])
                     [intros;apply H9
                        [unfold;intros;lapply (H8 ? H17);rewrite > fv_append;
index 41089172e56d6c76ece6e834aa665db4ba8feee9..4f5e1542232f753e7fbb209ecc3fbb0a7ec69760 100644 (file)
@@ -73,7 +73,7 @@ qed.
 
 lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ∈ t).
 intros;inversion H;intros
-  [destruct H2;left;symmetry;assumption
+  [destruct H2;left;symmetry;reflexivity
   |destruct H4;right;applyS H1]
 qed.
 
@@ -112,15 +112,12 @@ theorem append_to_or_in_list: \forall A:Type.\forall x:A.
 intros 3.
 elim l
   [right.apply H
-  |simplify in H1.inversion H1;intros
-    [destruct H3.left.rewrite < Hcut.
-     apply in_Base
-    |destruct H5.
-     elim (H l2)
-      [left.apply in_Skip.
-       rewrite < H4.assumption
-      |right.rewrite < H4.assumption
-      |rewrite > Hcut1.rewrite > H4.assumption
+  |simplify in H1.inversion H1;intros; destruct;
+    [left.apply in_Base
+    | elim (H l2)
+      [left.apply in_Skip. assumption
+      |right.assumption
+      |assumption
       ]
     ]
   ]
index 64b608cb9524602afa01054b31624d833f9d8d0c..ac530c38fe02b7df1766fd69ff93a637162131b0 100644 (file)
@@ -122,7 +122,7 @@ elim x.
   (* goal: x=pos y=pos *)
     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
     left.apply eq_f.assumption.
-    right.unfold Not.intros (H_inj).apply H. destruct H_inj. assumption.
+    right.unfold Not.intros (H_inj).apply H. destruct H_inj. reflexivity.
   (* goal: x=pos y=neg *)
     right.unfold Not.intro.apply (not_eq_pos_neg n n1). assumption.
 (* goal: x=neg *)
index f4ba8abdedd71decd9eb5745d0d71aca9cbef4aa..5b28071dcff455d2cc37d02a3f603861d05842e8 100644 (file)
@@ -35,7 +35,7 @@ apply prove_reflect; intros;
  [1: generalize in match H; rewrite > (b2pT ? ? (eqP (list_eqType d2) ? ?) H2); 
      intros; clear H H2; rewrite < (pirrel ? ? ? H1 H3 (eqType_decidable nat_eqType));
      reflexivity
- |2: unfold Not; intros (H3); destruct H3; rewrite > Hcut in H2;
+ |2: unfold Not; intros (H3); destruct H3;
      rewrite > (cmp_refl (list_eqType d2)) in H2; destruct H2;]
 qed.
 
index b68858d68b11f7bef762a24d88fa284660e2eca5..c1a03060b27ea43871a5c837776876d598771fb2 100644 (file)
@@ -98,7 +98,7 @@ cases c; intros (H); [ apply reflect_true | apply reflect_false ]
        [ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1;
          destruct H; rewrite > Hcut in H'; apply H'; reflexivity;
        | intros; lapply (IH ? H1) as H'; destruct H;
-         rewrite > Hcut1 in H'; apply H'; reflexivity;]]]]
+         apply H'; reflexivity;]]]]
 qed.
     
 definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).  
index 1d6a51494a7faf854732dc965a4ed5666ec9fa6d..55275c4807bfca6320d31eb3f135fb1173ee257e 100644 (file)
@@ -64,29 +64,28 @@ inductive complex (A,B : Type) : B → A → Type ≝
 | C1 : ∀x:nat.∀a:A.∀b:B. complex A B b a
 | C2 : ∀a,a1:A.∀b,b1:B.∀x:nat. complex A B b1 a1 → complex A B b a.
 
-
 theorem recursive1: ∀ x,y : nat. 
   (C1 ? ? O     (Some ? x) y) = 
   (C1 ? ? (S O) (Some ? x) y) → False.
-intros; destruct H;
+intros; destruct H.
 qed.
 
 theorem recursive2: ∀ x,y,z,t : nat. 
   (C1 ? ? t (Some ? x) y) = 
   (C1 ? ? z (Some ? x) y) → t=z.
-intros; destruct H;assumption.
+intros; destruct H; reflexivity.
 qed.
 
 theorem recursive3: ∀ x,y,z,t : nat. 
   C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? x) y) = 
   C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.
-intros; destruct H;assumption.
+intros; destruct H; reflexivity.
 qed.
 
 theorem recursive4: ∀ x,y,z,t : nat. 
   C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? z) y) = 
   C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.
-intros; destruct H;assumption.
+intros; destruct H; reflexivity.
 qed.
 
 theorem recursive2: ∀ x,y : nat.