Machine Logic

Coinductive puzzle, by Jasmin Blanchette and Dmitriy Traytel

08 Nov 2023

Coinduction has a reputation for being esoteric, but there are some situations where it is close to indispensable. One such scenario arose during an Isabelle refinement proof for a verified automatic theorem prover for first-order logic, a proof that also involved Anders Schlichtkrull. In that prover, execution traces can be finite or infinite, reflecting the undecidability of first-order logic. The refinement proof involves a simulation argument between two layers: an abstract specification and a concrete theorem prover, both given as transition systems (i.e., binary relations over states). A single “big” step of the concrete prover represents an entire iteration of the prover’s main loop and may therefore correspond to multiple “small” steps of the abstract prover.

The simulation proof requires relating the concrete layer with the abstract layer. The concrete “big-step” sequence is of the form $St_0 \leadsto^+ St_1 \leadsto^+ St_2 \leadsto^+ \cdots$, where the $St_i$’s are states and $\leadsto^+$ is the transitive closure of the abstract transition system. However, to complete the refinement, we must obtain a “small-step” sequence $St_0 \leadsto \cdots \leadsto St_1 \leadsto \cdots \leadsto St_2 \leadsto \cdots$.

If the big-step sequence is finite, the existence of the small-step sequence can be proved using induction. But in our semidecidable scenario, sequences may be infinite. One way to cope with this is to use coinductive methods. This blog entry presents a solution to this coinductive puzzle.

Preliminaries

To represent possibly infinite sequences of states, we use the coinductive datatype of lazy lists:

codatatype 'a llist = LNil | LCons 'a "'a llist"

Intuitively, lazy lists are like ordinary finite lists, except that they also allow infinite values such as LCons 0 (LCons 1 (LCons 2 ...)). However, the reasoning principles for coinductive types and predicates are rather different from their inductive counterparts, as we will see in a moment.

Let us review some useful vocabulary for lazy lists. First, the selectors lhd : 'a llist -> 'a and ltl : 'a llist -> 'a llist return the head and the tail, respectively, of an LCons value. For an LNil value, lhd returns a fixed arbitrary value and ltl returns LNil. Then the function llast : 'a llist -> 'a returns the last value of a finite lazy list. If there is no such value, because the lazy list is either empty or infinite, llast returns a fixed arbitrary value. Next, the function prepend concatenates a finite list and a lazy list:

fun prepend :: "'a list -> 'a llist -> 'a llist" where
  "prepend [] ys = ys"
| "prepend (x # xs) ys = LCons x (prepend xs ys)"

In the simulation proof, we do not work with arbitrary lazy lists but with nonempty lazy lists whose consecutive elements are related by the small-step or big-step transition relation. To capture this restriction, we use a coinductive predicate that characterizes such chains:

coinductive chain :: "('a ⇒ 'a ⇒ bool) ⇒ 'a llist ⇒ bool" for R :: "'a ⇒ 'a ⇒ bool" where
  "chain R (LCons x LNil)"
| "chain R xs ⟹ R x (lhd xs) ⟹ chain R (LCons x xs)"

The predicate has two introduction rules, one for singleton chains and one for longer chains. Had we worked with finite lists instead of lazy lists, we would have written the same definition replacing the coinductive keyword with inductive. The magic of coinduction allows us to apply the second introduction rule infinitely often. This is necessary when proving that an infinite lazy list forms a chain.

The big-step sequence should be a subsequence of the small-step sequence. We formalize coinductive subsequences via the predicate emb:

coinductive emb :: "'a llist ⇒ 'a llist ⇒ bool" where
  "lfinite xs ⟹ emb LNil xs"
| "emb xs ys ⟹ emb (LCons x xs) (prepend zs (LCons x ys))"

Our definition requires that finite lazy lists may not be embedded in infinite lazy lists. In our application, this matters because we want to ensure that only finite small-step sequences can simulate finite big-step sequences.

In Isabelle, a coinductive predicate P is accompanied by corresponding coinduction principles that allow us to prove positive statements of the form P .... For chain and emb we obtain the following principles:

