]> matita.cs.unibo.it Git - helm.git/commitdiff
attributes now in the proof status: commit 4
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 10 Jan 2007 17:14:52 +0000 (17:14 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 10 Jan 2007 17:14:52 +0000 (17:14 +0000)
13 files changed:
helm/software/components/content_pres/acic2Procedural.ml
helm/software/components/content_pres/cicClassify.ml
helm/software/components/content_pres/objPp.ml
helm/software/components/content_pres/proceduralTypes.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma [deleted file]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma [new file with mode: 0644]
helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma
helm/software/matita/contribs/prova.ma

index f568ac7c564bb9d5b21dc30f1405afa06c1a1839..18ded2e7969579acd0fb94707f00a6ce1afc8278 100644 (file)
@@ -37,7 +37,7 @@ module A    = Cic2acic
 module T    = CicUtil
 
 type status = {
-   sorts : (Cic.id, Cic2acic.sort_kind) Hashtbl.t;
+   sorts : (C.id, Cic2acic.sort_kind) Hashtbl.t;
    types : (C.id, A.anntypes) Hashtbl.t;
    prefix: string;
    max_depth: int option;
@@ -51,10 +51,12 @@ type status = {
 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
    before1, before2, List.hd after1, List.hd after2
+with Invalid_argument _ -> failwith "A2P.split2_last"
 
 let string_of_head = function
    | C.ASort _         -> "sort"
@@ -80,30 +82,39 @@ let add st entry intro =
    {st with entries = entry :: st.entries; intros = intro :: st.intros}
 
 let test_depth st =
+try   
    let msg = Printf.sprintf "Depth %u: " st.depth in
    match st.max_depth with
       | None   -> true, "" 
       | Some d -> 
          if st.depth < d then true, msg else false, "DEPTH EXCEDED"
+with Invalid_argument _ -> failwith "A2P.test_depth"
 
 let get_itype st v =
+try
    let id = T.id_of_annterm v in
    try Some ((Hashtbl.find st.types id).A.annsynthesized)
    with Not_found -> None
+with Invalid_argument _ -> failwith "A2P.get_itype"
 
 (* proof construction *******************************************************)
 
 let unused_premise = "UNUSED"
 
-let get_intro name t = match name with 
+let get_intro name t = 
+try
+match name with 
    | C.Anonymous -> unused_premise
    | C.Name s    -> 
       if DTI.does_not_occur 1 (cic t) then unused_premise else s
+with Invalid_argument _ -> failwith "A2P.get_intro"
 
 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
+with Invalid_argument _ -> failwith "A2P.mk_intros"
 
 let is_rewrite_right = function
    | C.AConst (_, uri, []) ->
@@ -117,7 +128,12 @@ let is_rewrite_left = function
 
 let mk_premise = function
    | C.ARel (_, _, _, binder) -> binder
-   | _                        -> assert false
+   | 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
    | C.AAppl (_, hd :: tl) as v -> 
@@ -150,8 +166,9 @@ and mk_proof st = function
    | 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 st) t in
+         let q = mk_proof (next (add st entry intro)) t in
          List.rev_append (mk_fwd_proof st dtext intro v) q
       else
         [P.Apply (what, dtext)]
@@ -193,23 +210,33 @@ and mk_proof st = function
       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")]
    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
+with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
 
 (* object costruction *******************************************************)
 
+let is_theorem pars =   
+   List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars || 
+   List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
+
 let mk_obj st = function
-   | C.AConstant (_, _, s, Some v, t, [], _) ->
+   | 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 text = Printf.sprintf "tactics: %u" count in
       P.Theorem (s, t, text) :: ast @ [P.Qed ""]
-   | _                                       -> assert false
+   | _                                                               ->
+      [P.Note "not a theorem"]
 
 (* interface functions ******************************************************)
 
index 155ab98f3fefe7dd936a8f803fe571efccb23984..0c464c7d94d4c8d7500aca63028a2fa4c228934f 100644 (file)
@@ -135,7 +135,7 @@ let classify t =
    in
    let map i (direct, _) = mk_inverse i direct in
    Array.iteri map b;
-   out_table b;
+(*   out_table b; *)
    List.rev_map snd (List.tl (Array.to_list b)), rc
 
 let aclassify t = classify (D.deannotate_term t)
index 68badf3242e3514b406c2deb76cf551bc5720061..3cdad5528a56dac0b13021fa9f743b74d95ee02b 100644 (file)
@@ -32,7 +32,8 @@ let term2pres n ids_to_inner_sorts annterm =
    in
    let bobj =
       CicNotationPres.box_of_mpres (
-         CicNotationPres.render ids_to_uris (TermContentPres.pp_ast ast)
+         CicNotationPres.render ~prec:90 ids_to_uris 
+           (TermContentPres.pp_ast ast)
       )
    in
    let render = function _::x::_ -> x | _ -> assert false in
@@ -41,7 +42,12 @@ let term2pres n ids_to_inner_sorts annterm =
    remove_closed_substs s
 
 let obj_to_string n style prefix obj =
-  let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in
+  let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = 
+     try Cic2acic.acic_object_of_cic_object obj
+     with e -> 
+        let msg = "Cic2ACic: " ^ Printexc.to_string e in
+       failwith msg
+  in
   match style with
      | GrafiteAst.Declarative ->
         let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
index 700fed082c1d89fe3357aff87796d20d9b0f2e17..be1dbee73e7ff7ae18d0cf503b24b4a0b64cf20f 100644 (file)
@@ -155,7 +155,7 @@ let rec render_step sep a = function
    | 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)
    | Branch ([], s)       -> a
-   | Branch ([ps], s)     -> render_steps a ps
+   | Branch ([ps], s)     -> cont sep (render_steps a ps)
    | Branch (pss, s)      ->
       let a =  mk_ob :: a in
       let body = mk_cb :: list_rev_map_concat render_steps mk_vb a pss in
index f38dbf8597dc3caa309f5fb60c45f30f5dc4d40d..ce9ea017b2c1565d6b82302e75f8d1582188a9b4 100644 (file)
@@ -75,7 +75,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
   function
   | Absurd (_, term) -> "absurd" ^ term_pp term
-  | Apply (_, term) -> "apply (" ^ term_pp term ^ ")" (* FG: rm parentheses *)
+  | Apply (_, term) -> "apply " ^ term_pp term
   | ApplyS (_, term, params) ->
      "applyS " ^ term_pp term ^
       String.concat " " 
@@ -93,7 +93,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Constructor (_,n) -> "constructor " ^ string_of_int n
   | Contradiction _ -> "contradiction"
   | Cut (_, ident, term) ->
-     "cut (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *)
+     "cut " ^ term_pp term ^
       (match ident with None -> "" | Some id -> " as " ^ id)
   | Decompose (_, [], what, names) ->
       sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names)) 
