Definition: lattice-structure
LatticeStructure ==
"Point":Type
"meet":self."Point" ⟶ self."Point" ⟶ self."Point"
"join":self."Point" ⟶ self."Point" ⟶ self."Point"
Lemma: lattice-structure_wf
LatticeStructure ∈ 𝕌'
Definition: lattice-point
Point(l) == l."Point"
Lemma: lattice-point_wf
∀[l:LatticeStructure]. (Point(l) ∈ Type)
Definition: lattice-meet
a ∧ b == l."meet" a b
Lemma: lattice-meet_wf
∀[l:LatticeStructure]. ∀[a,b:Point(l)]. (a ∧ b ∈ Point(l))
Definition: lattice-join
a ∨ b == l."join" a b
Lemma: lattice-join_wf
∀[l:LatticeStructure]. ∀[a,b:Point(l)]. (a ∨ b ∈ Point(l))
Definition: lattice-axioms
lattice-axioms(l) ==
(∀[a,b:Point(l)]. (a ∧ b = b ∧ a ∈ Point(l)))
∧ (∀[a,b:Point(l)]. (a ∨ b = b ∨ a ∈ Point(l)))
∧ (∀[a,b,c:Point(l)]. (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l)))
∧ (∀[a,b,c:Point(l)]. (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l)))
∧ (∀[a,b:Point(l)]. (a ∨ a ∧ b = a ∈ Point(l)))
∧ (∀[a,b:Point(l)]. (a ∧ a ∨ b = a ∈ Point(l)))
Lemma: lattice-axioms_wf
∀[l:LatticeStructure]. (lattice-axioms(l) ∈ ℙ)
Lemma: lattice-axioms-from-order
∀[l:LatticeStructure]
lattice-axioms(l)
supposing ∃R:Point(l) ⟶ Point(l) ⟶ ℙ
(((∀[a,b:Point(l)]. least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b))
∧ (∀[a,b:Point(l)]. greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)))
∧ Order(Point(l);x,y.R[x;y]))
Definition: lattice
Lattice == {l:LatticeStructure| lattice-axioms(l)}
Lemma: lattice_wf
Lattice ∈ 𝕌'
Lemma: lattice_properties
∀[l:Lattice]
((∀[a,b:Point(l)]. (a ∧ b = b ∧ a ∈ Point(l)))
∧ (∀[a,b:Point(l)]. (a ∨ b = b ∨ a ∈ Point(l)))
∧ (∀[a,b,c:Point(l)]. (a ∧ b ∧ c = a ∧ b ∧ c ∈ Point(l)))
∧ (∀[a,b,c:Point(l)]. (a ∨ b ∨ c = a ∨ b ∨ c ∈ Point(l)))
∧ (∀[a,b:Point(l)]. (a ∨ a ∧ b = a ∈ Point(l)))
∧ (∀[a,b:Point(l)]. (a ∧ a ∨ b = a ∈ Point(l))))
Definition: lattice-le
a ≤ b == a = a ∧ b ∈ Point(l)
Lemma: lattice-le_wf
∀[l:LatticeStructure]. ∀[a,b:Point(l)]. (a ≤ b ∈ Type)
Definition: lattice-hom
Hom(l1;l2) ==
{f:Point(l1) ⟶ Point(l2)|
∀[a,b:Point(l1)]. ((f a ∧ f b = (f a ∧ b) ∈ Point(l2)) ∧ (f a ∨ f b = (f a ∨ b) ∈ Point(l2)))}
Lemma: lattice-hom_wf
∀[l1,l2:LatticeStructure]. (Hom(l1;l2) ∈ Type)
Lemma: id-is-lattice-hom
∀[l:LatticeStructure]. (λx.x ∈ Hom(l;l))
Lemma: compose-lattice-hom
∀[l1,l2,l3:Lattice]. ∀[f:Hom(l1;l2)]. ∀[g:Hom(l2;l3)]. (g o f ∈ Hom(l1;l3))
Definition: mk-lattice
mk-lattice(T;m;j) == λx.x["Point" := T]["meet" := m]["join" := j]
Lemma: mk-lattice_wf
∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T].
mk-lattice(T;m;j) ∈ Lattice
supposing (∀[a,b:T]. (m[a;b] = m[b;a] ∈ T))
∧ (∀[a,b:T]. (j[a;b] = j[b;a] ∈ T))
∧ (∀[a,b,c:T]. (m[a;m[b;c]] = m[m[a;b];c] ∈ T))
∧ (∀[a,b,c:T]. (j[a;j[b;c]] = j[j[a;b];c] ∈ T))
∧ (∀[a,b:T]. (j[a;m[a;b]] = a ∈ T))
∧ (∀[a,b:T]. (m[a;j[a;b]] = a ∈ T))
Definition: divisibility-lattice
divisibility-lattice() == mk-lattice(ℕ;λa,b. gcd(a;b);λa,b. lcm(a;b))
Lemma: divisibility-lattice_wf
divisibility-lattice() ∈ Lattice
Definition: bounded-lattice-structure
BoundedLatticeStructure ==
"Point":Type
"meet":self."Point" ⟶ self."Point" ⟶ self."Point"
"join":self."Point" ⟶ self."Point" ⟶ self."Point"
"1":self."Point"
"0":self."Point"
Lemma: bounded-lattice-structure_wf
BoundedLatticeStructure ∈ 𝕌'
Lemma: bounded-lattice-structure-subtype
BoundedLatticeStructure ⊆r LatticeStructure
Definition: mk-bounded-lattice
mk-bounded-lattice(T;m;j;z;o) == λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o]
Definition: lattice-1
1 == l."1"
Lemma: lattice-1_wf
∀[l:BoundedLatticeStructure]. (1 ∈ Point(l))
Definition: lattice-0
0 == l."0"
Lemma: lattice-0_wf
∀[l:BoundedLatticeStructure]. (0 ∈ Point(l))
Definition: bounded-lattice-axioms
bounded-lattice-axioms(l) == (∀[a:Point(l)]. (a ∨ 0 = a ∈ Point(l))) ∧ (∀[a:Point(l)]. (a ∧ 1 = a ∈ Point(l)))
Lemma: bounded-lattice-axioms_wf
∀[l:BoundedLatticeStructure]. (bounded-lattice-axioms(l) ∈ ℙ)
Definition: bdd-lattice
BoundedLattice == {l:BoundedLatticeStructure| lattice-axioms(l) ∧ bounded-lattice-axioms(l)}
Lemma: bdd-lattice_wf
BoundedLattice ∈ 𝕌'
Lemma: bdd-lattice-subtype-lattice
BoundedLattice ⊆r Lattice
Lemma: mk-bounded-lattice_wf
∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T].
mk-bounded-lattice(T;m;j;z;o) ∈ BoundedLattice
supposing (∀[a,b:T]. (m[a;b] = m[b;a] ∈ T))
∧ (∀[a,b:T]. (j[a;b] = j[b;a] ∈ T))
∧ (∀[a,b,c:T]. (m[a;m[b;c]] = m[m[a;b];c] ∈ T))
∧ (∀[a,b,c:T]. (j[a;j[b;c]] = j[j[a;b];c] ∈ T))
∧ (∀[a,b:T]. (j[a;m[a;b]] = a ∈ T))
∧ (∀[a,b:T]. (m[a;j[a;b]] = a ∈ T))
∧ (∀[a:T]. (m[a;o] = a ∈ T))
∧ (∀[a:T]. (j[a;z] = a ∈ T))
Lemma: ext-eq-equiv
EquivRel(Type;A,B.A ≡ B)
Definition: e-type
EType == A,B:Type//A ≡ B
Lemma: e-type_wf
EType ∈ 𝕌'
Definition: p-type
PType == A,B:Type//(A
⇐⇒ B)
Lemma: p-type_wf
PType ∈ 𝕌'
Definition: e-isect
e-isect(A;B) == A ⋂ B
Lemma: e-isect_wf
∀[A,B:EType]. (e-isect(A;B) ∈ EType)
Definition: p-and
p-and(A;B) == A ∧ B
Lemma: p-and_wf
∀[A,B:PType]. (p-and(A;B) ∈ PType)
Definition: e-union
e-union(A;B) == A ⋃ B
Lemma: e-union_wf
∀[A,B:EType]. (e-union(A;B) ∈ EType)
Definition: p-or
p-or(A;B) == A ∨ B
Lemma: p-or_wf
∀[A,B:PType]. (p-or(A;B) ∈ PType)
Definition: type-lattice
type-lattice{i:l}() == mk-bounded-lattice(EType;λ2A B.e-isect(A;B);λ2A B.e-union(A;B);Void;Top)
Lemma: type-lattice_wf
type-lattice{i:l}() ∈ bdd-lattice{i':l}
Definition: iff-type-lattice
iff-type-lattice{i:l}() == mk-bounded-lattice(PType;λ2A B.p-and(A;B);λ2A B.p-or(A;B);False;True)
Definition: bounded-lattice-hom
Hom(l1;l2) == {f:Hom(l1;l2)| ((f 0) = 0 ∈ Point(l2)) ∧ ((f 1) = 1 ∈ Point(l2))}
Lemma: bounded-lattice-hom_wf
∀[l1,l2:BoundedLatticeStructure]. (Hom(l1;l2) ∈ Type)
Lemma: bounded-lattice-hom-equal
∀[l1,l2:BoundedLatticeStructure]. ∀[f,g:Hom(l1;l2)].
f = g ∈ Hom(l1;l2) supposing ∀x:Point(l1). ((f x) = (g x) ∈ Point(l2))
Lemma: compose-bounded-lattice-hom
∀[l1,l2,l3:BoundedLattice]. ∀[f:Hom(l1;l2)]. ∀[g:Hom(l2;l3)]. (g o f ∈ Hom(l1;l3))
Lemma: id-is-bounded-lattice-hom
∀[l:BoundedLattice]. (λx.x ∈ Hom(l;l))
Definition: distributive-lattice
DistributiveLattice ==
{l:LatticeStructure| lattice-axioms(l) ∧ (∀[a,b,c:Point(l)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l)))}
Lemma: distributive-lattice_wf
DistributiveLattice ∈ 𝕌'
Definition: mk-distributive-lattice
mk-distributive-lattice(T; m; j) == mk-lattice(T;m;j)
Lemma: mk-distributive-lattice_wf
∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T].
mk-distributive-lattice(T; m; j) ∈ DistributiveLattice
supposing (∀[a,b:T]. (m[a;b] = m[b;a] ∈ T))
∧ (∀[a,b:T]. (j[a;b] = j[b;a] ∈ T))
∧ (∀[a,b,c:T]. (m[a;m[b;c]] = m[m[a;b];c] ∈ T))
∧ (∀[a,b,c:T]. (j[a;j[b;c]] = j[j[a;b];c] ∈ T))
∧ (∀[a,b:T]. (j[a;m[a;b]] = a ∈ T))
∧ (∀[a,b:T]. (m[a;j[a;b]] = a ∈ T))
∧ (∀[a,b,c:T]. (m[a;j[b;c]] = j[m[a;b];m[a;c]] ∈ T))
Definition: bdd-distributive-lattice
BoundedDistributiveLattice ==
{l:BoundedLatticeStructure|
(lattice-axioms(l) ∧ bounded-lattice-axioms(l)) ∧ (∀[a,b,c:Point(l)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(l)))}
Lemma: bdd-distributive-lattice_wf
BoundedDistributiveLattice ∈ 𝕌'
Lemma: bdd-distributive-lattice-subtype-lattice
BoundedDistributiveLattice ⊆r Lattice
Lemma: bdd-distributive-lattice-subtype-bdd-lattice
BoundedDistributiveLattice ⊆r BoundedLattice
Lemma: bdd-distributive-lattice-subtype-distributive-lattice
BoundedDistributiveLattice ⊆r DistributiveLattice
Definition: mk-bounded-distributive-lattice
{points=T;meet=m;join=j;0=z;1=o} == mk-bounded-lattice(T;m;j;z;o)
Lemma: mk-bounded-distributive-lattice_wf
∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T].
{points=T;
meet=m;
join=j;
0=z;
1=o} ∈ BoundedDistributiveLattice
supposing (∀[a,b:T]. (m[a;b] = m[b;a] ∈ T))
∧ (∀[a,b:T]. (j[a;b] = j[b;a] ∈ T))
∧ (∀[a,b,c:T]. (m[a;m[b;c]] = m[m[a;b];c] ∈ T))
∧ (∀[a,b,c:T]. (j[a;j[b;c]] = j[j[a;b];c] ∈ T))
∧ (∀[a,b:T]. (j[a;m[a;b]] = a ∈ T))
∧ (∀[a,b:T]. (m[a;j[a;b]] = a ∈ T))
∧ (∀[a:T]. (m[a;o] = a ∈ T))
∧ (∀[a:T]. (j[a;z] = a ∈ T))
∧ (∀[a,b,c:T]. (m[a;j[b;c]] = j[m[a;b];m[a;c]] ∈ T))
Lemma: mk-bounded-distributive-lattice-from-order
∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T]. ∀[R:T ⟶ T ⟶ ℙ].
{points=T;
meet=m;
join=j;
0=z;
1=o} ∈ BoundedDistributiveLattice
supposing Order(T;x,y.R[x;y])
∧ (∀[a,b:T]. least-upper-bound(T;x,y.R[x;y];a;b;j[a;b]))
∧ (∀[a,b:T]. greatest-lower-bound(T;x,y.R[x;y];a;b;m[a;b]))
∧ (∀[a:T]. R[a;o])
∧ (∀[a:T]. R[z;a])
∧ (∀[a,b,c:T]. (m[a;j[b;c]] = j[m[a;b];m[a;c]] ∈ T))
Lemma: lattice-join-idempotent
∀[l:Lattice]. ∀[u:Point(l)]. (u ∨ u = u ∈ Point(l))
Lemma: lattice-meet-idempotent
∀[l:Lattice]. ∀[u:Point(l)]. (u ∧ u = u ∈ Point(l))
Lemma: lattice-le_weakening
∀[l:Lattice]. ∀[a,b:Point(l)]. a ≤ b supposing a = b ∈ Point(l)
Lemma: lattice-le_transitivity
∀[l:Lattice]. ∀[a,b,c:Point(l)]. (a ≤ c) supposing (a ≤ b and b ≤ c)
Lemma: lattice-le-order
∀l:Lattice. Order(Point(l);x,y.x ≤ y)
Lemma: lattice-le-iff
∀[l:Lattice]. ∀[a,b:Point(l)]. uiff(a ≤ b;b = a ∨ b ∈ Point(l))
Lemma: lattice-join-is-lub
∀l:Lattice. ∀a,b:Point(l). least-upper-bound(Point(l);x,y.x ≤ y;a;b;a ∨ b)
Lemma: lattice-meet-is-glb
∀l:Lattice. ∀a,b:Point(l). greatest-lower-bound(Point(l);x,y.x ≤ y;a;b;a ∧ b)
Lemma: lattice-le-meet
∀l:Lattice. ∀a,b,c:Point(l). (c ≤ a ∧ b
⇐⇒ c ≤ a ∧ c ≤ b)
Lemma: lattice-meet-le
∀l:Lattice. ∀a,b:Point(l). (a ∧ b ≤ a ∧ a ∧ b ≤ b)
Lemma: lattice-join-le
∀l:Lattice. ∀a,b,c:Point(l). (a ∨ b ≤ c
⇐⇒ a ≤ c ∧ b ≤ c)
Lemma: lattice-axioms-iff-order
∀l:LatticeStructure
(∃R:Point(l) ⟶ Point(l) ⟶ ℙ
(((∀[a,b:Point(l)]. least-upper-bound(Point(l);x,y.R[x;y];a;b;a ∨ b))
∧ (∀[a,b:Point(l)]. greatest-lower-bound(Point(l);x,y.R[x;y];a;b;a ∧ b)))
∧ Order(Point(l);x,y.R[x;y]))
⇐⇒ lattice-axioms(l))
Lemma: distributive-lattice-dual-distrib
∀[L:DistributiveLattice]. ∀[a,b,c:Point(L)]. (a ∨ b ∧ c = a ∨ b ∧ a ∨ c ∈ Point(L))
Lemma: distributive-lattice-distrib
∀[L:DistributiveLattice]. ∀[a,b,c:Point(L)].
((a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(L)) ∧ (b ∨ c ∧ a = b ∧ a ∨ c ∧ a ∈ Point(L)))
Lemma: distributive-lattice-dual-distrib2
∀[L:DistributiveLattice]. ∀[a,b,c:Point(L)]. (b ∧ c ∨ a = b ∨ a ∧ c ∨ a ∈ Point(L))
Lemma: lattice-0-le
∀[l:BoundedLattice]. ∀[x:Point(l)]. 0 ≤ x
Lemma: lattice-meet-0
∀[l:BoundedLattice]. ∀[x:Point(l)]. (0 ∧ x = 0 ∈ Point(l))
Lemma: lattice-0-meet
∀[l:BoundedLattice]. ∀[x:Point(l)]. (x ∧ 0 = 0 ∈ Point(l))
Lemma: lattice-join-0
∀[l:BoundedLattice]. ∀[x:Point(l)]. ((0 ∨ x = x ∈ Point(l)) ∧ (x ∨ 0 = x ∈ Point(l)))
Lemma: lattice-meet-1
∀[l:BoundedLattice]. ∀[x:Point(l)]. (x ∧ 1 = x ∈ Point(l))
Lemma: lattice-1-meet
∀[l:BoundedLattice]. ∀[x:Point(l)]. (1 ∧ x = x ∈ Point(l))
Lemma: le-lattice-1
∀[l:BoundedLattice]. ∀[x:Point(l)]. x ≤ 1
Lemma: lattice-join-1
∀[l:BoundedLattice]. ∀[x:Point(l)]. (1 ∨ x = 1 ∈ Point(l))
Lemma: lattice-1-join
∀[l:BoundedLattice]. ∀[x:Point(l)]. (x ∨ 1 = 1 ∈ Point(l))
Lemma: lattice-meet-eq-1
∀[l:BoundedLattice]. ∀[x,y:Point(l)]. uiff(x ∧ y = 1 ∈ Point(l);(x = 1 ∈ Point(l)) ∧ (y = 1 ∈ Point(l)))
Lemma: lattice-1-le-iff
∀[l:BoundedLattice]. ∀[b:Point(l)]. uiff(1 ≤ b;b = 1 ∈ Point(l))
Lemma: lattice-0-equal-lattice-1-implies
∀L:BoundedLattice. ((1 = 0 ∈ Point(L))
⇒ (∀x:Point(L). (0 = x ∈ Point(L))))
Lemma: order-preserving-map-lattice-lemma
∀[l1,l2:Lattice]. ∀[f:Point(l1) ⟶ Point(l2)].
(∀a,b:Point(l1). f a ∧ b ≤ f a ∧ f b) ∧ (∀a,b:Point(l1). f a ∨ f b ≤ f a ∨ b)
supposing ∀x,y:Point(l1). (x ≤ y
⇒ f x ≤ f y)
Lemma: order-preserving-map-is-lattice-hom
∀[l1,l2:Lattice]. ∀[f:Point(l1) ⟶ Point(l2)].
f ∈ Hom(l1;l2)
supposing (∀x,y:Point(l1). (x ≤ y
⇒ f x ≤ f y))
∧ (∀a,b:Point(l1). f a ∧ f b ≤ f a ∧ b)
∧ (∀a,b:Point(l1). f a ∨ b ≤ f a ∨ f b)
Lemma: order-preserving-map-is-bounded-lattice-hom
∀[l1,l2:BoundedLattice]. ∀[f:Point(l1) ⟶ Point(l2)].
f ∈ Hom(l1;l2)
supposing ((∀x,y:Point(l1). (x ≤ y
⇒ f x ≤ f y))
∧ (∀a,b:Point(l1). f a ∧ f b ≤ f a ∧ b)
∧ (∀a,b:Point(l1). f a ∨ b ≤ f a ∨ f b))
∧ ((f 0) = 0 ∈ Point(l2))
∧ ((f 1) = 1 ∈ Point(l2))
Comment: free distributive lattices using quotient doc
In order to construct a free distributive lattice on any type X of generators
(without assuming decidable equality or finiteness) we can use a
quotient type.⋅
Definition: dlattice-order
as
⇒ bs == (∀b∈bs.(∃a∈as. a ⊆ b))
Lemma: dlattice-order_wf
∀[X:Type]. ∀[as,bs:X List List]. (as
⇒ bs ∈ ℙ)
Lemma: dlattice-order-iff
∀[X:Type]. ∀as,bs:X List List. (as
⇒ bs
⇐⇒ ∀x:X List. ((x ∈ bs)
⇒ (∃y:X List. ((y ∈ as) ∧ l_subset(X;y;x)))))
Lemma: dlattice-order_transitivity
∀[X:Type]. ∀as,bs,cs:X List List. (as
⇒ bs
⇒ bs
⇒ cs
⇒ as
⇒ cs)
Lemma: dlattice-order_weakening
∀[X:Type]. ∀as,bs:X List List. ((as = bs ∈ (X List List))
⇒ as
⇒ bs)
Lemma: dlattice-order-append
∀X:Type. ∀a1,b1,a2,b2:X List List. (a1
⇒ b1
⇒ a2
⇒ b2
⇒ a1 @ a2
⇒ b1 @ b2)
Definition: dlattice-eq
dlattice-eq(X;as;bs) == as
⇒ bs ∧ bs
⇒ as
Lemma: dlattice-eq_wf
∀[X:Type]. ∀[as,bs:X List List]. (dlattice-eq(X;as;bs) ∈ ℙ)
Lemma: dlattice-eq-equiv
∀[X:Type]. EquivRel(X List List;as,bs.dlattice-eq(X;as;bs))
Definition: free-dl-type
free-dl-type(X) == as,bs:X List List//dlattice-eq(X;as;bs)
Lemma: free-dl-type_wf
∀[X:Type]. (free-dl-type(X) ∈ Type)
Definition: free-dl-join
free-dl-join(as;bs) == as @ bs
Lemma: free-dl-join_wf
∀[X:Type]. ∀[as,bs:free-dl-type(X)]. (free-dl-join(as;bs) ∈ free-dl-type(X))
Definition: free-dl-meet
free-dl-meet(as;bs) ==
accumulate (with value cs and list item a):
cs @ map(λb.(a @ b);bs)
over list:
as
with starting value:
[])
Lemma: free-dl-meet_wf_list
∀[X:Type]. ∀[as,bs:X List List]. (free-dl-meet(as;bs) ∈ X List List)
Lemma: member-free-dl-meet
∀[X:Type]
∀as,bs:X List List. ∀x:X List.
((x ∈ free-dl-meet(as;bs))
⇐⇒ ∃u,v:X List. ((u ∈ as) ∧ (v ∈ bs) ∧ (x = (u @ v) ∈ (X List))))
Lemma: dlattice-order-free-dl-meet
∀X:Type. ∀a1,b1,as,b2:X List List. (a1
⇒ b1
⇒ as
⇒ b2
⇒ free-dl-meet(a1;as)
⇒ free-dl-meet(b1;b2))
Lemma: free-dl-meet_wf
∀[X:Type]. ∀[as,bs:free-dl-type(X)]. (free-dl-meet(as;bs) ∈ free-dl-type(X))
Definition: free-dl
free-dl(X) == {points=free-dl-type(X);meet=λ2x y.free-dl-meet(x;y);join=λ2x y.free-dl-join(x;y);0=[];1=[[]]}
Lemma: free-dl_wf
∀[X:Type]. (free-dl(X) ∈ BoundedDistributiveLattice)
Definition: free-dl-generator
free-dl-generator(x) == [[x]]
Lemma: free-dl-generator_wf
∀[X:Type]. ∀[x:X]. (free-dl-generator(x) ∈ free-dl-type(X))
Lemma: free-dl-generators
∀[X:Type]
∀L:BoundedDistributiveLattice
∀[f,g:Hom(free-dl(X);L)].
f = g ∈ Hom(free-dl(X);L) supposing ∀x:X. ((f free-dl-generator(x)) = (g free-dl-generator(x)) ∈ Point(L))
Definition: fdl-hom
fdl-hom(L;f) ==
λz.accumulate (with value a and list item xs):
a ∨ accumulate (with value b and list item x):
b ∧ f x
over list:
xs
with starting value:
1)
over list:
z
with starting value:
0)
Lemma: fdl-hom_wf1
∀[X:Type]. ∀[L:BoundedDistributiveLattice]. ∀[f:X ⟶ Point(L)]. (fdl-hom(L;f) ∈ (X List List) ⟶ Point(L))
Lemma: fdl-hom_wf
∀[X:Type]. ∀[L:BoundedDistributiveLattice]. ∀[f:X ⟶ Point(L)]. (fdl-hom(L;f) ∈ Hom(free-dl(X);L))
Lemma: fdl-hom-agrees
∀[X:Type]. ∀[L:BoundedDistributiveLattice]. ∀[f:X ⟶ Point(L)].
∀x:X. ((fdl-hom(L;f) free-dl-generator(x)) = (f x) ∈ Point(L))
Definition: fdl-is-1
fdl-is-1(x) == (∃a∈x.isaxiom(a))_b
Lemma: fdl-is-1_wf
∀[X:Type]. ∀[x:Point(free-dl(X))]. (fdl-is-1(x) ∈ 𝔹)
Lemma: fdl-eq-1
∀[X:Type]. ∀x:Point(free-dl(X)). (x = 1 ∈ Point(free-dl(X))
⇐⇒ ↑fdl-is-1(x))
Lemma: fdl-0-not-1
∀[X:Type]. (¬(0 = 1 ∈ Point(free-dl(X))))
Lemma: fdl-1-join-irreducible
∀[X:Type]
∀x,y:Point(free-dl(X)). (x ∨ y = 1 ∈ Point(free-dl(X))
⇐⇒ (x = 1 ∈ Point(free-dl(X))) ∨ (y = 1 ∈ Point(free-dl(X))))
Definition: lattice-less
a < b == a ≤ b ∧ (¬(a = b ∈ Point(l)))
Lemma: lattice-less_wf
∀[l:LatticeStructure]. ∀[a,b:Point(l)]. (a < b ∈ ℙ)
Comment: distributive lattice with decidable equality doc
If the "points" of the lattice have decidable equality, then
we can implement some additional operations.
We use these for one construction of free distributive lattices.⋅
Definition: lattice-ble
lattice-ble(l;eq;a;b) == eq a a ∧ b
Lemma: lattice-ble_wf
∀[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)]. (lattice-ble(l;eq;a;b) ∈ 𝔹)
Lemma: assert-lattice-ble
∀[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)]. uiff(↑lattice-ble(l;eq;a;b);a ≤ b)
Definition: lattice-bless
lattice-bless(l;eq;a;b) == lattice-ble(l;eq;a;b) ∧b (¬b(eq a b))
Lemma: lattice-bless_wf
∀[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)]. (lattice-bless(l;eq;a;b) ∈ 𝔹)
Lemma: assert-lattice-bless
∀[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)]. uiff(↑lattice-bless(l;eq;a;b);a < b)
Definition: lattice-fset-meet
/\(s) == reduce(λx,y. x ∧ y;1;s)
Lemma: lattice-fset-meet_wf
∀[l:BoundedLattice]. ((∀x,y:Point(l). Dec(x = y ∈ Point(l)))
⇒ (∀[s:fset(Point(l))]. (/\(s) ∈ Point(l))))
Definition: lattice-fset-join
\/(s) == reduce(λx,y. x ∨ y;0;s)
Lemma: lattice-fset-join_wf
∀[l:BoundedLattice]. ((∀x,y:Point(l). Dec(x = y ∈ Point(l)))
⇒ (∀[s:fset(Point(l))]. (\/(s) ∈ Point(l))))
Lemma: lattice-fset-join-union
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))]. (\/(s1 ⋃ s2) = \/(s1) ∨ \/(s2) ∈ Point(l))
Lemma: lattice-fset-join-singleton
∀[l:BoundedLattice]. ∀[x:Point(l)]. (\/({x}) = x ∈ Point(l))
Lemma: lattice-fset-join-is-lub
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))].
((∀[s:fset(Point(l))]. ∀[x:Point(l)]. x ≤ \/(s) supposing x ∈ s)
∧ (∀[s:fset(Point(l))]. ∀[u:Point(l)]. ((∀x:Point(l). (x ∈ s
⇒ x ≤ u))
⇒ \/(s) ≤ u)))
Lemma: lattice-fset-join-le
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s:fset(Point(l))]. ∀[x:Point(l)].
(\/(s) ≤ x
⇐⇒ ∀p:Point(l). (p ∈ s
⇒ p ≤ x))
Lemma: lattice-fset-join_functionality_wrt_subset
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))]. \/(s1) ≤ \/(s2) supposing s1 ⊆ s2
Lemma: lattice-fset-join_functionality_wrt_subset2
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))]. \/(s1) ≤ \/(s2) supposing s1 ⊆ {0} ⋃ s2
Lemma: lattice-fset-meet-union
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))]. (/\(s1 ⋃ s2) = /\(s1) ∧ /\(s2) ∈ Point(l))
Lemma: lattice-fset-meet-singleton
∀[l:BoundedLattice]. ∀[x:Point(l)]. (/\({x}) = x ∈ Point(l))
Lemma: lattice-fset-meet-is-glb
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))].
((∀[s:fset(Point(l))]. ∀[x:Point(l)]. /\(s) ≤ x supposing x ∈ s)
∧ (∀[s:fset(Point(l))]. ∀[v:Point(l)]. ((∀x:Point(l). (x ∈ s
⇒ v ≤ x))
⇒ v ≤ /\(s))))
Lemma: lattice-fset-meet-is-1
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s:fset(Point(l))].
uiff(/\(s) = 1 ∈ Point(l);∀x:Point(l). (x ∈ s
⇒ (x = 1 ∈ Point(l))))
Lemma: lattice-fset-meet_functionality_wrt_subset
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))]. /\(s1) ≤ /\(s2) supposing s2 ⊆ s1
Lemma: lattice-meet-fset-join-distrib
∀[l:BoundedDistributiveLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].
(\/(s1) ∧ \/(s2) = \/(f-union(eq;eq;s1;a.λb.a ∧ b"(s2))) ∈ Point(l))
Lemma: lattice-hom-join
∀[l1,l2:BoundedLattice]. ∀[f:Hom(l1;l2)]. ∀[a,b:Point(l1)]. ((f a ∨ b) = f a ∨ f b ∈ Point(l2))
Lemma: lattice-hom-meet
∀[l1,l2:BoundedLattice]. ∀[f:Hom(l1;l2)]. ∀[a,b:Point(l1)]. ((f a ∧ b) = f a ∧ f b ∈ Point(l2))
Lemma: lattice-hom-fset-join
∀[l1,l2:BoundedLattice]. ∀[eq1:EqDecider(Point(l1))]. ∀[eq2:EqDecider(Point(l2))]. ∀[f:Hom(l1;l2)].
∀[s:fset(Point(l1))].
((f \/(s)) = \/(f"(s)) ∈ Point(l2))
Lemma: lattice-hom-fset-meet
∀[l1,l2:BoundedLattice]. ∀[eq1:EqDecider(Point(l1))]. ∀[eq2:EqDecider(Point(l2))]. ∀[f:Hom(l1;l2)].
∀[s:fset(Point(l1))].
((f /\(s)) = /\(f"(s)) ∈ Point(l2))
Lemma: lattice-hom-le
∀[l1,l2:BoundedLattice]. ∀[f:Hom(l1;l2)]. ∀[x,y:Point(l1)]. f x ≤ f y supposing x ≤ y
Comment: free distrib lattices using decidable equality doc
The following construction of free distributive lattices depends
on having decidable equality for the generators.
⋅
Definition: free-dist-lattice
free-dist-lattice(T; eq) ==
{points={ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;
meet=λac1,ac2. fset-ac-glb(eq;ac1;ac2);
join=λac1,ac2. fset-ac-lub(eq;ac1;ac2);
0={};
1={{}}}
Lemma: free-dist-lattice_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. (free-dist-lattice(T; eq) ∈ BoundedDistributiveLattice)
Lemma: free-dl-point
∀[T,eq:Top]. (Point(free-dist-lattice(T; eq)) ~ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
Lemma: free-dl-1
∀T:Type. ∀eq:EqDecider(T). ∀x:Point(free-dist-lattice(T; eq)). (x = 1 ∈ Point(free-dist-lattice(T; eq))
⇐⇒ {} ∈ x)
Lemma: free-dl-0-not-1
∀T:Type. ∀eq:EqDecider(T). (¬(0 = 1 ∈ Point(free-dist-lattice(T; eq))))
Lemma: decidable__equal_free-dl
∀[T:Type]. ∀eq:EqDecider(T). ∀x,y:Point(free-dist-lattice(T; eq)). Dec(x = y ∈ Point(free-dist-lattice(T; eq)))
Lemma: free-dl-meet
∀[T,eq,a,b:Top]. (a ∧ b ~ fset-ac-glb(eq;a;b))
Lemma: free-dl-join
∀[T,eq,a,b:Top]. (a ∨ b ~ fset-ac-lub(eq;a;b))
Lemma: free-dl-le
∀[T:Type]. ∀eq:EqDecider(T). ∀x,y:Point(free-dist-lattice(T; eq)). (x ≤ y
⇐⇒ fset-ac-le(eq;x;y))
Definition: free-dl-inc
free-dl-inc(x) == {{x}}
Lemma: free-dl-inc_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. (free-dl-inc(x) ∈ Point(free-dist-lattice(T; eq)))
Lemma: free-dl-1-join-irreducible
∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(free-dist-lattice(T; eq)).
(x ∨ y = 1 ∈ Point(free-dist-lattice(T; eq))
⇐⇒ (x = 1 ∈ Point(free-dist-lattice(T; eq))) ∨ (y = 1 ∈ Point(free-dist-lattice(T; eq))))
Definition: lattice-extend
lattice-extend(L;eq;eqL;f;ac) == \/(λxs./\(f"(xs))"(ac))
Lemma: lattice-extend_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
∀[ac:Point(free-dist-lattice(T; eq))].
(lattice-extend(L;eq;eqL;f;ac) ∈ Point(L))
Lemma: lattice-extend-1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
(lattice-extend(L;eq;eqL;f;1) = 1 ∈ Point(L))
Lemma: lattice-extend-dl-inc
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)]. ∀[x:T].
(lattice-extend(L;eq;eqL;f;free-dl-inc(x)) = (f x) ∈ Point(L))
Lemma: lattice-extend-order-preserving
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
∀[x,y:Point(free-dist-lattice(T; eq))].
lattice-extend(L;eq;eqL;f;x) ≤ lattice-extend(L;eq;eqL;f;y) supposing x ≤ y
Definition: lattice-extend'
lattice-extend'(L;eq;eqL;f;ac) == \/(λxs./\(f"(xs))"(ac))
Lemma: lattice-extend'_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
∀[ac:fset(fset(T))].
(lattice-extend'(L;eq;eqL;f;ac) ∈ Point(L))
Lemma: lattice-extend-join
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
∀[a,b:Point(free-dist-lattice(T; eq))].
lattice-extend(L;eq;eqL;f;a ∨ b) ≤ lattice-extend(L;eq;eqL;f;a) ∨ lattice-extend(L;eq;eqL;f;b)
Lemma: lattice-meet-join-images-distrib
∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀as,bs:fset(fset(Point(L))).
(\/(λls./\(ls)"(as)) ∧ \/(λls./\(ls)"(bs))
= \/(λls./\(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);as;as.λbs.as ⋃ bs"(bs))))
∈ Point(L))
Lemma: lattice-extend-meet
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
∀[a,b:Point(free-dist-lattice(T; eq))].
lattice-extend(L;eq;eqL;f;a) ∧ lattice-extend(L;eq;eqL;f;b) ≤ lattice-extend(L;eq;eqL;f;a ∧ b)
Lemma: lattice-extend-is-hom
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f:T ⟶ Point(L)].
(λac.lattice-extend(L;eq;eqL;f;ac) ∈ Hom(free-dist-lattice(T; eq);L))
Lemma: free-dist-lattice-property
∀T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f:T ⟶ Point(L).
∃g:Hom(free-dist-lattice(T; eq);L). (f = (g o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L)))
Lemma: lattice-fset-meet-free-dl-inc
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:fset(T)]. (/\(λx.free-dl-inc(x)"(s)) = {s} ∈ Point(free-dist-lattice(T; eq)))
Lemma: free-dl-basis
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-dist-lattice(T; eq))].
(x = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(free-dist-lattice(T; eq)))
Lemma: free-dist-lattice-hom-unique2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[g,h:Hom(free-dist-lattice(T; eq);L)].
g = h ∈ Hom(free-dist-lattice(T; eq);L) supposing ∀x:T. ((g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L))
Lemma: free-dist-lattice-hom-unique
∀T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f:T ⟶ Point(L).
∀g,h:Hom(free-dist-lattice(T; eq);L).
((f = (g o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L)))
⇒ (f = (h o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L)))
⇒ (g = h ∈ Hom(free-dist-lattice(T; eq);L)))
Lemma: decidable__equal-free-dist-lattice-point
∀[T:Type]. ∀eq:EqDecider(T). ∀a,b:Point(free-dist-lattice(T; eq)). Dec(a = b ∈ Point(free-dist-lattice(T; eq)))
Definition: opposite-lattice
opposite-lattice(L) == {points=Point(L);meet=λ2a b.a ∨ b;join=λ2a b.a ∧ b;0=1;1=0}
Lemma: opposite-lattice_wf
∀[L:BoundedDistributiveLattice]. (opposite-lattice(L) ∈ BoundedDistributiveLattice)
Lemma: opposite-lattice-point
∀[L:Top]. (Point(opposite-lattice(L)) ~ Point(L))
Lemma: opposite-lattice-0
∀[L:Top]. (0 ~ 1)
Lemma: opposite-lattice-1
∀[L:Top]. (1 ~ 0)
Lemma: opposite-lattice-meet
∀[L,a,b:Top]. (a ∧ b ~ a ∨ b)
Lemma: opposite-lattice-join
∀[L,a,b:Top]. (a ∨ b ~ a ∧ b)
Definition: fin-powerset-lattice
fin-powerset-lattice(T;eq) == mk-distributive-lattice(fset(T); λa,b. a ⋂ b; λa,b. a ⋃ b)
Lemma: fin-powerset-lattice_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. (fin-powerset-lattice(T;eq) ∈ DistributiveLattice)
Definition: finite-powerset-lattice
finite-powerset-lattice(T;eq;whole) == {points=fset(T);meet=λa,b. a ⋂ b;join=λa,b. a ⋃ b;0={};1=whole}
Lemma: finite-powerset-lattice_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[whole:fset(T)].
finite-powerset-lattice(T;eq;whole) ∈ BoundedDistributiveLattice supposing ∀x:T. x ∈ whole
Definition: sub-powerset-lattice
sub-powerset-lattice(T;eq;whole;P) == {points={s:fset(T)| P s} ;meet=λa,b. a ⋂ b;join=λa,b. a ⋃ b;0={};1=whole}
Lemma: sub-powerset-lattice_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[whole:fset(T)]. ∀[P:fset(T) ⟶ ℙ].
sub-powerset-lattice(T;eq;whole;P) ∈ BoundedDistributiveLattice
supposing (∀x:T. x ∈ whole) ∧ (∀a,b:fset(T). ((P a)
⇒ (P b)
⇒ ((P a ⋃ b) ∧ (P a ⋂ b)))) ∧ (P {}) ∧ (P whole)
Definition: up-set-lattice
up-set-lattice(T;eq;whole;x,y.le[x; y]) == sub-powerset-lattice(T;eq;whole;λs.∀x,y:T. (x ∈ s
⇒ le[x; y]
⇒ y ∈ s))
Lemma: up-set-lattice_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[whole:fset(T)]. ∀[le:T ⟶ T ⟶ ℙ].
up-set-lattice(T;eq;whole;x,y.le[x;y]) ∈ BoundedDistributiveLattice supposing (∀x:T. x ∈ whole) ∧ Trans(T;x,y.le[x;y])
Definition: constrained-antichain-lattice
constrained-antichain-lattice(T;eq;P) ==
{points={ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;
meet=λac1,ac2. glb(P;ac1;ac2);
join=λac1,ac2. lub(P;ac1;ac2);
0={};
1={{}}}
Lemma: constrained-antichain-lattice_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹].
constrained-antichain-lattice(T;eq;P) ∈ BoundedDistributiveLattice
supposing (∀x,y:fset(T). (y ⊆ x
⇒ (↑(P x))
⇒ (↑(P y)))) ∧ (↑(P {}))
Lemma: cal-point
∀[T,eq,P:Top].
(Point(constrained-antichain-lattice(T;eq;P)) ~ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} )
Definition: cal-filter
cal-filter(s;x.P[x]) == {x ∈ s | P[x]}
Lemma: cal-filter_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:Point(constrained-antichain-lattice(T;eq;P))]. ∀[Q:{x:fset(T)|
↑P[x]} ⟶ 𝔹].
(cal-filter(s;x.Q[x]) ∈ Point(constrained-antichain-lattice(T;eq;P)))
Lemma: cal-filter-decomp
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:Point(constrained-antichain-lattice(T;eq;P))]. ∀[Q:{x:fset(T)|
↑P[x]} ⟶ 𝔹].
(s = cal-filter(s;x.Q[x]) ∨ cal-filter(s;x.¬bQ[x]) ∈ Point(constrained-antichain-lattice(T;eq;P)))
Definition: free-dist-lattice-with-constraints
free-dist-lattice-with-constraints(T;eq;x.Cs[x]) ==
constrained-antichain-lattice(T;eq;λs.fset-contains-none(eq;s;x.Cs[x]))
Lemma: free-dist-lattice-with-constraints_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))].
(free-dist-lattice-with-constraints(T;eq;x.Cs[x]) ∈ BoundedDistributiveLattice)
Lemma: free-dlwc-point
∀[T,eq,Cs:Top].
(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) ~ {ac:fset(fset(T))|
(↑fset-antichain(eq;ac))
∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} )
Lemma: decidable__equal-free-dist-lattice-with-constraints-point
∀[T:Type]
∀eq:EqDecider(T). ∀Cs:T ⟶ fset(fset(T)). ∀a,b:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).
Dec(a = b ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
Lemma: free-dlwc-point-subtype
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))].
(Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) ⊆r Point(free-dist-lattice(T; eq)))
Lemma: free-dlwc-meet
∀[T,eq,a,b,cs:Top]. (a ∧ b ~ glb(λs.fset-contains-none(eq;s;x.cs[x]);a;b))
Lemma: free-dlwc-join
∀[T,eq,a,b,cs:Top]. (a ∨ b ~ lub(λs.fset-contains-none(eq;s;x.cs[x]);a;b))
Lemma: free-dlwc-le
∀[T:Type]
∀eq:EqDecider(T). ∀cs:T ⟶ fset(fset(T)). ∀x,y:Point(free-dist-lattice-with-constraints(T;eq;x.cs[x])).
(x ≤ y
⇐⇒ fset-ac-le(eq;x;y))
Definition: free-dlwc-inc
free-dlwc-inc(eq;a.Cs[a];x) == if fset-null({c ∈ Cs[x] | deq-f-subset(eq) c {x}}) then {{x}} else {} fi
Lemma: free-dlwc-inc_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[x:T].
(free-dlwc-inc(eq;a.Cs[a];x) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
Lemma: free-dlwc-1
∀[T:Type]
∀eq:EqDecider(T). ∀Cs:T ⟶ fset(fset(T)). ∀x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).
(x = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
⇐⇒ {} ∈ x)
Lemma: free-dlwc-1-join-irreducible
∀T:Type. ∀eq:EqDecider(T). ∀Cs:T ⟶ fset(fset(T)). ∀x,y:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])).
(x ∨ y = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
⇐⇒ (x = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
∨ (y = 1 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))))
Definition: lattice-extend-wc
lattice-extend-wc(L;eq;eqL;f;ac) == lattice-extend(L;eq;eqL;f;ac)
Lemma: lattice-extend-wc_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[f:T ⟶ Point(L)]. ∀[ac:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
(lattice-extend-wc(L;eq;eqL;f;ac) ∈ Point(L))
Lemma: lattice-extend-wc-1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[f:T ⟶ Point(L)].
(lattice-extend-wc(L;eq;eqL;f;1) = 1 ∈ Point(L))
Lemma: lattice-extend-dlwc-inc
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[f:T ⟶ Point(L)].
∀[x:T]. (lattice-extend-wc(L;eq;eqL;f;free-dlwc-inc(eq;a.Cs[a];x)) = (f x) ∈ Point(L))
supposing ∀x:T. ∀c:fset(T). (c ∈ Cs[x]
⇒ (/\(f"(c)) = 0 ∈ Point(L)))
Lemma: lattice-fset-meet-free-dlwc-inc
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[s:fset(T)].
/\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s)) = {s} ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))
supposing ↑fset-contains-none(eq;s;x.Cs[x])
Lemma: free-dlwc-basis
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[x:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
(x = \/(λs./\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(s))"(x)) ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])))
Lemma: free-dlwc-satisfies-constraints
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))].
((∀x:T. ∀c:fset(T). (c ∈ Cs[x]
⇒ x ∈ c))
⇒ (∀x:T. ∀c:fset(T).
(c ∈ Cs[x]
⇒ (/\(λx.free-dlwc-inc(eq;a.Cs[a];x)"(c)) = 0 ∈ Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))))))
Lemma: lattice-extend-wc-order-preserving
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[f:T ⟶ Point(L)]. ∀[x,y:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
lattice-extend-wc(L;eq;eqL;f;x) ≤ lattice-extend-wc(L;eq;eqL;f;y) supposing x ≤ y
Lemma: lattice-extend-wc-join
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[f:T ⟶ Point(L)]. ∀[a,b:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
lattice-extend-wc(L;eq;eqL;f;a ∨ b) ≤ lattice-extend-wc(L;eq;eqL;f;a) ∨ lattice-extend-wc(L;eq;eqL;f;b)
Lemma: lattice-extend-wc-meet
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[f:T ⟶ Point(L)].
∀[a,b:Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))].
lattice-extend-wc(L;eq;eqL;f;a) ∧ lattice-extend-wc(L;eq;eqL;f;b) ≤ lattice-extend-wc(L;eq;eqL;f;a ∧ b)
supposing ∀x:T. ∀c:fset(T). (c ∈ Cs[x]
⇒ (/\(f"(c)) = 0 ∈ Point(L)))
Lemma: lattice-extend-is-hom-constrained
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[f:T ⟶ Point(L)].
λac.lattice-extend-wc(L;eq;eqL;f;ac) ∈ Hom(free-dist-lattice-with-constraints(T;eq;x.Cs[x]);L)
supposing ∀x:T. ∀c:fset(T). (c ∈ Cs[x]
⇒ (/\(f"(c)) = 0 ∈ Point(L)))
Lemma: free-dist-lattice-with-constraints-property
∀[T:Type]
∀eq:EqDecider(T)
∀[Cs:T ⟶ fset(fset(T))]
∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f:T ⟶ Point(L).
∃g:Hom(free-dist-lattice-with-constraints(T;eq;x.Cs[x]);L)
(f = (g o (λx.free-dlwc-inc(eq;a.Cs[a];x))) ∈ (T ⟶ Point(L)))
supposing ∀x:T. ∀c:fset(T). (c ∈ Cs[x]
⇒ (/\(f"(c)) = 0 ∈ Point(L)))
Definition: face-lattice-constraints
face-lattice-constraints(x) == case x of inl(a) => {{inl a,inr a }} | inr(a) => {{inl a,inr a }}
Lemma: face-lattice-constraints_wf
∀[T:Type]. ∀[x:T + T]. (face-lattice-constraints(x) ∈ fset(fset(T + T)))
Definition: face-lattice
face-lattice(T;eq) == free-dist-lattice-with-constraints(T + T;union-deq(T;T;eq;eq);x.face-lattice-constraints(x))
Lemma: face-lattice_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. (face-lattice(T;eq) ∈ BoundedDistributiveLattice)
Definition: face-lattice0
(x=0) == {{inl x}}
Lemma: face-lattice0-is-inc
∀T:Type. ∀eq:EqDecider(T). ∀x:T. ((x=0) ~ free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inl x))
Lemma: face-lattice0_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ((x=0) ∈ Point(face-lattice(T;eq)))
Definition: face-lattice1
(x=1) == {{inr x }}
Lemma: face-lattice1-is-inc
∀T:Type. ∀eq:EqDecider(T). ∀x:T. ((x=1) ~ free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inr x ))
Lemma: face-lattice1_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ((x=1) ∈ Point(face-lattice(T;eq)))
Lemma: fl-point
∀[T:Type]. ∀[eq:EqDecider(T)].
Point(face-lattice(T;eq)) ≡ {ac:fset(fset(T + T))|
(↑fset-antichain(union-deq(T;T;eq;eq);ac))
∧ (∀a:fset(T + T). (a ∈ ac
⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z ∈ a)))))}
Lemma: fl-point-sq
∀[T,eq:Top].
(Point(face-lattice(T;eq)) ~ {ac:fset(fset(T + T))|
(↑fset-antichain(union-deq(T;T;eq;eq);ac))
∧ fset-all(ac;a.fset-contains-none(union-deq(T;T;eq;
eq);a;x.face-lattice-constraints(x)))} )
Definition: fl-deq
fl-deq(T;eq) == deq-fset(deq-fset(union-deq(T;T;eq;eq)))
Lemma: fl-deq_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. (fl-deq(T;eq) ∈ EqDecider(Point(face-lattice(T;eq))))
Lemma: decidable__equal-fl-point
∀[T:Type]. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)). Dec(x = y ∈ Point(face-lattice(T;eq)))
Definition: fl-vertex
fl-vertex(u) == {{u}}
Lemma: fl-vertex_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[u:T + T]. (fl-vertex(u) ∈ Point(face-lattice(T;eq)))
Lemma: fl-meet-0-1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ((x=0) ∧ (x=1) = 0 ∈ Point(face-lattice(T;eq)))
Lemma: face-lattice-property
∀T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f0,f1:T ⟶ Point(L).
∃g:Hom(face-lattice(T;eq);L) [(∀x:T. (((g (x=0)) = (f0 x) ∈ Point(L)) ∧ ((g (x=1)) = (f1 x) ∈ Point(L))))]
supposing ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
Lemma: face-lattice-basis
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(face-lattice(T;eq))].
(x = \/(λs./\(λu.{{u}}"(s))"(x)) ∈ Point(face-lattice(T;eq)))
Lemma: face-lattice-induction
∀T:Type. ∀eq:EqDecider(T).
∀[P:Point(face-lattice(T;eq)) ⟶ ℙ]
((∀x:Point(face-lattice(T;eq)). SqStable(P[x]))
⇒ P[0]
⇒ P[1]
⇒ (∀x,y:Point(face-lattice(T;eq)). (P[x]
⇒ P[y]
⇒ P[x ∨ y]))
⇒ (∀x:Point(face-lattice(T;eq)). (P[x]
⇒ (∀i:T. (P[(i=0) ∧ x] ∧ P[(i=1) ∧ x]))))
⇒ (∀x:Point(face-lattice(T;eq)). P[x]))
Lemma: face-lattice-le-1
∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)). (x ≤ y
⇐⇒ fset-ac-le(union-deq(T;T;eq;eq);x;y))
Lemma: face-lattice-le
∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).
(x ≤ y
⇐⇒ ∀s:fset(T + T). (s ∈ x
⇒ (↓∃t:fset(T + T). (t ∈ y ∧ t ⊆ s))))
Lemma: face-lattice-subset-le
∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)). (x ⊆ y
⇒ x ≤ y)
Definition: fl-filter
fl-filter(s;x.Q[x]) == cal-filter(s;x.Q[x])
Lemma: fl-filter_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Q:{x:fset(T + T)|
↑fset-contains-none(union-deq(T;T;eq;eq);x;x.face-lattice-constraints(x))} ⟶ 𝔹].
∀[s:Point(face-lattice(T;eq))].
(fl-filter(s;x.Q[x]) ∈ Point(face-lattice(T;eq)))
Lemma: fl-filter-subset
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Q:fset(T + T) ⟶ 𝔹]. ∀[s:fset(fset(T + T))]. fl-filter(s;x.Q[x]) ⊆ s
Lemma: fl-filter-filter
∀[P,Q,s:Top]. (fl-filter(fl-filter(s;x.P[x]);x.Q[x]) ~ fl-filter(s;x.P[x] ∧b Q[x]))
Lemma: fl-filter-decomp
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[s:Point(face-lattice(T;eq))].
∀[Q:{x:fset(T + T)| ↑fset-contains-none(union-deq(T;T;eq;eq);x;x.face-lattice-constraints(x))} ⟶ 𝔹].
(s = fl-filter(s;x.Q[x]) ∨ fl-filter(s;x.¬bQ[x]) ∈ Point(face-lattice(T;eq)))
Lemma: fset-ac-le-face-lattice0
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T]. ∀[s:fset(fset(T + T))].
(fset-all(s;x.inl i ∈b x)
⇐⇒ fset-ac-le(union-deq(T;T;eq;eq);s;(i=0)))
Lemma: fset-ac-le-face-lattice1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T]. ∀[s:fset(fset(T + T))].
(fset-all(s;x.inr i ∈b x)
⇐⇒ fset-ac-le(union-deq(T;T;eq;eq);s;(i=1)))
Lemma: implies-le-face-lattice-join
∀T:Type. ∀eq:EqDecider(T). ∀x,y,z:Point(face-lattice(T;eq)).
((∀s:fset(T + T). (s ∈ z
⇒ ((↓∃t:fset(T + T). (t ∈ x ∧ t ⊆ s)) ∨ (↓∃t:fset(T + T). (t ∈ y ∧ t ⊆ s)))))
⇒ z ≤ x ∨ y)
Lemma: implies-le-face-lattice-join3
∀T:Type. ∀eq:EqDecider(T). ∀u,x,y,z:Point(face-lattice(T;eq)).
((∀s:fset(T + T)
(s ∈ z
⇒ ((↓∃t:fset(T + T). (t ∈ u ∧ t ⊆ s))
∨ (↓∃t:fset(T + T). (t ∈ x ∧ t ⊆ s))
∨ (↓∃t:fset(T + T). (t ∈ y ∧ t ⊆ s)))))
⇒ z ≤ u ∨ x ∨ y)
Definition: fl-all
(∀i.phi) == fl-filter(phi;x.(¬binl i ∈b x) ∧b (¬binr i ∈b x))
Lemma: fl-all_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[phi:Point(face-lattice(T;eq))]. ∀[i:T]. ((∀i.phi) ∈ Point(face-lattice(T;eq)))
Lemma: fl-all-decomp
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[phi:Point(face-lattice(T;eq))]. ∀[i:T].
(phi = (∀i.phi) ∨ phi ∧ (i=0) ∨ phi ∧ (i=1) ∈ Point(face-lattice(T;eq)))
Definition: fl-lift
fl-lift(T;eq;L;eqL;f0;f1) == TERMOF{face-lattice-property:o, 1:l, 1:l} T eq L eqL f0 f1
Lemma: fl-lift_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f0,f1:T ⟶ Point(L)].
fl-lift(T;eq;L;eqL;f0;f1) ∈ {g:Hom(face-lattice(T;eq);L)|
∀x:T. (((g (x=0)) = (f0 x) ∈ Point(L)) ∧ ((g (x=1)) = (f1 x) ∈ Point(L)))}
supposing ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
Lemma: face-lattice-hom-unique
∀T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f0,f1:T ⟶ Point(L).
∀[g,h:Hom(face-lattice(T;eq);L)].
g = h ∈ Hom(face-lattice(T;eq);L)
supposing (∀x:T. (g (x=0) ∧ g (x=1) = 0 ∈ Point(L)))
∧ (∀x:T. ((g (x=0)) = (h (x=0)) ∈ Point(L)))
∧ (∀x:T. ((g (x=1)) = (h (x=1)) ∈ Point(L)))
Lemma: face-lattice-1-join-irreducible
∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).
(x ∨ y = 1 ∈ Point(face-lattice(T;eq))
⇐⇒ (x = 1 ∈ Point(face-lattice(T;eq))) ∨ (y = 1 ∈ Point(face-lattice(T;eq))))
Lemma: fl-lift-unique
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f0,f1:T ⟶ Point(L)].
∀g:Hom(face-lattice(T;eq);L)
fl-lift(T;eq;L;eqL;f0;f1) = g ∈ Hom(face-lattice(T;eq);L)
supposing ∀x:T. (((g (x=0)) = (f0 x) ∈ Point(L)) ∧ ((g (x=1)) = (f1 x) ∈ Point(L)))
supposing ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
Lemma: fl-lift-unique2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f0,f1:T ⟶ Point(L)].
∀g:Hom(face-lattice(T;eq);L)
∀x:Point(face-lattice(T;eq)). ((fl-lift(T;eq;L;eqL;f0;f1) x) = (g x) ∈ Point(L))
supposing ∀x:T. (((g (x=0)) = (f0 x) ∈ Point(L)) ∧ ((g (x=1)) = (f1 x) ∈ Point(L)))
supposing ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
Definition: free-DeMorgan-lattice
free-DeMorgan-lattice(T;eq) == free-dist-lattice(T + T; union-deq(T;T;eq;eq))
Lemma: free-DeMorgan-lattice_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. (free-DeMorgan-lattice(T;eq) ∈ BoundedDistributiveLattice)
Definition: free-dml-deq
free-dml-deq(T;eq) == deq-fset(deq-fset(union-deq(T;T;eq;eq)))
Lemma: free-dml-deq_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. (free-dml-deq(T;eq) ∈ EqDecider(Point(free-DeMorgan-lattice(T;eq))))
Lemma: free-dml-0-not-1
∀T:Type. ∀eq:EqDecider(T). (¬(0 = 1 ∈ Point(free-DeMorgan-lattice(T;eq))))
Definition: is-dml-1
is-dml-1(T;eq;x) == free-dml-deq(T;eq) x 1
Lemma: is-dml-1_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-DeMorgan-lattice(T;eq))]. (is-dml-1(T;eq;x) ∈ 𝔹)
Lemma: assert-is-dml-1
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-DeMorgan-lattice(T;eq))].
uiff(↑is-dml-1(T;eq;x);x = 1 ∈ Point(free-DeMorgan-lattice(T;eq)))
Definition: dminc
<i> == free-dl-inc(inl i)
Lemma: dminc_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T]. (<i> ∈ Point(free-DeMorgan-lattice(T;eq)))
Definition: dmopp
<1-i> == free-dl-inc(inr i )
Lemma: dmopp_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T]. (<1-i> ∈ Point(free-DeMorgan-lattice(T;eq)))
Definition: dm-neg
¬(x) ==
lattice-extend(opposite-lattice(free-DeMorgan-lattice(T;eq));union-deq(T;T;eq;eq);
deq-fset(deq-fset(union-deq(T;T;eq;eq)));λz.case z of inl(a) => {{inr a }} | inr(a) => {{inl a}};x)
Lemma: dm-neg_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-DeMorgan-lattice(T;eq))]. (¬(x) ∈ Point(free-DeMorgan-lattice(T;eq)))
Lemma: dm-neg-is-hom
∀[T:Type]. ∀[eq:EqDecider(T)].
(λx.¬(x) ∈ Hom(free-DeMorgan-lattice(T;eq);opposite-lattice(free-DeMorgan-lattice(T;eq))))
Lemma: dm-neg-properties
∀[T:Type]. ∀[eq:EqDecider(T)].
((∀[x,y:Point(free-DeMorgan-lattice(T;eq))]. (¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(free-DeMorgan-lattice(T;eq))))
∧ (∀[x,y:Point(free-DeMorgan-lattice(T;eq))]. (¬(x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(free-DeMorgan-lattice(T;eq))))
∧ (¬(0) = 1 ∈ Point(free-DeMorgan-lattice(T;eq)))
∧ (¬(1) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))))
Lemma: dm-neg-is-hom-opposite
∀[T:Type]. ∀[eq:EqDecider(T)].
(λx.¬(x) ∈ Hom(opposite-lattice(free-DeMorgan-lattice(T;eq));free-DeMorgan-lattice(T;eq)))
Lemma: dm-neg-opp
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T]. (¬(<1-i>) = <i> ∈ Point(free-DeMorgan-lattice(T;eq)))
Lemma: dm-neg-inc
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[i:T]. (¬(<i>) = <1-i> ∈ Point(free-DeMorgan-lattice(T;eq)))
Lemma: dm-neg-neg
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:Point(free-DeMorgan-lattice(T;eq))].
(¬(¬(x)) = x ∈ Point(free-DeMorgan-lattice(T;eq)))
Definition: DeMorgan-algebra-structure
DeMorganAlgebraStructure ==
"Point":Type
"meet":self."Point" ⟶ self."Point" ⟶ self."Point"
"join":self."Point" ⟶ self."Point" ⟶ self."Point"
"1":self."Point"
"0":self."Point"
"neg":self."Point" ⟶ self."Point"
Lemma: DeMorgan-algebra-structure_wf
DeMorganAlgebraStructure ∈ 𝕌'
Lemma: DeMorgan-algebra-structure-subtype
DeMorganAlgebraStructure ⊆r BoundedLatticeStructure
Definition: dma-neg
¬(x) == dma."neg" x
Lemma: dma-neg_wf
∀[dma:DeMorganAlgebraStructure]. ∀[x:Point(dma)]. (¬(x) ∈ Point(dma))
Definition: DeMorgan-algebra-axioms
DeMorgan-algebra-axioms(dma) ==
(∀x:Point(dma). (¬(¬(x)) = x ∈ Point(dma))) ∧ (∀x,y:Point(dma). (¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(dma)))
Lemma: DeMorgan-algebra-axioms_wf
∀[dma:DeMorganAlgebraStructure]. (DeMorgan-algebra-axioms(dma) ∈ ℙ)
Definition: DeMorgan-algebra
DeMorganAlgebra ==
{dma:DeMorganAlgebraStructure|
lattice-axioms(dma)
∧ bounded-lattice-axioms(dma)
∧ (∀[a,b,c:Point(dma)]. (a ∧ b ∨ c = a ∧ b ∨ a ∧ c ∈ Point(dma)))
∧ DeMorgan-algebra-axioms(dma)}
Lemma: DeMorgan-algebra_wf
DeMorganAlgebra ∈ 𝕌'
Lemma: DeMorgan-algebra-subtype
DeMorganAlgebra ⊆r BoundedDistributiveLattice
Lemma: DeMorgan-algebra-laws
∀[dma:DeMorganAlgebra]
((∀x:Point(dma). (¬(¬(x)) = x ∈ Point(dma)))
∧ (∀x,y:Point(dma). (¬(x ∧ y) = ¬(x) ∨ ¬(y) ∈ Point(dma)))
∧ (∀x,y:Point(dma). (¬(x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(dma)))
∧ (¬(0) = 1 ∈ Point(dma))
∧ (¬(1) = 0 ∈ Point(dma)))
Lemma: implies-DeMorgan-algebra-axioms
∀[dma:DeMorganAlgebraStructure]
((∀x:Point(dma). (¬(¬(x)) = x ∈ Point(dma)))
⇒ (∀x,y:Point(dma). (¬(x ∨ y) = ¬(x) ∧ ¬(y) ∈ Point(dma)))
⇒ DeMorgan-algebra-axioms(dma))
Definition: mk-DeMorgan-algebra
mk-DeMorgan-algebra(L;n) == L["neg" := n]
Lemma: mk-DeMorgan-algebra_wf
∀[L:BoundedDistributiveLattice]. ∀[n:Point(L) ⟶ Point(L)].
mk-DeMorgan-algebra(L;n) ∈ DeMorganAlgebra
supposing (∀x:Point(L). ((n (n x)) = x ∈ Point(L)))
∧ ((∀x,y:Point(L). ((n x ∧ y) = n x ∨ n y ∈ Point(L))) ∨ (∀x,y:Point(L). ((n x ∨ y) = n x ∧ n y ∈ Point(L))))
Lemma: mk-DeMorgan-algebra-equal-bounded-lattice
∀[L:BoundedLatticeStructure]. ∀[n:Top]. (mk-DeMorgan-algebra(L;n) = L ∈ BoundedLatticeStructure)
Definition: dma-hom
dma-hom(dma1;dma2) == {f:Hom(dma1;dma2)| ∀[a:Point(dma1)]. (¬(f a) = (f ¬(a)) ∈ Point(dma2))}
Lemma: dma-hom_wf
∀[dma1:DeMorganAlgebra]. ∀dma2:DeMorganAlgebra. (dma-hom(dma1;dma2) ∈ Type)
Lemma: id-is-dma-hom
∀[dma:DeMorganAlgebra]. (λx.x ∈ dma-hom(dma;dma))
Lemma: compose-dma-hom
∀[dma1,dma2,dma3:DeMorganAlgebra]. ∀[f:dma-hom(dma1;dma2)]. ∀[g:dma-hom(dma2;dma3)]. (g o f ∈ dma-hom(dma1;dma3))
Definition: free-DeMorgan-algebra
free-DeMorgan-algebra(T;eq) == mk-DeMorgan-algebra(free-DeMorgan-lattice(T;eq);λx.¬(x))
Lemma: free-DeMorgan-algebra_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. (free-DeMorgan-algebra(T;eq) ∈ DeMorganAlgebra)
Lemma: free-dma-point
∀[T,eq:Top]. (Point(free-DeMorgan-algebra(T;eq)) ~ Point(free-DeMorgan-lattice(T;eq)))
Lemma: free-dma-point-subtype
∀[T:Type]. ∀[eq:EqDecider(T)]. (Point(free-DeMorgan-lattice(T;eq)) ⊆r Point(free-DeMorgan-algebra(T;eq)))
Lemma: free-dma-neg
∀[T,eq,x:Top]. (¬(x) ~ ¬(x))
Lemma: free-dma-hom-is-lattice-hom
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[dm:BoundedDistributiveLattice].
(Hom(free-DeMorgan-lattice(T;eq);dm) = Hom(free-DeMorgan-algebra(T;eq);dm) ∈ Type)
Lemma: free-DeMorgan-algebra-property
∀T:Type. ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm).
(∃g:dma-hom(free-DeMorgan-algebra(T;eq);dm) [(∀i:T. ((g <i>) = (f i) ∈ Point(dm)))])
Definition: free-dma-lift
free-dma-lift(T;eq;dm;eq2;f) == TERMOF{free-DeMorgan-algebra-property:o, 1:l, 1:l} T eq dm eq2 f
Lemma: free-dma-lift_wf
∀T:Type. ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm).
(free-dma-lift(T;eq;dm;eq2;f) ∈ {g:dma-hom(free-DeMorgan-algebra(T;eq);dm)| ∀i:T. ((g <i>) = (f i) ∈ Point(dm))} )
Lemma: free-dma-lift-inc
∀T:Type. ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm). ∀i:T.
((free-dma-lift(T;eq;dm;eq2;f) <i>) = (f i) ∈ Point(dm))
Lemma: free-dma-lift-0
∀T:Type. ∀eq:EqDecider(T). ∀dm:DeMorganAlgebra. ∀eq2:EqDecider(Point(dm)). ∀f:T ⟶ Point(dm).
∀x:Point(free-DeMorgan-algebra(T;eq)).
(free-dma-lift(T;eq;dm;eq2;f) x) = 0 ∈ Point(dm) supposing x = 0 ∈ Point(free-DeMorgan-algebra(T;eq))
Lemma: free-DeMorgan-algebra-hom-unique
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[dm:DeMorganAlgebra]. ∀[eq2:EqDecider(Point(dm))].
∀f:T ⟶ Point(dm)
∀[g,h:dma-hom(free-DeMorgan-algebra(T;eq);dm)].
g = h ∈ dma-hom(free-DeMorgan-algebra(T;eq);dm) supposing ∀i:T. ((g <i>) = (h <i>) ∈ Point(dm))
Lemma: free-dma-lift-unique
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[dm:DeMorganAlgebra]. ∀[eq2:EqDecider(Point(dm))]. ∀[f:T ⟶ Point(dm)].
∀[g:dma-hom(free-DeMorgan-algebra(T;eq);dm)].
free-dma-lift(T;eq;dm;eq2;f) = g ∈ dma-hom(free-DeMorgan-algebra(T;eq);dm)
supposing ∀i:T. ((g <i>) = (f i) ∈ Point(dm))
Lemma: free-dma-lift-unique2
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[dm:DeMorganAlgebra]. ∀[eq2:EqDecider(Point(dm))]. ∀[f:T ⟶ Point(dm)].
∀[g:dma-hom(free-DeMorgan-algebra(T;eq);dm)].
∀x:Point(free-DeMorgan-algebra(T;eq)). ((free-dma-lift(T;eq;dm;eq2;f) x) = (g x) ∈ Point(dm))
supposing ∀i:T. ((g <i>) = (f i) ∈ Point(dm))
Lemma: free-dma-lift-id
∀T:Type. ∀eq:EqDecider(T).
(free-dma-lift(T;eq;free-DeMorgan-algebra(T;eq);free-dml-deq(T;eq);λi.<i>)
= (λx.x)
∈ dma-hom(free-DeMorgan-algebra(T;eq);free-DeMorgan-algebra(T;eq)))
Definition: dma-lift-compose
dma-lift-compose(I;J;eqi;eqj;f;g) == free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f) o g
Lemma: dma-lift-compose_wf
∀[I,J,K:Type]. ∀[eqi:EqDecider(I)]. ∀[eqj:EqDecider(J)]. ∀[f:J ⟶ Point(free-DeMorgan-algebra(I;eqi))].
∀[g:K ⟶ Point(free-DeMorgan-algebra(J;eqj))].
(dma-lift-compose(I;J;eqi;eqj;f;g) ∈ K ⟶ Point(free-DeMorgan-algebra(I;eqi)))
Lemma: dma-lift-compose-assoc
∀[I,J,K,H:Type]. ∀[eqi:EqDecider(I)]. ∀[eqj:EqDecider(J)]. ∀[eqk:EqDecider(K)].
∀[f:J ⟶ Point(free-DeMorgan-algebra(I;eqi))]. ∀[g:K ⟶ Point(free-DeMorgan-algebra(J;eqj))].
∀[h:H ⟶ Point(free-DeMorgan-algebra(K;eqk))].
(dma-lift-compose(I;K;eqi;eqk;dma-lift-compose(I;J;eqi;eqj;f;g);h)
= dma-lift-compose(I;J;eqi;eqj;f;dma-lift-compose(J;K;eqj;eqk;g;h))
∈ (H ⟶ Point(free-DeMorgan-algebra(I;eqi))))
Definition: general-bounded-lattice-structure
A generalized bounded lattice structure includes
all the components of a bounded lattice, and, in addition,
a relation E on the points of the lattice.
When we define a generalized bounded lattice, E will be an
equivalence relation on the points, and the lattice axioms
will hold upto E-equivalence.⋅
GeneralBoundedLatticeStructure ==
"Point":Type
"meet":self."Point" ⟶ self."Point" ⟶ self."Point"
"join":self."Point" ⟶ self."Point" ⟶ self."Point"
"1":self."Point"
"0":self."Point"
"E":self."Point" ⟶ self."Point" ⟶ ℙ
Lemma: general-bounded-lattice-structure_wf
GeneralBoundedLatticeStructure ∈ 𝕌'
Lemma: general-bounded-lattice-structure-subtype
GeneralBoundedLatticeStructure ⊆r BoundedLatticeStructure
Definition: lattice-equiv
a ≡ b == l."E" a b
Lemma: lattice-equiv_wf
∀[l:GeneralBoundedLatticeStructure]. ∀[a,b:Point(l)]. (a ≡ b ∈ ℙ)
Definition: general-lattice-axioms
E is an equivalence relation on the lattice points.
The usual axioms for a bounded lattice hold "upto E-equivalence".
For example the (constructive) real numbers in a closed interval
form a generalized bounded lattice where E is ⌜x = y⌝ (req).⋅
general-lattice-axioms(l) ==
EquivRel(Point(l);a,b.a ≡ b)
∧ (∀[a,b:Point(l)]. a ∧ b ≡ b ∧ a)
∧ (∀[a,b:Point(l)]. a ∨ b ≡ b ∨ a)
∧ (∀[a,b,c:Point(l)]. a ∧ b ∧ c ≡ a ∧ b ∧ c)
∧ (∀[a,b,c:Point(l)]. a ∨ b ∨ c ≡ a ∨ b ∨ c)
∧ (∀[a,b:Point(l)]. a ∨ a ∧ b ≡ a)
∧ (∀[a,b:Point(l)]. a ∧ a ∨ b ≡ a)
∧ (∀[a:Point(l)]. a ∨ 0 ≡ a)
∧ (∀[a:Point(l)]. a ∧ 1 ≡ a)
Lemma: general-lattice-axioms_wf
∀[l:GeneralBoundedLatticeStructure]. (general-lattice-axioms(l) ∈ ℙ)
Definition: general-bounded-lattice
GeneralBoundedLattice == {l:GeneralBoundedLatticeStructure| general-lattice-axioms(l)}
Lemma: general-bounded-lattice_wf
GeneralBoundedLattice ∈ 𝕌'
Definition: mk-general-bounded-lattice
mk-general-bounded-lattice(T;m;j;z;o;E) == λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o]["E" := E]
Lemma: mk-general-bounded-lattice_wf
∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T]. ∀[E:T ⟶ T ⟶ ℙ].
mk-general-bounded-lattice(T;m;j;z;o;E) ∈ GeneralBoundedLattice
supposing EquivRel(T;x,y.E x y)
∧ (∀[a,b:T]. (E m[a;b] m[b;a]))
∧ (∀[a,b:T]. (E j[a;b] j[b;a]))
∧ (∀[a,b,c:T]. (E m[a;m[b;c]] m[m[a;b];c]))
∧ (∀[a,b,c:T]. (E j[a;j[b;c]] j[j[a;b];c]))
∧ (∀[a,b:T]. (E j[a;m[a;b]] a))
∧ (∀[a,b:T]. (E m[a;j[a;b]] a))
∧ (∀[a:T]. (E m[a;o] a))
∧ (∀[a:T]. (E j[a;z] a))
Definition: general-bounded-distributive-lattice
GeneralBoundedDistributiveLattice ==
{l:GeneralBoundedLatticeStructure| general-lattice-axioms(l) ∧ (∀[a,b,c:Point(l)]. a ∧ b ∨ c ≡ a ∧ b ∨ a ∧ c)}
Lemma: general-bounded-distributive-lattice_wf
GeneralBoundedDistributiveLattice ∈ 𝕌'
Definition: mk-general-bounded-dist-lattice
mk-general-bounded-dist-lattice(T;m;j;z;o;E) == mk-general-bounded-lattice(T;m;j;z;o;E)
Lemma: mk-general-bounded-dist-lattice_wf
∀[T:Type]. ∀[m,j:T ⟶ T ⟶ T]. ∀[z,o:T]. ∀[E:T ⟶ T ⟶ ℙ].
mk-general-bounded-dist-lattice(T;m;j;z;o;E) ∈ GeneralBoundedDistributiveLattice
supposing EquivRel(T;x,y.E x y)
∧ (∀[a,b:T]. (E m[a;b] m[b;a]))
∧ (∀[a,b:T]. (E j[a;b] j[b;a]))
∧ (∀[a,b,c:T]. (E m[a;m[b;c]] m[m[a;b];c]))
∧ (∀[a,b,c:T]. (E j[a;j[b;c]] j[j[a;b];c]))
∧ (∀[a,b:T]. (E j[a;m[a;b]] a))
∧ (∀[a,b:T]. (E m[a;j[a;b]] a))
∧ (∀[a:T]. (E m[a;o] a))
∧ (∀[a:T]. (E j[a;z] a))
∧ (∀[a,b,c:T]. (E m[a;j[b;c]] j[m[a;b];m[a;c]]))
Definition: quotient-dl
l//x,y.eq[x; y] == {points=x,y:Point(l)//eq[x; y];meet=l."meet";join=l."join";0=l."0";1=l."1"}
Lemma: quotient-dl_wf
∀[l:BoundedDistributiveLattice]. ∀[eq:Point(l) ⟶ Point(l) ⟶ ℙ].
(l//x,y.eq[x;y] ∈ BoundedDistributiveLattice) supposing
((∀a,c,b,d:Point(l). (eq[a;c]
⇒ eq[b;d]
⇒ eq[a ∨ b;c ∨ d])) and
(∀a,c,b,d:Point(l). (eq[a;c]
⇒ eq[b;d]
⇒ eq[a ∧ b;c ∧ d])) and
EquivRel(Point(l);x,y.eq[x;y]))
Comment: free DeMorgan algebra using quotient doc
To construct the face lattice on an arbitrary type X of generators,
we can start with the free distributive lattice ⌜free-dl(X + X)⌝ on generators
X + X. We call generator inl x (x=0) and inr x is (x=1).
Then we form a quotient of that lattice so that (x=0) ∧ (x=1) = 0 ∈ Point(free-dl(X + X)).
⋅
Definition: flip-union
flip-union(x) == case x of inl(a) => inr a | inr(a) => inl a
Lemma: flip-union_wf
∀[X:Type]. ∀[x:X + X]. (flip-union(x) ∈ X + X)
Definition: flattice-order
flattice-order(X;as;bs) == (∀b∈bs.(∃x∈b. (∃y∈b. y = flip-union(x) ∈ (X + X))) ∨ (∃a∈as. a ⊆ b))
Lemma: flattice-order_wf
∀[X:Type]. ∀[as,bs:(X + X) List List]. (flattice-order(X;as;bs) ∈ ℙ)
Lemma: flattice-order_transitivity
∀[X:Type]. ∀as,bs,cs:(X + X) List List. (flattice-order(X;as;bs)
⇒ flattice-order(X;bs;cs)
⇒ flattice-order(X;as;cs))
Lemma: flattice-order-append
∀X:Type. ∀a1,b1,as,bs:(X + X) List List.
(flattice-order(X;a1;b1)
⇒ flattice-order(X;as;bs)
⇒ flattice-order(X;a1 @ as;b1 @ bs))
Lemma: flattice-order-meet
∀X:Type. ∀a1,b1,as,bs:(X + X) List List.
(flattice-order(X;a1;b1)
⇒ flattice-order(X;as;bs)
⇒ flattice-order(X;free-dl-meet(a1;as);free-dl-meet(b1;bs)))
Definition: flattice-equiv
flattice-equiv(X;x;y) ==
↓∃as,bs:(X + X) List List
((x = as ∈ Point(free-dl(X + X)))
∧ (y = bs ∈ Point(free-dl(X + X)))
∧ flattice-order(X;as;bs)
∧ flattice-order(X;bs;as))
Lemma: flattice-equiv_wf
∀[X:Type]. ∀[x,y:Point(free-dl(X + X))]. (flattice-equiv(X;x;y) ∈ ℙ)
Lemma: flattice-equiv-equiv
∀[X:Type]. EquivRel(Point(free-dl(X + X));x,y.flattice-equiv(X;x;y))
Definition: f-lattice
f-lattice(X) == free-dl(X + X)//x,y.flattice-equiv(X;x;y)
Lemma: f-lattice_wf
∀[X:Type]. (f-lattice(X) ∈ BoundedDistributiveLattice)
Definition: distributive-lattice-cat
BddDistributiveLattice ==
Cat(ob = BoundedDistributiveLattice;
arrow(G,H) = Hom(G;H);
id(G) = λx.x;
comp(G,H,K,f,g) = g o f)
Lemma: distributive-lattice-cat_wf
BddDistributiveLattice ∈ SmallCategory'
Definition: free-dl-functor
FreeDistLattice == functor(ob(X) = free-dl(X);arrow(X,Y,f) = fdl-hom(free-dl(Y);λx.free-dl-generator(f x)))
Lemma: free-dl-functor_wf
FreeDistLattice ∈ Functor(TypeCat;BddDistributiveLattice)
Definition: forget-lattice
ForgetLattice == functor(ob(ltt) = Point(ltt);arrow(G,H,f) = f)
Lemma: forget-lattice_wf
ForgetLattice ∈ Functor(BddDistributiveLattice;TypeCat)
Lemma: free-dist-lattice-adjunction
FreeDistLattice -| ForgetLattice
Home
Index