1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "logic/equality.ma".
17 inductive And (A,B:CProp) : CProp ≝
18 conj: A → B → And A B.
20 interpretation "constructive and" 'and x y = (And x y).
22 inductive exT (A:Type) (P:A→CProp) : CProp ≝
23 ex_introT: ∀w:A. P w → exT A P.
25 interpretation "CProp exists" 'exists \eta.x = (exT _ x).
27 record powerset (A: Type) : Type ≝ { char: A → CProp }.
29 notation "hvbox(2 \sup A)" non associative with precedence 45
30 for @{ 'powerset $A }.
32 interpretation "powerset" 'powerset A = (powerset A).
34 definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
36 notation "hvbox(a break ∈ b)" non associative with precedence 45
39 interpretation "mem" 'mem a S = (mem _ S a).
41 record axiom_set : Type ≝
44 C: ∀a:A. i a → 2 \sup A
47 inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
48 refl: ∀a:A. a ∈ U → covers A U a
49 | infinity: ∀a:A. ∀j: i ? a. coversl A U (C ? a j) → covers A U a
50 with coversl : (2 \sup A) → CProp ≝
51 iter: ∀V:2 \sup A.(∀a:A.a ∈ V → covers A U a) → coversl A U V.
53 notation "hvbox(a break ◃ b)" non associative with precedence 45
54 for @{ 'covers $a $b }.
56 interpretation "coversl" 'covers A U = (coversl _ U A).
57 interpretation "covers" 'covers a U = (covers _ U a).
59 definition covers_elim ≝
60 λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
61 λH1:∀a:A. a ∈ U → a ∈ P.
62 λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → b ∈ P) → a ∈ P.
63 let rec aux (a:A) (p:a ◃ U) on p : a ∈ P ≝
64 match p return λaa.λ_:aa ◃ U.aa ∈ P with
66 | infinity a j q ⇒ H2 a j q (auxl (C ? a j) q)
68 and auxl (V: 2 \sup A) (q: V ◃ U) on q : ∀b. b ∈ V → b ∈ P ≝
69 match q return λVV.λ_:VV ◃ U.∀b. b ∈ VV → b ∈ P with
70 [ iter VV f ⇒ λb.λr. aux b (f b r) ]
74 coinductive fish (A:axiom_set) (U: 2 \sup A) : A → CProp ≝
75 mk_fish: ∀a:A. (a ∈ U ∧ ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ fish A U y) → fish A U a.
76 definition fishl ≝ λA:axiom_set.λU:2 \sup A.λV:2 \sup A. ∃a. a ∈ V ∧ fish ? U a.
78 notation "hvbox(a break ⋉ b)" non associative with precedence 45
81 interpretation "fishl" 'fish A U = (fishl _ U A).
82 interpretation "fish" 'fish a U = (fish _ U a).
84 let corec fish_rec (A:axiom_set) (U: 2 \sup A)
85 (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
86 (H2: ∀a:A. a ∈ P → ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ y ∈ P) :
87 ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
93 [ ex_introT (y: A) (Ha: y ∈ C ? a j ∧ y ∈ P) ⇒
95 [ conj (fHa: y ∈ C ? a j) (sHa: y ∈ P) ⇒
96 ex_introT A (λy.y ∈ C ? a j ∧ fish A U y) y
97 (conj ? ? fHa (fish_rec A U P H1 H2 y sHa))
101 theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
107 theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
109 apply (covers_elim ?? (mk_powerset A (λa.a ◃ V)) ??? H); simplify; intros;
120 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
127 theorem cotransitivity:
128 ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
130 apply (fish_rec ?? (mk_powerset A (λa.a ⋉ U)) ??? H); simplify; intros;
133 | cases H2 in j; clear H2; cases H3; clear H3;
137 theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
139 generalize in match H; clear H; generalize in match V; clear V;
140 apply (covers_elim ?? (mk_powerset A (λa.∀p:2 \sup A.a ⋉ p → U ⋉ p)) ??? H1);
141 clear H1; simplify; intros;
145 | cases H2 in j H H1; clear H2 a1; intros;
147 cases (H4 i); clear H4; cases H; clear H;
148 apply (H2 w); clear H2;
152 definition singleton ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A.a=b).
154 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
156 interpretation "singleton" 'singl a = (singleton _ a).
158 definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {b}.
160 interpretation "covered by one" 'leq a b = (leq _ a b).
162 theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
169 theorem leq_trans: ∀A:axiom_set.∀a,b,c:A. a ≤ b → b ≤ c → a ≤ c.
172 apply (transitivity ???? H);
180 definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
182 notation "↑a" with precedence 80 for @{ 'uparrow $a }.
184 interpretation "uparrow" 'uparrow a = (uparrow _ a).
186 definition overlaps ≝ λA:Type.λU,V:2 \sup A.∃a:A. a ∈ U ∧ a ∈ V.
188 notation "hvbox(a break ≬ b)" non associative with precedence 45
189 for @{ 'overlaps $a $b }.
191 interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
193 definition intersects ≝ λA:Type.λU,V:2 \sup A.mk_powerset ? (λa:A. a ∈ U ∧ a ∈ V).
195 notation "hvbox(a break ∩ b)" non associative with precedence 55
196 for @{ 'intersects $a $b }.
198 interpretation "intersects" 'intersects U V = (intersects _ U V).
200 definition downarrow ≝ λA:axiom_set.λU:2 \sup A.mk_powerset ? (λa:A. ↑a ≬ U).
202 notation "↓a" with precedence 80 for @{ 'downarrow $a }.
204 interpretation "downarrow" 'downarrow a = (downarrow _ a).
206 definition fintersects ≝ λA:axiom_set.λU,V:2 \sup A.↓U ∩ ↓V.
208 notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
210 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
212 record convergent_generated_topology : Type ≝
214 convergence: ∀a:AA.∀U,V:2 \sup AA. a ◃ U → a ◃ V → a ◃ U ↓ V