Nice: cotransitivity proved.

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 257139aef9c495de557c3285a756dabd0ee97032..d828f8c4ea2c7445127f43d2727c0e2915315c1e 100644 (file)
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -12,10 +12,19 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/connectives.ma".
 include "logic/equality.ma".
 
-record powerset (A: Type) : Type ≝ { char: A → Prop }.
+inductive And (A,B:CProp) : CProp ≝
+ conj: A → B → And A B.
+ 
+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).
+
+record powerset (A: Type) : Type ≝ { char: A → CProp }.
 
 notation "hvbox(2 \sup A)" non associative with precedence 45
 for @{ 'powerset $A }.
@@ -48,21 +57,21 @@ interpretation "covers" 'covers a U = (covers _ U a).
 interpretation "coversl" 'covers A U = (coversl _ U A).
 
 definition covers_elim ≝
- λA:axiom_set.λU: 2 \sup A.λP:A → CProp.
-  λH1:∀a:A. a ∈ U → P a.
-   λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → P b) → P a.
-    let rec aux (a:A) (p:a ◃ U) on p : P a ≝
-     match p return λaa.λ_:aa ◃ U.P aa with
+ λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
+  λH1:∀a:A. a ∈ U → a ∈ P.
+   λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → b ∈ P) → a ∈ P.
+    let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝
+     match p return λaa.λ_:aa ◃ U.aa ∈ P with
       [ refl a q ⇒ H1 a q
       | infinity a j q ⇒ H2 a j q (auxl (C ? a j) q)
       ]
-    and auxl (V: 2 \sup A) (q: V ◃ U) on q : ∀b. b ∈ V → P b ≝
-     match q return λVV.λ_:VV ◃ U.∀b. b ∈ VV → P b with
+    and auxl (V: 2 \sup A) (q: V ◃ U) on q : ∀b. b ∈ V → b ∈ P ≝
+     match q return λVV.λ_:VV ◃ U.∀b. b ∈ VV → b ∈ P with
       [ iter VV f ⇒ λb.λr. aux b (f b r) ]
     in
-     aux. 
+     aux.
 
-coinductive fish (A:axiom_set) (U: 2 \sup A) : A → Prop ≝
+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.
 
 notation "hvbox(a break ⋉ b)" non associative with precedence 45
@@ -79,10 +88,10 @@ let corec fish_rec (A:axiom_set) (U: 2 \sup A)
    (conj ? ? (H1 ? p)
    (λj: i ? a.
     match H2 a p j with
-     [ ex_intro (y: A) (Ha: y ∈ C ? a j ∧ y ∈ P) ⇒
+     [ ex_introT (y: A) (Ha: y ∈ C ? a j ∧ y ∈ P) ⇒
         match Ha with
          [ conj (fHa: y ∈ C ? a j) (sHa: y ∈ P) ⇒
-            ex_intro A (λy.y ∈ C ? a j ∧ fish A U y) y
+            ex_introT A (λy.y ∈ C ? a j ∧ fish A U y) y
              (conj ? ? fHa (fish_rec A U P H1 H2 y sHa))
          ]
      ])).
@@ -95,7 +104,7 @@ qed.
 
 theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
  intros;
- elim H using covers_elim;
+ apply (covers_elim ?? (mk_powerset A (λa.a ◃ V)) ??? H); intros;
   [ cases H1 in H2;
     intro;
     apply H2;
@@ -113,3 +122,12 @@ theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
  assumption.
 qed.
 
+theorem cotransitivity:
+ ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b. 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.
\ No newline at end of file