From 5832735b721c0bd8567c8f0be761a9136363a2a6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 13 Mar 2016 17:30:14 +0000 Subject: [PATCH] - new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/) - source specifier on inductive/coinductive types (implies matitaclan all) - minor additions --- matita/components/binaries/Makefile | 5 +- matita/components/content/notationPp.ml | 8 ++-- matita/components/content/notationPt.ml | 6 +-- matita/components/content/notationUtil.ml | 8 ++-- .../content_pres/cicNotationParser.ml | 6 ++- .../components/disambiguation/disambiguate.ml | 4 +- .../grafite_parser/grafiteParser.ml | 47 ++++++++++--------- .../ng_cic_content/interpretations.ml | 4 +- .../ng_disambiguation/grafiteDisambiguate.ml | 4 +- .../ng_disambiguation/nCicDisambiguate.ml | 8 ++-- .../lambdadelta/basic_2/computation/gcp_cr.ma | 2 +- .../basic_2/grammar/lenv_length.ma | 2 +- .../basic_2/grammar/lenv_weight.ma | 2 +- .../basic_2/grammar/term_vector.ma | 2 +- .../basic_2/grammar/term_weight.ma | 2 +- .../contribs/lambdadelta/basic_2/static/sd.ma | 2 +- .../lambdadelta/ground_2/lib/arith.ma | 4 +- .../contribs/lambdadelta/ground_2/lib/list.ma | 4 +- .../lambdadelta/ground_2/lib/list2.ma | 4 +- .../lambdadelta/ground_2/lib/streams_eq.ma | 6 +-- .../lambdadelta/ground_2/lib/streams_tls.ma | 4 +- .../ground_2/relocation/mr2_plus.ma | 2 +- .../ground_2/relocation/nstream.ma | 2 +- .../ground_2/relocation/nstream_after.ma | 4 +- .../ground_2/relocation/nstream_eq.ma | 4 +- .../ground_2/relocation/nstream_id.ma | 2 +- .../ground_2/relocation/nstream_istot.ma | 2 +- .../ground_2/relocation/rtmap_after.ma | 36 +++++++------- .../ground_2/relocation/rtmap_at.ma | 6 +-- .../ground_2/relocation/rtmap_eq.ma | 6 +-- .../ground_2/relocation/rtmap_isid.ma | 10 ++-- .../ground_2/relocation/rtmap_istot.ma | 12 +++-- .../ground_2/relocation/rtmap_sand.ma | 4 +- .../ground_2/relocation/rtmap_sle.ma | 4 +- .../ground_2/relocation/rtmap_sor.ma | 4 +- .../ground_2/relocation/rtmap_tls.ma | 2 +- matita/matita/lib/basics/core_notation.ma | 19 +++++++- matita/matita/lib/fail.txt | 27 +++++++++++ matita/matita/lib/inconsistent.ma | 25 ++++++++++ matita/matita/matita.lang | 1 - 40 files changed, 193 insertions(+), 113 deletions(-) create mode 100644 matita/matita/lib/fail.txt create mode 100644 matita/matita/lib/inconsistent.ma diff --git a/matita/components/binaries/Makefile b/matita/components/binaries/Makefile index 66af4a5f6..15ff284f3 100644 --- a/matita/components/binaries/Makefile +++ b/matita/components/binaries/Makefile @@ -2,8 +2,9 @@ H=@ #CSC: saturate is broken after the huge refactoring of auto/paramodulation #CSC: by Andrea -#BINARIES=extractor table_creator utilities saturate -#BINARIES=transcript +#BINARIES=extractor table_creator utilities saturate transcript +#FG: my binaries +BINARIES=mac matex matitadep probe xoa all: $(BINARIES:%=rec@all@%) opt: $(BINARIES:%=rec@opt@%) diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index baf92236c..49002d108 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -281,7 +281,7 @@ let string_of_source = function | `Generated -> "generated " let pp_obj pp_term = function - | Ast.Inductive (params, types) -> + | Ast.Inductive (params, types, source) -> let pp_constructors constructors = String.concat "\n" (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ)) @@ -295,7 +295,8 @@ let pp_obj pp_term = function | [] -> assert false | (name, inductive, typ, constructors) :: tl -> let fst_typ_pp = - sprintf "%sinductive %s%s: %s \\def\n%s" + sprintf "%s%sinductive %s%s: %s \\def\n%s" + (string_of_source source) (if inductive then "" else "co") name (pp_params pp_term params) (pp_term typ) (pp_constructors constructors) in @@ -309,7 +310,8 @@ let pp_obj pp_term = function (match body with | None -> "" | Some body -> "\\def\n " ^ pp_term body) - | Ast.Record (params,name,ty,fields) -> + | Ast.Record (params,name,ty,fields, source) -> + string_of_source source ^ "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ " \\def {" ^ pp_fields pp_term fields ^ "\n}" | Ast.LetRec (kind, definitions, (source, _, _)) -> diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml index 52d433aa2..c718a20ba 100644 --- a/matita/components/content/notationPt.ml +++ b/matita/components/content/notationPt.ml @@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option (** To be increased each time the term type below changes, used for "safe" * marshalling *) -let magic = 7 +let magic = 8 type term = (* CIC AST *) @@ -173,7 +173,7 @@ type cic_appl_pattern = type 'term inductive_type = string * bool * 'term * (string * 'term) list type 'term obj = - | Inductive of 'term capture_variable list * 'term inductive_type list + | Inductive of 'term capture_variable list * 'term inductive_type list * NCic.source (** parameters, list of loc * mutual inductive types *) | Theorem of string * 'term * 'term option * NCic.c_attr (** name, type, body, attributes @@ -183,7 +183,7 @@ type 'term obj = * will be given in proof editing mode using the tactical language, * unless the flavour is an Axiom *) - | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list + | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list * NCic.source (** left parameters, name, type, fields *) | LetRec of induction_kind * ('term capture_variable list * 'term capture_variable * 'term * int) list * NCic.f_attr (* (params, name, body, decreasing arg) list, attributes *) diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml index 823febdb6..82096f80b 100644 --- a/matita/components/content/notationUtil.ml +++ b/matita/components/content/notationUtil.ml @@ -362,21 +362,21 @@ let freshen_obj obj = let freshen_capture_variable (n, t) = freshen_term n, HExtlib.map_option freshen_term t in let freshen_capture_variables = List.map freshen_capture_variable in match obj with - | NotationPt.Inductive (params, indtypes) -> + | NotationPt.Inductive (params, indtypes, attrs) -> let indtypes = List.map (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors)) indtypes in - NotationPt.Inductive (freshen_capture_variables params, indtypes) + NotationPt.Inductive (freshen_capture_variables params, indtypes, attrs) | NotationPt.Theorem (n, t, ty_opt, attrs) -> let ty_opt = match ty_opt with None -> None | Some ty -> Some (freshen_term ty) in NotationPt.Theorem (n, freshen_term t, ty_opt, attrs) - | NotationPt.Record (params, n, ty, fields) -> + | NotationPt.Record (params, n, ty, fields, attrs) -> NotationPt.Record (freshen_capture_variables params, n, - freshen_term ty, freshen_name_ty_b fields) + freshen_term ty, freshen_name_ty_b fields, attrs) | NotationPt.LetRec (kind, definitions, attrs) -> let definitions = List.map diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index df0a781c0..1e6860281 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -657,7 +657,8 @@ EXTEND args = LIST1 arg; index_name = OPT [ "on"; id = single_arg -> id ]; ty = OPT [ SYMBOL ":" ; p = term -> p ]; - SYMBOL <:unicode> (* ≝ *); body = term -> + opt_body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in let rec position_of name p = function | [] -> None, p | n :: _ when n = name -> Some p, p @@ -695,7 +696,8 @@ EXTEND name = single_arg; args = LIST0 arg; ty = OPT [ SYMBOL ":" ; p = term -> p ]; - SYMBOL <:unicode> (* ≝ *); body = term -> + opt_body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in let args = List.concat (List.map diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml index 58e600a42..f27c723b0 100644 --- a/matita/components/disambiguation/disambiguate.ml +++ b/matita/components/disambiguation/disambiguate.ml @@ -315,7 +315,7 @@ let domain_of_obj ~context ast = @ (match bo with None -> [] | Some bo -> domain_of_term [] bo) - | Ast.Inductive (params,tyl) -> + | Ast.Inductive (params,tyl,_) -> let context, dom = List.fold_left (fun (context, dom) (var, ty) -> @@ -335,7 +335,7 @@ let domain_of_obj ~context ast = List.map (fun (_,ty) -> domain_of_term context_w_types ty) cl)) tyl) - | Ast.Record (params,var,ty,fields) -> + | Ast.Record (params,var,ty,fields,_) -> let context, dom = List.fold_left (fun (context, dom) (var, ty) -> diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 25024f26d..91086b46d 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -58,12 +58,12 @@ let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t) let default_associativity = Gramext.NonA -let mk_rec_corec src ind_kind defs loc = - let attrs = src, `Definition, `Regular in +let mk_rec_corec src flavour ind_kind defs loc = + let attrs = src, flavour, `Regular in (loc, N.LetRec (ind_kind, defs, attrs)) -let nmk_rec_corec src ind_kind defs loc index = - let loc,t = mk_rec_corec src ind_kind defs loc in +let nmk_rec_corec src flavour ind_kind defs loc index = + let loc,t = mk_rec_corec src flavour ind_kind defs loc in G.NObj (loc,t,index) let shift_vars binder (vars, ty) bo = @@ -529,27 +529,33 @@ EXTEND | src = source; IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term -> let attrs = src, `Axiom, `Regular in G.NObj (loc, N.Theorem (name, typ, None, attrs),i) - | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty) - | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ; - paramspec = OPT inverter_param_list ; - outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> - G.NInverter (loc,name,indty,paramspec,outsort) - | src = source; LETCOREC ; defs = let_codefs -> - nmk_rec_corec src `CoInductive defs loc true - | src = source; LETREC ; defs = let_defs -> - nmk_rec_corec src `Inductive defs loc true -(* FG: no source since no i_attr in N.Inductive *) - | IDENT "inductive"; spec = inductive_spec -> + | src = source; IDENT "inductive"; spec = inductive_spec -> let (params, ind_types) = spec in - G.NObj (loc, N.Inductive (params, ind_types),true) -(* FG: no source since no i_attr in N.Inductive *) - | IDENT "coinductive"; spec = inductive_spec -> + G.NObj (loc, N.Inductive (params, ind_types, src),true) + | src = source; IDENT "coinductive"; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) ind_types in - G.NObj (loc, N.Inductive (params, ind_types),true) + G.NObj (loc, N.Inductive (params, ind_types, src),true) + | src = source; IDENT "record" ; (params,name,ty,fields) = record_spec -> + G.NObj (loc, N.Record (params,name,ty,fields,src),true) +(* FG: new syntax for inductive/coinductive definitions and statements *) + | src = source; IDENT "rec"; nflavour = ntheorem_flavour; defs = let_defs -> + nmk_rec_corec src nflavour `Inductive defs loc true + | src = source; IDENT "corec"; nflavour = ntheorem_flavour; defs = let_codefs -> + nmk_rec_corec src nflavour `CoInductive defs loc true +(**) + | LETCOREC ; defs = let_codefs -> + nmk_rec_corec `Provided `Definition `CoInductive defs loc true + | LETREC ; defs = let_defs -> + nmk_rec_corec `Provided `Definition `Inductive defs loc true + | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty) + | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ; + paramspec = OPT inverter_param_list ; + outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> + G.NInverter (loc,name,indty,paramspec,outsort) | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; SYMBOL <:unicode> ; u2 = tactic_term -> let urify = function @@ -570,9 +576,6 @@ EXTEND "to"; target = term -> t,ty,(id,source),target ] -> let compose = compose = None in G.NCoercion(loc,name,compose,spec) -(* FG: no source since no i_attr in N.Record *) - | IDENT "record" ; (params,name,ty,fields) = record_spec -> - G.NObj (loc, N.Record (params,name,ty,fields),true) | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with"; m = LIST0 [ u1 = URI; SYMBOL <:unicode>; u2 = URI -> u1,u2 ] -> G.NCopy (loc,s,NUri.uri_of_string u, diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml index e2c8c76d0..47b1ac063 100644 --- a/matita/components/ng_cic_content/interpretations.ml +++ b/matita/components/ng_cic_content/interpretations.ml @@ -646,9 +646,9 @@ let nmap_obj0 status ~idref (_, _, metasenv, subst, kind) = | None -> None in N.Theorem (n, ty, xbo, attrs) - | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) -> + | NCic.Inductive (is_ind, lno, itl, (src, `Regular)) -> let captures, context = build_captures lno itl in - N.Inductive (captures, List.map (build_inductive is_ind lno context) itl) + N.Inductive (captures, List.map (build_inductive is_ind lno context) itl, src) | _ -> assert false (* NCic.Fixpoint (is_rec, ifl, _) -> *) let nmap_obj status = with_idrefs nmap_obj0 status diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml index baa28b2d6..9cfbbc8c0 100644 --- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml @@ -248,8 +248,8 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) = in let name = match obj with - | NotationPt.Inductive (_,(name,_,_,_)::_) - | NotationPt.Record (_,name,_,_) -> name ^ ".ind" + | NotationPt.Inductive (_,(name,_,_,_)::_,_) + | NotationPt.Record (_,name,_,_,_) -> name ^ ".ind" | NotationPt.Theorem (name,_,_,_) -> name ^ ".con" | NotationPt.LetRec (_,(_,(NotationPt.Ident (name, None),_),_,_)::_,_) -> name ^ ".con" | NotationPt.LetRec _ diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 24e69a43d..5c0d0a7d5 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -439,7 +439,7 @@ let interpretate_obj status ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo in NCic.Constant ([],name,Some bo,ty',attrs)) - | NotationPt.Inductive (params,tyl) -> + | NotationPt.Inductive (params,tyl,source) -> let context,params = let context,res = List.fold_left @@ -492,10 +492,10 @@ let interpretate_obj status ) tyl in let height = (* XXX calculate *) 0 in - let attrs = `Provided, `Regular in + let attrs = source, `Regular in uri, height, [], [], NCic.Inductive (inductive,leftno,tyl,attrs) - | NotationPt.Record (params,name,ty,fields) -> + | NotationPt.Record (params,name,ty,fields,source) -> let context,params = let context,res = List.fold_left @@ -546,7 +546,7 @@ let interpretate_obj status let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in let height = (* XXX calculate *) 0 in - let attrs = `Provided, `Record field_names in + let attrs = source, `Record field_names in uri, height, [], [], NCic.Inductive (true,leftno,tyl,attrs) | NotationPt.LetRec (kind, defs, attrs) -> diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma index dc9c4498e..b60a87aef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma @@ -66,7 +66,7 @@ definition cfun: candidate → candidate → candidate ≝ ⬇*[Ⓕ, cs] L ≡ K → ⬆*[cs] T ≡ U → C1 G L W → C2 G L (ⓐW.U). (* the reducibility candidate associated to an atomic arity *) -let rec acr (RP:candidate) (A:aarity) on A: candidate ≝ +rec definition acr (RP:candidate) (A:aarity) on A: candidate ≝ match A with [ AAtom ⇒ RP | APair B A ⇒ cfun (acr RP B) (acr RP A) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma index 29fee0ef1..f608f8c3c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma @@ -16,7 +16,7 @@ include "basic_2/grammar/lenv.ma". (* LENGTH OF A LOCAL ENVIRONMENT ********************************************) -let rec length L ≝ match L with +rec definition length L ≝ match L with [ LAtom ⇒ 0 | LPair L _ _ ⇒ ⫯(length L) ]. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma index 9bd6e8260..c9d79e5f5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma @@ -17,7 +17,7 @@ include "basic_2/grammar/lenv.ma". (* WEIGHT OF A LOCAL ENVIRONMENT ********************************************) -let rec lw L ≝ match L with +rec definition lw L ≝ match L with [ LAtom ⇒ 0 | LPair L _ V ⇒ lw L + ♯{V} ]. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma index 192b78637..1dbfd8f64 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma @@ -18,7 +18,7 @@ include "basic_2/grammar/term_simple.ma". (* TERMS ********************************************************************) -let rec applv Vs T on Vs ≝ +rec definition applv Vs T on Vs ≝ match Vs with [ nil ⇒ T | cons hd tl ⇒ ⓐhd. (applv tl T) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma index 3787abe93..23659262d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma @@ -17,7 +17,7 @@ include "basic_2/grammar/term.ma". (* WEIGHT OF A TERM *********************************************************) -let rec tw T ≝ match T with +rec definition tw T ≝ match T with [ TAtom _ ⇒ 1 | TPair _ V T ⇒ tw V + tw T + 1 ]. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma index a16d19042..2bf43b5ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma @@ -84,7 +84,7 @@ definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) …. ] defined. -let rec sd_d (h:sh) (k:nat) (d:nat) on d : sd h ≝ +rec definition sd_d (h:sh) (k:nat) (d:nat) on d : sd h ≝ match d with [ O ⇒ sd_O h | S d ⇒ match d with diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 325e07d38..1ba525475 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -220,7 +220,7 @@ qed-. (* Iterators ****************************************************************) (* Note: see also: lib/arithemetics/bigops.ma *) -let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝ +rec definition iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝ match n with [ O ⇒ nil | S k ⇒ op (iter k B op nil) @@ -249,7 +249,7 @@ qed. (* Trichotomy operator ******************************************************) (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *) -let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝ +rec definition tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝ match n1 with [ O ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ] | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma index 9e8d1ff41..baa9179e9 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma @@ -26,7 +26,7 @@ interpretation "nil (list)" 'Nil = (nil ?). interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl). -let rec length (A:Type[0]) (l:list A) on l ≝ match l with +rec definition length (A:Type[0]) (l:list A) on l ≝ match l with [ nil ⇒ 0 | cons _ l ⇒ ⫯(length A l) ]. @@ -34,7 +34,7 @@ let rec length (A:Type[0]) (l:list A) on l ≝ match l with interpretation "length (list)" 'card l = (length ? l). -let rec all A (R:predicate A) (l:list A) on l ≝ +rec definition all A (R:predicate A) (l:list A) on l ≝ match l with [ nil ⇒ ⊤ | cons hd tl ⇒ R hd ∧ all A R tl diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma index f73099445..b9a7327de 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma @@ -27,7 +27,7 @@ interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?). interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl). -let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with +rec definition append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with [ nil2 ⇒ l2 | cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2 ]. @@ -35,7 +35,7 @@ let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with interpretation "append (list of pairs)" 'Append l1 l2 = (append2 ? ? l1 l2). -let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with +rec definition length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with [ nil2 ⇒ 0 | cons2 _ _ l ⇒ ⫯(length2 A1 A2 l) ]. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma index 839811603..9435b5010 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma @@ -44,11 +44,11 @@ qed-. (* Basic properties *********************************************************) -let corec eq_stream_refl: ∀A. reflexive … (eq_stream A) ≝ ?. +corec lemma eq_stream_refl: ∀A. reflexive … (eq_stream A). #A * #b #t @eq_seq // qed. -let corec eq_stream_sym: ∀A. symmetric … (eq_stream A) ≝ ?. +corec lemma eq_stream_sym: ∀A. symmetric … (eq_stream A). #A #t1 #t2 * -t1 -t2 #t1 #t2 #b1 #b2 #Hb #Ht @eq_seq /2 width=1 by/ qed-. @@ -58,7 +58,7 @@ lemma eq_stream_repl_sym: ∀A,R. eq_stream_repl_back A R → eq_stream_repl_fwd (* Main properties **********************************************************) -let corec eq_stream_trans: ∀A. Transitive … (eq_stream A) ≝ ?. +corec theorem eq_stream_trans: ∀A. Transitive … (eq_stream A). #A #t1 #t * -t1 -t #t1 #t #b1 #b * #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H -b /3 width=7 by eq_seq/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma index 96b9abe98..d2d6bcc30 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma @@ -17,9 +17,9 @@ include "ground_2/lib/streams_hdtl.ma". (* STREAMS ******************************************************************) -let rec tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?. +rec definition tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?. cases n -n [ #t @t | #n #t @tl @(tls … n t) ] -qed. +defined. interpretation "recursive tail (strams)" 'Drops n f = (tls ? n f). diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma index 11ffaa407..da3380da9 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma @@ -16,7 +16,7 @@ include "ground_2/relocation/mr2.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) -let rec pluss (cs:mr2) (i:nat) on cs ≝ match cs with +rec definition pluss (cs:mr2) (i:nat) on cs ≝ match cs with [ nil2 ⇒ ◊ | cons2 l m cs ⇒ {l + i, m} @ pluss cs i ]. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma index 8d7dacc4e..c852317f8 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma @@ -25,7 +25,7 @@ interpretation "push (nstream)" 'Lift f = (push f). definition next: rtmap → rtmap. * #n #f @(⫯n@f) -qed. +defined. interpretation "next (nstream)" 'Successor f = (next f). diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma index a9b022b4d..f8b71a6a5 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma @@ -17,7 +17,7 @@ include "ground_2/relocation/rtmap_after.ma". (* RELOCATION N-STREAM ******************************************************) -let corec compose: rtmap → rtmap → rtmap ≝ ?. +corec definition compose: rtmap → rtmap → rtmap. #f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2 @(↓*[⫯n2] f1) defined. @@ -81,7 +81,7 @@ lemma after_apply: ∀n2,f1,f2,f. (↓*[⫯n2] f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ] qed-. -let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?. +corec lemma after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f. * #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1 [ cases n2 -n2 [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma index 4d979cefb..1b6c466ba 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma @@ -32,7 +32,7 @@ lemma eq_inv_seq: ∀g1,g2. g1 ≗ g2 → ∀f1,f2,n1,n2. n1@f1 = g1 → n2@f2 = n1 = n2 ∧ f1 ≗ f2. /2 width=1 by eq_inv_seq_aux/ qed-. -let corec nstream_eq: ∀f1,f2. f1 ≗ f2 → f1 ≐ f2 ≝ ?. +corec lemma nstream_eq: ∀f1,f2. f1 ≗ f2 → f1 ≐ f2. * #n1 #f1 * #n2 #f2 #Hf cases (eq_inv_gen … Hf) -Hf * #g1 #g2 #Hg #H1 #H2 [ cases (push_inv_seq_dx … H1) -H1 * -n1 #H1 @@ -45,7 +45,7 @@ let corec nstream_eq: ∀f1,f2. f1 ≗ f2 → f1 ≐ f2 ≝ ?. ] qed-. -let corec nstream_inv_eq: ∀f1,f2. f1 ≐ f2 → f1 ≗ f2 ≝ ?. +corec lemma nstream_inv_eq: ∀f1,f2. f1 ≐ f2 → f1 ≗ f2. * #n1 #f1 * #n2 #f2 #H cases (eq_stream_inv_seq ??? H) -H [2,3,4,5,6,7: // ] #Hf * -n2 cases n1 -n1 /3 width=5 by eq_push/ #n @eq_next /3 width=5 by eq_seq/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma index 11307fbd2..28d0e02f0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma @@ -17,7 +17,7 @@ include "ground_2/relocation/rtmap_eq.ma". (* RELOCATION N-STREAM ******************************************************) -let corec id: rtmap ≝ ↑id. +corec definition id: rtmap ≝ ↑id. interpretation "identity (nstream)" 'Identity = (id). diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma index d2bd0837e..0bf3c4da8 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma @@ -18,7 +18,7 @@ include "ground_2/relocation/rtmap_istot.ma". (* RELOCATION N-STREAM ******************************************************) -let rec apply (i: nat) on i: rtmap → nat ≝ ?. +rec definition apply (i: nat) on i: rtmap → nat ≝ ?. * #n #f cases i -i [ @n | #i lapply (apply i f) -apply -i -f diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma index cdded4f97..3db5d524f 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma @@ -161,7 +161,7 @@ qed-. (* Basic properties *********************************************************) -let corec after_eq_repl_back_2: ∀f1,f. eq_repl_back (λf2. f2 ⊚ f1 ≡ f) ≝ ?. +corec lemma after_eq_repl_back_2: ∀f1,f. eq_repl_back (λf2. f2 ⊚ f1 ≡ f). #f1 #f #f2 * -f2 -f1 -f #f21 #f1 #f #g21 [1,2: #g1 ] #g #Hf #H21 [1,2: #H1 ] #H #g22 #H0 [ cases (eq_inv_px … H0 … H21) -g21 /3 width=7 by after_refl/ @@ -170,11 +170,11 @@ let corec after_eq_repl_back_2: ∀f1,f. eq_repl_back (λf2. f2 ⊚ f1 ≡ f) ] qed-. -lemma after_eq_repl_fwd_2: ∀f1,f. eq_repl_fwd (λf2. f2 ⊚ f1 ≡ f). +lemma after_eq_repl_fwd_2: ∀f1,f. eq_repl_fwd (λf2. f2 ⊚ f1 ≡ f). #f1 #f @eq_repl_sym /2 width=3 by after_eq_repl_back_2/ qed-. -let corec after_eq_repl_back_1: ∀f2,f. eq_repl_back (λf1. f2 ⊚ f1 ≡ f) ≝ ?. +corec lemma after_eq_repl_back_1: ∀f2,f. eq_repl_back (λf1. f2 ⊚ f1 ≡ f). #f2 #f #f1 * -f2 -f1 -f #f2 #f11 #f #g2 [1,2: #g11 ] #g #Hf #H2 [1,2: #H11 ] #H #g2 #H0 [ cases (eq_inv_px … H0 … H11) -g11 /3 width=7 by after_refl/ @@ -183,11 +183,11 @@ let corec after_eq_repl_back_1: ∀f2,f. eq_repl_back (λf1. f2 ⊚ f1 ≡ f) ] qed-. -lemma after_eq_repl_fwd_1: ∀f2,f. eq_repl_fwd (λf1. f2 ⊚ f1 ≡ f). +lemma after_eq_repl_fwd_1: ∀f2,f. eq_repl_fwd (λf1. f2 ⊚ f1 ≡ f). #f2 #f @eq_repl_sym /2 width=3 by after_eq_repl_back_1/ qed-. -let corec after_eq_repl_back_0: ∀f1,f2. eq_repl_back (λf. f2 ⊚ f1 ≡ f) ≝ ?. +corec lemma after_eq_repl_back_0: ∀f1,f2. eq_repl_back (λf. f2 ⊚ f1 ≡ f). #f2 #f1 #f * -f2 -f1 -f #f2 #f1 #f01 #g2 [1,2: #g1 ] #g01 #Hf01 #H2 [1,2: #H1 ] #H01 #g02 #H0 [ cases (eq_inv_px … H0 … H01) -g01 /3 width=7 by after_refl/ @@ -196,15 +196,15 @@ let corec after_eq_repl_back_0: ∀f1,f2. eq_repl_back (λf. f2 ⊚ f1 ≡ f) ] qed-. -lemma after_eq_repl_fwd_0: ∀f2,f1. eq_repl_fwd (λf. f2 ⊚ f1 ≡ f). +lemma after_eq_repl_fwd_0: ∀f2,f1. eq_repl_fwd (λf. f2 ⊚ f1 ≡ f). #f2 #f1 @eq_repl_sym /2 width=3 by after_eq_repl_back_0/ qed-. (* Main properties **********************************************************) -let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 → - ∀f1,f2. f1 ⊚ f2 ≡ f0 → - ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?. +corec theorem after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 → + ∀f1,f2. f1 ⊚ f2 ≡ f0 → + ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4. #f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4 [ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg cases (after_inv_xxp … Hg0 … H0) -g0 @@ -226,9 +226,9 @@ let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 → ] qed-. -let corec after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 → - ∀f2, f3. f2 ⊚ f3 ≡ f0 → - ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4 ≝ ?. +corec theorem after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 → + ∀f2, f3. f2 ⊚ f3 ≡ f0 → + ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4. #f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4 [ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg cases (after_inv_xxp … Hg0 … H0) -g0 @@ -252,7 +252,7 @@ qed-. (* Main inversion lemmas on after *******************************************) -let corec after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ≗ y ≝ ?. +corec theorem after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ≗ y. #f1 #f2 #x #y * -f1 -f2 -x #f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy [ cases (after_inv_ppx … Hy … H1 H2) -g1 -g2 /3 width=8 by eq_push/ @@ -276,12 +276,12 @@ qed. (* Inversion lemmas on isid *************************************************) -let corec isid_after_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊚ f2 ≡ f2 ≝ ?. +corec lemma isid_after_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊚ f2 ≡ f2. #f1 * -f1 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * #g2 #H2 /3 width=7 by after_push, after_refl/ qed-. -let corec isid_after_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ⊚ f2 ≡ f1 ≝ ?. +corec lemma isid_after_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ⊚ f2 ≡ f1. #f2 * -f2 #f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) * #g1 #H1 [ /3 width=7 by after_refl/ | @(after_next … H1 H1) /3 width=3 by isid_push/ @@ -296,14 +296,14 @@ lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 /3 width=6 by isid_after_dx, after_mono/ qed-. -let corec after_fwd_isid1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ≝ ?. +corec lemma after_fwd_isid1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄. #f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H [ /4 width=6 by isid_inv_push, isid_push/ ] cases (isid_inv_next … H … H0) qed-. -let corec after_fwd_isid2: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f2⦄ ≝ ?. +corec lemma after_fwd_isid2: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f2⦄. #f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H [ /4 width=6 by isid_inv_push, isid_push/ ] @@ -419,7 +419,7 @@ lemma after_fwd_isid_dx: ∀f2,f1,f. 𝐓⦃f⦄ → f2 ⊚ f1 ≡ f → f2 ≗ /3 width=8 by at_inj, at_eq_repl_back/ qed-. -let corec after_inj_O_aux: ∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1 ≝ ?. +corec fact after_inj_O_aux: ∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1. #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f cases (at_inv_pxp … H1f1) -H1f1 [ |*: // ] #g1 #H1 lapply (istot_inv_push … H2f1 … H1) -H2f1 #H2g1 diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma index 00ee4edb2..e60a2affc 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma @@ -183,7 +183,7 @@ qed-. (* Basic properties *********************************************************) -let corec at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @⦃i1, f⦄ ≡ i2) ≝ ?. +corec lemma at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @⦃i1, f⦄ ≡ i2). #i1 #i2 #f1 #H1 cases H1 -f1 -i1 -i2 [ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /2 width=2 by at_refl/ | #f1 #i1 #i2 #Hf1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /3 width=7 by at_push/ @@ -286,9 +286,9 @@ qed. lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2. /3 width=6 by isid_inv_at, at_mono/ qed-. -(* Advancedd properties on isid *********************************************) +(* Advanced properties on isid **********************************************) -let corec isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄ ≝ ?. +corec lemma isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄. #f #Hf lapply (Hf 0) #H cases (at_fwd_id_ex … H) -H #g #H @(isid_push … H) /3 width=7 by at_inv_npn/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma index 4430c2f8a..8f0f5d0df 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma @@ -36,12 +36,12 @@ definition eq_repl_fwd (R:predicate …) ≝ (* Basic properties *********************************************************) -let corec eq_refl: reflexive … eq ≝ ?. +corec lemma eq_refl: reflexive … eq. #f cases (pn_split f) * #g #Hg [ @(eq_push … Hg Hg) | @(eq_next … Hg Hg) ] -Hg // qed. -let corec eq_sym: symmetric … eq ≝ ?. +corec lemma eq_sym: symmetric … eq. #f1 #f2 * -f1 -f2 #f1 #f2 #g1 #g2 #Hf #H1 #H2 [ @(eq_push … H2 H1) | @(eq_next … H2 H1) ] -g2 -g1 /2 width=1 by/ @@ -129,7 +129,7 @@ qed-. (* Main properties **********************************************************) -let corec eq_trans: Transitive … eq ≝ ?. +corec theorem eq_trans: Transitive … eq. #f1 #f * -f1 -f #f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2 [ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma index 5ad6aa83c..7dde16d0f 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma @@ -43,7 +43,9 @@ lemma isid_inv_next: ∀g. 𝐈⦃g⦄ → ∀f. ⫯f = g → ⊥. #f #Hf * -g #g #H elim (discr_next_push … H) qed-. -let corec isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≗ f2 ≝ ?. +(* Main inversion lemmas ****************************************************) + +corec theorem isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≗ f2. #f1 #f2 #H1 #H2 cases (isid_inv_gen … H1) -H1 cases (isid_inv_gen … H2) -H2 @@ -52,7 +54,7 @@ qed-. (* Basic properties *********************************************************) -let corec isid_eq_repl_back: eq_repl_back … isid ≝ ?. +corec lemma isid_eq_repl_back: eq_repl_back … isid. #f1 #H cases (isid_inv_gen … H) -H #g1 #Hg1 #H1 #f2 #Hf cases (eq_inv_px … Hf … H1) -f1 /3 width=3 by isid_push/ @@ -63,11 +65,11 @@ lemma isid_eq_repl_fwd: eq_repl_fwd … isid. (* Alternative definition ***************************************************) -let corec eq_push_isid: ∀f. ↑f ≗ f → 𝐈⦃f⦄ ≝ ?. +corec lemma eq_push_isid: ∀f. ↑f ≗ f → 𝐈⦃f⦄. #f #H cases (eq_inv_px … H) -H /4 width=3 by isid_push, eq_trans/ qed. -let corec eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f ≝ ?. +corec lemma eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f. #f * -f #f #g #Hf #Hg @(eq_push … Hg) [2: @eq_push_inv_isid // | skip ] @eq_f // diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma index d4e80390f..561a8ef6b 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma @@ -47,10 +47,11 @@ lemma istot_tls: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃⫱*[n]f⦄. #n elim n -n /3 width=1 by istot_tl/ qed. -(* Advanced forward lemmas on at ********************************************) +(* Main forward lemmas on at ************************************************) -let corec at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ → - (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) → f1 ≗ f2 ≝ ?. +corec theorem at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ → + (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) → + f1 ≗ f2. #f1 cases (pn_split f1) * #g1 #H1 #f2 cases (pn_split f2) * #g2 #H2 #Hf1 #Hf2 #Hi @@ -69,7 +70,7 @@ let corec at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ → ] qed-. -(* Main properties on at ****************************************************) +(* Advanced properties on at ************************************************) lemma at_dec: ∀f,i1,i2. 𝐓⦃f⦄ → Decidable (@⦃i1, f⦄ ≡ i2). #f #i1 #i2 #Hf lapply (Hf i1) -Hf * @@ -79,7 +80,8 @@ lemma at_dec: ∀f,i1,i2. 𝐓⦃f⦄ → Decidable (@⦃i1, f⦄ ≡ i2). ] qed-. -lemma is_at_dec_le: ∀f,i2,i. 𝐓⦃f⦄ → (∀i1. i1 + i ≤ i2 → @⦃i1, f⦄ ≡ i2 → ⊥) → Decidable (∃i1. @⦃i1, f⦄ ≡ i2). +lemma is_at_dec_le: ∀f,i2,i. 𝐓⦃f⦄ → (∀i1. i1 + i ≤ i2 → @⦃i1, f⦄ ≡ i2 → ⊥) → + Decidable (∃i1. @⦃i1, f⦄ ≡ i2). #f #i2 #i #Hf elim i -i [ #Ht @or_intror * /3 width=3 by at_increasing/ | #i #IH #Ht elim (at_dec f (i2-i) i2) /3 width=2 by ex_intro, or_introl/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma index 5f707a571..86ad267c6 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma @@ -73,12 +73,12 @@ qed-. (* Basic properties *********************************************************) -let corec sand_refl: ∀f. f ⋒ f ≡ f ≝ ?. +corec lemma sand_refl: ∀f. f ⋒ f ≡ f. #f cases (pn_split f) * #g #H [ @(sand_pp … H H H) | @(sand_nn … H H H) ] -H // qed. -let corec sand_sym: ∀f1,f2,f. f1 ⋒ f2 ≡ f → f2 ⋒ f1 ≡ f ≝ ?. +corec lemma sand_sym: ∀f1,f2,f. f1 ⋒ f2 ≡ f → f2 ⋒ f1 ≡ f. #f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g [ @sand_pp | @sand_pn | @sand_np | @sand_nn ] /2 width=7 by/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma index b27488644..616460173 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma @@ -67,7 +67,7 @@ qed-. (* properties on isid *******************************************************) -let corec sle_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊆ f2 ≝ ?. +corec lemma sle_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊆ f2. #f1 * -f1 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * /3 width=5 by sle_weak, sle_push/ @@ -75,7 +75,7 @@ qed. (* inversion lemmas on isid *************************************************) -let corec sle_inv_isid_dx: ∀f1,f2. f1 ⊆ f2 → 𝐈⦃f2⦄ → 𝐈⦃f1⦄ ≝ ?. +corec lemma sle_inv_isid_dx: ∀f1,f2. f1 ⊆ f2 → 𝐈⦃f2⦄ → 𝐈⦃f1⦄. #f1 #f2 * -f1 -f2 #f1 #f2 #g1 #g2 #Hf * * #H [2,3: elim (isid_inv_next … H) // ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma index 7b437099e..9b093603c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma @@ -73,12 +73,12 @@ qed-. (* Basic properties *********************************************************) -let corec sor_refl: ∀f. f ⋓ f ≡ f ≝ ?. +corec lemma sor_refl: ∀f. f ⋓ f ≡ f. #f cases (pn_split f) * #g #H [ @(sor_pp … H H H) | @(sor_nn … H H H) ] -H // qed. -let corec sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f ≝ ?. +corec lemma sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f. #f1 #f2 #f * -f1 -f2 -f #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g [ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma index d46148840..11a0c9092 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma @@ -17,7 +17,7 @@ include "ground_2/relocation/rtmap_tl.ma". (* RELOCATION MAP ***********************************************************) -let rec tls (f:rtmap) (n:nat) on n: rtmap ≝ match n with +rec definition tls (f:rtmap) (n:nat) on n: rtmap ≝ match n with [ O ⇒ f | S m ⇒ ⫱(tls f m) ]. interpretation "tls (rtmap)" 'DropPreds n f = (tls f n). diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma index dd672ee84..77e44c201 100644 --- a/matita/matita/lib/basics/core_notation.ma +++ b/matita/matita/lib/basics/core_notation.ma @@ -109,7 +109,7 @@ notation < "hvbox(term 46 n break ≅ \sub p term 46 m)" non associative with precedence 45 for @{ 'congruent $n $m $p }. -(* other notations **********************************************************) +(* pairs, projections *******************************************************) notation "hvbox(\langle term 19 a, break term 19 b\rangle)" with precedence 90 for @{ 'pair $a $b}. @@ -126,6 +126,8 @@ notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b notation > "\fst" with precedence 90 for @{'pi1}. notation > "\snd" with precedence 90 for @{'pi2}. +(* implication **************************************************************) + notation "hvbox(a break \to b)" right associative with precedence 20 for @{ \forall $_:$a.$b }. @@ -134,6 +136,8 @@ notation < "hvbox(a break \to b)" right associative with precedence 20 for @{ \Pi $_:$a.$b }. +(* orders *******************************************************************) + notation "hvbox(a break \leq b)" non associative with precedence 45 for @{ 'leq $a $b }. @@ -150,6 +154,8 @@ notation "hvbox(a break \gt b)" non associative with precedence 45 for @{ 'gt $a $b }. +(* negated equality *********************************************************) + notation > "hvbox(a break \neq b)" non associative with precedence 45 for @{ 'neq ? $a $b }. @@ -158,6 +164,8 @@ notation < "hvbox(a break maction (\neq) (\neq\sub t) b)" non associative with precedence 45 for @{ 'neq $t $a $b }. +(* negated orders ***********************************************************) + notation "hvbox(a break \nleq b)" non associative with precedence 45 for @{ 'nleq $a $b }. @@ -174,6 +182,8 @@ notation "hvbox(a break \ngtr b)" non associative with precedence 45 for @{ 'ngtr $a $b }. +(* divides, negated divides *************************************************) + notation "hvbox(a break \divides b)" non associative with precedence 45 for @{ 'divides $a $b }. @@ -182,6 +192,8 @@ notation "hvbox(a break \ndivides b)" non associative with precedence 45 for @{ 'ndivides $a $b }. +(* arithmetics **************************************************************) + notation "hvbox(a break + b)" left associative with precedence 55 for @{ 'plus $a $b }. @@ -225,6 +237,8 @@ notation "\sqrt a" non associative with precedence 65 for @{ 'sqrt $a }. +(* logical connectives ******************************************************) + notation "hvbox(a break \lor b)" left associative with precedence 30 for @{ 'or $a $b }. @@ -245,6 +259,7 @@ notation "hvbox(a break \leftrightarrow b)" left associative with precedence 25 for @{ 'iff $a $b }. +(* subsets ******************************************************************) notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90 for @{ 'powerset $A }. @@ -283,6 +298,8 @@ for @{ 'union $a $b }. (* \cup *) notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}. +(* other notations **********************************************************) + notation "hvbox(a break \approx b)" non associative with precedence 45 for @{ 'napart $a $b}. diff --git a/matita/matita/lib/fail.txt b/matita/matita/lib/fail.txt new file mode 100644 index 000000000..4330dddb1 --- /dev/null +++ b/matita/matita/lib/fail.txt @@ -0,0 +1,27 @@ +matitac.opt turing/multi_to_mono/multi_to_mono.maFAIL 0m00.54s 0m00.52s 0m00.01s +matitac.opt binding/names.ma FAIL 0m00.07s 0m00.07s 0m00.00s +matitac.opt binding/fp.ma + matitac.opt binding/names.ma FAIL 0m00.12s 0m00.12s 0m00.00s +matitac.opt binding/fp.ma FAIL 0m00.13s 0m00.12s 0m00.00s +matitac.opt binding/ln.ma + matitac.opt binding/names.ma FAIL 0m00.07s 0m00.07s 0m00.00s +matitac.opt binding/ln.ma FAIL 0m00.43s 0m00.43s 0m00.00s +matitac.opt binding/ln_concrete.ma + matitac.opt binding/names.ma FAIL 0m00.06s 0m00.06s 0m00.00s +matitac.opt binding/ln_concrete.ma FAIL 0m00.49s 0m00.48s 0m00.00s +matitac.opt finite_lambda/reduction.ma + matitac.opt finite_lambda/terms_and_types.ma FAIL 0m00.47s 0m00.47s 0m00.00s +matitac.opt finite_lambda/reduction.ma FAIL 0m00.48s 0m00.47s 0m00.00s +matitac.opt finite_lambda/typing.ma + matitac.opt finite_lambda/reduction.ma + matitac.opt finite_lambda/terms_and_types.ma FAIL 0m00.39s 0m00.39s 0m00.00s + matitac.opt finite_lambda/reduction.ma FAIL 0m00.39s 0m00.39s 0m00.00s +matitac.opt finite_lambda/typing.ma FAIL 0m00.39s 0m00.39s 0m00.00s +matitac.opt finite_lambda/confluence.ma + matitac.opt finite_lambda/reduction.ma + matitac.opt finite_lambda/terms_and_types.ma FAIL 0m00.42s 0m00.41s 0m00.00s + matitac.opt finite_lambda/reduction.ma FAIL 0m00.42s 0m00.42s 0m00.00s +matitac.opt finite_lambda/confluence.ma FAIL 0m00.42s 0m00.42s 0m00.00s +matitac.opt finite_lambda/terms_and_types.ma FAIL 0m00.38s 0m00.38s 0m00.00s +matitac.opt reverse_complexity/toolkit.ma FAIL 0m14.70s 0m14.62s 0m00.07s +matitac.opt reverse_complexity/hierarchy.ma FAIL 0m00.71s 0m00.70s 0m00.00s diff --git a/matita/matita/lib/inconsistent.ma b/matita/matita/lib/inconsistent.ma new file mode 100644 index 000000000..efac1e02c --- /dev/null +++ b/matita/matita/lib/inconsistent.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basics/logic.ma". + +axiom boh: (False → False) = True. + +definition J: False → False ≝ λf. match f in False with [ ]. + +definition I2: True ≝ match boh with [ refl ⇒ J ]. + +let rec err (u: True): False ≝ match u with [ I ⇒ err I2 ]. + +lemma oops: False ≝ err I. diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang index ea9a08e13..136efe573 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -84,7 +84,6 @@ definition inductive coinductive - let fact lemma remark -- 2.39.2