X xs ⟹
(⋀xs'. X xs' ⟹
      (∃x. xs' = LCons x LNil) ∨
      (∃xs x. xs' = LCons x xs ∧ (X xs ∨ chain R xs) ∧ R x (lhd xs))) ⟹
chain R xs

X xs ys ⟹
(⋀xs' ys'.
    X xs' ys' ⟹
    (∃ys. xs' = LNil ∧ ys' = ys ∧ lfinite ys) ∨
    (∃xs ys x zs. xs' = LCons x xs ∧ ys' = prepend zs (LCons x ys) ∧ (X xs ys ∨ emb xs ys))) ⟹
emb xs ys

These principles embody the fact that chain and emb are the greatest (“most true”) predicates stable under the application of their respective introduction rules. For example for emb, given a binary relation X stable under emb’s introduction rules, any arguments satisfying X also satisfy emb. Stability under introduction rules means that for any arguments xs' and ys' satisfying X that correspond to the arguments of emb in either one of emb’s two introduction rules, the arguments of the self-calls also satisfy X.

The main theorem

We are now ready to state our desired theorem:

lemma "chain R⇧+⇧+ xs ⟹ ∃ys. chain R ys ∧ emb xs ys ∧ lhd ys = lhd xs ∧ llast ys = llast xs"

In words, given a big-step sequence xs whose consecutive elements are related by the transitive closure R⇧+⇧+ of a relation R, there exists a small-step sequence ys whose consecutive elements are related by R. The small-step sequence must embed, using emb, the big-step sequence. In addition, the sequences’ first and last elements must coincide. If both sequences are infinite, their last elements are equal by definition to the same fixed arbitrary value, as explained above.

The proof

To prove the theorem, we instantiate the existential quantifier with a witness, which we define corecursively:

corec wit :: "('a ⇒ 'a ⇒ bool) ⇒ 'a llist ⇒ 'a llist" where
  "wit R xs = (case xs of LCons x (LCons y xs) ⇒
     LCons x (prepend (pick R x y) (wit R (LCons y xs))) | _ ⇒ xs)"

The wit function fills the gaps between consecutive values of the big-step sequence with arbitrarily chosen intermediate values that form finite chains. We use Hilbert’s choice operator to construct these chains:

definition pick :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ 'a list" where
  "pick R x y = (SOME xs. chain R (llist_of (x # xs @ [y])))"

Here, llist_of converts finite lists to lazy lists, which allows us to reuse the chain predicate. The pick function is characterized by the following property:

lemma "R⇧+⇧+ x y ⟹ chain R (llist_of (x # pick x y @ [y]))"

Going back to wit’s definition, we may wonder why Isabelle accepts it in the first place. The definition is not obviously productive, a requirement that would ensure its totality. Productive definitions generate at least one constructor after calling themselves. In our case, LCons is that constructor, but prepend stands in the way and could potentially destroy constructors produced by the self-call to wit. However, we know that prepend is friendly enough to only add constructors and not to remove them. In Isabelle, we can register it as a “friend”, which convinces our favorite proof assistant to accept the above definition.

It remains to prove the four conjuncts of our main theorem, taking ys to be wit R xs.

First, we prove chain R⇧+⇧+ xs ⟹ lhd (wit R xs) = lhd xs by simple rewriting.

Second, we attempt to show chain R⇧+⇧+ xs ⟹ emb xs (wit R xs) using emb’s coinduction principle. To this end, Isabelle’s coinduction proof method instantiates X with the canonical relation λxs ys. ys = wit xs ∧ chain R⇧+⇧+ xs. After some simplification, we arrive at a goal requiring us to prove (∃zs. LCons x (prepend (pick x y) (wit (LCons y xs))) = prepend zs (LCons x (wit (LCons y xs)))) whose two side have the prepend in different positions (on one side before the x, on the other side after). We would like to insert a second prepend zs' (where zs' would be existentially quantified) on the right-hand side, so that we can instantiate zs with the empty list and zs' with pick x y, making both sides equal. We can achieve this by modifying X to be λxs ys. ∃zs'. ys = prepend zs' (wit xs) ∧ chain R⇧+⇧+ xs. A more principled alternative is to manually derive the following generalized coinduction principle, which inserts prepend zs' at the right place:

X xs ys ⟹
(⋀xs' ys'.
    X xs' ys' ⟹
    (∃ys. xs' = LNil ∧ ys' = ys ∧ lfinite ys) ∨
    (∃xs ys x zs zs'. xs' = LCons x xs ∧ ys' = prepend zs (LCons x (prepend zs' ys)) ∧ (X xs ys ∨ emb xs ys))) ⟹
emb xs ys

This approach is an instance of a general technique called coinduction up to.

Third, we need to prove chain R⇧+⇧+ xs ⟹ llast (wit R xs) = llast xs. Since we now know that emb xs (wit R xs) holds, by definition of emb only two cases are possible. Either both wit R xs and xs are finite lazy lists, in which case the property follows by induction, or both are infinite, in which case their last elements are equal to the notorious fixed arbitrary value.

Fourth, when attempting to prove chain R⇧+⇧+ xs ⟹ chain R (wit R xs), we run into a similar issue as in the proof of the second conjunct. The resolution is also similar. We manually derive a coinduction-up-to principle for chain with respect to prepend:

X xs ⟹
(⋀xs'. X xs' ⟹
      (∃x. xs' = LCons x LNil) ∨
      (∃xs x zs'. xs' = LCons x (prepend zs' xs) ∧ (X xs ∨ chain R xs) ∧ chain R (llist_of (y # zs' @ [lhd xs])))) ⟹
chain R xs

This principle additionally involves a generalization of the side condition R y (lhd xs) to chain R (llist_of (y # zs' @ [lhd xs])) to incorporate zs'.

Conclusion

We successfully solved the coinductive puzzle that arose during our verification of an automatic theorem prover. At its core, the puzzle has little to do with theorem proving; instead, it is about refinement of possibly nonterminating transition systems. Our proof can be found in the AFP. On the plus side, Isabelle conveniently allowed us to define all the functions and predicates we needed to carry out the proof, including functions whose productivity relied on “friends”. On the minus side, the proof of an easy-looking theorem required some ingenuity. In particular, we found ourselves deriving coinduction-up-to principles for coinductive predicates manually to use them for definitions involving “friends”. An avenue for future work would be to derive such principles automatically.