From 71b481a2c2c95d9f80ff49f828336098b3de3924 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 9 Jul 2008 13:40:43 +0000
Subject: [PATCH] minor fixes

---
 .../matita/library/demo/formal_topology.ma    | 68 ++++++++-----------
 1 file changed, 27 insertions(+), 41 deletions(-)

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 05711b7b6..6a3235445 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -19,10 +19,8 @@ inductive And (A,B:CProp) : CProp ≝
  
 interpretation "constructive and" 'and x y = (And x y).
 
-inductive exT (A:Type) (P:A→CProp) : CProp ≝
-  ex_introT: ∀w:A. P w → exT A P.
-
-interpretation "CProp exists" 'exists \eta.x = (exT _ x).
+inductive exT2 (A:Type) (P,Q:A→CProp) : CProp ≝
+  ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
 
 record powerset (A: Type) : Type ≝ { char: A → CProp }.
 
@@ -44,17 +42,17 @@ record axiom_set : Type ≝
    C: ∀a:A. i a → 2 \sup A
  }.
 
-inductive iter (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝
-   cycle: (∀a:A.a ∈ V → covers a) → iter A U V covers.
+inductive for_all (A: axiom_set) (U,V: 2 \sup A) (covers: A → CProp) : CProp ≝
+   iter: (∀a:A.a ∈ V → covers a) → for_all A U V covers.
 
 inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
    refl: ∀a:A. a ∈ U → covers A U a
- | infinity: ∀a:A. ∀j: i ? a. iter A U (C ? a j) (covers A U) → covers A U a.
+ | infinity: ∀a:A. ∀j: i ? a. for_all A U (C ? a j) (covers A U) → covers A U a.
 
 notation "hvbox(a break ◃ b)" non associative with precedence 45
-for @{ 'covers $a $b }.
+for @{ 'covers $a $b }. (* a \ltri b *)
 
-interpretation "coversl" 'covers A U = (iter _ U A (covers _ U)).
+interpretation "coversl" 'covers A U = (for_all _ U A (covers _ U)).
 interpretation "covers" 'covers a U = (covers _ U a).
 
 definition covers_elim ≝
@@ -67,36 +65,34 @@ definition covers_elim ≝
       | infinity a j q ⇒
          H2 a j q
           match q return λ_:(C ? a j) ◃ U.∀b. b ∈ (C ? a j) → b ∈ P with
-          [ cycle f ⇒ λb.λr. aux b (f b r) ]]
+          [ iter f ⇒ λb.λr. aux b (f b r) ]]
     in
      aux.
 
+inductive ex_such (A : axiom_set) (U,V : 2 \sup A) (fish: A → CProp) : CProp ≝
+ found : ∀a. a ∈ V → fish a → ex_such A U V fish.
+
 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.
+ mk_fish: ∀a:A. a ∈ U → (∀j: i ? a. ex_such A U (C ? a j) (fish A U)) → fish A U a.
 
 notation "hvbox(a break ⋉ b)" non associative with precedence 45
-for @{ 'fish $a $b }.
+for @{ 'fish $a $b }. (* a \ltimes b *)
 
-interpretation "fishl" 'fish A U = (fishl _ U A).
+interpretation "fishl" 'fish A U = (ex_such _ U A (fish _ U)).
 interpretation "fish" 'fish a U = (fish _ U a).
 
 let corec fish_rec (A:axiom_set) (U: 2 \sup A)
  (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
-  (H2: ∀a:A. a ∈ P → ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ y ∈ P) :
+  (H2: ∀a:A. a ∈ P → ∀j: i ? a. exT2 ? (λy.y ∈ C ? a j) (λy.y ∈ P)) :
    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
  λa,p.
   mk_fish A U a
-   (conj ? ? (H1 ? p)
+   (H1 ? p)
    (λj: i ? a.
     match H2 a p j with
-     [ ex_introT (y: A) (Ha: y ∈ C ? a j ∧ y ∈ P) ⇒
-        match Ha with
-         [ conj (fHa: y ∈ C ? a j) (sHa: y ∈ P) ⇒
-            ex_introT A (λy.y ∈ C ? a j ∧ fish A U y) y
-             (conj ? ? fHa (fish_rec A U P H1 H2 y sHa))
-         ]
-     ])).
+     [ ex_introT2 (y: A) (HyC : y ∈ C ? a j) (HyP : y ∈ P) ⇒
+         found ???? y HyC (fish_rec A U P H1 H2 y HyP)
+     ]).
 
 theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
  intros;
@@ -107,10 +103,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); simplify; intros;
-  [ cases H1 in H2;
-    intro;
-    apply H2;
-    assumption
+  [ cases H1 in H2; apply H2;
   | apply infinity;
      [ assumption
      | constructor 1;
@@ -120,7 +113,6 @@ qed.
 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
  intros;
  cases H;
- cases H1;
  assumption.
 qed.
 
@@ -128,10 +120,9 @@ theorem cotransitivity:
  ∀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]
+  [ apply H1; apply H2;
+  | cases H2 in j; clear H2; intro i;
+    cases (H4 i); clear H4; exists[apply a3] assumption]
 qed.
 
 theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
@@ -139,14 +130,9 @@ theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U 
  generalize in match H; clear H; 
  apply (covers_elim ?? (mk_powerset A (λa.a ⋉ V → U ⋉ V)) ??? 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]
+  [ exists [apply a1] assumption
+  | cases H2 in j H H1; clear H2 a1; intros; 
+    cases (H1 i); clear H1; apply (H3 a1); assumption]
 qed.
 
 definition singleton ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A.a=b).
@@ -183,7 +169,7 @@ notation "↑a" with precedence 80 for @{ 'uparrow $a }.
 
 interpretation "uparrow" 'uparrow a = (uparrow _ a).
 
-definition overlaps ≝ λA:Type.λU,V:2 \sup A.∃a:A. a ∈ U ∧ a ∈ V.
+definition overlaps ≝ λA:Type.λU,V:2 \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
 
 notation "hvbox(a break ≬ b)" non associative with precedence 45
 for @{ 'overlaps $a $b }.
-- 
2.39.2