From 8c0ccf03dbefd83818bc3b6849634f422f8ec727 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Jan 2009 23:07:58 +0000
Subject: [PATCH] o_continous_relations are really o_relation_pair... up to a
 bug of Matita (a meta left in the metasenv :-(

---
 .../o-basic_pairs_to_o-basic_topologies.ma    | 63 ++++++++++++++-----
 1 file changed, 47 insertions(+), 16 deletions(-)

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 f34c3c074..f2f6af020 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
@@ -111,6 +111,20 @@ lemma lemma_10_3_b: ∀S,T.∀R:arrows2 OA S T.∀p. R* (R (R* p)) = 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;
  (* BAD *)
@@ -176,21 +190,38 @@ definition o_continuous_relation_of_o_relation_pair:
  constructor 1;
   [ apply (t \sub \f);
   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
-    lapply (.= †e); [3: apply rule t \sub \f; |4: apply Hletin; |1,2: skip]
-    cut ((t \sub \f ∘ (⊩)) ∘ (⊩)* = ?);
-     [ 
-     
-      lapply (Hcut U); apply Hletin;
-      whd in Hcut;: apply rule (rel BP2);
-    
-    generalize in match U; clear e; 
-    change with (t \sub \f ((⊩) ((⊩)* U)) =(⊩) ((⊩)* (t \sub \f U)));
-    change in ⊢ (? ? ? % ?) with ((t \sub \f ∘ ((⊩) ∘ (⊩)* )) U);
-    
-    
+    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;
+    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);
+    change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
+    apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
+    apply (.= Hcut ^ -1);
+    change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
+    apply (prop11 ?? t \sub \f);
+    apply (e ^ -1);
   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
-    lapply (.= †e); [3: apply rule (t \sub \f ⎻* ); |4: apply Hletin; |1,2: skip]
-    change with (t \sub \f ⎻* ((⊩)⎻* ((⊩)⎻ U)) = (⊩)⎻* ((⊩)⎻ (t \sub \f⎻* U)));
-    
-  ]
+    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;
+    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);
+    change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
+    apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
+    apply (.= Hcut ^ -1);
+    change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
+    apply (prop11 ?? t \sub \f⎻* );
+    apply (e ^ -1); ]
 qed.
\ No newline at end of file
-- 
2.39.2