From 1883bb697368eda63861ebbb233062f74abd20d1 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 4 Jul 2008 11:57:33 +0000
Subject: [PATCH] Compatibility finished.

---
 .../matita/library/demo/formal_topology.ma    | 23 ++++++++++++++++---
 1 file changed, 20 insertions(+), 3 deletions(-)

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index d828f8c4e..ca544b598 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -53,8 +53,8 @@ with coversl : (2 \sup A) → CProp ≝
 notation "hvbox(a break ◃ b)" non associative with precedence 45
 for @{ 'covers $a $b }.
 
-interpretation "covers" 'covers a U = (covers _ U a).
 interpretation "coversl" 'covers A U = (coversl _ U A).
+interpretation "covers" 'covers a U = (covers _ U a).
 
 definition covers_elim ≝
  λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
@@ -73,10 +73,12 @@ definition covers_elim ≝
 
 coinductive fish (A:axiom_set) (U: 2 \sup A) : A → CProp ≝
  mk_fish: ∀a:A. (a ∈ U ∧ ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ fish A U y) → fish A U a.
+definition fishl ≝ λA:axiom_set.λU:2 \sup A.λV:2 \sup A. ∃a. a ∈ V ∧ fish ? U a.
 
 notation "hvbox(a break ⋉ b)" non associative with precedence 45
 for @{ 'fish $a $b }.
 
+interpretation "fishl" 'fish A U = (fishl _ U A).
 interpretation "fish" 'fish a U = (fish _ U a).
 
 let corec fish_rec (A:axiom_set) (U: 2 \sup A)
@@ -104,7 +106,7 @@ qed.
 
 theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
  intros;
- apply (covers_elim ?? (mk_powerset A (λa.a ◃ V)) ??? H); intros;
+ apply (covers_elim ?? (mk_powerset A (λa.a ◃ V)) ??? H); simplify; intros;
   [ cases H1 in H2;
     intro;
     apply H2;
@@ -123,11 +125,26 @@ theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
 qed.
 
 theorem cotransitivity:
- ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b. b ⋉ U → b ∈ V) → a ⋉ V.
+ ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
  intros;
  apply (fish_rec ?? (mk_powerset A (λa.a ⋉ U)) ??? H); simplify; intros;
   [ apply H1;
     assumption
   | cases H2 in j; clear H2; cases H3; clear H3;
     assumption]
+qed.
+
+theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
+ intros;
+ generalize in match H; clear H; generalize in match V; clear V;
+ apply (covers_elim ?? (mk_powerset A (λa.∀p:2 \sup A.a ⋉ p → U ⋉ p)) ??? H1);
+ clear H1; simplify; intros;
+  [ exists [apply a1]
+    split;
+    assumption
+  | cases H2 in j H H1; clear H2 a1; intros;
+    cases H; clear H;
+    cases (H4 i); clear H4; cases H; clear H;
+    apply (H2 w); clear H2;
+    assumption]
 qed.
\ No newline at end of file
-- 
2.39.2