Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] pairs and friends

Email Gateway (Aug 22 2022 at 14:11):

From: Thomas Sternagel <Thomas.Sternagel@uibk.ac.at>
Dear mailing list,

In Isabelle/HOL development version 6703434c96d6 I have the following
problem: I want to have a friendly function 'foo' (which I reduced so
much, that it does not do anything useful anymore for sake of a minimal
example). If I use the type "a list ⇒ 'a stream ⇒ 'a stream" everything
works out as expected, but if I switch to streams of pairs, like shown
below I get the following error message:

Cannot have type variable "'a" in the argument types when it does not
occur in the result type

Now "'a" clearly appears in the result type, so I don't see what is
going wrong.

theory Foo
imports
"~~/src/HOL/Library/Stream"
"~~/src/HOL/Library/BNF_Corec"
begin
primcorec foo :: "'a list ⇒
('a × 'a) stream ⇒ ('a × 'a) stream" where
"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"

friend_of_corec foo :: "'a list ⇒
('a × 'a) stream ⇒ ('a × 'a) stream" where
"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"

end

Cheers,
Tom

Email Gateway (Aug 22 2022 at 14:11):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Thomas,

I'm on vacation for two weeks starting today and won't be able to look into this until then. I hope we can support your function. In any case, the error message is wrong. Hopefully, you can either wait until then or find a workaround.

Cheers,

Jasmin

Email Gateway (Aug 22 2022 at 14:11):

From: Thomas Sternagel <Thomas.Sternagel@uibk.ac.at>
I see. Have a nice vacation. I will try to figure something out.
Thanks,
Tom

Email Gateway (Aug 22 2022 at 14:11):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Tom,

an admittedly ugly temporary workaround is to use a separate codatatype for streams of pairs:

codatatype 'a pairstream = SCons (shd: "'a × 'a") (stl: "'a pairstream”)

corecursive (friend) foo :: "'a list ⇒ 'a pairstream ⇒ 'a pairstream" where
"foo us T = (case us of
[] ⇒ SCons (shd T) (stl T)
| u # us ⇒ SCons (shd T) (stl T))"
unfolding relator_eq[symmetric] by transfer_prover

Cheers,
Dmitriy

Email Gateway (Aug 22 2022 at 14:12):

From: Thomas Sternagel <Thomas.Sternagel@uibk.ac.at>
Dear Jasmin,

On 10/24/2016 11:08 AM, Jasmin Blanchette wrote:

Dear Thomas,

In Isabelle/HOL development version 6703434c96d6 I have the following
problem: I want to have a friendly function 'foo' (which I reduced so
much, that it does not do anything useful anymore for sake of a minimal
example). If I use the type "a list ⇒ 'a stream ⇒ 'a stream" everything
works out as expected, but if I switch to streams of pairs, like shown
below I get the following error message:

Cannot have type variable "'a" in the argument types when it does not
occur in the result type

Thank you for the bug report.

In principle, I believe your example could be made to work. Unfortunately, I tried a few solutions and they all break some subtle invariants in our construction. I suspect I would need at least one day to work this out.

For the moment, I have merely improved the message and documented the limitation.

How important is this for you? Have you found a satisfactory work-around in the meantime? I doubt I will get around to removing this limitation in time for the release (Makarius is planning to branch off from development branch on Friday), but it's on my TODO list along with some wishes by Andreas Lochbihler.

since this is not the only problem in my formalization relying on
corecursion, I abandoned it for the time being.
I will have to rethink my overall approach.
So at the moment it is not very urgent.

Cheers,

Jasmin

Thanks,
Tom

Email Gateway (Aug 22 2022 at 14:15):

From: Thomas Sternagel <Thomas.Sternagel@uibk.ac.at>
Thanks for the tip, Dmitriy. I will try it.

Cheers,
Tom

Last updated: Nov 21 2024 at 12:39 UTC