I'd like to write down some definitions (and prove some lemmas!) about paths in a graph. Let's say that the graph is given implicitly by a relation of type 'a => 'a => bool. To talk about a possibly infinite path in the graph, I thought a sensible thing was to use a lazy list codatatype like 'a llist as given in "Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL" (datatypes.pdf in the Isabelle distribution).
This works well enough, but I'd then I'd like to define a predicate that takes such a list and a graph relation and evaluates to true iff the list defines a valid path in the graph: any pair of adjacent entries in the list must be an edge.
If I was using 'a list as a type to represent the paths, this would be easy: I'd just define the predicate using primrec. However, the co-inductive definitions I can find all seem to generate or consume the data one element at a time, rather than being able to make a statement about the whole thing. Obviously, I realise that the resulting predicate won't be computable (because it is making a statement about infinite streams), so it might have a \forall in there somewhere, but that's fine - I want to use it for developing a theory, not generating code.
How can I define such a predicate? (And how could I prove the obvious associated introduction and elimination lemmas that make it useful?)
Thanks!
I suppose the most idiomatic way to do this is to use a coinductive predicate. Intuitively, this is like a normal inductive predicate except that you also allow ‘infinite derivation trees’:
type_synonym 'a graph = "'a ⇒ 'a ⇒ bool"
codatatype 'a llist = LNil | LCons 'a "'a llist"
coinductive is_path :: "'a graph ⇒ 'a llist ⇒ bool" for g :: "'a graph" where
is_path_LNil:
"is_path g LNil"
| is_path_singleton:
"is_path g (LCons x LNil)"
| is_path_LCons:
"g x y ⟹ is_path g (LCons y path) ⟹ is_path g (LCons x (LCons y path))"
This gives you introduction rules is_path.intros and an elimination rule is_path.cases.
When you want to show that an inductive predicate holds, you just use its introduction rules; when you want to show that an inductive predicate implies something else, you use induction with its induction rule.
With coinductive predicates, it is typically the other way round: When you want to show that a coinductive predicate implies something else, you just use its elimination rules. When you want to show that a coinductive predicate holds, you have to use coinduction.