|
|
|
|
@ -125,7 +125,7 @@ we could take the previous natural number, and it would be a bound as well).
|
|
|
|
|
Thus, I define the `Height` predicate to require that a chain of the desired
|
|
|
|
|
height exists, and that this height bounds the length of all other chains.
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Chain.agda" 47 53 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Chain.agda" 47 48 >}}
|
|
|
|
|
|
|
|
|
|
Finally, for a lattice to have a finite height, the type of chains formed by using
|
|
|
|
|
its less-than operator needs to have that height (satisfy the `Height h` predicate).
|
|
|
|
|
@ -133,7 +133,7 @@ To avoid having to thread through the equivalence relation, congruence proof,
|
|
|
|
|
and more, I define a specialized predicate for lattices specifically.
|
|
|
|
|
I do so as a "method" in my `IsLattice` record.
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice.agda" 183 210 "hl_lines = 27 28">}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice.agda" 153 180 "hl_lines = 27 28">}}
|
|
|
|
|
|
|
|
|
|
Thus, bringing the operators and other definitions of `IsLattice` into scope
|
|
|
|
|
will also bring in the `FixedHeight` predicate.
|
|
|
|
|
@ -192,7 +192,7 @@ three or more comparisons.
|
|
|
|
|
Thus, the above-below lattice has a length of two comparisons (or alternatively,
|
|
|
|
|
three elements).
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 363 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 358 >}}
|
|
|
|
|
|
|
|
|
|
And that's it.
|
|
|
|
|
|
|
|
|
|
@ -262,7 +262,7 @@ be collapsed into \(f(a) \not< f(a)\), changing its length. Finally,
|
|
|
|
|
the function needs to produce equivalent outputs when giving equivalent inputs.
|
|
|
|
|
The result is the following lemma:
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice.agda" 226 247 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice.agda" 196 217 >}}
|
|
|
|
|
|
|
|
|
|
Given this, and two lattices of finite height, we construct the full product
|
|
|
|
|
chain by lifting the `A` chain into the product via \(a \mapsto (a, \bot_2)\),
|
|
|
|
|
@ -270,7 +270,7 @@ lifting the `B` chain into the product via \(b \mapsto (\top_1, b)\), and
|
|
|
|
|
concatenating the results. This works because the first chain ends with
|
|
|
|
|
\((\top_1, \bot_2)\), and the second starts with it.
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 169 171 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 177 179 >}}
|
|
|
|
|
|
|
|
|
|
This gets us the longest chain; what remains is to prove that this chain's
|
|
|
|
|
length is the bound of all other changes. To do so, we need to work in
|
|
|
|
|
@ -292,15 +292,15 @@ and will put the implementation in a collapsible detail block. One last
|
|
|
|
|
detail is that the need to decide which chain to grow --- and thus which element
|
|
|
|
|
has increased --- is what introduces the need for decidable equality.
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 149 149 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 158 158 >}}
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 149 163 "" "**(Click here for the implementation of `unzip`)**" >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 158 172 "" "**(Click here for the implementation of `unzip`)**" >}}
|
|
|
|
|
|
|
|
|
|
Having decomposed the product chain into constituent chains, we simply combine
|
|
|
|
|
the facts that they have to be bounded by the height of the `A` and `B` lattices,
|
|
|
|
|
as well as the fact that they bound the combined chain.
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 165 175 "hl_lines = 8-10" >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 174 183 "hl_lines = 8-9" >}}
|
|
|
|
|
|
|
|
|
|
This completes the proof!
|
|
|
|
|
|
|
|
|
|
@ -326,7 +326,7 @@ lattices as input.
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 7 11 >}}
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 23 24 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 21 22 >}}
|
|
|
|
|
|
|
|
|
|
At a high level, the proof goes by induction on the number of applications
|
|
|
|
|
of the product. There's just one trick. I'd like to build up an `isLattice`
|
|
|
|
|
@ -347,18 +347,18 @@ To build up with the lattice instance and --- if possible --- the finite height
|
|
|
|
|
instance, I needed to allow for the constituent lattices being either finite
|
|
|
|
|
or infinite. I supported this by defining a helper type:
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 40 55 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 34 40 >}}
|
|
|
|
|
|
|
|
|
|
Then, I defined the "everything at once" type, in which, instead of
|
|
|
|
|
a field for the proof of finite height, has a field that constructs
|
|
|
|
|
this proof _if the necessary additional information is present_.
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 57 76 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 42 55 >}}
|
|
|
|
|
|
|
|
|
|
Finally, the proof by induction. It's actually relatively long, so I'll
|
|
|
|
|
include it as a collapsible block.
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 78 120 "" "**(Click here to expand the inductive proof)**" >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/IterProd.agda" 57 95 "" "**(Click here to expand the inductive proof)**" >}}
|
|
|
|
|
|
|
|
|
|
### Fixed Height of the Map Lattice
|
|
|
|
|
|
|
|
|
|
@ -472,11 +472,11 @@ As you can tell, the chain porting mechanism is doing the heavy lifting here.
|
|
|
|
|
It's relatively easy to implement given the conditions we've set on
|
|
|
|
|
conversion functions, in both directions:
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Isomorphism.agda" 52 64 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Isomorphism.agda" 51 63 >}}
|
|
|
|
|
|
|
|
|
|
With that, we can prove the second lattice's finite height:
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Isomorphism.agda" 66 80 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Isomorphism.agda" 65 72 >}}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The conversion functions are also not too difficult to define. I give
|
|
|
|
|
@ -485,12 +485,12 @@ properties (such as the fact that `from` and `to` are inverses, preserve
|
|
|
|
|
equivalence, and distribute over join) here. You can view them by clicking
|
|
|
|
|
the link at the top of the code block below.
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/FiniteValueMap.agda" 68 85 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/FiniteValueMap.agda" 67 84 >}}
|
|
|
|
|
|
|
|
|
|
Above, `FiniteValueMap ks` is the type of maps whose keys are fixed to
|
|
|
|
|
`ks`; defined as follows:
|
|
|
|
|
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/FiniteMap.agda" 58 60 >}}
|
|
|
|
|
{{< codelines "agda" "agda-spa/Lattice/FiniteMap.agda" 50 52 >}}
|
|
|
|
|
|
|
|
|
|
Proving the remaining properties (which as I mentioned, I omit from
|
|
|
|
|
the main body of the post) is sufficient to apply the isomorphism,
|
|
|
|
|
|