From 3ce05ecd50428a27ce17adb070620aeeaf2aed65 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 10 Jan 2007 17:14:52 +0000 Subject: [PATCH] attributes now in the proof status: commit 4 --- .../content_pres/acic2Procedural.ml | 39 ++++++- .../components/content_pres/cicClassify.ml | 2 +- .../software/components/content_pres/objPp.ml | 10 +- .../content_pres/proceduralTypes.ml | 2 +- .../components/grafite/grafiteAstPp.ml | 10 +- .../LAMBDA-TYPES/Level-1/Base/blt/defs.ma | 2 +- .../LAMBDA-TYPES/Level-1/Base/ext/arith.ma | 2 +- .../LAMBDA-TYPES/Level-1/Base/ext/tactics.ma | 2 +- .../LAMBDA-TYPES/Level-1/Base/plist/defs.ma | 2 +- .../Level-1/Base/{ext => }/preamble.ma | 8 +- .../LAMBDA-TYPES/Level-1/Base/types/defs.ma | 104 +++++++++--------- helm/software/matita/contribs/prova.ma | 11 +- 12 files changed, 117 insertions(+), 77 deletions(-) rename helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/{ext => }/preamble.ma (96%) diff --git a/helm/software/components/content_pres/acic2Procedural.ml b/helm/software/components/content_pres/acic2Procedural.ml index f568ac7c5..18ded2e79 100644 --- a/helm/software/components/content_pres/acic2Procedural.ml +++ b/helm/software/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/helm/software/components/content_pres/cicClassify.ml b/helm/software/components/content_pres/cicClassify.ml index 155ab98f3..0c464c7d9 100644 --- a/helm/software/components/content_pres/cicClassify.ml +++ b/helm/software/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/helm/software/components/content_pres/objPp.ml b/helm/software/components/content_pres/objPp.ml index 68badf324..3cdad5528 100644 --- a/helm/software/components/content_pres/objPp.ml +++ b/helm/software/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/helm/software/components/content_pres/proceduralTypes.ml b/helm/software/components/content_pres/proceduralTypes.ml index 700fed082..be1dbee73 100644 --- a/helm/software/components/content_pres/proceduralTypes.ml +++ b/helm/software/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/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index f38dbf859..ce9ea017b 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma index 3c64c05f2..ceb52445e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma index 2ebbe44de..db6954922 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma index 57901bfd5..d5509cd45 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma index 9bd72de7a..f53e2d1ac 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma similarity index 96% rename from helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma rename to helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma index 6a41598bb..5f5915958 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble". +set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble". include' "../../../../legacy/coq.ma". @@ -154,9 +154,9 @@ 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:/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/ext/preamble/f_equal.con + cic:/matita/LAMBDA-TYPES/Level-1/Base/preamble/f_equal.con cic:/matita/legacy/coq/f_equal1.con. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma index e2bfeaa7c..2eaacdde5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma index 7751a0d1f..a3357f8e0 100644 --- a/helm/software/matita/contribs/prova.ma +++ b/helm/software/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". +*) -- 2.39.2