]> matita.cs.unibo.it Git - helm.git/commitdiff
procedural: added fwd rewrite in arbitrary proofs (not just premises)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 12 Jan 2007 19:34:58 +0000 (19:34 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 12 Jan 2007 19:34:58 +0000 (19:34 +0000)
            added whd conversion before intros when needed
prova.ma  : highlighted a bug with the "in" clause of the "match" constr.

components/content_pres/.depend
components/content_pres/.depend.opt
components/content_pres/Makefile
components/content_pres/acic2Procedural.ml
components/content_pres/proceduralConversion.ml [new file with mode: 0644]
components/content_pres/proceduralConversion.mli [new file with mode: 0644]
components/content_pres/proceduralTypes.ml
components/content_pres/proceduralTypes.mli
matita/contribs/prova.ma

index 759898ac62d342cc27c7eedb2251fb840dbbc47d..78cde4140ab91a9780f28b05dc7b582173092baf 100644 (file)
@@ -32,6 +32,8 @@ content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
     cicNotationPres.cmx box.cmx content2pres.cmi 
 cicClassify.cmo: cicClassify.cmi 
 cicClassify.cmx: cicClassify.cmi 
+proceduralConversion.cmo: proceduralConversion.cmi 
+proceduralConversion.cmx: proceduralConversion.cmi 
 proceduralTypes.cmo: proceduralTypes.cmi 
 proceduralTypes.cmx: proceduralTypes.cmi 
 acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi 
index 759898ac62d342cc27c7eedb2251fb840dbbc47d..78cde4140ab91a9780f28b05dc7b582173092baf 100644 (file)
@@ -32,6 +32,8 @@ content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
     cicNotationPres.cmx box.cmx content2pres.cmi 
 cicClassify.cmo: cicClassify.cmi 
 cicClassify.cmx: cicClassify.cmi 
+proceduralConversion.cmo: proceduralConversion.cmi 
+proceduralConversion.cmx: proceduralConversion.cmi 
 proceduralTypes.cmo: proceduralTypes.cmi 
 proceduralTypes.cmx: proceduralTypes.cmi 
 acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi 
index a3b153029b6391b5cefb7918193ec1d52ac90220..9c627cb234a91db05b90eb4cd32d10d349412f28 100644 (file)
@@ -1,24 +1,25 @@
 PACKAGE = content_pres
 PREDICATES =
 
-INTERFACE_FILES =              \
-       renderingAttrs.mli      \
-       cicNotationLexer.mli    \
-       cicNotationParser.mli   \
-       mpresentation.mli       \
-       box.mli                 \
-       content2presMatcher.mli \
-       termContentPres.mli     \
-       cicNotationPres.mli     \
-       boxPp.mli               \
-       content2pres.mli        \
-       cicClassify.mli         \
-       proceduralTypes.mli     \
-       acic2Procedural.mli     \
-       objPp.mli               \
-       sequent2pres.mli        \
+INTERFACE_FILES =               \
+       renderingAttrs.mli       \
+       cicNotationLexer.mli     \
+       cicNotationParser.mli    \
+       mpresentation.mli        \
+       box.mli                  \
+       content2presMatcher.mli  \
+       termContentPres.mli      \
+       cicNotationPres.mli      \
+       boxPp.mli                \
+       content2pres.mli         \
+       cicClassify.mli          \
+       proceduralConversion.mli \
+       proceduralTypes.mli      \
+       acic2Procedural.mli      \
+       objPp.mli                \
+       sequent2pres.mli         \
        $(NULL)
-IMPLEMENTATION_FILES =         \
+IMPLEMENTATION_FILES =          \
        $(INTERFACE_FILES:%.mli=%.ml)
 
 cicNotationPres.cmi: OCAMLOPTIONS += -rectypes
index 9b8dbf06383143c7759c9b7f06bb1c95df6ec83a..c92d108e5500f3ed4bb0c159a04399fdc68d4fa3 100644 (file)
  *)
 
 module C    = Cic
-module L    = CicClassify
-module P    = ProceduralTypes
 module D    = Deannotate
 module DTI  = DoubleTypeInference
 module TC   = CicTypeChecker 
