Stream: Beginner Questions

Topic: ✔ Coinductive/inductive reasoning


view this post on Zulip 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?

view this post on Zulip Mathias Fleury (Aug 15 2021 at 10:51):

does try0/nitpick/sledgehammer/quickcheck individually also loop?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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]"

view this post on Zulip 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.

view this post on Zulip Notification Bot (Aug 18 2021 at 19:19):

Eric Bond has marked this topic as resolved.


Last updated: Sep 25 2022 at 23:25 UTC