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?

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 `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.

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.

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]"`

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.

Last updated: Jul 15 2022 at 23:21 UTC