I'm new to coinduction proofs in Isabelle. I'm able to prove simple bisimulation lemmas on streams. However, once I try to mix coinductive definitions with inductive definitions, Isabelle freezes.
try spins forever on
lemma "take 2 (natsFrom 0) = [0,1]" or even simpler goals like
lemma "shd (natsFrom 0) = 0"
Does this have something to do with Isabelle trying to eagerly evaluate an infinite stream?
does try0/nitpick/sledgehammer/quickcheck individually also loop?
Quickcheck is probably the culprit. What it does is to generate Poly/ML code for the statement in question and evaluate it on example data. However, there is no out-of-the-box support for laziness in Isabelle's code generation to Poly/ML, so anything involving infinite structures like this one will simply loop forever or quickly run out of memory.
So one possible workaround is to just not use QuickCheck here (which means not using
try as well). I for one never use
try at all, I just use
try0 (which tries some typical proof methods like
auto, but no "disproof" methods like QuickCheck and nitpick and not sledgehammer either) or sledgehammer by itself.
Another one is to import
HOL-Library.Code_Lazy and do
code_lazy_type stream to register streams as lazy codatatypes for code generation. Then
QuickCheck seems to work as expected.
Note that QuickCheck is a diagnostic tool that is not at the core of Isabelle. Code generation is a cool feature but is also very much seperate from the reasoning core of Isabelle/HOL. Isabelle/HOL itself has absolutely no problems at all with infinite structures such as these.
So I've annotated the
stream type with
code_lazy_type and I'm able to compute values.
value "take' 3 nats" yields
[0,1,2] this previously spun forever thanks to eager evaluation.
Sledgehammer/try still have no luck on very simple statements like
lemma "take' 3 nats = [0,1,2]"
Sledgehammer is not really made for evaluating terms. Since
take' is probably defined by recursion over
3, the easiest approach to evaluation (if you really do need that) is to prove lemmas like
take' 0 xs =  n > 0 ⟹ take' n xs = shd xs # take' (n - 1) (stl xs)
(assuming that's what the projection functions for your stream type are called) and then add those rules to the simplifier.
In case you're not aware of it, note that we do have stream library in the standard library.
Eric Bond has marked this topic as resolved.
Last updated: Sep 25 2022 at 23:25 UTC