@@ -107,7 +107,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Demodulate _ -> "demodulate"
   | Destruct (_, term) -> "destruct " ^ term_pp term
   | Elim (_, term, using, num, idents) ->
-      sprintf "elim (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *)
+      sprintf "elim " ^ term_pp term ^
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
       ^ pp_intros_specs (num, idents) 
   | ElimType (_, term, using, num, idents) ->
@@ -144,7 +144,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
         (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
   | Left _ -> "left"
   | LetIn (_, term, ident) -> 
-     sprintf "letin %s \\def %s" ident ("(" ^ term_pp term ^ ")") (* FG: rm parentheses *)
+     sprintf "letin %s \\def %s" ident (term_pp term)
   | Reduce (_, kind, pat) ->
       sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat)
   | Reflexivity _ -> "reflexivity"
@@ -155,7 +155,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Rewrite (_, pos, t, pattern, names) -> 
       sprintf "rewrite %s %s %s%s" 
         (if pos = `LeftToRight then ">" else "<")
-        ("(" ^ term_pp t ^ ")") (* FG: rm parentheses *)
+        (term_pp t)
         (pp_tactic_pattern pattern)
        (if names = [] then "" else " as " ^ pp_idents names)
   | Right _ -> "right"
index 3c64c05f2a72583ef58f250e62f3f1a230a8af9e..ceb52445e2275eb8bdf21ce579e993e83744959c 100644 (file)
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/blt/defs".
 
-include "ext/preamble.ma".
+include "preamble.ma".
 
 definition blt:
  nat \to (nat \to bool)
index 2ebbe44de123451605a5c03a5dfb9ea53dd2aa8c..db695492205d9d371321bd39048fa7bfe5921d02 100644 (file)
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/arith".
 
-include "ext/preamble.ma".
+include "preamble.ma".
 
 theorem nat_dec:
  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to 
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
deleted file mode 100644 (file)
index 6a41598..0000000
+++ /dev/null
@@ -1,162 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble".
-
-include' "../../../../legacy/coq.ma".
-
-(* FG: This is because "and" is a reserved keyword of the parser *)
-alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
-
-(* FG/CSC: These aliases should disappear: we would like to write something
- *         like: "disambiguate in cic:/Coq/*"
- *)
-alias symbol "plus" = "Coq's natural plus".
-alias symbol "leq" = "Coq's natural 'less or equal to'".
-alias symbol "neq" = "Coq's not equal to (leibnitz)".
-alias symbol "eq" = "Coq's leibnitz's equality".
-
-alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
-alias id "conj" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1/1)".
-alias id "eq_add_S" = "cic:/Coq/Init/Peano/eq_add_S.con".
-alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
-alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
-alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
-alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
-alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con".
-alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)".
-alias id "ex_intro2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1/1)".
-alias id "false" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)".
-alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
-alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
-alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
-alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con".
-alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
-alias id "le_lt_n_Sm" = "cic:/Coq/Arith/Lt/le_lt_n_Sm.con".
-alias id "le_lt_or_eq" = "cic:/Coq/Arith/Lt/le_lt_or_eq.con".
-alias id "le_n" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)".
-alias id "le_n_O_eq" = "cic:/Coq/Arith/Le/le_n_O_eq.con".
-alias id "le_not_lt" = "cic:/Coq/Arith/Lt/le_not_lt.con".
-alias id "le_n_S" = "cic:/Coq/Arith/Le/le_n_S.con".
-alias id "le_O_n" = "cic:/Coq/Arith/Le/le_O_n.con".
-alias id "le_or_lt" = "cic:/Coq/Arith/Lt/le_or_lt.con".
-alias id "le_plus_l" = "cic:/Coq/Arith/Plus/le_plus_l.con".
-alias id "le_plus_minus" = "cic:/Coq/Arith/Minus/le_plus_minus.con".
-alias id "le_plus_minus_r" = "cic:/Coq/Arith/Minus/le_plus_minus_r.con".
-alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
-alias id "le_S" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/2)".
-alias id "le_S_n" = "cic:/Coq/Arith/Le/le_S_n.con".
-alias id "le_Sn_n" = "cic:/Coq/Arith/Le/le_Sn_n.con".
-alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con".
-alias id "lt" = "cic:/Coq/Init/Peano/lt.con".
-alias id "lt_irrefl" = "cic:/Coq/Arith/Lt/lt_irrefl.con".
-alias id "lt_le_S" = "cic:/Coq/Arith/Lt/lt_le_S.con".
-alias id "lt_n_S" = "cic:/Coq/Arith/Lt/lt_n_S.con".
-alias id "minus" = "cic:/Coq/Init/Peano/minus.con".
-alias id "minus_n_O" = "cic:/Coq/Arith/Minus/minus_n_O.con".
-alias id "minus_plus" = "cic:/Coq/Arith/Minus/minus_plus.con".
-alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias id "nat_ind" = "cic:/Coq/Init/Datatypes/nat_ind.con".
-alias id "not" = "cic:/Coq/Init/Logic/not.con".
-alias id "not_eq_S" = "cic:/Coq/Init/Peano/not_eq_S.con".
-alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
-alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
-alias id "or_ind" = "cic:/Coq/Init/Logic/or_ind.con".
-alias id "or_introl" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/1)".
-alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)".
-alias id "O_S" = "cic:/Coq/Init/Peano/O_S.con".
-alias id "plus_assoc" = "cic:/Coq/Arith/Plus/plus_assoc.con".
-alias id "plus_assoc_reverse" = "cic:/Coq/Arith/Plus/plus_assoc_reverse.con".
-alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
-alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
-alias id "plus_le_compat" = "cic:/Coq/Arith/Plus/plus_le_compat.con".
-alias id "plus_le_reg_l" = "cic:/Coq/Arith/Plus/plus_le_reg_l.con".
-alias id "plus_lt_reg_l" = "cic:/Coq/Arith/Plus/plus_lt_reg_l.con".
-alias id "plus_n_Sm" = "cic:/Coq/Init/Peano/plus_n_Sm.con".
-alias id "plus_reg_l" = "cic:/Coq/Arith/Plus/plus_reg_l.con".
-alias id "pred" = "cic:/Coq/Init/Peano/pred.con".
-alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
-alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
-alias id "true" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)".
-alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
-alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
-alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
-alias id "plus_le_lt_compat" = "cic:/Coq/Arith/Plus/plus_le_lt_compat.con".
-alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
-alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
-alias id "and_ind" = "cic:/Coq/Init/Logic/and_ind.con".
-alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
-alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
-alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
-alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
-alias id "f_equal3" = "cic:/Coq/Init/Logic/f_equal3.con".
-alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con".
-alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
-alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
-alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
-alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
-alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
-alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
-alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
-alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
-alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
-alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
-alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
-alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
-alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con".
-alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
-alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
-alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con".
-alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con".
-alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con".
-alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con".
-alias id "plus_lt_compat" = "cic:/Coq/Arith/Plus/plus_lt_compat.con".
-alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con".
-alias id "minus_n_n" = "cic:/Coq/Arith/Minus/minus_n_n.con".
-
-theorem f_equal: \forall A,B:Type. \forall f:A \to B.
-                 \forall x,y:A. x = y \to f x = f y.
- intros. elim H. reflexivity.
-qed.
-
-theorem sym_eq: \forall A:Type. \forall x,y:A. x = y \to y = x.
- intros. rewrite > H. reflexivity.
-qed.
-
-theorem sym_not_eq: \forall A:Type. \forall x,y:A. x \neq y \to y \neq x.
- unfold not. intros. apply H. symmetry. assumption.
-qed.
-
-theorem trans_eq : ∀A:Type.∀x,y,z:A.x=y→y=z→x=z.
- intros;
- transitivity y;
- assumption.
-qed.
-
-theorem plus_reg_l: \forall (n,m,p:nat). n + m = n + p \to m = p.
- intros. apply plus_reg_l; auto.
-qed.
-
-theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m.
- intros. apply plus_le_reg_l; auto.
-qed.
-
-default "equality"
- cic:/Coq/Init/Logic/eq.ind
- cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble/sym_eq.con
- cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble/trans_eq.con
- cic:/Coq/Init/Logic/eq_ind.con
- cic:/Coq/Init/Logic/eq_ind_r.con
- cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble/f_equal.con
- cic:/matita/legacy/coq/f_equal1.con.
index 57901bfd5d78016d0e0690cb50f52a8004647946..d5509cd45c73fa97eb0bab6d10af50fc166997c4 100644 (file)
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/tactics".
 
-include "ext/preamble.ma".
+include "preamble.ma".
 
 theorem insert_eq:
  \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: 
index 9bd72de7a19dbbfb7368cf917ea43e2bb14673bc..f53e2d1acf5caab7d8afcb512aaf55f8243267de 100644 (file)
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/plist/defs".
 
-include "ext/preamble.ma".
+include "preamble.ma".
 
 inductive PList: Set \def
 | PNil: PList
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma
new file mode 100644 (file)
index 0000000..5f59159
--- /dev/null
@@ -0,0 +1,162 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble".
+
+include' "../../../../legacy/coq.ma".
+
+(* FG: This is because "and" is a reserved keyword of the parser *)
+alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
+
+(* FG/CSC: These aliases should disappear: we would like to write something
+ *         like: "disambiguate in cic:/Coq/*"
+ *)
+alias symbol "plus" = "Coq's natural plus".
+alias symbol "leq" = "Coq's natural 'less or equal to'".
+alias symbol "neq" = "Coq's not equal to (leibnitz)".
+alias symbol "eq" = "Coq's leibnitz's equality".
+
+alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
+alias id "conj" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1/1)".
+alias id "eq_add_S" = "cic:/Coq/Init/Peano/eq_add_S.con".
+alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
+alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
+alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con".
+alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
+alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con".
+alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)".
+alias id "ex_intro2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1/1)".
+alias id "false" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)".
+alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
+alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
+alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con".
+alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
+alias id "le_lt_n_Sm" = "cic:/Coq/Arith/Lt/le_lt_n_Sm.con".
+alias id "le_lt_or_eq" = "cic:/Coq/Arith/Lt/le_lt_or_eq.con".
+alias id "le_n" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)".
+alias id "le_n_O_eq" = "cic:/Coq/Arith/Le/le_n_O_eq.con".
+alias id "le_not_lt" = "cic:/Coq/Arith/Lt/le_not_lt.con".
+alias id "le_n_S" = "cic:/Coq/Arith/Le/le_n_S.con".
+alias id "le_O_n" = "cic:/Coq/Arith/Le/le_O_n.con".
+alias id "le_or_lt" = "cic:/Coq/Arith/Lt/le_or_lt.con".
+alias id "le_plus_l" = "cic:/Coq/Arith/Plus/le_plus_l.con".
+alias id "le_plus_minus" = "cic:/Coq/Arith/Minus/le_plus_minus.con".
+alias id "le_plus_minus_r" = "cic:/Coq/Arith/Minus/le_plus_minus_r.con".
+alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
+alias id "le_S" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/2)".
+alias id "le_S_n" = "cic:/Coq/Arith/Le/le_S_n.con".
+alias id "le_Sn_n" = "cic:/Coq/Arith/Le/le_Sn_n.con".
+alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con".
+alias id "lt" = "cic:/Coq/Init/Peano/lt.con".
+alias id "lt_irrefl" = "cic:/Coq/Arith/Lt/lt_irrefl.con".
+alias id "lt_le_S" = "cic:/Coq/Arith/Lt/lt_le_S.con".
+alias id "lt_n_S" = "cic:/Coq/Arith/Lt/lt_n_S.con".
+alias id "minus" = "cic:/Coq/Init/Peano/minus.con".
+alias id "minus_n_O" = "cic:/Coq/Arith/Minus/minus_n_O.con".
+alias id "minus_plus" = "cic:/Coq/Arith/Minus/minus_plus.con".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "nat_ind" = "cic:/Coq/Init/Datatypes/nat_ind.con".
+alias id "not" = "cic:/Coq/Init/Logic/not.con".
+alias id "not_eq_S" = "cic:/Coq/Init/Peano/not_eq_S.con".
+alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
+alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
+alias id "or_ind" = "cic:/Coq/Init/Logic/or_ind.con".
+alias id "or_introl" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/1)".
+alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)".
+alias id "O_S" = "cic:/Coq/Init/Peano/O_S.con".
+alias id "plus_assoc" = "cic:/Coq/Arith/Plus/plus_assoc.con".
+alias id "plus_assoc_reverse" = "cic:/Coq/Arith/Plus/plus_assoc_reverse.con".
+alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
+alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
+alias id "plus_le_compat" = "cic:/Coq/Arith/Plus/plus_le_compat.con".
+alias id "plus_le_reg_l" = "cic:/Coq/Arith/Plus/plus_le_reg_l.con".
+alias id "plus_lt_reg_l" = "cic:/Coq/Arith/Plus/plus_lt_reg_l.con".
+alias id "plus_n_Sm" = "cic:/Coq/Init/Peano/plus_n_Sm.con".
+alias id "plus_reg_l" = "cic:/Coq/Arith/Plus/plus_reg_l.con".
+alias id "pred" = "cic:/Coq/Init/Peano/pred.con".
+alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
+alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
+alias id "true" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)".
+alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
+alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
+alias id "plus_le_lt_compat" = "cic:/Coq/Arith/Plus/plus_le_lt_compat.con".
+alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
+alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
+alias id "and_ind" = "cic:/Coq/Init/Logic/and_ind.con".
+alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
+alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
+alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con".
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
+alias id "f_equal3" = "cic:/Coq/Init/Logic/f_equal3.con".
+alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con".
+alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
+alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con".
+alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
+alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
+alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con".
+alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con".
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
+alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
+alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con".
+alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
+alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con".
+alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con".
+alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con".
+alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con".
+alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con".
+alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con".
+alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con".
+alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con".
+alias id "plus_lt_compat" = "cic:/Coq/Arith/Plus/plus_lt_compat.con".
+alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con".
+alias id "minus_n_n" = "cic:/Coq/Arith/Minus/minus_n_n.con".
+
+theorem f_equal: \forall A,B:Type. \forall f:A \to B.
+                 \forall x,y:A. x = y \to f x = f y.
+ intros. elim H. reflexivity.
+qed.
+
+theorem sym_eq: \forall A:Type. \forall x,y:A. x = y \to y = x.
+ intros. rewrite > H. reflexivity.
+qed.
+
+theorem sym_not_eq: \forall A:Type. \forall x,y:A. x \neq y \to y \neq x.
+ unfold not. intros. apply H. symmetry. assumption.
+qed.
+
+theorem trans_eq : ∀A:Type.∀x,y,z:A.x=y→y=z→x=z.
+ intros;
+ transitivity y;
+ assumption.
+qed.
+
+theorem plus_reg_l: \forall (n,m,p:nat). n + m = n + p \to m = p.
+ intros. apply plus_reg_l; auto.
+qed.
+
+theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m.
+ intros. apply plus_le_reg_l; auto.
+qed.
+
+default "equality"
+ cic:/Coq/Init/Logic/eq.ind
+ cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble/sym_eq.con
+ cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble/trans_eq.con
+ cic:/Coq/Init/Logic/eq_ind.con
+ cic:/Coq/Init/Logic/eq_ind_r.con
+ cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble/f_equal.con
+ cic:/matita/legacy/coq/f_equal1.con.
index e2bfeaa7c9bf784cb54e3333fe99be536151349c..2eaacdde5e91d1da0ffdc402517598b88e0acd54 100644 (file)
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs".
 
-include "ext/preamble.ma".
+include "preamble.ma".
 
 inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
 | and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))).
@@ -32,101 +32,101 @@ inductive or4 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop): Prop \def
 | or4_intro2: P2 \to (or4 P0 P1 P2 P3)
 | or4_intro3: P3 \to (or4 P0 P1 P2 P3).
 
-inductive ex3 (A0: Set) (P0: (A0 \to Prop)) (P1: (A0 \to Prop)) (P2: (A0 \to 
-Prop)): Prop \def
+inductive ex3 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to 
+Prop): Prop \def
 | ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0 
 P0 P1 P2)))).
 
-inductive ex4 (A0: Set) (P0: (A0 \to Prop)) (P1: (A0 \to Prop)) (P2: (A0 \to 
-Prop)) (P3: (A0 \to Prop)): Prop \def
+inductive ex4 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to Prop) 
+(P3: A0 \to Prop): Prop \def
 | ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0) 
 \to (ex4 A0 P0 P1 P2 P3))))).
 
-inductive ex_2 (A0: Set) (A1: Set) (P0: (A0 \to (A1 \to Prop))): Prop \def
+inductive ex_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)): Prop \def
 | ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1 
 P0))).
 
-inductive ex2_2 (A0: Set) (A1: Set) (P0: (A0 \to (A1 \to Prop))) (P1: (A0 \to 
-(A1 \to Prop))): Prop \def
+inductive ex2_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to 
+(A1 \to Prop)): Prop \def
 | ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) 
 \to (ex2_2 A0 A1 P0 P1)))).
 
-inductive ex3_2 (A0: Set) (A1: Set) (P0: (A0 \to (A1 \to Prop))) (P1: (A0 \to 
-(A1 \to Prop))) (P2: (A0 \to (A1 \to Prop))): Prop \def
+inductive ex3_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to 
+(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)): Prop \def
 | ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) 
 \to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))).
 
-inductive ex4_2 (A0: Set) (A1: Set) (P0: (A0 \to (A1 \to Prop))) (P1: (A0 \to 
-(A1 \to Prop))) (P2: (A0 \to (A1 \to Prop))) (P3: (A0 \to (A1 \to Prop))): 
-Prop \def
+inductive ex4_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to 
+(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)) (P3: A0 \to (A1 \to Prop)): Prop 
+\def
 | ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) 
 \to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))).
 
-inductive ex_3 (A0: Set) (A1: Set) (A2: Set) (P0: (A0 \to (A1 \to (A2 \to 
-Prop)))): Prop \def
+inductive ex_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
+Prop))): Prop \def
 | ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 
 x2) \to (ex_3 A0 A1 A2 P0)))).
 
-inductive ex2_3 (A0: Set) (A1: Set) (A2: Set) (P0: (A0 \to (A1 \to (A2 \to 
-Prop)))) (P1: (A0 \to (A1 \to (A2 \to Prop)))): Prop \def
+inductive ex2_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
+Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))): Prop \def
 | ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 
 x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))).
 
-inductive ex3_3 (A0: Set) (A1: Set) (A2: Set) (P0: (A0 \to (A1 \to (A2 \to 
-Prop)))) (P1: (A0 \to (A1 \to (A2 \to Prop)))) (P2: (A0 \to (A1 \to (A2 \to 
-Prop)))): Prop \def
+inductive ex3_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
+Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to 
+Prop))): Prop \def
 | ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 
 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1 
 P2)))))).
 
-inductive ex4_3 (A0: Set) (A1: Set) (A2: Set) (P0: (A0 \to (A1 \to (A2 \to 
-Prop)))) (P1: (A0 \to (A1 \to (A2 \to Prop)))) (P2: (A0 \to (A1 \to (A2 \to 
-Prop)))) (P3: (A0 \to (A1 \to (A2 \to Prop)))): Prop \def
+inductive ex4_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
+Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to 
+Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
 | ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 
 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0 
 A1 A2 P0 P1 P2 P3))))))).
 
-inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: (A0 \to (A1 \to 
-(A2 \to (A3 \to Prop))))) (P1: (A0 \to (A1 \to (A2 \to (A3 \to Prop))))) (P2: 
-(A0 \to (A1 \to (A2 \to (A3 \to Prop))))): Prop \def
+inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to 
+(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0 
+\to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
 | ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to 
 (ex3_4 A0 A1 A2 A3 P0 P1 P2))))))).
 
-inductive ex4_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: (A0 \to (A1 \to 
-(A2 \to (A3 \to Prop))))) (P1: (A0 \to (A1 \to (A2 \to (A3 \to Prop))))) (P2: 
-(A0 \to (A1 \to (A2 \to (A3 \to Prop))))) (P3: (A0 \to (A1 \to (A2 \to (A3 
-\to Prop))))): Prop \def
+inductive ex4_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to 
+(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0 
+\to (A1 \to (A2 \to (A3 \to Prop)))) (P3: A0 \to (A1 \to (A2 \to (A3 \to 
+Prop)))): Prop \def
 | ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to 
 ((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))).
 
-inductive ex4_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: (A0 
-\to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))) (P1: (A0 \to (A1 \to (A2 \to 
-(A3 \to (A4 \to Prop)))))) (P2: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to 
-Prop)))))) (P3: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))): Prop \def
+inductive ex4_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to 
+(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to 
+(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3: 
+A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
 | ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to 
 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1 
 P2 P3))))))))).
 
-inductive ex5_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: (A0 
-\to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))) (P1: (A0 \to (A1 \to (A2 \to 
-(A3 \to (A4 \to Prop)))))) (P2: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to 
-Prop)))))) (P3: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))) (P4: (A0 
-\to (A1 \to (A2 \to (A3 \to (A4 \to Prop)))))): Prop \def
+inductive ex5_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to 
+(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to 
+(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3: 
+A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4: A0 \to (A1 \to (A2 \to 
+(A3 \to (A4 \to Prop))))): Prop \def
 | ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to 
 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to 
 (ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))).
 
 inductive ex6_6 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set) 
-(P0: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop))))))) (P1: (A0 \to 
-(A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop))))))) (P2: (A0 \to (A1 \to (A2 
-\to (A3 \to (A4 \to (A5 \to Prop))))))) (P3: (A0 \to (A1 \to (A2 \to (A3 \to 
-(A4 \to (A5 \to Prop))))))) (P4: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 
-\to Prop))))))) (P5: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to 
-Prop))))))): Prop \def
+(P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P1: A0 \to 
+(A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P2: A0 \to (A1 \to (A2 
+\to (A3 \to (A4 \to (A5 \to Prop)))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to 
+(A4 \to (A5 \to Prop)))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 
+\to Prop)))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to 
+Prop)))))): Prop \def
 | ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1 
 x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5) 
@@ -134,13 +134,13 @@ x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5)
 A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))).
 
 inductive ex6_7 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set) 
-(A6: Set) (P0: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop)))))))) (P1: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop)))))))) (P2: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop)))))))) (P3: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop)))))))) (P4: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop)))))))) (P5: (A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
-Prop)))))))): Prop \def
+(A6: Set) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
+Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
+Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
+Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
+Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
+Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to 
+Prop))))))): Prop \def
 | ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall 
 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2 
 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6) 
index 7751a0d1f62476d90a4241d96f1c5d8c87a2fc1d..a3357f8e0d62f977e059418a4cbad07f21384c44 100644 (file)
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/tests".
+set "baseuri" "cic:/matita/test/prova".
 
-include "../contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma".
+include "../contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma".
 
 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)".
@@ -51,3 +51,10 @@ alias id "THead" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xp
 
 inline procedural
    "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".
+(*
+inline procedural
+   "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3/ty3_sred_wcpr0_pr0.con".
+
+inline procedural
+   "cic:/Coq/Reals/RiemannInt/FTC_Riemann.con".
+*)