in
subst,metasenv,hd,ugraph
-and warn_if_not_unique xxx to1 to2 carr car1 car2 =
+and warn_if_not_unique xxx car1 car2 =
+ let unopt =
+ function
+ | Some (_,Cic.Appl(Cic.Const(u,_)::_)) -> UriManager.string_of_uri u
+ | Some (_,t) -> CicPp.ppterm t
+ | None -> "id"
+ in
match xxx with
| [] -> ()
- | (m2,_,c2,c2')::_ ->
- let m1,c1,c1' = carr,to1,to2 in
- let unopt =
- function Some (_,t) -> CicPp.ppterm t
- | None -> "id"
- in
+ | _ ->
HLog.warn
- ("There are two minimal joins of "^ 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')
+ ("There are "^string_of_int (List.length xxx + 1)^
+ " minimal joins of "^ CoercDb.string_of_carr car1^" and "^
+ CoercDb.string_of_carr car2^": " ^
+ String.concat " and "
+ (List.map
+ (fun (m2,_,c2,c2') ->
+ " via "^CoercDb.string_of_carr m2^" via "^unopt c2^" + "^unopt c2')
+ xxx))
(* NUOVA UNIFICAZIONE *)
(* A substitution is a (int * Cic.term) list that associates a
let subst',metasenv,ugraph =
(*DEBUGGING ONLY:
prerr_endline
- ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
+ ("conclude: " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
" <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
*)
fo_unif_subst test_equality_only subst context
in
if subst = subst' then raise exn
else
-(*DEBUGGING ONLY:
+(*DEBUGGING ONLY:
let subst,metasenv,ugrph as res =
*)
fo_unif_subst test_equality_only subst' context
metasenv (C.Appl l1) (C.Appl l2) ugraph
-(*DEBUGGING ONLY:
+(*DEBUGGING ONLY:
in
(prerr_endline
- (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+ ("OK: "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
" <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
res)
*)
in
+(*DEBUGGING ONLY:
+prerr_endline (Printf.sprintf
+"Pullback problem\nterm1: %s\nterm2: %s\ncar1: %s\ncar2: %s\nlast_tl1: %s
+last_tl2: %s\nhead1_c: %s\nhead2_c: %s\n"
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context)
+(CoercDb.string_of_carr car1)
+(CoercDb.string_of_carr car2)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1 context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2 context)
+(CoercDb.string_of_carr head1_c)
+(CoercDb.string_of_carr head2_c)
+);
+*)
if CoercDb.eq_carr car1 car2 then
match last_tl1,last_tl2 with
| C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
CoercGraph.meets
metasenv subst context (grow1,car1) (grow2,car2)
in
- (match meets with
- | [] -> raise exn
- | (carr,metasenv,to1,to2)::xxx ->
- warn_if_not_unique xxx to1 to2 carr car1 car2;
+ (match
+ HExtlib.list_findopt
+ (fun (carr,metasenv,to1,to2) meet_no ->
+ try
let last_tl1',(subst,metasenv,ugraph) =
match grow1,to1 with
| true,Some (last,coerced) ->
metasenv coerced last_tl2 ugraph
| _ -> last_tl2,(subst,metasenv,ugraph)
in
- conclude subst metasenv ugraph last_tl1' last_tl2')
+ if meet_no > 0 then
+ HLog.warn ("Using pullback number " ^ string_of_int
+ meet_no);
+ Some
+ (conclude subst metasenv ugraph last_tl1' last_tl2')
+ with
+ | UnificationFailure _
+ | Uncertain _ -> None)
+ meets
+ with
+ | Some x -> x
+ | None -> raise exn)
(* }}} pullback *)
(* {{{ CSC: This is necessary because of the "elim H" tactic
where the type of H is only reducible to an
(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
* (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
-let rec min acc = function
+let rec min acc skipped = function
| c::tl ->
- if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
- | [] -> acc
+ if List.exists (lb c) (tl@acc)
+ then min acc (c::skipped) tl else min (c::acc) skipped tl
+ | [] -> acc, skipped
+;;
+
+
+let sort l =
+ let low, high = min [] [] l in low @ high
;;
let meets metasenv subst context (grow_left,left) (grow_right,right) =
in
List.map
(fun (c,uo1,uo2) ->
- let metasenv, uo1 =
- if grow_left then saturate metasenv uo1 else metasenv, None in
- let metasenv, uo2 =
- if grow_right then saturate metasenv uo2 else metasenv, None in
+ let metasenv, uo1 = saturate metasenv uo1 in
+ let metasenv, uo2 = saturate metasenv uo2 in
c,metasenv, uo1, uo2)
- (min [] (intersect (grow left) (grow right)))
+ (sort (intersect
+ (if grow_left then grow left else [left,None])
+ (if grow_right then grow right else [right,None])))
;;
(* EOF *)
CicPp.ppterm (Cic.Sort s1) ^ " <> " ^
CicPp.ppterm (Cic.Sort s2)); false)
| _ ->
+ let ty', _ =
+ CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
+ CicUniv.oblivion_ugraph
+ in
+ if CicUtil.alpha_equivalence ty ty' then
(HLog.warn
("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
"it is a duplicate of " ^ UriManager.string_of_uri u);
- true))
+ true)
+ else false
+
+ )
ul)
(CoercDb.to_list ())
in
(confondendola con la coercion per gli oggetti di SET *)
record concrete_space : Type1 ≝
{ bp:> BP;
- converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩_bp (U ↓ V);
+ converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
all_covered: ∀x: carr1 (concr bp). x ⊩ form bp
}.
apply or_prop3;
]
| intros; split; simplify;
- [3: unfold arrows1_of_ORelation_setoid;
- apply ((†e)‡(†e1));
+ [3: unfold arrows1_of_ORelation_setoid; apply ((†e)‡(†e1));
|1: apply ((†e)‡(†e1));
|2,4: apply ((†e1)‡(†e));]]
qed.
alias symbol "eq" = "setoid1 eq".
+(* qui la notazione non va *)
+lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = (binary_join ? p q).
+ intros;
+ apply oa_leq_antisym;
+ [ apply oa_density; intros;
+ apply oa_overlap_sym;
+ unfold binary_join; simplify;
+ apply (. (oa_join_split : ?));
+ exists; [ apply false ]
+ apply oa_overlap_sym;
+ assumption
+ | unfold binary_join; simplify;
+ apply (. (oa_join_sup : ?)); intro;
+ cases i; whd in ⊢ (? ? ? ? ? % ?);
+ [ assumption | apply oa_leq_refl ]]
+qed.
+
+lemma overlap_monotone_left: ∀S:OA.∀p,q,r:S. p ≤ q → p >< r → q >< r.
+ intros;
+ apply (. (leq_to_eq_join : ?)‡#);
+ [ apply f;
+ | skip
+ | apply oa_overlap_sym;
+ unfold binary_join; simplify;
+ apply (. (oa_join_split : ?));
+ exists [ apply true ]
+ apply oa_overlap_sym;
+ assumption; ]
+qed.
+
+(* Part of proposition 9.9 *)
+lemma f_minus_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R⎻ p ≤ R⎻ q.
+ intros;
+ apply (. (or_prop2 : ?));
+ apply oa_leq_trans; [2: apply f; | skip | apply (. (or_prop2 : ?)^ -1); apply oa_leq_refl;]
+qed.
+
+(* Part of proposition 9.9 *)
+lemma f_minus_star_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R⎻* p ≤ R⎻* q.
+ intros;
+ apply (. (or_prop2 : ?)^ -1);
+ apply oa_leq_trans; [3: apply f; | skip | apply (. (or_prop2 : ?)); apply oa_leq_refl;]
+qed.
+
+(* Part of proposition 9.9 *)
+lemma f_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R p ≤ R q.
+ intros;
+ apply (. (or_prop1 : ?));
+ apply oa_leq_trans; [2: apply f; | skip | apply (. (or_prop1 : ?)^ -1); apply oa_leq_refl;]
+qed.
+
+(* Part of proposition 9.9 *)
+lemma f_star_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R* p ≤ R* q.
+ intros;
+ apply (. (or_prop1 : ?)^ -1);
+ apply oa_leq_trans; [3: apply f; | skip | apply (. (or_prop1 : ?)); apply oa_leq_refl;]
+qed.
+
+lemma lemma_10_2_a: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R⎻* (R⎻ p).
+ intros;
+ apply (. (or_prop2 : ?)^-1);
+ apply oa_leq_refl.
+qed.
+
+lemma lemma_10_2_b: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* p) ≤ p.
+ intros;
+ apply (. (or_prop2 : ?));
+ apply oa_leq_refl.
+qed.
+
+lemma lemma_10_2_c: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R* (R p).
+ intros;
+ apply (. (or_prop1 : ?)^-1);
+ apply oa_leq_refl.
+qed.
+
+lemma lemma_10_2_d: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* p) ≤ p.
+ intros;
+ apply (. (or_prop1 : ?));
+ apply oa_leq_refl.
+qed.
+
+lemma lemma_10_3_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
+ intros; apply oa_leq_antisym;
+ [ apply lemma_10_2_b;
+ | apply f_minus_image_monotone;
+ apply lemma_10_2_a; ]
+qed.
+
+lemma lemma_10_3_b: ∀S,T.∀R:arrows2 OA S T.∀p. R* (R (R* p)) = R* p.
+ intros; apply oa_leq_antisym;
+ [ apply f_star_image_monotone;
+ apply (lemma_10_2_d ?? R p);
+ | apply lemma_10_2_c; ]
+qed.
+
+lemma lemma_10_3_c: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R p)) = R p.
+ intros; apply oa_leq_antisym;
+ [ apply lemma_10_2_d;
+ | apply f_image_monotone;
+ apply (lemma_10_2_c ?? R p); ]
+qed.
+
+lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
+ intros; apply oa_leq_antisym;
+ [ apply f_minus_star_image_monotone;
+ apply (lemma_10_2_b ?? R p);
+ | apply lemma_10_2_a; ]
+qed.
+
+lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
+ intros; apply (†(lemma_10_3_a ?? R p));
+qed.
+
+lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
+intros; apply (†(lemma_10_3_b ?? R p));
+qed.
+
+lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
+ intros; split; intro; apply oa_overlap_sym; assumption.
+qed.
+
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
definition o_basic_topology_of_o_basic_pair: BP → BTop.
intro t;
[ apply (t \sub \f);
| unfold o_basic_topology_of_o_basic_pair; simplify; intros;
apply sym1;
- unfold in ⊢ (? ? ? (? ? ? ? %) ?);
apply (.= †(†e));
change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
apply (.= COM ^ -1);
change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
- unfold in ⊢ (? ? ? % %); apply (†e^-1);
+ apply (†e^-1);
| unfold o_basic_topology_of_o_basic_pair; simplify; intros;
apply sym1;
- unfold in ⊢ (? ? ? (? ? ? ? %) ?);
apply (.= †(†e));
change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
apply (.= COM ^ -1);
change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
- unfold in ⊢ (? ? ? % %); apply (†e^-1);]
-qed.
\ No newline at end of file
+ apply (†e^-1);]
+qed.
| intros;
apply sym1;
change in match ((s ∘ r) U) with (s (r U));
- (*<BAD>*) unfold FunClass_1_OF_carr2;
- apply (.= (reduced : ?)\sup -1);
- [ (*BAD*) change with (eq1 ? (r U) (J ? (r U)));
- (* BAD U *) apply (.= (reduced ??? U ?)); [ assumption | apply refl1 ]
+ apply (.= (reduced : ?)\sup -1);
+ [ apply (.= (reduced :?)); [ assumption | apply refl1 ]
| apply refl1]
| intros;
apply sym1;
first [apply refl | assumption]]]
qed.
-(*
definition setoid_of_REL : objs1 REL → setoid ≝ λx.x.
coercion setoid_of_REL.
-*)
definition binary_relation_setoid_of_arrow1_REL :
∀P,Q. arrows1 REL P Q → binary_relation_setoid P Q ≝ λP,Q,x.x.
projects / helm.git / commitdiff