Write a bit more, enable support for paragraph links
Signedoffby: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
4938cdaecd
commit
ee8b1f5dc0

@ 33,6 +33,10 @@ defaultContentLanguage = 'en'


[markup.goldmark.extensions.passthrough.delimiters]


block = [['\[', '\]'], ['$$', '$$']]


inline = [['\(', '\)']]


[markup.goldmark.parser]


[markup.goldmark.parser.attribute]


block = true


title = true




[languages]


[languages.en]





@ 249,6 +249,7 @@ It turns out to be convenient, however, to not require definitional equality


would force us to consider lists with the same elements but a different


order to be unequal. Instead, we parameterize our definition of `IsSemilattice`


by a binary relation `_≈_`, which we ask to be an [equivalence relation](https://en.wikipedia.org/wiki/Equivalence_relation).


{#definitionalequality}




{{< codelines "Agda" "agdaspa/Lattice.agda" 23 39 >}}







@ 52,10 +52,13 @@ for both types:




Elements of \(L_1 \times L_2\) are in the form \((l_1, l_2)\), where


\(l_1 \in L_1\) and \(l_2 \in L_2\). The first thing we can get out of the


way is define what it means for two such elements to be equal. That's easy


enough: we have an equality predicate `_≈₁_` that checks if an element


way is define what it means for two such elements to be equal. Recall that


we opted for a [custom equivalence relation]({{< relref "01_spa_agda_lattices#definitionalequality" >}})


instead of definitional equality to allow similar elements to be considered


equal; we'll have to define a similar relation for our new product lattice.


That's easy enough: we have an equality predicate `_≈₁_` that checks if an element


of \(L_1\) is equal to another, and we have `_≈₂_` that does the same for \(L_2\).


It's reasonably to say that _pairs_ of elements are equal if their respective


It's reasonable to say that _pairs_ of elements are equal if their respective


first and second elements are equal:




{{< latex >}}



@ 65,3 +68,38 @@ first and second elements are equal:


In Agda:




{{< codelines "Agda" "agdaspa/Lattice/Prod.agda" 39 40 >}}




Verifying that this relation has the properties of an equivalence relation


boils down to the fact that `_≈₁_` and `_≈₂_` are themselves equivalence


relations.




{{< codelines "Agda" "agdaspa/Lattice/Prod.agda" 42 48 >}}




In fact, defining \((\sqcup)\) and \((\sqcap)\) by simply applying the


corresponding operators from \(L_1\) and \(L_2\) seems quite natural as well.




{{< latex >}}


(l_1, l_2) \sqcup (j_1, j_2) \triangleq (l_1 \sqcup_1 j_1, l_2 \sqcup_2 j_2) \\


(l_1, l_2) \sqcap (j_1, j_2) \triangleq (l_1 \sqcap_1 j_1, l_2 \sqcap_2 j_2)


{{< /latex >}}




In Agda:




{{< codelines "Agda" "agdaspa/Lattice/Prod.agda" 50 54 >}}




All that's left is to prove the various (semi)lattice properties. Intuitively,


we can see that since the "combined" operator `_≈_` just independently applies


the element operators `_≈₁_` and `_≈₂_`, as long as they are idempotent,


commutative, and associative, so is the "combined" operator itself.


Moreover, the proofs that `_⊔_` and `_⊓_` form semilattices are identical


up to replacing \((\sqcup)\) with \((\sqcap)\). Thus, in Agda, we can write


the code once, parameterizing it by the binary operators involved (and proofs


that these operators obey the semilattice laws).




{{< codelines "Agda" "agdaspa/Lattice/Prod.agda" 56 82 >}}




Similarly to the semilattice properties, proving lattice properties boils


down to applying the lattice properties of \(L_1\) and \(L_2\) to


individual components.




{{< codelines "Agda" "agdaspa/Lattice/Prod.agda" 84 96 >}}




Loading…
Reference in New Issue
Block a user