The goal of this lecture note is to introduce lazy lists (i.e., list-like data structures that are constructed on demand instead of inductively and that may be finite), and to the infrastructure to reason about lazy lists.
Unlike lists that are constructed inductively, i.e., from a base case (the empty list) and iteratively using cons, lazy lists are constructed “co-inductively”, i.e., from the beginning towards the end, where this end is constructed on demand. Unlike streams, though, lazy lists might terminate:
CoInductive lazy_list (V : Type) : Type :=
LNil : lazy_list V
| LCons : V -> lazy_list V -> lazy_list V.
Structural equality is an inductive notion, one that only applies to data that are constructed inductively. For lazy lists, the corresponding coinductive notion is known as “bisimilarity”, which translates to “if it is constructed the same, it is the same”:
CoInductive bisimilar : forall (V : Type), (V -> V -> bool) -> lazy_list V -> lazy_list V -> Prop :=
| Bisimilar_LNil :
forall (V : Type)
(eqb_V : V -> V -> bool),
bisimilar V eqb_V (Nil V) (Nil V)
| Bisimilar_LCons :
forall (V : Type)
(eqb_V : V -> V -> bool)
(v1 v2 : V),
eqb_V v1 v2 = true ->
forall v1s v2s : lazy_list V,
bisimilar V eqb_V v1s v2s ->
bisimilar V eqb_V (LCons V v1 v1s) (LCons V v2 v2s).
Prove that bisimilar is an equivalence relation, i.e., that it is reflexive, symmetric, and transitive.
Created [10 Apr 2025]