From: Ferruccio Guidi Date: Wed, 10 Jan 2007 17:14:52 +0000 (+0000) Subject: attributes now in the proof status: commit 4 X-Git-Tag: 0.4.95@7852~670 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c1e0024285a65a7d3e31bbdf77ad5d12bcdde36c;p=helm.git attributes now in the proof status: commit 4 --- diff --git a/components/content_pres/acic2Procedural.ml b/components/content_pres/acic2Procedural.ml index f568ac7c5..18ded2e79 100644 --- a/components/content_pres/acic2Procedural.ml +++ b/components/content_pres/acic2Procedural.ml @@ -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 ******************************************************) diff --git a/components/content_pres/cicClassify.ml b/components/content_pres/cicClassify.ml index 155ab98f3..0c464c7d9 100644 --- a/components/content_pres/cicClassify.ml +++ b/components/content_pres/cicClassify.ml @@ -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) diff --git a/components/content_pres/objPp.ml b/components/content_pres/objPp.ml index 68badf324..3cdad5528 100644 --- a/components/content_pres/objPp.ml +++ b/components/content_pres/objPp.ml @@ -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 diff --git a/components/content_pres/proceduralTypes.ml b/components/content_pres/proceduralTypes.ml index 700fed082..be1dbee73 100644 --- a/components/content_pres/proceduralTypes.ml +++ b/components/content_pres/proceduralTypes.ml @@ -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 diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index f38dbf859..ce9ea017b 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -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" diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma index 3c64c05f2..ceb52445e 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma @@ -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) diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma index 2ebbe44de..db6954922 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma @@ -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/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma deleted file mode 100644 index 6a41598bb..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma +++ /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. diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma index 57901bfd5..d5509cd45 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma @@ -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: diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma index 9bd72de7a..f53e2d1ac 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma @@ -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/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma new file mode 100644 index 000000000..5f5915958 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma @@ -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. diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma index e2bfeaa7c..2eaacdde5 100644 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma @@ -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) diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma index 7751a0d1f..a3357f8e0 100644 --- a/matita/contribs/prova.ma +++ b/matita/contribs/prova.ma @@ -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". +*)