From 0080faad4e730c227b6bbb2549407b23703b477a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 19 Jan 2009 09:56:34 +0000 Subject: [PATCH] all pullbacks are attempted in sequence, removed many unfold --- .../cic_unification/cicUnification.ml | 71 +++++++--- .../components/cic_unification/coercGraph.ml | 22 +-- .../components/library/librarySync.ml | 10 +- .../overlap/concrete_spaces.ma | 2 +- .../formal_topology/overlap/o-algebra.ma | 3 +- .../o-basic_pairs_to_o-basic_topologies.ma | 130 +++++++++++++++++- .../overlap/o-basic_topologies.ma | 6 +- .../formal_topology/overlap/relations.ma | 2 - 8 files changed, 202 insertions(+), 44 deletions(-) diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml index 52fdfa19a..fca316fa3 100644 --- a/helm/software/components/cic_unification/cicUnification.ml +++ b/helm/software/components/cic_unification/cicUnification.ml @@ -302,21 +302,25 @@ and beta_expand_many test_equality_only metasenv subst context t args ugraph = 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 @@ -666,7 +670,7 @@ prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl 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 @@ -674,19 +678,33 @@ prerr_endline 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 @@ -730,10 +748,10 @@ res) 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) -> @@ -750,7 +768,18 @@ res) 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 diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index 17301e4d6..61df4ceb5 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -304,10 +304,16 @@ let lb (c,_,_) = (* 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) = @@ -321,12 +327,12 @@ 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 *) diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index da2d69ec1..a0a0f324e 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -325,10 +325,18 @@ and 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 diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma index 46e537864..791af46b3 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma @@ -18,7 +18,7 @@ include "basic_pairs.ma". (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 }. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma index b17dacbaf..b278adfc0 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma @@ -286,8 +286,7 @@ constructor 1; 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. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma index bdadaf0fe..179107957 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma @@ -17,6 +17,128 @@ include "o-basic_topologies.ma". 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; @@ -65,7 +187,6 @@ definition o_continuous_relation_of_o_relation_pair: [ 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: @@ -76,10 +197,9 @@ definition o_continuous_relation_of_o_relation_pair: 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: @@ -90,5 +210,5 @@ definition o_continuous_relation_of_o_relation_pair: 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. diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma index 8847eef31..30a8b476c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma @@ -106,10 +106,8 @@ definition continuous_relation_comp: | intros; apply sym1; change in match ((s ∘ r) U) with (s (r U)); - (**) 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; diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma index 74a7c7d78..307797566 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma @@ -98,10 +98,8 @@ definition REL: category1. 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. -- 2.39.2