raise Not_a_proof
| C.AAppl (id,li) ->
(try coercion
- seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts
+ seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts
with NotApplicable ->
try rewrite
seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
}
| _ -> raise NotApplicable
-and coercion seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts =
+and coercion seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts =
match li with
| ((Cic.AConst _) as he)::tl
| ((Cic.AMutInd _) as he)::tl
| ((Cic.AMutConstruct _) as he)::tl when
- CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
- !hide_coercions ->
- let rec last =
- function
- [] -> assert false
- | [t] -> t
- | _::tl -> last tl
+ (match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+ | None -> false | Some (_,_,_,_,cpos) -> cpos < List.length tl)
+ && !hide_coercions ->
+ let cpos,sats =
+ match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+ | None -> assert false
+ | Some (_,_,_,sats,cpos) -> cpos, sats
in
- acic2content
- seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+ let x = List.nth tl cpos in
+ let _,rest =
+ try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[]
+ in
+ if rest = [] then
+ acic2content
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
+ x
+ else
+ acic2content
+ seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
+ (Cic.AAppl (id,x::rest))
| _ -> raise NotApplicable
and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
| Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
| Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
| Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t ->
- let last_n n l =
- let rec aux =
- function
- [] -> assert false
- | [_] as l -> l,1
- | he::tl ->
- let (res,len) as res' = aux tl in
- if len < n then
- he::res,len + 1
- else
- res'
- in
- match fst (aux l) with
- [] -> assert false
- | [t] -> t
- | Ast.AttributedTerm (_,(Ast.Appl l))::tl ->
- idref aid (Ast.Appl (l@tl))
- | l -> idref aid (Ast.Appl l)
- in
(match LibraryObjects.destroy_nat t with
| Some n -> idref aid (Ast.Num (string_of_int n, -1))
| None ->
let deannot_he = Deannotate.deannotate_term he in
- if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions
- then
- (match CoercDb.is_a_coercion_to_funclass deannot_he with
- | None -> idref aid (last_n 1 (List.map k tl))
- | Some i -> idref aid (last_n (i+1) (List.map k tl)))
+ let coercion_info = CoercDb.is_a_coercion deannot_he in
+ if coercion_info <> None && !Acic2content.hide_coercions then
+ match coercion_info with
+ | None -> assert false
+ | Some (_,_,_,sats,cpos) ->
+ if cpos < List.length tl then
+ let _,rest =
+ try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[]
+ in
+ if rest = [] then
+ idref aid (List.nth (List.map k tl) cpos)
+ else
+ idref aid (Ast.Appl (List.map k (List.nth tl cpos::rest)))
+ else
+ idref aid (Ast.Appl (List.map k tl))
else
idref aid (Ast.Appl (List.map k args)))
| Cic.AAppl (aid,args) ->
;;
let is_a_double_coercion t =
- let last_of l =
- let rec aux acc = function
- | x::[] -> acc,x
- | x::tl -> aux (acc@[x]) tl
- | [] -> assert false
- in
- aux [] l
+ let rec subst_nth n x l =
+ match n,l with
+ | _, [] -> []
+ | 0, _::tl -> x :: tl
+ | n, hd::tl -> hd :: subst_nth (n-1) x tl
in
let imp = Cic.Implicit None in
let dummyres = false,imp, imp,imp,imp in
match t with
- | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
- (match last_of tl with
- | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
- let sib2,head = last_of tl2 in
- true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
- (c2::sib2@[imp])])
+ | Cic.Appl l1 ->
+ (match CoercGraph.coerced_arg l1 with
+ | Some (Cic.Appl l2, pos1) ->
+ (match CoercGraph.coerced_arg l2 with
+ | Some (x, pos2) ->
+ true, List.hd l1, List.hd l2, x,
+ Cic.Appl (subst_nth (pos1 + 1)
+ (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
+ | _ -> dummyres)
| _ -> dummyres)
| _ -> dummyres
+;;
let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
=
(* given he:hety, gives beack all (c he) such that (c e):?->? *)
let fix_arity n metasenv context subst he hetype ugraph =
let hetype = CicMetaSubst.apply_subst subst hetype in
- let src = CoercDb.coerc_carr_of_term hetype in
- let tgt = CoercDb.Fun 0 in
+ let src = CoercDb.coerc_carr_of_term hetype 0 in
+ let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in
match CoercGraph.look_for_coercion' metasenv subst context src tgt with
| CoercGraph.NoCoercion -> []
- | CoercGraph.NotMetaClosed
- | CoercGraph.NotHandled _ ->
+ | CoercGraph.NotHandled ->
raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
| CoercGraph.SomeCoercionToTgt candidates
| CoercGraph.SomeCoercion candidates ->
CoercGraph.look_for_coercion metasenv subst context infty expty
in
match coer with
- | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
- "coerce_atom_to_something fails since not meta closed"))
| CoercGraph.NoCoercion
- | CoercGraph.SomeCoercionToTgt _
- | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
+ | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
+ "coerce_atom_to_something fails since no coercions found"))
+ | CoercGraph.NotHandled when
+ not (CicUtil.is_meta_closed infty) ||
+ not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
+ "coerce_atom_to_something fails since carriers have metas"))
+ | CoercGraph.NotHandled -> raise (RefineFailure (lazy
"coerce_atom_to_something fails since no coercions found"))
| CoercGraph.SomeCoercion candidates ->
debug_print (lazy (string_of_int (List.length candidates) ^
| UnificationFailure s
| Uncertain s as exn ->
(match l1, l2 with
- | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
- (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
- CoercDb.is_a_coercion' c1 &&
- CoercDb.is_a_coercion' c2 &&
+ | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
+ (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
+ CoercDb.is_a_coercion cc1 <> None &&
+ CoercDb.is_a_coercion cc2 <> None &&
not (UriManager.eq uri1 uri2) ->
-(*DEBUGGING ONLY:
+(*DEBUGGING ONLY:
prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
let res =
-*)
- let rec look_for_first_coercion c tl =
- match
- CicMetaSubst.apply_subst subst (HExtlib.list_last tl)
- with
- Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl')
- when CoercDb.is_a_coercion' c' ->
- look_for_first_coercion c' tl'
- | last_tl -> c,last_tl
+ *)
+ let inner_coerced t =
+ let t = CicMetaSubst.apply_subst subst t in
+ let rec aux c x t =
+ match t with
+ | Cic.Appl l ->
+ (match CoercGraph.coerced_arg l with
+ | None -> c, x
+ | Some (t,_) -> aux (List.hd l) t t)
+ | _ -> c, x
+ in
+ aux (Cic.Implicit None) (Cic.Implicit None) t
in
- let c1,last_tl1 = look_for_first_coercion c1 tl1 in
- let c2,last_tl2 = look_for_first_coercion c2 tl2 in
- let car1 =
- CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in
- let car2 =
- CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in
+ let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
+ let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
+ let car1, car2 =
+ match
+ CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
+ with
+ | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
+ | _ -> assert false
+ in
+ let head1_c, head2_c =
+ match
+ CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
+ with
+ | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
+ | _ -> assert false
+ in
+ let unfold uri ens args =
+ let o, _ =
+ CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
+ in
+ assert (ens = []);
+ match o with
+ | Cic.Constant (_,Some bo,_,_,_) ->
+ CicReduction.head_beta_reduce ~delta:false
+ (Cic.Appl (bo::args))
+ | _ -> assert false
+ in
if CoercDb.eq_carr car1 car2 then
- (match last_tl1,last_tl2 with
- C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn
- | C.Meta _, _
- | _, C.Meta _ ->
+ match last_tl1,last_tl2 with
+ | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
+ | _, C.Meta _
+ | C.Meta _, _ ->
let subst,metasenv,ugraph =
fo_unif_subst test_equality_only subst context
metasenv last_tl1 last_tl2 ugraph
in
fo_unif_subst test_equality_only subst context
- metasenv (C.Appl l1) (C.Appl l2) ugraph
- | _ -> raise exn)
+ metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
+ | _ when CoercDb.eq_carr head1_c head2_c ->
+ let l1, l2 =
+ (* composite VS composition + metas avoiding
+ * coercions not only in coerced position *)
+ if c1 = cc1 then
+ unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
+ else Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
+ in
+ fo_unif_subst test_equality_only subst context
+ metasenv l1 l2 ugraph
+ | _ -> raise exn
else
let meets =
CoercGraph.meets metasenv subst context car1 car2
in
- (match meets with
+ (match meets with
| [] -> raise exn
| (carr,metasenv,to1,to2)::xxx ->
(match xxx with
- [] -> ()
+ | [] -> ()
| (m2,_,c2,c2')::_ ->
let m1,_,c1,c1' = carr,metasenv,to1,to2 in
let unopt =
in
HLog.warn
("There are two minimal joins of "^
- CoercDb.name_of_carr car1^" and "^
- CoercDb.name_of_carr car2^": " ^
- CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^
- unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^
+ CoercDb.string_of_carr car1^" and "^
+ CoercDb.string_of_carr car2^": " ^
+ CoercDb.string_of_carr m1 ^ " via "^unopt c1^" + "^
+ unopt c1'^" and "^CoercDb.string_of_carr m2^" via "^
unopt c2^" + "^unopt c2'));
let last_tl1',(subst,metasenv,ugraph) =
match last_tl1,to1 with
prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
res
*)
+
(*CSC: This is necessary because of the "elim H" tactic
where the type of H is only reducible to an
inductive type. This could be extended from inductive
| SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
| SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
| NoCoercion
- | NotMetaClosed
- | NotHandled of string Lazy.t
+ | NotHandled
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
let saturate_coercion ul metasenv subst context =
let cl =
- List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in
- let funclass_arityl =
- let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in
- List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+ List.map
+ (fun u,saturations ->
+ let t = CicUtil.term_of_uri u in
+ let arity =
+ match CoercDb.is_a_coercion t with
+ | Some (_,CoercDb.Fun i,_,_,_) -> i
+ | _ -> 0
+ in
+ arity,t,saturations) ul
in
let freshmeta = CicMkImplicit.new_meta metasenv subst in
- List.map2
- (fun arity (c,saturations) ->
+ List.map
+ (fun (arity,c,saturations) ->
let ty,_ =
CicTypeChecker.type_of_aux' ~subst metasenv context c
CicUniv.oblivion_ugraph in
match args with
[] -> c
| _ -> Cic.Appl (c::args)
- ) funclass_arityl cl
+ ) cl
;;
(* searches a coercion fron src to tgt in the !coercions list *)
let look_for_coercion' metasenv subst context src tgt =
+ let is_dead = function CoercDb.Dead -> true | _ -> false in
let pp_l s l =
match l with
| [] ->
debug_print
(lazy
(sprintf ":-( coercion non trovata[%s] da %s a %s" s
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
+ (CoercDb.string_of_carr src)
+ (CoercDb.string_of_carr tgt)));
| _::_ ->
debug_print (lazy (
sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
(List.length l)
- (CoercDb.name_of_carr src)
- (CoercDb.name_of_carr tgt)));
+ (CoercDb.string_of_carr src)
+ (CoercDb.string_of_carr tgt)));
in
- try
+ if is_dead src || is_dead tgt then NotHandled
+ else
let l =
CoercDb.find_coercion
(fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
pp_l "approx" l;
(match l with
| [] -> NoCoercion
- | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
+ | ul ->
+ SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
| ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
- with
- | CoercDb.EqCarrNotImplemented s -> NotHandled s
- | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
;;
let look_for_coercion metasenv subst context src tgt =
- let src_uri = CoercDb.coerc_carr_of_term src in
- let tgt_uri = CoercDb.coerc_carr_of_term tgt in
+ let src_uri = CoercDb.coerc_carr_of_term src 0 in
+ let tgt_uri = CoercDb.coerc_carr_of_term tgt 0 in
look_for_coercion' metasenv subst context src_uri tgt_uri
let source_of t =
- try
- let uri = CicUtil.uri_of_term t in
- CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
- with Invalid_argument _ -> assert false (* t must be a coercion *)
+ match CoercDb.is_a_coercion t with
+ | None -> assert false
+ | Some (CoercDb.Sort s,_,_,_,_) -> Cic.Sort s
+ | Some (CoercDb.Uri u,_,_,_,_) -> CicUtil.term_of_uri u
+ | Some _ -> assert false (* t must be a coercion not to funclass *)
+;;
let generate_dot_file () =
let module Pp = GraphvizPp.Dot in
~edge_attrs:["fontsize", "10"] fmt;
let l = CoercDb.to_list () in
let pp_description carr =
- match CoercDb.uri_of_carr carr with
- | None -> ()
- | Some uri ->
- Pp.node (CoercDb.name_of_carr carr)
- ~attrs:["href", UriManager.string_of_uri uri] fmt in
+ match carr with
+ | CoercDb.Uri uri ->
+ Pp.node (CoercDb.string_of_carr carr)
+ ~attrs:["href", UriManager.string_of_uri uri] fmt
+ | _ -> ()
+ in
List.iter
(fun (src, tgt, ul) ->
- let src_name = CoercDb.name_of_carr src in
- let tgt_name = CoercDb.name_of_carr tgt in
+ let src_name = CoercDb.string_of_carr src in
+ let tgt_name = CoercDb.string_of_carr tgt in
pp_description src;
pp_description tgt;
List.iter
- (fun (u,saturations) ->
+ (fun (u,saturations,_) ->
Pp.edge src_name tgt_name
~attrs:[ "label",
(UriManager.name_of_uri u ^
let coerced_arg l =
match l with
- | [] | [_] -> assert false
- | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
+ | [] | [_] -> None
| c::tl ->
- let arity =
- match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a
- in
- (* decide a decent structure for coercion carriers so that all this stuff is
- * useless *)
- let pi =
- (* this calculation is not complete, since we have strange carriers *)
- let rec count_pi = function
- | Cic.Prod(_,_,t) -> 1+ (count_pi t)
- | _ -> 0
- in
- let uri = CicUtil.uri_of_term c in
- match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
- | Cic.Constant (_, _, ty, _, _) -> count_pi ty
- | _ -> assert false
- in
- try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
+ match CoercDb.is_a_coercion c with
+ | None -> None
+ | Some (_,_,_,_,cpos) ->
+ if List.length tl > cpos then Some (List.nth tl cpos, cpos) else None
;;
(************************* meet calculation stuff ********************)
let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
-let splat e l = List.map (fun x -> e, Some x) l;;
+let splat e l = List.map (fun (x1,x2,_) -> e, Some (x1,x2)) l;;
(* : carr -> (carr * uri option) where the option is always Some *)
let get_coercions_to carr =
| SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
| SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
| NoCoercion
- | NotMetaClosed
- | NotHandled of string Lazy.t
+ | NotHandled
val look_for_coercion :
Cic.metasenv -> Cic.substitution -> Cic.context ->
val generate_dot_file: unit -> string
(* given the Appl contents returns the argument of the head coercion *)
-val coerced_arg: Cic.term list -> Cic.term option
+val coerced_arg: Cic.term list -> (Cic.term * int) option
(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
val meets :
type 'a eval_from_moo =
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-let coercion_moo_statement_of (uri,arity, saturations) =
+let coercion_moo_statement_of (uri,arity, saturations,_) =
GrafiteAst.Coercion
(HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
saturations (GrafiteTypes.get_baseuri status)
in
let moo_content =
- List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
+ List.map coercion_moo_statement_of ((uri,arity,saturations,0)::compounds)
in
let status = GrafiteTypes.add_moo_content moo_content status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
- List.map (fun u,_,_ -> u) compounds
+ List.map (fun u,_,_,_ -> u) compounds
module MatitaStatus =
struct
in
let is_a_coercion, arity_coercion = is_a_coercion uri in
if is_a_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_coercion,0))
+ Some (uri, coercion_moo_statement_of (uri,arity_coercion,0,0))
else if is_a_wanted_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_wanted,0))
+ Some (uri, coercion_moo_statement_of (uri,arity_wanted,0,0))
else
None)
lemmas)
add_composites:bool -> GrafiteTypes.status ->
UriManager.uri -> int -> int ->
string (* baseuri *) ->
- GrafiteTypes.status * (UriManager.uri * int * int) list
- (* URI, arity, saturations *)
+ GrafiteTypes.status * (UriManager.uri * int * int * int) list
+ (* URI, arity, saturations, cpos *)
val time_travel:
present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit
(fun _ _ _ _ _ -> [] :
CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
- (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * int) list)
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj *
+ int * int) list)
;;
let set_close_coercion_graph f = close_coercion_graph_ref := f;;
(CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
(CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
- int (* saturations *) * Cic.obj * int (* arity *)) list)
+ int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list)
-> unit
val close_coercion_graph:
CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
(CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
- int (* saturations *) * Cic.obj * int (* arity *) ) list
+ int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list
(* $Id$ *)
+let debug = false
+let debug_print =
+ if debug then fun x -> prerr_endline (Lazy.force x)
+ else ignore
+;;
+
type coerc_carr =
| Uri of UriManager.uri
| Sort of Cic.sort
- | Term of Cic.term
| Fun of int
+ | Dead
;;
-exception EqCarrNotImplemented of string Lazy.t
-exception EqCarrOnNonMetaClosed
+type saturations = int
+type coerced_pos = int
+type coercion_entry =
+ coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos
+
+type coerc_db = (* coercion_entry grouped by carrier with molteplicity *)
+ (coerc_carr * coerc_carr *
+ (UriManager.uri * int * saturations * coerced_pos) list) list
-let db = ref []
+let db = ref ([] : coerc_db)
+let dump () = !db
+let restore coerc_db = db := coerc_db
-let coerc_carr_of_term t =
+let rec coerc_carr_of_term t a =
try
- match t with
- | Cic.Sort s -> Sort s
- | Cic.Prod _ -> Fun 0
- (* BUG: this should be the real arity. The computation
- requires menv, context etc.., but since carrs are compared discharging Fun
- arity... it works *)
- | Cic.Appl (t::_)
- | t -> Uri (CicUtil.uri_of_term t)
- with Invalid_argument _ ->
- Term t
+ match t, a with
+ | Cic.Sort s, 0 -> Sort s
+ | Cic.Appl (t::_), 0 -> coerc_carr_of_term t a
+ | t, 0 -> Uri (CicUtil.uri_of_term t)
+ | _, n -> Fun n
+ with Invalid_argument _ -> Dead
;;
-let uri_of_carr = function
- | Uri u -> Some u
- | _ -> None
-
-let rec name_of_carr = function
+let string_of_carr = function
| Uri u -> UriManager.name_of_uri u
| Sort s -> CicPp.ppsort s
- | Term (Cic.Appl ((Cic.Const (uri, _))::_))
- | Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_))
- | Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) ->
- UriManager.name_of_uri uri
- | Term (Cic.Prod (_,_,t)) -> name_of_carr (Term t)
- | Term t ->
- prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t);
- "FixTheNameMangler"
| Fun i -> "FunClass_" ^ string_of_int i
+ | Dead -> "UnsupportedCarrier"
;;
let eq_carr ?(exact=false) src tgt =
| _ -> coarse_eq)
| Sort (Cic.Type _), Sort (Cic.Type _) -> true
| Sort src, Sort tgt when src = tgt -> true
- | Term t1, Term t2 ->
- if t1 = t2 then true
- else
- if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then
- raise
- (EqCarrNotImplemented
- (lazy ("Unsupported carr for coercions: " ^
- CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
- else raise EqCarrOnNonMetaClosed
- | Fun _,Fun _ -> true (* only one Funclass? *)
-(* | Fun i,Fun j when i=j -> true *)
- | Term t, _
- | _, Term t when not (CicUtil.is_meta_closed t) -> raise EqCarrOnNonMetaClosed
+ | Fun _,Fun _ when not exact -> true (* only one Funclass *)
+ | Fun i,Fun j when i = j -> true (* only one Funclass *)
| _, _ -> false
;;
let to_list () =
- List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b -> a,b) l) !db
+ List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) !db
;;
let rec myfilter p = function
| (s,t,l)::tl ->
let l =
HExtlib.filter_map
- (fun (u,n,saturations) ->
- if p (s,t,u,saturations) then
- if n = 1 then
- None
- else
- Some (u,n-1,saturations)
- else
- Some (u,n,saturations))
+ (fun (u,n,saturations,cpos) as e ->
+ if p (s,t,u,saturations,cpos) then
+ if n = 1 then None
+ else Some (u,n-1,saturations,cpos)
+ else Some e)
l
in
if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
let remove_coercion p = db := myfilter p !db;;
let find_coercion f =
- List.map
- (fun uri,_,saturations -> uri,saturations)
- (List.flatten
+ List.map
+ (fun (uri,_,saturations,_) -> uri,saturations)
+ (List.flatten
(HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db))
;;
-let get_carr uri =
+let is_a_coercion t =
try
- let src, tgt, _ =
- List.find
- (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq uri x) xl)
- !db
- in
- src, tgt
- with Not_found -> assert false (* uri must be a coercion *)
+ let uri = CicUtil.uri_of_term t in
+ match
+ HExtlib.filter_map
+ (fun (src,tgt,xl) ->
+ let xl = List.filter (fun (x,_,_,_) -> UriManager.eq uri x) xl in
+ if xl = [] then None else Some (src,tgt,xl))
+ !db
+ with
+ | [] -> None
+ | (_,_,[])::_ -> assert false
+ | [src,tgt,[u,_,s,p]] -> Some (src,tgt,u,s,p)
+ | (src,tgt,(u,_,s,p)::_)::_ ->
+ debug_print
+ (lazy "coercion has multiple entries, returning the first one");
+ Some (src,tgt,u,s,p)
+ with Invalid_argument _ ->
+ debug_print (lazy "this term is not a constant");
+ None
;;
-let is_a_coercion u =
- List.exists
- (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq u x) xl)
- !db
-;;
-
-let is_a_coercion' t =
- try
- let uri = CicUtil.uri_of_term t in
- is_a_coercion uri
- with Invalid_argument _ -> false
-;;
-
-let is_a_coercion_to_funclass t =
- try
- let uri = CicUtil.uri_of_term t in
- match snd (get_carr uri) with
- | Fun i -> Some i
- | _ -> None
- with Invalid_argument _ -> None
-
-
-let term_of_carr = function
- | Uri u -> CicUtil.term_of_uri u
- | Sort s -> Cic.Sort s
- | Fun _ -> assert false
- | Term _ -> assert false
-;;
-
-let add_coercion (src,tgt,u,saturations) =
+let add_coercion (src,tgt,u,saturations,cpos) =
let f s t = eq_carr s src && eq_carr t tgt in
let where = List.filter (fun (s,t,_) -> f s t) !db in
let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
match where with
- | [] -> db := (src,tgt,[u,1,saturations]) :: !db
+ | [] -> db := (src,tgt,[u,1,saturations,cpos]) :: !db
| (src,tgt,l)::tl ->
assert (tl = []); (* not sure, this may be a feature *)
- if List.exists (fun (x,_,_) -> UriManager.eq u x) l then
- let l' = List.map
- (fun (x,n,saturations') ->
+ if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then
+ let l = List.map
+ (fun (x,n,x_saturations,x_cpos) as e ->
if UriManager.eq u x then
- (x,n+1,saturations)
- else
- (x,n,saturations))
+ (* not sure, this may be a feature *)
+ (assert (x_saturations = saturations && x_cpos = cpos);
+ (x,n+1,saturations,cpos))
+ else e)
l
in
- db := (src,tgt,l')::tl @ rest
+ db := (src,tgt,l)::tl @ rest
else
- db := (src,tgt,(u,1,saturations)::l)::tl @ rest
-
+ db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest
;;
-type coerc_db = (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
-let dump () = !db
-let restore coerc_db = db := coerc_db
*)
- (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph/CicCoercion/librarySync
- *
- * and may be merged with CicCoercion...
- *
- * **)
-
-
- (** XXX WARNING: non-reentrant *)
-type coerc_carr =
+type coerc_carr = private
| Uri of UriManager.uri (* const, mutind, mutconstr *)
| Sort of Cic.sort (* Prop, Set, Type *)
- | Term of Cic.term (* nothing supported *)
| Fun of int
+ | Dead
;;
-exception EqCarrNotImplemented of string Lazy.t
-exception EqCarrOnNonMetaClosed
val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool
-val coerc_carr_of_term: Cic.term -> coerc_carr
-val name_of_carr: coerc_carr -> string
-val uri_of_carr: coerc_carr -> UriManager.uri option
+val string_of_carr: coerc_carr -> string
+
+(* takes a term in whnf ~delta:false and a desired ariety *)
+val coerc_carr_of_term: Cic.term -> int -> coerc_carr
val to_list:
unit ->
- (coerc_carr * coerc_carr * (UriManager.uri * int) list) list
+ (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
type coerc_db
val dump: unit -> coerc_db
val restore: coerc_db -> unit
-val add_coercion:
- coerc_carr * coerc_carr * UriManager.uri * int -> unit
+(* src carr, tgt carr, uri, saturations, coerced position
+ * invariant:
+ * if the constant pointed by uri has n argments
+ * n = coerced position + saturations + FunClass arity
+ *)
-val remove_coercion:
- (coerc_carr * coerc_carr * UriManager.uri * int -> bool) -> unit
+type saturations = int
+type coerced_pos = int
+type coercion_entry =
+ coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos
+val add_coercion: coercion_entry -> unit
+val remove_coercion: (coercion_entry -> bool) -> unit
val find_coercion:
(coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list
-val is_a_coercion: UriManager.uri -> bool
-val is_a_coercion': Cic.term -> bool
-val is_a_coercion_to_funclass: Cic.term -> int option
-val get_carr: UriManager.uri -> coerc_carr * coerc_carr
-
-val term_of_carr: coerc_carr -> Cic.term
-
+val is_a_coercion: Cic.term -> coercion_entry option
let add_single_obj uri obj refinement_toolkit =
let module RT = RefinementTool in
let obj =
- if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
- not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
- then
- refinement_toolkit.RT.pack_coercion_obj obj
- else
- obj
+ if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None
+ then refinement_toolkit.RT.pack_coercion_obj obj
+ else obj
in
let dbd = LibraryDb.instance () in
if CicEnvironment.in_library uri then
let remove_all_coercions () =
UriManager.UriHashtbl.clear coercion_hashtbl;
- CoercDb.remove_coercion (fun (_,_,_,_) -> true)
+ CoercDb.remove_coercion (fun _ -> true)
let stack = ref [];;
in
aux ty
in
- let src_carr, tgt_carr =
+ let src_carr, tgt_carr, no_args =
let get_classes arity saturations l =
(* this is the ackerman's function revisited *)
let rec aux = function
in
let types = spine2list coer_ty in
let src,tgt = get_classes arity saturations types in
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
- match tgt with
- None -> assert false
- | Some `Funclass -> CoercDb.Fun arity
- | Some (`Class tgt) ->
- CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0,
+ (match tgt with
+ | None -> assert false
+ | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
+ | Some (`Class tgt) ->
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
+ List.length types - 1
in
let already_in_obj src_carr tgt_carr uri obj =
List.exists
(fun (s,t,ul) ->
List.exists
- (fun u,_ ->
+ (fun u,_,_ ->
let bo =
match obj with
| Cic.Constant (_, Some bo, _, _, _) -> bo
ul)
(CoercDb.to_list ())
in
+ let cpos = no_args - arity - saturations - 1 in
if not add_composites then
- (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+ (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
[])
else
baseuri
in
let new_coercions =
- List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
+ List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj))
new_coercions
in
- let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
+ let composite_uris =
+ List.map (fun (_,_,uri,_,_,_,_) -> uri) new_coercions
+ in
(* update the DB *)
List.iter
- (fun (src,tgt,uri,saturations,_,_) ->
- CoercDb.add_coercion (src,tgt,uri,saturations))
+ (fun (src,tgt,uri,saturations,_,_,cpos) ->
+ CoercDb.add_coercion (src,tgt,uri,saturations,cpos))
new_coercions;
- CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+ CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
(* add the composites obj and they eventual lemmas *)
let lemmas =
List.fold_left
- (fun acc (_,tgt,uri,saturations,obj,arity) ->
+ (fun acc (_,tgt,uri,saturations,obj,arity,cpos) ->
add_single_obj uri obj refinement_toolkit;
- (uri,arity,saturations)::acc)
+ (uri,arity,saturations,cpos)::acc)
[] new_coercions
in
(* store that composite_uris are related to uri. the first component is
composites_in_db;*)
UriManager.UriHashtbl.remove coercion_hashtbl uri;
CoercDb.remove_coercion
- (fun (_,_,u,_) -> UriManager.eq uri u);
+ (fun (_,_,u,_,_) -> UriManager.eq uri u);
(* remove from the DB *)
List.iter
- (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
+ (fun u ->
+ CoercDb.remove_coercion (fun (_,_,u1,_,_) -> UriManager.eq u u1))
composites_in_db;
(* remove composites from the lib *)
List.iter remove_single_obj composites_in_lib
prerr_endline "---";
*)
(*CSC: I throw the arity away. See comment above *)
- List.map (fun u,_,_ -> u) x
+ List.map (fun u,_,_,_ -> u) x
end
else
[]
add_composites:bool ->
RefinementTool.kit -> UriManager.uri -> int (* arity *) ->
int (* saturations *) -> string (* baseuri *) ->
- (UriManager.uri * int * int) list (* URI, arity, saturations *)
+ (UriManager.uri * int * int * int) list (* URI, arity, saturations, cpos *)
(* inverse of add_coercion, removes both the eventually created composite *)
(* coercions and the information that [uri] and the composites are coercion *)
* (source, list of coercions to follow, target)
*)
let get_closure_coercions src tgt uri coercions =
- let enrich (uri,sat) tgt =
+ let enrich (uri,sat,_) tgt =
let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
uri,sat,arity
in
let uri = enrich uri tgt in
let eq_carr ?exact s t =
- debug_print (lazy(CoercDb.name_of_carr s^" VS "^CoercDb.name_of_carr t));
- try
- let rc = CoercDb.eq_carr ?exact s t in
- debug_print(lazy(string_of_bool rc));
- rc
- with
- | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed ->
- debug_print (lazy("false"));
- false
+ debug_print(lazy(CoercDb.string_of_carr s^" VS "^CoercDb.string_of_carr t));
+ let rc = CoercDb.eq_carr ?exact s t in
+ debug_print(lazy(string_of_bool rc));
+ rc
in
match src,tgt with
| CoercDb.Uri _, CoercDb.Uri _ ->
- debug_print (lazy ("Uri, Uri4"));
+ debug_print (lazy ("Uri, Uri4"));
let c_from_tgt =
List.filter
(fun (f,t,_) ->
-
- debug_print (lazy ("Uri, Uri3"));
- eq_carr f tgt (*&& not (eq_carr t src)*))
+ debug_print (lazy ("Uri, Uri3"));
+ eq_carr f tgt)
coercions
in
let c_to_src =
List.filter
(fun (f,t,_) ->
-
- debug_print (lazy ("Uri, Uri2"));
- eq_carr t src (*&& not (eq_carr f tgt)*))
+ debug_print (lazy ("Uri, Uri2"));
+ eq_carr t src)
coercions
in
(HExtlib.flatten_map
| (i,_,_)::_ when i = n -> acc
| _::tl -> position_of n (acc + 1) tl
in
- let saturations_res =
+ let saturations_res, position_of_meta_to_be_coerced =
match meta_to_be_coerced with
- | None -> 0
+ | None -> 0,0
| Some meta_to_be_coerced ->
debug_print
(lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced));
position_of meta_to_be_coerced 0 sorted in
debug_print (lazy ("POSITION_OF_META_TO_BE_COERCED: " ^
string_of_int position_of_meta_to_be_coerced));
- List.length sorted - position_of_meta_to_be_coerced - 1
+ List.length sorted - position_of_meta_to_be_coerced - 1,
+ position_of_meta_to_be_coerced
in
debug_print (lazy ("SATURATIONS: " ^ string_of_int saturations_res));
- sorted, saturations_res
+ sorted, saturations_res, position_of_meta_to_be_coerced
in
let namer l n =
let l = List.map (function Cic.Name s -> s | _ -> "A") l in
let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in
debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
let old_insert_coercions = !CicRefine.insert_coercions in
- let c, metasenv, univ, saturationsres =
+ let c, metasenv, univ, saturationsres, cpos =
try
CicRefine.insert_coercions := false;
let term, ty, metasenv, ugraph =
in
debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv));
- let body_metasenv, saturationsres =
+ let body_metasenv, saturationsres, cpos =
order_body_menv term body_metasenv c1_pis c2_pis
in
debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
debug_print (lazy ("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
debug_print (lazy ("####################"));
CicRefine.insert_coercions := old_insert_coercions;
- term, metasenv, ugraph, saturationsres
+ term, metasenv, ugraph, saturationsres, cpos
with
| CicRefine.RefineFailure s
| CicRefine.Uncertain s -> debug_print s;
CicRefine.insert_coercions := old_insert_coercions;
raise exn
in
- c, metasenv, univ, saturationsres, arity2
+ c, metasenv, univ, saturationsres, arity2, cpos
;;
let build_obj c univ arity =
(* removes from l the coercions that are in !coercions *)
let filter_duplicates l coercions =
List.filter (
- fun (src,l1,tgt) ->
- not (List.exists (fun (s,t,l2) ->
- CoercDb.eq_carr s src &&
- CoercDb.eq_carr t tgt &&
- try
- List.for_all2 (fun (u1,_,_) (u2,_) -> UriManager.eq u1 u2) l1 l2
- with
- | Invalid_argument "List.for_all2" -> debug_print (lazy("XXX")); false)
- coercions))
+ fun (src,l1,tgt) ->
+ not (List.exists (fun (s,t,l2) ->
+ CoercDb.eq_carr s src &&
+ CoercDb.eq_carr t tgt &&
+ try
+ List.for_all2 (fun (u1,_,_) (u2,_,_) -> UriManager.eq u1 u2) l1 l2
+ with
+ | Invalid_argument "List.for_all2" ->
+ debug_print (lazy("XXX")); false)
+ coercions))
l
+;;
let mangle s t l =
(*List.fold_left
let close_coercion_graph src tgt uri saturations baseuri =
(* check if the coercion already exists *)
let coercions = CoercDb.to_list () in
- let todo_list = get_closure_coercions src tgt (uri,saturations) coercions in
+ let todo_list = get_closure_coercions src tgt (uri,saturations,0) coercions in
debug_print (lazy("composed " ^ string_of_int (List.length todo_list)));
let todo_list = filter_duplicates todo_list coercions in
try
List.fold_left
(fun acc (src, l , tgt) ->
try
- (match l with
+ match l with
| [] -> assert false
| (he,saturations1,arity1) :: tl ->
let first_step =
- Cic.Constant ("",
- Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+ Cic.Constant ("", Some (CicUtil.term_of_uri he),
Cic.Sort Cic.Prop, [], obj_attrs arity1),
saturations1,
- arity1
+ arity1,0
in
let o,_ =
List.fold_left (fun (o,univ) (coer,saturations2,arity2) ->
match o with
- | Cic.Constant (_,Some u,_,[],_),saturations1,arity1 ->
- let t, menv, univ, saturationsres, arityres =
+ | Cic.Constant (_,Some u,_,[],_),saturations1,arity1,_ ->
+ let t, menv, univ, saturationsres, arityres, cposres =
generate_composite' (u,saturations1,arity1)
- (CoercDb.term_of_carr (CoercDb.Uri coer),
+ (CicUtil.term_of_uri coer,
saturations2, arity2) [] [] univ
in
if (menv = []) then
HLog.warn "MENV non empty after composing coercions";
let o,univ = build_obj t univ arityres in
- (o,saturationsres,arityres),univ
+ (o,saturationsres,arityres,cposres),univ
| _ -> assert false
) (first_step, CicUniv.oblivion_ugraph) tl
in
- let name_src = CoercDb.name_of_carr src in
- let name_tgt = CoercDb.name_of_carr tgt in
+ let name_src = CoercDb.string_of_carr src in
+ let name_tgt = CoercDb.string_of_carr tgt in
let by = List.map (fun u,_,_ -> UriManager.name_of_uri u) l in
let name = mangle name_tgt name_src by in
let c_uri =
number_if_already_defined baseuri name
- (List.map (fun (_,_,u,_,_,_) -> u) acc)
+ (List.map (fun (_,_,u,_,_,_,_) -> u) acc)
in
- let named_obj,saturations,arity =
+ let named_obj,saturations,arity,cpos =
match o with
- | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity ->
- Cic.Constant (name,bo,ty,vl,attrs),saturations,arity
+ | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity,cpos ->
+ Cic.Constant (name,bo,ty,vl,attrs),saturations,arity,cpos
| _ -> assert false
in
- (src,tgt,c_uri,saturations,named_obj,arity))::acc
+ (src,tgt,c_uri,saturations,named_obj,arity,cpos)::acc
with UnableToCompose -> acc
) [] todo_list
in
(* generate_composite (c2 (c1 s)) in the universe graph univ
* both living in the same context and metasenv *)
let generate_composite c1 c2 context metasenv univ sat1 sat2 =
- let a,b,c,_,_ =
+ let a,b,c,_,_,_ =
generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ
in
a,b,c
CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
(CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
- int (* saturations *) * Cic.obj * int (* arity *)) list
+ int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list
exception UnableToCompose
let rec dummies_of_coercions =
function
- | Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
+ | Cic.Appl (c::l) when CoercDb.is_a_coercion c <> None ->
Cic.Meta (-1,[])
| Cic.Appl l ->
let l' = List.map dummies_of_coercions l in Cic.Appl l'
intros; elim n; [reflexivity] simplify; rewrite > H; reflexivity;
qed.
-inductive sorted (T:Type) (lt : T → T → Prop): list T → Prop ≝
-| sorted_nil : sorted T lt []
-| sorted_one : ∀x. sorted T lt [x]
-| sorted_cons : ∀x,y,tl. lt x y → sorted T lt (y::tl) → sorted T lt (x::y::tl).
+record rel : Type ≝ {
+ rel_T :> Type;
+ rel_op :2> rel_T → rel_T → Prop
+}.
+
+record trans_rel : Type ≝ {
+ o_rel :> rel;
+ o_tra : ∀x,y,z: o_rel.o_rel x y → o_rel y z → o_rel x z
+}.
+
+lemma trans: ∀r:trans_rel.∀x,y,z:r.r x y → r y z → r x z.
+apply o_tra;
+qed.
+
+inductive sorted (lt : trans_rel): list (rel_T lt) → Prop ≝
+| sorted_nil : sorted lt []
+| sorted_one : ∀x. sorted lt [x]
+| sorted_cons : ∀x,y,tl. lt x y → sorted lt (y::tl) → sorted lt (x::y::tl).
lemma nth_nil: ∀T,i.∀def:T. \nth [] def i = def.
intros; elim i; simplify; [reflexivity;] assumption; qed.
intros; cases l in H; [intros; cases (not_le_Sn_O ? H);] intros; constructor 1;
qed.
-lemma sorted_tail: ∀T,r,x,l.sorted T r (x::l) → sorted T r l.
+lemma sorted_tail: ∀r,x,l.sorted r (x::l) → sorted r l.
intros; inversion H; intros; [destruct H1;|destruct H1;constructor 1;]
destruct H4; assumption;
qed.
-lemma sorted_skip:
- ∀T,r,x,y,l.
- transitive T r → sorted T r (x::y::l) → sorted T r (x::l).
-intros; inversion H1; intros; [1,2: destruct H2]
-destruct H5; inversion H3; intros; [destruct H5]
-[1: destruct H5; constructor 2;
-|2: destruct H8; constructor 3; [apply (H ??? H2 H5);]
- apply (sorted_tail ???? H3);]
+lemma sorted_skip: ∀r,x,y,l. sorted r (x::y::l) → sorted r (x::l).
+intros (r x y l H1); inversion H1; intros; [1,2: destruct H]
+destruct H4; inversion H2; intros; [destruct H4]
+[1: destruct H4; constructor 2;
+|2: destruct H7; constructor 3; [ apply (o_tra ? ??? H H4);]
+ apply (sorted_tail ??? H2);]
qed.
-lemma sorted_tail_bigger : ∀T,r,x,l,d.sorted T r (x::l) → ∀i. i < \len l → r x (\nth l d i).
+lemma sorted_tail_bigger : ∀r,x,l,d.sorted r (x::l) → ∀i. i < \len l → r x (\nth l d i).
intros 4; elim l; [ cases (not_le_Sn_O i H1);]
cases i in H2;
-[2: intros; apply (H d ? n);[apply (sorted_skip ????? H1)|apply le_S_S_to_le; apply H2]
+[2: intros; apply (H ? n);[apply (sorted_skip ???? H1)|apply le_S_S_to_le; apply H2]
|1: intros; inversion H1; intros; [1,2: destruct H3]
destruct H6; simplify; assumption;]
qed.
apply le_plus_n_r;]
|2,3: clear H6;
cases (aux n1) in H5 ⊢ %; intros;
- change in match (a â\8c©w,H5â\8cª) in H6 ⊢ % with (a w);
+ change in match (a â\89ªw,H5â\89«) in H6 ⊢ % with (a w);
cases H5; clear H5; cases H7; clear H7;
[1: left; split; [ apply (le_S ?? H5); | assumption]
|3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
include "lebesgue.ma".
include "models/nat_order_continuous.ma".
-alias symbol "pair" = "dependent pair".
theorem nat_lebesgue_oc:
∀a:sequence ℕ.∀l,u:ℕ.∀H:∀i:nat.a i ∈ [l,u].
∀x:ℕ.a order_converges x →
x ∈ [l,u] ∧
∀h:x ∈ [l,u].
- uniform_converge {[l,u]} â\8c\8an,â\8c©a n,H nâ\8cªâ\8c\8b â\8c©x,hâ\8cª.
+ uniform_converge {[l,u]} â\8c\8an,â\89ªa n,H nâ\89«â\8c\8b â\89ªx,hâ\89«.
intros; apply lebesgue_oc; [apply nat_us_is_oc] assumption;
qed.
definition order_converge ≝
λO:ordered_set.λa:sequence O.λx:O.
exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
- (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
+ (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
(u i) is_supremum ⌊w,a (w+i)⌋).
notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
HLog.debug
((String.concat ","
(List.map
- (fun u,saturations ->
+ (fun u,saturations,_ ->
UriManager.name_of_uri u ^
"(" ^ string_of_int saturations ^ ")")
ul)) ^ ":"
- ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
+ ^ CoercDb.string_of_carr s ^ " -> " ^ CoercDb.string_of_carr t))
(CoercDb.to_list ()));
addDebugSeparator ();
let mview () = (MatitaMathView.sequentsViewer_instance ())#cicMathView in
None, "Type checking assertion failed: " ^ Lazy.force msg
| LibrarySync.AlreadyDefined s ->
None, "Already defined: " ^ UriManager.string_of_uri s
- | CoercDb.EqCarrNotImplemented msg ->
- None, ("EqCarrNotImplemented: " ^ Lazy.force msg)
| DisambiguateChoices.Choice_not_found msg ->
None, ("Disambiguation choice not found: " ^ Lazy.force msg)
| MatitaEngine.EnrichedWithLexiconStatus (exn,_) ->
projects / helm.git / commitdiff