-module U    = CicUniv
+module Un   = CicUniv
 module UM   = UriManager
 module Obj  = LibraryObjects
 module HObj = HelmLibraryObjects
 module A    = Cic2acic
-module T    = CicUtil
+module Ut   = CicUtil
+module E    = CicEnvironment
+
+module Cl   = CicClassify
+module T    = ProceduralTypes
+module Cn   = ProceduralConversion
 
 type status = {
-   sorts : (C.id, Cic2acic.sort_kind) Hashtbl.t;
+   sorts : (C.id, A.sort_kind) Hashtbl.t;
    types : (C.id, A.anntypes) Hashtbl.t;
    prefix: string;
    max_depth: int option;
    depth: int;
    entries: C.context;
-   intros: string list
+   intros: string list;
+   ety: C.annterm option
 }
 
 (* helpers ******************************************************************)
@@ -53,8 +57,8 @@ let cic = D.deannotate_term
 let split2_last l1 l2 =
 try
    let n = pred (List.length l1) in
-   let before1, after1 = P.list_split n l1 in
-   let before2, after2 = P.list_split n l2 in
+   let before1, after1 = T.list_split n l1 in
+   let before2, after2 = T.list_split n l2 in
    before1, before2, List.hd after1, List.hd after2
 with Invalid_argument _ -> failwith "A2P.split2_last"
 
@@ -76,9 +80,13 @@ let string_of_head = function
    | C.AMeta _         -> "meta"
    | C.AImplicit _     -> "implict"
 
-let next st = {st with depth = succ st.depth; intros = []}
+let next st = {st with depth = succ st.depth; intros = []; ety = None}
+
+let set_ety st ety =
+   if st.ety = None then {st with ety = ety} else st
 
-let add st entry intro = 
+let add st entry intro ety = 
+   let st = set_ety st ety in
    {st with entries = entry :: st.entries; intros = intro :: st.intros}
 
 let test_depth st =
@@ -90,17 +98,54 @@ try
          if st.depth < d then true, msg else false, "DEPTH EXCEDED"
 with Invalid_argument _ -> failwith "A2P.test_depth"
 
-let get_itype st v =
+let is_rewrite_right = function
+   | C.AConst (_, uri, []) ->
+      UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri
+   | _                     -> false
+
+let is_rewrite_left = function
+   | C.AConst (_, uri, []) ->
+      UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
+   | _                     -> false
+(*
+let get_ind_name uri tno xcno =
+try   
+   let ts = match E.get_obj Un.empty_ugraph uri with
+      | C.InductiveDefinition (ts, _, _,_), _ -> ts 
+      | _                                     -> assert false
+   in
+   let tname, cs = match List.nth ts tno with
+      | (name, _, _, cs) -> name, cs
+   in
+   match xcno with
+      | None     -> tname
+      | Some cno -> fst (List.nth cs (pred cno))
+with Invalid_argument _ -> failwith "A2P.get_ind_name"
+*)
+let get_inner_types st v =
 try
-   let id = T.id_of_annterm v in
-   try Some ((Hashtbl.find st.types id).A.annsynthesized)
+   let id = Ut.id_of_annterm v in
+   try match Hashtbl.find st.types id with
+      | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et)
+      | {A.annsynthesized = st; A.annexpected = None}    -> Some (st, st)
    with Not_found -> None
