the new coercion behaviour (variants + composition with ID) and the new

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-basic_pairs_to_o-basic_topologies.ma

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 f2f6af0208c5c914fa25ab41db74f806e7da9804..c66e709dd8c14032673936df02bbabe208a864af 100644 (file)
--- 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
@@ -15,8 +15,10 @@
 include "o-basic_pairs.ma".
 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.
+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;
@@ -126,18 +128,12 @@ lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R
 qed.
 
 lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
- intros;
- (* BAD *)
- lapply (†(lemma_10_3_a ?? R p)); [2: apply (R⎻* ); | skip | apply Hletin ]
+ intros; apply (†(lemma_10_3_a ?? R p));
 qed.
 
-(* VEERY BAD! *)
-axiom lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
-(*
- intros;
- (* BAD *)
- lapply (†(lemma_10_3_b ?? R p)); [2: apply rule R; | skip | apply Hletin ]
-qed. *)
+lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
+intros; unfold in ⊢ (? ? ? % %); 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.
@@ -145,7 +141,7 @@ 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;
+ intro t;
  constructor 1;
   [ apply (form t);
   | apply (□_t ∘ Ext⎽t);
@@ -186,42 +182,35 @@ qed.
 definition o_continuous_relation_of_o_relation_pair:
  ∀BP1,BP2.arrows2 BP BP1 BP2 →
   arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
- intros;
+ intros (BP1 BP2 t);
  constructor 1;
   [ apply (t \sub \f);
   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
     apply sym1;
-    alias symbol "refl" = "refl1".
-    apply (.= †?); [1: apply (t \sub \f (((◊_BP1∘(⊩)* ) U))); |
-    lapply (†e); [2: apply rule t \sub \f; | skip | apply Hletin]]
-    change in ⊢ (? ? ? % ?) with ((◊_BP2 ∘(⊩)* ) ((t \sub \f ∘ (◊_BP1∘(⊩)* )) U));
-    lapply (comp_assoc2 ????? (⊩)* (⊩) t \sub \f);
-    apply (.= †(Hletin ?)); clear Hletin;
+    unfold in ⊢ (? ? ? (? ? ? ? %) ?);
+    apply (.= †(†e));
     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
-    cut ?;
-     [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e3 ^ -1 ((⊩)* U));] | 2,4: skip]
-    apply (.= †Hcut);
+    cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
+      cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+    apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
     apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
-    apply (.= Hcut ^ -1);
+    apply (.= COM ^ -1);
     change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
-    apply (prop11 ?? t \sub \f);
-    apply (e ^ -1);
+    change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
+    unfold in ⊢ (? ? ? % %); apply (†e^-1);
   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
     apply sym1;
-    apply (.= †?); [1: apply (t \sub \f⎻* ((((⊩)⎻* ∘ (⊩)⎻) U))); |
-    lapply (†e); [2: apply rule (t \sub \f⎻* ); | skip | apply Hletin]]
-    change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘(⊩)⎻ ) ((t \sub \f⎻* ∘ ((⊩)⎻*∘(⊩)⎻ )) U));
-    lapply (comp_assoc2 ????? (⊩)⎻ (⊩)⎻* t \sub \f⎻* );
-    apply (.= †(Hletin ?)); clear Hletin;
+    unfold in ⊢ (? ? ? (? ? ? ? %) ?);
+    apply (.= †(†e));
     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
-    cut ?;
-     [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e1 ^ -1 ((⊩)⎻ U));] | 2,4: skip]
-    apply (.= †Hcut);
+    cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
+      cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+    apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
     apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
-    apply (.= Hcut ^ -1);
+    apply (.= COM ^ -1);
     change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
-    apply (prop11 ?? t \sub \f⎻* );
-    apply (e ^ -1); ]
+    change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
+    unfold in ⊢ (? ? ? % %); apply (†e^-1);]
 qed.
\ No newline at end of file