Eric Bond (Aug 13 2021 at 23:43): Eric Bond (Aug 13 2021 at 23:43):Hello!
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.
ex)
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?
Mathias Fleury (Aug 15 2021 at 10:51):does try0/nitpick/sledgehammer/quickcheck individually also loop?
Manuel Eberl (Aug 15 2021 at 11:15):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 blast and 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.
Manuel Eberl (Aug 15 2021 at 11:17):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.
Eric Bond (Aug 16 2021 at 23:20):Thanks!
So I've annotated the stream type with code_lazy_type and I'm able to compute values.
ex 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]"
Manuel Eberl (Aug 17 2021 at 05:45):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.
Notification Bot (Aug 18 2021 at 19:19):Eric Bond has marked this topic as resolved.
Last updated: Dec 21 2024 at 16:20 UTC