(* *)
(**************************************************************************)
-include "logic/connectives.ma".
include "logic/equality.ma".
+include "logic/cprop_connectives.ma".
-record powerset (A: Type) : Type ≝ { char: A → Prop }.
+record powerset (A : Type) : Type ≝ { char : A → CProp }.
-notation "hvbox(2 \sup A)" non associative with precedence 45
-for @{ 'powerset $A }.
+interpretation "char" 'subset p = (mk_powerset ? p).
-interpretation "powerset" 'powerset A = (powerset A).
+interpretation "pwset" 'powerset a = (powerset a).
-definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
+interpretation "in" 'mem a X = (char ? X a).
-notation "hvbox(a break ∈ b)" non associative with precedence 45
-for @{ 'mem $a $b }.
+definition subseteq ≝ λA.λu,v:\Omega \sup A.∀x.x ∈ u → x ∈ v.
-interpretation "mem" 'mem a S = (mem _ S a).
+interpretation "subseteq" 'subseteq u v = (subseteq ? u v).
-record axiom_set : Type ≝
- { A:> Type;
- i: A → Type;
- C: ∀a:A. i a → 2 \sup A
- }.
+definition overlaps ≝ λA.λU,V : Ω \sup A. exT2 ? (λx.x ∈ U) (λx.x ∈ V).
+
+interpretation "overlaps" 'overlaps u v = (overlaps ? u v).
+
+definition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
+
+interpretation "intersect" 'intersects u v = (intersect ? u v).
+
+record axiom_set : Type ≝ {
+ A:> Type;
+ i: A → Type;
+ C: ∀a:A. i a → Ω \sup A
+}.
-inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
+inductive for_all (A: axiom_set) (U,V: Ω \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: \Omega \sup A) : A → CProp ≝
refl: ∀a:A. a ∈ U → covers A U a
- | infinity: ∀a:A. ∀j: i ? a. coversl A U (C ? a j) → covers A U a
-with coversl : (2 \sup A) → CProp ≝
- iter: ∀V:2 \sup A.(∀a:A.a ∈ V → covers A U a) → coversl A U V.
+ | 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 "covers" 'covers a U = (covers _ U a).
-interpretation "coversl" 'covers A U = (coversl _ U A).
+interpretation "coversl" 'covers A U = (for_all ? U A (covers ? U)).
+interpretation "covers" 'covers a U = (covers ? U a).
-axiom 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.
- ∀a:A.∀p:a ◃ U.P 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 → (∀b. b ∈ C ? a j → b ∈ P) → a ∈ P.
- let rec aux (a:A) (p:a ◃ U) : a ∈ P ≝
- match p return λaa.λ_.aa ∈ P with
+ λA:axiom_set.λU: \Omega \sup A.λP:\Omega \sup A.
+ λH1: U ⊆ 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 (auxl (C ? a j) q)
- ]
- and auxl (V: 2 \sup A) (q: V ◃ U) : ∀b. b ∈ V → b ∈ P ≝
- match q return λVV.λ_.∀b. b ∈ VV → b ∈ P with
- [ iter VV f ⇒ λb.λr. aux b (f b r) ]
+ | 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.
-*)
-coinductive fish (A:axiom_set) (U: 2 \sup A) : A → Prop ≝
- mk_fish: ∀a:A. (a ∈ U ∧ ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ fish A U y) → fish A U a.
+inductive ex_such (A : axiom_set) (U,V : \Omega \sup A) (fish: A → CProp) : CProp ≝
+ found : ∀a. a ∈ V → fish a → ex_such A U V fish.
+
+coinductive fish (A:axiom_set) (U: \Omega \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 }.
+for @{ 'fish $a $b }. (* a \ltimes b *)
-interpretation "fish" 'fish a U = (fish _ 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) :
+let corec fish_rec (A:axiom_set) (U: \Omega \sup A)
+ (P: Ω \sup A) (H1: P ⊆ U)
+ (H2: ∀a:A. a ∈ P → ∀j: i ? a. C ? a j ≬ 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_intro (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
- (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;
theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
intros;
- elim H using covers_elim;
- [ cases H1 in H2;
- intro;
- apply H2;
- assumption
+ apply (covers_elim ?? {a | a ◃ V} ??? H); simplify; intros;
+ [ cases H1 in H2; apply H2;
| apply infinity;
[ assumption
| constructor 1;
assumption]]
-qed.
\ No newline at end of file
+qed.
+
+theorem covers_elim2:
+ ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
+ (∀a:A. a ∈ U → P a) →
+ (∀a:A.∀V:Ω \sup A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
+ ∀a:A. a ◃ U → P a.
+ intros;
+ change with (a ∈ {a | P a});
+ apply (covers_elim ?????? H2);
+ [ intros 2; simplify; apply H; assumption
+ | intros;
+ simplify in H4 ⊢ %;
+ apply H1;
+ [ apply (C ? a1 j);
+ | autobatch;
+ | assumption;
+ | 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 x] assumption
+ | cases H2 in j H H1; clear H2 a1; intros;
+ cases (H1 i); clear H1; apply (H3 a1); assumption]
+qed.
+
+definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
+
+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).
+
+interpretation "uparrow" 'uparrow a = (uparrow ? a).
+
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
+
+interpretation "downarrow" 'downarrow a = (downarrow ? a).
+
+definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
+
+interpretation "fintersects" 'fintersects U V = (fintersects ? U V).
+
+record convergent_generated_topology : Type ≝
+ { AA:> axiom_set;
+ convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
+ }.
projects / helm.git / blobdiff