Parameterized lists with void elements

This example shows one possible way of dealing with generic lists (with potentially void elements) in CITP, including operations for appending lists – denoted $l_1\! \mathrel{@} l_2$ – computing their lengths – denoted $\text{len}(l)$ – or reversing lists – denoted $\text{rev}(l)$. We prove that the append operation is associative and that, moreover, both the length and the reverse operations distribute over append. In symbols:

1. $ (l_1\!\mathrel{@} l_2) \mathrel{@} l_3 = l_1\!\mathrel{@} (l_2\!\mathrel{@} l_3) $
2. $\text{len}(l_1\!\mathrel{@} l_2) = \text{len}(l_1) + \text{len}(l_2)$
3. $\text{rev}(l_1\!\mathrel{@} l_2) = \text{rev}(l_2) \mathrel{@} \text{len}(l_1)$

Specification

See list.maude for the full specification.

Verification

1. Associativity of append

LISTS |- eq L1:List @(L2:List @ L3:List)=(L1:List @ L2:List)@ L3:List ;

See assoc.maude for the full proof.

2. Distributivity of length over append

LISTS |- eq len(L1:List @ L2:List)= len(L1:List)+ len(L2:List) ;

See distLen.maude for the full proof.

3. Distributivity of reverse over append

LISTS-ASSOC |- eq rev(L1:List @ L2:List)= rev(L2:List)@ rev(L1:List);

See distRev.maude for the full proof.