-with Invalid_argument _ -> failwith "A2P.get_itype"
+with Invalid_argument _ -> failwith "A2P.get_inner_types"
+
+let get_inner_sort st v =
+try
+   let id = Ut.id_of_annterm v in
+   try Hashtbl.find st.sorts id
+   with Not_found -> `Type (CicUniv.fresh())
+with Invalid_argument _ -> failwith "A2P.get_sort"
 
 (* proof construction *******************************************************)
 
 let unused_premise = "UNUSED"
 
+let defined_premise = "DEFINED"
+
+let assumed_premise = "ASSUMED"
+
 let get_intro name t = 
 try
 match name with 
@@ -113,114 +158,128 @@ let mk_intros st script =
 try
    if st.intros = [] then script else
    let count = List.length st.intros in
-   P.Intros (Some count, List.rev st.intros, "") :: script
+   let p0 = T.Whd (count, "") in
+   let p1 = T.Intros (Some count, List.rev st.intros, "") in
+   match st.ety with
+      | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script
+      | _                                   -> p1 :: script
 with Invalid_argument _ -> failwith "A2P.mk_intros"
+(*
+let rec mk_premise st dtext = function
+   | C.ARel (_, _, _, binder)  -> [], binder
+   | where                     -> 
+      let name = contracted_premise in
+      mk_fwd_proof st dtext name where, name
+*)
+let rec mk_fwd_rewrite st dtext name tl direction =
+   let what, where = List.nth tl 5, List.nth tl 3 in
+   let rewrite premise =
+      [T.Rewrite (direction, what, Some (premise, name), dtext)]
+   in
+   match where with
+      | C.ARel (_, _, _, binder) -> rewrite binder
+      | _                        -> 
+        assert (get_inner_sort st where = `Prop);
+        let pred, old = List.nth tl 2, List.nth tl 1 in
+        let pred_name = defined_premise in
+        let pred_text = "extracted" in
+         let p1 = T.LetIn (pred_name, pred, pred_text) in
+        let cut_name = assumed_premise in
+        let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in
+        let cut_text = "" in
+         let p2 = T.Cut (cut_name, cut_type, cut_text) in
+         let qs = [rewrite cut_name; mk_proof (next st) where] in 
+         [T.Branch (qs, ""); p2; p1] 
 
-let is_rewrite_right = function
-   | C.AConst (_, uri, []) ->
-      UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri
-   | _                     -> false
-
-let is_rewrite_left = function
-   | C.AConst (_, uri, []) ->
-      UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
-   | _                     -> false
-
-let mk_premise = function
-   | C.ARel (_, _, _, binder) -> binder
-   | C.AVar (_, uri, _)
-   | C.AConst (_, uri, _)                  -> UM.name_of_uri uri
-   | C.ASort (_, sort)                     -> assert false
-   | C.AMutInd (_, uri, tno, _)            -> assert false
-   | C.AMutConstruct (_, uri, tno, cno, _) -> assert false
-   | _                                     -> assert false
-
-let rec mk_fwd_proof st dtext name = function
+and mk_fwd_proof st dtext name = function
    | C.AAppl (_, hd :: tl) as v -> 
