\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Arith.Rat
\import Category
\import Data.Array
\import Data.Bool
\import Data.Or
\import Equiv
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.Lattice
\import Order.Lattice.CompleteLattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Set
\import Topology.Locale
\import Topology.Locale.Points
\import Topology.Locale.PreorderSite
\open SiteLocale
\open Locale
\open CompleteLattice
\open Cover
\open MeetSemilattice
\open JoinSemilattice
\open LinearOrder(dec<_<=)
\type Interval (Q : StrictPoset) => \Sigma (a b : Q) (a < b)
\instance IntervalPoset (Q : BiorderedSet) : Poset (Interval Q)
| <= => <=
| <=-refl => (<=-refl, <=-refl)
| <=-transitive t s => (<=-transitive s.1 t.1, <=-transitive t.2 s.2)
| <=-antisymmetric t s => ext (<=-antisymmetric s.1 t.1, <=-antisymmetric t.2 s.2)
\where {
\type \infix 4 <= {Q : BiorderedSet} (x y : Interval Q) => \Sigma (y.1 Q.<= x.1) (x.2 Q.<= y.2)
}
\instance IntervalBiordered (Q : BiorderedSet) : BiorderedSet (Interval Q)
| Poset => IntervalPoset Q
| < => <
| <-irreflexive p => <-irreflexive p.1
| <-transitive a<b b<c => (b<c.1 <∘ a<b.1, a<b.2 <∘ b<c.2)
| <-transitive-right a<=b b<c => (b<c.1 <∘l a<=b.1, a<=b.2 <∘r b<c.2)
| <-transitive-left a<b b<=c => (b<=c.1 <∘r a<b.1, a<b.2 <∘l b<=c.2)
| <=-less a<b => (<=-less a<b.1, <=-less a<b.2)
\where {
\type \infix 4 < {Q : BiorderedSet} (x y : Interval Q) => \Sigma (y.1 Q.< x.1) (x.2 Q.< y.2)
}
\instance RealPres (Q : LinearOrder.Dec) : PreorderSite (Interval Q)
| Preorder => IntervalPoset Q
| isBasicCover a U =>
(\Sigma (b c : Q) (a1<b : a.1 < b) (b<c : b < c) (c<a2 : c < a.2) (U = \lam x => (x = (a.1, c, a1<b <∘ b<c)) || (x = (b, a.2, b<c <∘ c<a2)))) ||
(U = \lam x => \Sigma (a.1 < x.1) (x.2 < a.2))
| basic-cover-stable {x} {y} x<=y {U} => \case \elim U, \elim __ \with {
| _, byLeft (b,c,y1<b,b<c,c<y2,idp) => \case dec<_<= x.1 b, dec<_<= c x.2 \with {
| inl x1<b, inl c<x2 => inP (_, byLeft (b, c, x1<b, b<c, c<x2, idp), \lam {z} => \case \elim z, \elim __ \with {
| _, byLeft idp => inP (_, byLeft idp, (x<=y.1, <=-refl))
| _, byRight idp => inP (_, byRight idp, (<=-refl, x<=y.2))
}, \lam {t} => \case \elim t, \elim __ \with {
| _, byLeft idp => (<=-refl, <=-less c<x2)
| _, byRight idp => (<=-less x1<b, <=-refl)
})
| _, inr x2<=c => inP (_, byRight idp, \lam {z} s => inP (_, byLeft idp, (x<=y.1 <=∘ <=-less s.1, <=-less s.2 <=∘ x2<=c)), \lam s => (<=-less s.1, <=-less s.2))
| inr b<=x1, _ => inP (_, byRight idp, \lam {z} s => inP (_, byRight idp, (b<=x1 <=∘ <=-less s.1, <=-less s.2 <=∘ x<=y.2)), \lam s => (<=-less s.1, <=-less s.2))
}
| _, byRight idp => inP (_, byRight idp, \lam {x} (a1<x1,x2<a2) => inP (x, (x<=y.1 <∘r a1<x1, x2<a2 <∘l x<=y.2), <=-refl), \lam s => (<=-less s.1, <=-less s.2))
}
\where {
\open Topology.Locale.Real (RealPres)
\lemma subcanonical {Q : DenseLinearOrder.Dec} : (RealPres Q).IsSubcanonical
=> \lam {x} {U} x<=U {y} => \case \elim U, \elim x<=U \with {
| _, byLeft (a,b,x1<a,a<b,b<x2,idp) => \lam h => \case dec<_<= x.1 y.1, dec<_<= y.2 x.2 \with {
| inl x1<y1, _ => absurd $ (h $ byLeft idp).1 x1<y1
| _, inl y2<x2 => absurd $ (h $ byRight idp).2 y2<x2
| inr y1<=x1, inr x2<=y2 => (y1<=x1,x2<=y2)
}
| _, byRight idp => \lam h => \case dec<_<= x.1 y.1, dec<_<= y.2 x.2 \with {
| inl x1<y1, _ => \case isDense (<_meet-univ x1<y1 x.3) \with {
| inP (b,x1<b,b<y1x2) => \case isDense x1<b \with {
| inP (a,x1<a,a<b) => absurd $ (h {a,b,a<b} (x1<a, b<y1x2 <∘l meet-right)).1 $ a<b <∘ b<y1x2 <∘l meet-left
}
}
| _, inl y2<x2 => \case isDense (<_join-univ x.3 y2<x2) \with {
| inP (a,x1y2<a,a<x2) => \case isDense a<x2 \with {
| inP (b,a<b,b<x2) => absurd $ (h {a,b,a<b} (join-left <∘r x1y2<a, b<x2)).2 $ join-right <∘r x1y2<a <∘ a<b
}
}
| inr y1<=x1, inr x2<=y2 => (y1<=x1,x2<=y2)
}
}
\lemma embed-char {Q : DenseLinearOrder.Dec} {a b : Interval Q} : (embed a).1 b <-> b <= a
=> (PreorderSite.subcanonical-cover1 RealPres.subcanonical, cover-inj __ idp)
\lemma toPointwiseCover {Q : DenseLinearOrder.Dec} {a : Interval Q} {U : Set (Interval Q)} (a<=U : Cover a U) {x : Q} (a1<x : a.1 < x) (x<a2 : x < a.2) : ∃ (b : U) (b.1 < x) (x < b.2) \elim a<=U
| cover-inj {b} a<=b Ub => inP (b, Ub, a<=b.1 <∘r a1<x, x<a2 <∘l a<=b.2)
| cover-trans (byLeft (b,c,a1<b,b<c,c<a2,idp)) T<=U => \case dec<_<= x c \with {
| inl x<c => toPointwiseCover (T<=U (byLeft idp)) a1<x x<c
| inr c<=x => toPointwiseCover (T<=U (byRight idp)) (b<c <∘l c<=x) x<a2
}
| cover-trans (byRight idp) T<=U => \case isDense a1<x, isDense x<a2 \with {
| inP (y1,a1<y1,y1<x), inP (y2,x<y2,y2<a2) => toPointwiseCover (T<=U {y1, y2, y1<x <∘ x<y2} (a1<y1, y2<a2)) y1<x x<y2
}
\lemma <<-intervals {Q : DenseLinearOrder.Dec} {x y : Interval Q} (r : x < y) : x PreorderSite.<< y
=> <<-char <=-less (\lam {a} {b} a<b {U} b<=U => \case \elim U, \elim b<=U \with {
| _, byLeft (c,d,b1<c,c<d,d<b2,idp) => \case isDense (<_meet-univ a<b.1 b1<c), isDense (<_join-univ a<b.2 d<b2), isDense c<d \with {
| inP (b1',b1<b1',b1'<a1c), inP (b2',a2d<b2',b2'<b2), inP (c',c<c',c'<d) => \case isDense c'<d \with {
| inP (d',c'<d',d'<d) => inP (
(b1', d', b1'<a1c <∘ meet-right <∘r c<c' <∘ c'<d') :: (c', b2', c'<d <∘ join-right <∘r a2d<b2') :: nil,
cover-left {_} {_} {b1', b2', b1'<a1c <∘ meet-right <∘r c<d <∘ join-right <∘r a2d<b2'} (<=-less b1'<a1c <=∘ meet-left, join-left <=∘ <=-less a2d<b2') $
cover-sub (cover-basic $ byLeft (c', d', b1'<a1c <∘ meet-right <∘r c<c', c'<d', d'<d <∘ join-right <∘r a2d<b2', idp)) \case \elim __ \with {
| byLeft p => inP (0, inv p)
| byRight p => inP (1, inv p)
},
\case \elim __ \with {
| 0 => inP (_, byLeft idp, (b1<b1', d'<d))
| 1 => inP (_, byRight idp, (c<c', b2'<b2))
})
}
}
| _, byRight idp => \case isDense a<b.1, isDense a<b.2 \with {
| inP (b1',b1<b1',b1'<a1), inP (b2',a2<b2',b2'<b2) => inP (a :: nil, cover-refl $ TSetIm-con (later 0), \lam (0) => inP ((b1', b2', b1'<a1 <∘ a.3 <∘ a2<b2'), (b1<b1', b2'<b2), (b1'<a1, a2<b2')))
}
}) r
\lemma locallyCompact {Q : DenseLinearOrder.Dec} : (RealPres Q).IsLocallyCompact
=> \lam x => cover-sub (cover-basic $ byRight idp) \lam s => <<-intervals s
}
\func RealLocale : Locale => SiteLocale (RealPres RatField)
\where {
\lemma locallyCompact : RealLocale.IsLocallyCompact
=> PreorderSite.locallyCompact-locale.1 RealPres.locallyCompact
\lemma <=<-intervals {x y : Interval RatField} (r : x < y) : embed x <=< embed y
=> make<=< $ halves3-cover r.1 r.2 <=∘ join-monotone (join-univ (RealLocale.<=-curry {_} {embed x} $ lowerHalf.lowerHalf_embed<=0 <=-refl) (RealLocale.<=-curry {_} {embed x} $ upperHalf.upperHalf_embed<=0 <=-refl)) <=-refl
\lemma regular : RealLocale.IsRegularLocale
=> regular-site \lam x => later $ cover-trans (byRight idp) \lam r => cover-refl (<=<-intervals r)
\func ratPoint (x : Rat) : CompleteFilter RealLocale
=> site-point (sitePoint x)
\where
\func sitePoint (p : Rat) : SitePoint (RealPres RatField) \cowith
| F a => \Sigma (a.1 < p) (p < a.2)
| sitePoint-mono (x1<p,p<x2) x<=y => (x<=y.1 <∘r x1<p, p<x2 <∘l x<=y.2)
| sitePoint-top => inP ((p - 1, p + 1, linarith), (linarith, linarith))
| sitePoint-meet {x} {y} (x1<p,p<x2) (y1<p,p<y2) =>
\have | x1y1<p => <_join-univ x1<p y1<p
| p<x2y2 => <_meet-univ p<x2 p<y2
\in inP ((x.1 ∨ y.1, x.2 ∧ y.2, x1y1<p <∘ p<x2y2), (x1y1<p, p<x2y2), RealPres.embed-char.2 (join-left, meet-left), RealPres.embed-char.2 (join-right, meet-right))
| sitePoint-cover {x} {U} x<=U (x1<p,p<x2) => \case \elim U, \elim x<=U \with {
| _, byLeft (b,c,x1<b,b<c,c<x2,idp) => \case dec<_<= p c \with {
| inl p<c => inP (_, byLeft idp, (x1<p, p<c))
| inr c<=p => inP (_, byRight idp, (b<c <∘l c<=p, p<x2))
}
| _, byRight idp => \case isDense x1<p, isDense p<x2 \with {
| inP (y1,x1<y1,y1<p), inP (y2,p<y2,y2<x2) => inP ((y1, y2, y1<p <∘ p<y2), (x1<y1, y2<x2), (y1<p, p<y2))
}
}
\lemma hasStronglyDensePoints : HasStronglyDensePoints RealLocale
=> hasStronglyDensePoints-site $ later \lam a => \case isDense a.3 \with {
| inP (x,a1<x,x<a2) => cover-refl $ inP (ratPoint.sitePoint x, (a1<x, x<a2))
}
}
\sfunc lowerHalf (x : Rat) : RealLocale
=> SJoin {_} {Interval RatField} embed \lam s => s.2 <= x
\where {
\lemma lowerHalf-char {x : Rat} {a : Interval RatField} : (lowerHalf x).1 a <-> a.2 <= x
=> rewrite (\peval lowerHalf x) (\lam p => \case dec<_<= x a.2 \with {
| inl x<a2 => absurd \case isDense (<_join-univ a.3 x<a2) \with {
| inP (y,a1x<y,y<a2) => \case RealPres.toPointwiseCover p (join-left <∘r a1x<y) y<a2 \with {
| inP (b, inP (_, inP ((c,c2<=x),idp), b<=c), b1<y, y<b2) => c2<=x $ join-right <∘r a1x<y <∘ y<b2 <∘l (RealPres.embed-char.1 b<=c).2
}
}
| inr a2<=x => a2<=x
}, \lam p => cover-refl $ inP (_, SetIm-con p, cover-refl idp))
\lemma lowerHalf-cover {b x : Rat} {c : Interval RatField} (c1<x : c.1 < x) (b<=c2 : b <= c.2) : lowerHalf b <= lowerHalf x ∨ embed c
=> meet-univ <=-refl (top-univ <=∘ halves-cover c1<x) <=∘ ldistr>= <=∘ join-monotone meet-right (meet-comm =<= halves-inter <=-refl b<=c2)
\lemma lowerHalf_embed<=embed {x : Rat} {c : Interval RatField} (c1<x : c.1 < x) : lowerHalf x ∧ embed c <= embed (c.1, x, c1<x)
=> \lam {y} s => RealPres.embed-char.2 $ later ((RealPres.embed-char.1 s.2).1, lowerHalf.lowerHalf-char.1 s.1)
\lemma lowerHalf_embed<=0 {x : Rat} {c : Interval RatField} (x<=c1 : x <= c.1) : lowerHalf x ∧ embed c <= bottom
=> \lam {y} s => absurd $ x<=c1 $ (RealPres.embed-char.1 s.2).1 <∘r y.3 <∘l lowerHalf.lowerHalf-char.1 s.1
}
\sfunc upperHalf (x : Rat) : RealLocale
=> SJoin {_} {Interval RatField} embed \lam s => x <= s.1
\where {
\lemma upperHalf-char {x : Rat} {a : Interval RatField} : (upperHalf x).1 a <-> x <= a.1
=> rewrite (\peval upperHalf x) (\lam p => \case dec<_<= a.1 x \with {
| inl a1<x => absurd \case isDense (<_meet-univ a.3 a1<x) \with {
| inP (y,a1<y,y<a2x) => \case RealPres.toPointwiseCover p a1<y (y<a2x <∘l meet-left) \with {
| inP (b, inP (_, inP ((c,x<=c1),idp), b<=c), b1<y, y<b2) => x<=c1 $ (RealPres.embed-char.1 b<=c).1 <∘r b1<y <∘ y<a2x <∘l meet-right
}
}
| inr x<=a1 => x<=a1
}, \lam p => cover-refl $ inP (_, SetIm-con p, cover-refl idp))
\lemma upperHalf-cover {a x : Rat} {c : Interval RatField} (c1<=a : c.1 <= a) (x<c2 : x < c.2) : upperHalf a <= embed c ∨ upperHalf x
=> meet-univ <=-refl (top-univ <=∘ halves-cover x<c2) <=∘ ldistr>= <=∘ join-monotone (halves-inter c1<=a <=-refl) meet-right
\lemma upperHalf_embed<=embed {x : Rat} {c : Interval RatField} (x<c2 : x < c.2) : upperHalf x ∧ embed c <= embed (x, c.2, x<c2)
=> \lam {y} s => RealPres.embed-char.2 $ later (upperHalf.upperHalf-char.1 s.1, (RealPres.embed-char.1 s.2).2)
\lemma upperHalf_embed<=0 {x : Rat} {c : Interval RatField} (c2<=x : c.2 <= x) : upperHalf x ∧ embed c <= bottom
=> \lam {y} s => absurd $ c2<=x $ upperHalf.upperHalf-char.1 s.1 <∘r y.3 <∘l (RealPres.embed-char.1 s.2).2
}
\lemma halves-cover {x y : Rat} (x<y : x < y) : top <= lowerHalf y ∨ upperHalf x
=> rewrite (\peval lowerHalf y, \peval upperHalf x) \lam {z} _ => \case dec<_<= z.1 x, dec<_<= y z.2 \with {
| inl z1<x, inl y<z2 => cover-trans (byLeft (x,y,z1<x,x<y,y<z2,idp)) \lam {t} => \case \elim t, \elim __ \with {
| _, byLeft idp => cover-refl $ inP (_, byLeft idp, cover-refl $ inP (_, SetIm-con <=-refl, cover-refl idp))
| _, byRight idp => cover-refl $ inP (_, byRight idp, cover-refl $ inP (_, SetIm-con <=-refl, cover-refl idp))
}
| _, inr z2<=y => cover-refl $ inP (_, byLeft idp, cover-refl $ inP (_, SetIm-con z2<=y, cover-refl idp))
| inr x<=z1, _ => cover-refl $ inP (_, byRight idp, cover-refl $ inP (_, SetIm-con x<=z1, cover-refl idp))
}
\lemma halves3-cover {x y : Rat} {a : Interval RatField} (a1<x : a.1 < x) (y<a2 : y < a.2) : top <= lowerHalf x ∨ upperHalf y ∨ embed a
=> halves-cover a1<x <=∘ join-monotone <=-refl (upperHalf.upperHalf-cover <=-refl y<a2 <=∘ =_<= join-comm) <=∘ =_<= (inv join-assoc)
\lemma halves-inter {x y : Rat} {c : Interval RatField} (c1<=x : c.1 <= x) (y<=c2 : y <= c.2) : upperHalf x ∧ lowerHalf y <= embed c
=> rewrite (\peval lowerHalf y, \peval upperHalf x) \lam {z} (z<=x,z<=y) => cover-refine (cover-inter z<=x z<=y)
\lam {t} (inP (a, inP (_, inP ((a',x<=a'1),idp), a<=a'), b, inP (_, inP ((b',b'2<=y),idp), b<=b'), t<=a, t<=b)) =>
inP (_, idp, (c1<=x <=∘ x<=a'1 <=∘ (RealPres.embed-char.1 a<=a').1 <=∘ t<=a.1, t<=b.2 <=∘ (RealPres.embed-char.1 b<=b').2 <=∘ b'2<=y <=∘ y<=c2))
\func closedInterval (x y : Rat) => (nucleus x y).locale
\where {
\func nucleus (x y : Rat) : Nucleus
=> closed (lowerHalf x ∨ upperHalf y)
\lemma compact (x y : Rat) : (closedInterval x y).IsCompact
=> \case withoutLowerBound x, withoutUpperBound (x ∨ y) \with {
| inP (a,a<x), inP (b,xy<b) => \case isDense a<x, isDense xy<b \with {
| inP (a',a<a',a'<x), inP (b',xy<b',b'<b) =>
\have a'<b' => a'<x <∘ join-left <∘r xy<b'
\in closed-compact (closed-isClosed _) (<<-left (PreorderSite.<<-site.1 (RealPres.<<-intervals {_} {a',b',a'<b'} {a, b, a<a' <∘ a'<b' <∘ b'<b} (a<a',b'<b))) top-univ) $ closed<=open $ halves3-cover a'<x (join-right <∘r xy<b')
}
}
}
\func rat_real : LocaleHom (discreteLocale Rat) RealLocale
=> LocaleSite.adjointMap $ later \new PreorderSiteHom {
| func p x => \Sigma (p.1 < x) (x < p.2)
| func-<= x<=y {z} (x1<z,z<x2) => (x<=y.1 <∘r x1<z, z<x2 <∘l x<=y.2)
| func-basicCover {x} {U} => \case \elim U, \elim __ \with {
| _, byLeft (b,c,x1<b,b<c,c<x2,idp) => \lam {z} (x1<z,z<x2) => \case dec<_<= z c \with {
| inl z<c => inP (_, SetIm-con (byLeft idp), (x1<z, z<c))
| inr c<=z => inP (_, SetIm-con (byRight idp), (b<c <∘l c<=z, z<x2))
}
| _, byRight idp => \lam {z} (x1<z,z<x2) => \case isDense x1<z, isDense z<x2 \with {
| inP (y1,x1<y1,y1<z), inP (y2,z<y2,y2<x2) => inP (_, SetIm-cone (later (y1, y2, y1<z <∘ z<y2)) (x1<y1, y2<x2), (y1<z, z<y2))
}
}
| func-flat-top {U} => cover-basic \lam {x} Ux => inP (_, TSetIm-con $ later (x - 1, x + 1, linarith), (linarith, linarith))
| func-flat-meet {x} {y} {U} U<=x U<=y => cover-basic \lam {z} Uz =>
\have | (x1<z,z<x2) => U<=x Uz
| (y1<z,z<y2) => U<=y Uz
| x1y1<z => <_join-univ x1<z y1<z
| z<x2y2 => <_meet-univ z<x2 z<y2
\in inP (_, TSetIm-con $ later ((x.1 ∨ y.1, x.2 ∧ y.2, x1y1<z <∘ z<x2y2), ((join-left, meet-left), (join-right, meet-right))), (x1y1<z, z<x2y2))
}