X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fformal_topology.ma;h=a683784081bcf5064d92690d3952309b172404a5;hb=8f4162a9db17a597d4fba49eb957009fc0268378;hp=54c6aa629e0edc819f05b62d54f8f964b806c32d;hpb=839d7d2a1c009f20318a9cbdedd99e95d11d3e74;p=helm.git

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 54c6aa629..a68378408 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -12,26 +12,219 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/connectives.ma".
+include "logic/equality.ma".
 
-coinductive fish (A:Type) (i: A → Type) (C: ∀a:A.i a → A → Prop) (U: A → Prop)
-               : A → Prop
-≝
- mk_foo: ∀a:A. (U a ∧ ∀j: i a. ∃y: A. C a j y ∧ fish A i C U y) → fish A i C U a.
+inductive And (A,B:CProp) : CProp ≝
+ conj: A → B → And A B.
+ 
+interpretation "constructive and" 'and x y = (And x y).
 
-let corec fish_rec (A:Type) (i: A → Type) (C: ∀a:A.i a → A → Prop) (U: A → Prop)
- (P: A → Prop) (H1: ∀a:A. P a → U a)
-  (H2: ∀a:A. P a → ∀j: i a. ∃y: A. C a j y ∧ P y) :
-   ∀a:A. ∀p: P a. fish A i C U a ≝
+inductive Or (A,B:CProp) : CProp ≝
+ | or_intro_l: A → Or A B
+ | or_intro_r: B → Or A B. 
+ 
+interpretation "constructive or" 'or x y = (Or x y).
+
+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 }.
+
+notation "hvbox(2 \sup A)" non associative with precedence 45
+for @{ 'powerset $A }.
+
+interpretation "powerset" 'powerset A = (powerset A).
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
+
+definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+interpretation "mem" 'mem a S = (mem _ S a).
+
+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 }. (* \between *)
+
+interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
+
+definition subseteq ≝ λA:Type.λU,V:2 \sup A.∀a:A. a ∈ U → a ∈ V.
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
+
+definition intersects ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∧ a ∈ V}.
+
+notation "hvbox(a break ∩ b)" non associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+interpretation "intersects" 'intersects U V = (intersects _ U V).
+
+definition union ≝ λA:Type.λU,V:2 \sup A.{a | a ∈ U ∨ a ∈ V}.
+
+notation "hvbox(a break ∪ b)" non associative with precedence 55
+for @{ 'union $a $b }. (* \cup *)
+
+interpretation "union" 'union U V = (union _ U V).
+
+record axiom_set : Type ≝ { 
+  A:> Type;
+  i: A → Type;
+  C: ∀a:A. i a → 2 \sup A
+}.
+
+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. 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 }. (* a \ltri b *)
+
+interpretation "coversl" 'covers A U = (for_all _ U A (covers _ U)).
+interpretation "covers" 'covers a U = (covers _ U a).
+
+definition covers_elim ≝
+ λ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 → C ? a j ⊆ 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
+          match q return λ_:(C ? a j) ◃ U. C ? a j ⊆ P with
+          [ 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. 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 }. (* a \ltimes b *)
+
+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. C ? a j ≬ P):
+   ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
  λa,p.
-  mk_foo A i C U a
-   (conj ? ? (H1 ? p)
-   (λj: i a.
+  mk_fish A U a
+   (H1 ? p)
+   (λj: i ? a.
     match H2 a p j with
-     [ ex_intro (y: A) (Ha: C a j y ∧ P y) ⇒
-        match Ha with
-         [ conj (fHa: C a j y) (sHa: P y) ⇒
-            ex_intro A (λy.C a j y ∧ fish A i C U y) y
-             (conj ? ? fHa (fish_rec A i C U P H1 H2 y sHa))
-         ]
-     ])).
\ No newline at end of file
+     [ 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;
+ apply refl;
+ assumption.
+qed.
+
+theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
+ intros;
+ apply (covers_elim ?? {a | a ◃ V} ??? H); simplify; intros;
+  [ cases H1 in H2; apply H2;
+  | apply infinity;
+     [ assumption
+     | constructor 1;
+       assumption]]
+qed.
+
+theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
+ intros;
+ cases H;
+ assumption.
+qed.
+
+theorem cotransitivity:
+ ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
+ intros;
+ apply (fish_rec ?? {a|a ⋉ U} ??? H); simplify; intros;
+  [ 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.
+ intros;
+ generalize in match H; clear H; 
+ apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
+ clear H1; simplify; intros;
+  [ 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.{b | a=b}.
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+interpretation "singleton" 'singl a = (singleton _ a).
+
+definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
+
+interpretation "covered by one" 'leq a b = (leq _ a b).
+
+theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
+ intros;
+ apply refl;
+ normalize;
+ reflexivity.
+qed.
+
+theorem leq_trans: ∀A:axiom_set.∀a,b,c:A. a ≤ b → b ≤ c → a ≤ c.
+ intros;
+ unfold in H H1 ⊢ %;
+ apply (transitivity ???? H);
+ constructor 1;
+ intros;
+ normalize in H2;
+ rewrite < H2;
+ assumption.
+qed.
+
+definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
+
+notation "↑a" with precedence 80 for @{ 'uparrow $a }.
+
+interpretation "uparrow" 'uparrow a = (uparrow _ a).
+
+definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
+
+notation "↓a" with precedence 80 for @{ 'downarrow $a }.
+
+interpretation "downarrow" 'downarrow a = (downarrow _ a).
+
+definition fintersects ≝ λA:axiom_set.λU,V:2 \sup A.↓U ∩ ↓V.
+
+notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
+
+interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
+
+record convergent_generated_topology : Type ≝
+ { AA:> axiom_set;
+   convergence: ∀a:AA.∀U,V:2 \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V
+ }.
+