-      if is_rewrite_right hd then
-         let what, where = List.nth tl 5, List.nth tl 3 in
-        let premise = mk_premise where in
-        [P.Rewrite (true, what, Some (premise, name), dtext)] 
-      else if is_rewrite_left hd then
-         let what, where = List.nth tl 5, List.nth tl 3 in
-        let premise = mk_premise where in
-        [P.Rewrite (false, what, Some (premise, name), dtext)]
-      else begin match get_itype st v with
-         | Some ty ->
-           let qs = [[P.Id ""]; mk_proof (next st) v] in
-           [P.Branch (qs, ""); P.Cut (name, ty, dtext)]
-         | None    ->         
-            let ty, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in
-            let (classes, rc) as h = L.classify ty in
-            let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in
-            [P.LetIn (name, v, dtext ^ text)]
+      if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else  
+      if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
+      begin match get_inner_types st v with
+         | Some (ity, _) ->
+           let qs = [[T.Id ""]; mk_proof (next st) v] in
+           [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
+         | None          ->
+            let ty, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in
+            let (classes, rc) as h = Cl.classify ty in
+            let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
+            [T.LetIn (name, v, dtext ^ text)]
       end
    | v                          -> 
-      [P.LetIn (name, v, dtext)] 
+      [T.LetIn (name, v, dtext)] 
 
 and mk_proof st = function
-   | C.ALambda (_, name, v, t) -> 
+   | C.ALambda (_, name, v, t) as what -> 
       let entry = Some (name, C.Decl (cic v)) in
       let intro = get_intro name t in
-      mk_proof (add st entry intro) t
+      let ety = match get_inner_types st what with
+         | Some (_, ety) -> Some ety
+        | None          -> None
+      in
+      mk_proof (add st entry intro ety) t
    | C.ALetIn (_, name, v, t) as what ->
       let proceed, dtext = test_depth st in
       let script = if proceed then 
          let entry = Some (name, C.Def (cic v, None)) in
          let intro = get_intro name t in
-         let q = mk_proof (next (add st entry intro)) t in
+         let q = mk_proof (next (add st entry intro None)) t in
          List.rev_append (mk_fwd_proof st dtext intro v) q
       else
-        [P.Apply (what, dtext)]
+        [T.Apply (what, dtext)]
       in
       mk_intros st script
    | C.ARel _ as what           ->
       let _, dtext = test_depth st in
-      let script = [P.Apply (what, dtext)] in 
+      let text = "assumption" in
+      let script = [T.Apply (what, dtext ^ text)] in 
       mk_intros st script
+   | C.AMutConstruct _ as what   ->
+      let _, dtext = test_depth st in
+      let script = [T.Apply (what, dtext)] in 
+      mk_intros st script   
    | C.AAppl (_, hd :: tl) as t  ->
       let proceed, dtext = test_depth st in
       let script = if proceed then
-         let ty, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in
-         let (classes, rc) as h = L.classify ty in
-         let synth = L.S.singleton 0 in
-         let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in
+         let ty, _ = TC.type_of_aux' [] st.entries (cic hd) Un.empty_ugraph in
+         let (classes, rc) as h = Cl.classify ty in
+         let synth = Cl.S.singleton 0 in
+         let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
          match rc with
             | Some (i, j) when i > 1 ->
               let classes, tl, _, what = split2_last classes tl in
-              let synth = L.S.add 1 synth in
+              let synth = Cl.S.add 1 synth in
               let qs = mk_bkd_proofs (next st) synth classes tl in
                if is_rewrite_right hd then 
-                 [P.Rewrite (false, what, None, dtext); P.Branch (qs, "")]
+                 [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
               else if is_rewrite_left hd then 
-                 [P.Rewrite (true, what, None, dtext); P.Branch (qs, "")]
+                 [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
               else   
                  let using = Some hd in
-                 [P.Elim (what, using, dtext ^ text); P.Branch (qs, "")]
+                 [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
            | _                                             ->
               let qs = mk_bkd_proofs (next st) synth classes tl in
-               [P.Apply (hd, dtext ^ text); P.Branch (qs, "")]
+               [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
       else
-         [P.Apply (t, dtext)]
+         [T.Apply (t, dtext)]
       in
       mk_intros st script
    | t ->
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
-      let script = [P.Note text] in
+      let script = [T.Note text] in
       mk_intros st script
 
 and mk_bkd_proofs st synth classes ts =
 try 
    let _, dtext = test_depth st in   
    let aux inv v =
-      if L.overlaps synth inv then None else
-      if L.S.is_empty inv then Some (mk_proof st v) else
-      Some [P.Apply (v, dtext ^ "dependent")]
+      if Cl.overlaps synth inv then None else
+      if Cl.S.is_empty inv then Some (mk_proof st v) else
+      Some [T.Apply (v, dtext ^ "dependent")]
    in
    let l1, l2 = List.length classes, List.length ts in
    if l1 > l2 then failwith "partial application" else
    if l1 < l2 then failwith "too many arguments" else
-   P.list_map2_filter aux classes ts
+   T.list_map2_filter aux classes ts
 with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
 
 (* object costruction *******************************************************)
@@ -231,10 +290,10 @@ let is_theorem pars =
 
 let mk_obj st = function
    | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
-      let ast = mk_proof st v in
-      let count = P.count_steps 0 ast in
+      let ast = mk_proof (set_ety st (Some t)) v in
+      let count = T.count_steps 0 ast in
       let text = Printf.sprintf "tactics: %u" count in
-      P.Theorem (s, t, text) :: ast @ [P.Qed ""]
+      T.Theorem (s, t, text) :: ast @ [T.Qed ""]
    | _                                                               ->
       failwith "not a theorem"
 
@@ -248,9 +307,10 @@ let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj =
       max_depth = None;
       depth     = 0;
       entries   = [];
-      intros    = []
+      intros    = [];
+      ety       = None
    } in
    prerr_endline "Level 2 transformation";
    let steps = mk_obj st aobj in
    prerr_endline "grafite rendering";
-   List.rev (P.render_steps [] steps)
+   List.rev (T.render_steps [] steps)
diff --git a/components/content_pres/proceduralConversion.ml b/components/content_pres/proceduralConversion.ml
new file mode 100644 (file)
index 0000000..e506a8f
--- /dev/null
@@ -0,0 +1,32 @@
+(* Copyright (C) 2003-2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module C = Cic
+
+let rec need_whd i = function
+   | C.ACast (_, t, _)               -> need_whd i t
+   | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t
+   | _                    when i > 0 -> true
+   | _                               -> false
diff --git a/components/content_pres/proceduralConversion.mli b/components/content_pres/proceduralConversion.mli
new file mode 100644 (file)
index 0000000..448112c
--- /dev/null
@@ -0,0 +1,26 @@
+(* Copyright (C) 2003-2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val need_whd: int -> Cic.annterm -> bool
index 0ef73e2488d84b170a45f23f1edfc0e8d5c1ce9d..b7f6d3c6b68b2baf49909f448e86c5aa2f83e3e4 100644 (file)
@@ -75,6 +75,7 @@ type step = Note of note
          | Rewrite of how * what * where * note
          | Elim of what * using option * note
          | Apply of what * note
+         | Whd of count * note
          | Branch of step list list * note
 
 (* annterm constructors *****************************************************)
@@ -85,6 +86,8 @@ let mk_arel i b = Cic.ARel ("", "", i, b)
 
 let floc = H.dummy_floc
 
+let hole = C.AImplicit ("", Some `Hole)
+
 let mk_note str = G.Comment (floc, G.Note (floc, str))
 
 let mk_theorem name t = 
@@ -114,7 +117,6 @@ let mk_letin name what =
    mk_tactic tactic
 
 let mk_rewrite direction what where =
-   let hole = C.AImplicit ("", Some `Hole) in
    let direction = if direction then `RightToLeft else `LeftToRight in 
    let pattern, rename = match where with
       | None                 -> (None, [], Some hole), []
@@ -131,6 +133,11 @@ let mk_apply t =
    let tactic = G.Apply (floc, t) in
    mk_tactic tactic
 
+let mk_whd i =
+   let pattern = None, [], Some hole in
+   let tactic = G.Reduce (floc, `Whd, pattern) in
+   mk_tactic tactic
+
 let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None))
 
 let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None))
@@ -154,6 +161,7 @@ let rec render_step sep a = function
    | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
    | Elim (t, xu, s)      -> mk_note s :: cont sep (mk_elim t xu :: a)
    | Apply (t, s)         -> mk_note s :: cont sep (mk_apply t :: a)
+   | Whd (c, s)           -> mk_note s :: cont sep (mk_whd c :: a)
    | Branch ([], s)       -> a
    | Branch ([ps], s)     -> render_steps sep a ps
    | Branch (pss, s)      ->
index ebadd9da8b1fa24e8e7697c69db9a6072dcea58e..b06acd1049b1938e815ae4a37c37136fd4150dbb 100644 (file)
@@ -51,10 +51,11 @@ type step = Note of note
          | Rewrite of how * what * where * note
          | Elim of what * using option * note
          | Apply of what * note
+         | Whd of count * note
          | Branch of step list list * note
 
 val render_steps: 
-   (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> 
+   (what, 'a, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> 
    step list -> 
    (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list
 
index a3357f8e0d62f977e059418a4cbad07f21384c44..a2012b12f2ca6a18ee633d6d68c3861fd7442d4d 100644 (file)
@@ -16,6 +16,26 @@ set "baseuri" "cic:/matita/test/prova".
 
 include "../contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma".
 
+alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)".
+alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)".
+(*
+alias id "B" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1)".
+*)
+theorem not_abbr_abst:
+ (Abbr\neq Abst)
+.(* tactics: 7 *)
+whd in \vdash (%).
+intros 1 (H).
+letin DEFINED \def (\lambda ee:B
+ .match ee in B return \lambda _:B.Prop with 
+  [Abbr\rArr True|Abst\rArr False|Void\rArr False]).(* extracted *)
+cut (DEFINED Abbr) as ASSUMED;
+[rewrite > H in ASSUMED:(%) as (H0)
+|apply I
+].
+elim H0 using False_ind names 0.(* 2 C I 2 0 *)
+qed.
+
 alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)".
 alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)".
 alias id "Appl" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/F.ind#xpointer(1/1/1)".