Email Gateway (Aug 22 2022 at 14:11): Email Gateway (Aug 22 2022 at 14:11):From: Thomas Sternagel <Thomas.Sternagel@uibk.ac.at>
Dear list,
another question on corecursion and friends in Isabelle/HOL development
version 6703434c96d6:
In theory 'Foo' below I am able to show that function "some" which
depends on an inductive set "A" is friendly but when I try to do the
same for function "some'" defined similarly but depending on the
inductive set "C X" instead, I get the error message:
"Eps" not polymorphic enough to be applied like this and no friend
I'm not quite sure why the former works whereas the latter fails.
Maybe someone besides Jasmin is able to answer this one?
theory Foo
imports
"~~/src/HOL/Library/Stream"
"~~/src/HOL/Library/BNF_Corec"
begin
inductive_set A :: "'a stream set" where "s ∈ A"
primcorec some :: "'a ⇒ 'a stream ⇒ 'a stream" where
"some a s = (let t = SOME v. v ∈ A in SCons a (stl t))"
friend_of_corec some :: "'a ⇒ 'a stream ⇒ 'a stream" where
"some a s = (let t = SOME v. v ∈ A in SCons a (stl t))"
by (auto simp add: stream.expand)
inductive_set C :: "'a set ⇒ 'a stream set" for X :: "'a set" where
"shd s ∈ X ⟹ s ∈ C X"
primcorec some' :: "'a set ⇒ 'a ⇒ 'a stream ⇒ 'a stream" where
"some' X a s = (let t = SOME v. v ∈ C X in SCons a (stl t))"
friend_of_corec some' :: "'a set ⇒ 'a ⇒ 'a stream ⇒ 'a stream" where
"some' X a s = (let t = SOME v. v ∈ C X in SCons a (stl t))"
end
Cheers,
Tom
Email Gateway (Aug 22 2022 at 14:20):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Thomas,
At the heart of "corec" and friends is a procedure we call "surface synthesis". It is described in our paper draft "Friends with Benefits" (found e.g. on my home page).
That synthesis is difficult to explain, but in short, if it succeeds, you still have to prove parametricity of whatever polymorphic constants in ran along the way. And I can already guarantee you that you will not succeed at proving "Eps" parametric, because it is not. (In general, underspecification is a killer for parametricity.)
Cheers,
Jasmin
Last updated: Apr 19 2024 at 04:17 UTC