Some Backgrounds
Lattice is an abstract algebraic structure commonly used in static program analysis to explain the termination of recursions or loops. A lattice is a partial-order set where given two elements in the set, we can always find their greatest lower bound and their least upper bound in the set. A partial-order set is a set with a binary operator $\le$, which has three properties (we use $A$ to refer to the set):
(1) Self-reflexivity: $\forall a. a\in A\rightarrow a\le a$
(2) Anti-symmetry: if $a\le b$ and $b\le a$, then $a=b$
(3) Transitivity: if $a\le b$ and $b \le c$, then $a\le c$
In the theory of software analysis, we almost always deal with complete lattices, where every finite non-empty set of elements has its least upper bound and its greatest lower bound. However, almost all materials I saw omit the proof of that every finite lattice is a complete lattice. In this article, I'll show you how to prove it by first proving the associativity of two basic operations: to get the least upper bound of two elements and to get the greatest lower bound of two elements.
In the proof, we use $(L, \le)$ to define a lattice on a partial-order set $L$. We define $a\vee b$ to be the least upper bound of two elements in the lattic: $a$ and $b$. We define $a\wedge b$ to be their greatest lower bound. Note that we don't use '$\vee$' or '$\wedge$' as logical 'or' or 'and' operators.
Lemma 1: Order Preservation
If $a,b,c,d\in (L, \le)$, and $a\le c, b\le d$, then we have $a\vee b\le c\vee d$, also $a\wedge b\le c\wedge d$
Proof:
Let's start by proving the conclusion of least upper bound.
From the definition of least upper bound, we know that $c\le c\vee d$. As $a\le c$, we know that $a\le c\vee d$. In the same way, we can also know that $b\le c\vee d$. Therefore, $c\vee d$ is an upper bound of $a$ and $b$. The least upper bound of $a$ and $b$ must be a lower bound of $c\vee d$, i.e. $$a\vee b\le c\vee d$$
Similarly, we can prove: $$a\wedge b\le c\wedge d$$
$\blacksquare$
Lemma 2: Associativity
If $\alpha,\beta,\gamma\in(L,\le)$, then $(\alpha\wedge\beta)\wedge\gamma=\alpha\wedge(\beta\wedge\gamma)$, also $(\alpha\vee\beta)\vee\gamma=\alpha\vee(\beta\vee\gamma)$
Proof:
Let's start with the greatest lower bound part.
According to the definition of greatest lower bound, we can get that $\alpha\wedge\beta\le\beta$. Lattices have the property of self-reflexivity. Thus, we know that $\gamma\le\gamma$. By lemma 1, we know that $$(\alpha\wedge\beta)\wedge\gamma\le\beta\wedge\gamma$$
On the other hand, we know that $$(\alpha\wedge\beta)\wedge\gamma\le\alpha\wedge\beta\le\alpha$$
From the two results above, we can know that $(\alpha\wedge\beta)\wedge\gamma$ is a lower bound of $\alpha$ and $(\beta\wedge\gamma)$ and thus must be a lower bound of the greatest lower bound of both, i.e. $$(\alpha\wedge\beta)\wedge\gamma\le\alpha\wedge(\beta\wedge\gamma)$$
Similarly, we can prove $$\alpha\wedge(\beta\wedge\gamma)\le(\alpha\wedge\beta)\wedge\gamma$$
Lattices have the property of anti-symmetry. Therefore, we conclude that $$\alpha\wedge(\beta\wedge\gamma)=(\alpha\wedge\beta)\wedge\gamma$$
In the same way can we prove that $(\alpha\vee\beta)\vee\gamma=\alpha\vee(\beta\vee\gamma)$. The lemma is now proved.
$\blacksquare$
Lemma 3: Finite Completeness
Every finite non-empty subset of $L$ has its greatest lower bound and its least upper bound in $L$.
Proof:
We do the least upper bound first.
Assume that $S=\{a_1, a_2, ..., a_{|s|}\}$, then for any element $a_i$, $a_i\le a_i\vee(\vee_{a\in S-{a_i}}\ a) = (\vee_{a\in S}\ a)$ must hold. It means that $(\vee_{a\in S}\ a)$ is an upper bound of $S$. It's obvious that $(\vee_{a\in S}\ a)$ is an element in $L$. This can be explained by the associativity of the get-least-upper-bound operation and the definition of lattice.
Suppose there exists another upper bound of $S$, named $x$, then it holds that $$\forall a. a\in S\rightarrow a\le x$$
By repeatedly applying lemma 1 and lemma 2 on $S$, we can get: $$ a_1\vee a_2\vee ... \vee a_{|S|} = \vee_{a\in S}\ a \le x\vee x\vee ...\vee x = x$$
You can see that every upper bound of $S$ other than $(\vee_{a\in S}\ a)$ cann't be lower than $(\vee_{a\in S}\ a)$, i.e. $(\vee_{a\in S}\ a)$ is the least upper bound of $S$.
Similarly, we can prove that $(\wedge_{a\in S}\ a)$ is the greatest lower bound of $S$.
$\blacksquare$
Theorem: Completeness of Finite Lattices
Every non-empty finite lattice is a complete lattice
Proof:
In the proof of lemma 3, make $S$ be $L$.
$\blacksquare$
After the Proof
In fact, there is an equivalent definition of lattice, where we define '$\vee$' and '$\wedge$' to be commutative, associative, idempotent and absorptive. From that definition, we need to prove that given two elements $a$ and $b$ in a lattice, $a\vee b$ is their least upper bound and $a\wedge b$ is their greatest lower bound.
You may think the conclusion is obvious and may wonder why we need to use such a long proof. It's obvious because you regard $\vee$ and $\wedge$ as ordinary arithmetic operators like plus and multiplication, which are inherently associative. But the two operations on lattices are abstract and may not be associative. The definitions of the two operations before the proof don't tell us they are associative, so we have to prove that first. The key point of the proof is to show that the associativity law holds on both operations.
