#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@%)
| `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))
| [] -> 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
(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, _, _)) ->
(** To be increased each time the term type below changes, used for "safe"
* marshalling *)
-let magic = 7
+let magic = 8
type term =
(* CIC AST *)
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
* 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 *)
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
args = LIST1 arg;
index_name = OPT [ "on"; id = single_arg -> id ];
ty = OPT [ SYMBOL ":" ; p = term -> p ];
- SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+ opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); 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
name = single_arg;
args = LIST0 arg;
ty = OPT [ SYMBOL ":" ; p = term -> p ];
- SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+ opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
let args =
List.concat
(List.map
@ (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) ->
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) ->
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 =
| 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<lt>> ; u2 = tactic_term ->
let urify = function
"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<mapsto>>; u2 = URI -> u1,u2 ] ->
G.NCopy (loc,s,NUri.uri_of_string u,
| 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
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 _
~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
) 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
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) ->
⬇*[Ⓕ, 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)
(* 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)
].
(* 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}
].
(* 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)
(* 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
].
]
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
(* 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)
(* 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 ]
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)
].
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
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
].
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)
].
(* 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-.
(* 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/
(* 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).
(* 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
].
definition next: rtmap → rtmap.
* #n #f @(⫯n@f)
-qed.
+defined.
interpretation "next (nstream)" 'Successor f = (next f).
(* 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.
]
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/
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
]
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/
(* RELOCATION N-STREAM ******************************************************)
-let corec id: rtmap ≝ ↑id.
+corec definition id: rtmap ≝ ↑id.
interpretation "identity (nstream)"
'Identity = (id).
(* 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
(* 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/
]
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/
]
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/
]
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
]
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
(* 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/
(* 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/
/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/ ]
/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
(* 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/
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/
(* 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/
(* 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
#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
(* 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/
(* 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 //
#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
]
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 *
]
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/
(* 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/
(* 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/
(* 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) // ]
(* 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/
(* 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).
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}.
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 }.
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 }.
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 }.
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 }.
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 }.
non associative with precedence 45
for @{ 'ndivides $a $b }.
+(* arithmetics **************************************************************)
+
notation "hvbox(a break + b)"
left associative with precedence 55
for @{ 'plus $a $b }.
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 }.
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 }.
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}.
--- /dev/null
+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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
<keyword>definition</keyword>
<keyword>inductive</keyword>
<keyword>coinductive</keyword>
- <keyword>let</keyword>
<keyword>fact</keyword>
<keyword>lemma</keyword>
<keyword>remark</keyword>
projects / helm.git / commitdiff