Wolfgang Jeltsch (Aug 01 2023 at 15:25): Wolfgang Jeltsch (Aug 01 2023 at 15:25):Consider the following minimal example:
codatatype 'a option_stream =
OptionCons ‹'a option› ‹'a option_stream›
corec example :: "unit option_stream" where
"example = OptionCons (Some ()) example"
This is rejected by the coinduction package with the following error message:
Proof failed.
1. option_stream.congclp ?R x2 y2 ⟹ rel_option (=) x1 x1
2. x1 = y1 ⟹ option_stream.congclp ?R x2 y2 ⟹ option_stream.congclp ?R x2 y2
The error(s) above occurred for the goal statement⌂:
x1 = y1 ⟹ option_stream.congclp ?R x2 y2 ⟹ option_stream.congclp ?R (OptionCons x1 x2) (OptionCons y1 y2)
When choosing the show_types option, it becomes clear that the proof is to be conducted in a polymorphic setting, because the error message becomes the following one:
Proof failed.
1. option_stream.congclp (?R::?'a option_stream ⇒ ?'a option_stream ⇒ bool) x2 y2 ⟹ rel_option (=) x1 x1
2. x1 = y1 ⟹ option_stream.congclp (?R::?'a option_stream ⇒ ?'a option_stream ⇒ bool) x2 y2 ⟹ option_stream.congclp ?R x2 y2
variables:
x1, y1 :: ?'a option
x2, y2 :: ?'a option_stream
?R :: ?'a option_stream ⇒ ?'a option_stream ⇒ bool
The error(s) above occurred for the goal statement⌂:
(x1::?'a option) = (y1::?'a option) ⟹ option_stream.congclp (?R::?'a option_stream ⇒ ?'a option_stream ⇒ bool) (x2::?'a option_stream) (y2::?'a option_stream) ⟹ option_stream.congclp ?R (OptionCons x1 x2) (OptionCons y1 y2)
Now consider the following non-polymorphic version of the above code:
codatatype unit_option_stream =
UnitOptionCons ‹unit option› ‹unit_option_stream›
corec example' where
"example' = UnitOptionCons (Some ()) example'"
This one succeeds.
What is wrong here? Am I missing something important, or is this a bug in action?
By the way, also the polymorphic example does succeed when using primcorec, but in my actual use case I need corec, because I need to introduce several layers of data constructors in each round.
Wolfgang Jeltsch (Aug 01 2023 at 16:27):I should add that even using corecursive is not an option: it shows me the same error message and fails before even presenting me a proof goal.
Mathias Fleury (Aug 01 2023 at 16:30):I would ask on the mailing list (@Dmitriy Traytel might be around but he is more active on the mailing list)
Mathias Fleury (Aug 01 2023 at 16:30):I assume that unit is used internally as a sentinel value somewhere in a definition
Mathias Fleury (Aug 01 2023 at 16:30):but the specialists are on the mailing list, not here…
Gokul (Aug 01 2023 at 17:02):I have a question, what does "hd []" evaluate to? Actaully I am trying to prove something like "x ∉ (hd ([]))"
Wolfgang Jeltsch (Aug 01 2023 at 17:05):You should start a new thread for this question.
Gokul (Aug 01 2023 at 17:05):Sorry, sure will do the same
Wolfgang Jeltsch (Aug 01 2023 at 17:07):Mathias Fleury said:
I assume that unit is used internally as a sentinel value somewhere in a definition
It rather seems that the use of option causes the problems. If you drop option from the type definition and then use it in the concrete type parameter of the example value (replacing unit by unit option), it works. That said, I think it should also work with option being part of the type.
Dmitriy Traytel (Aug 01 2023 at 20:00):I am reading along here, but am currently on vacation without a device capable of running Isabelle. I‘ll reply properly when I’m back next week. From distance, I can say that we have had problems when some native types (sums, products) showed up explicitly in codatatypes, where they were confusing some of corec‘s tactics. Some of these are documented in the corec tutorial. Maybe this is a similar problem with the option type indeed. Also there is a way of helping corec‘s tactics by providing some additional simp rules via an attribute (forgot the name, corec_simps or the like; this is hopefully also mentioned in the tutorial). Maybe adding option.rel_eq as a simp rule would help here.
Wolfgang Jeltsch (Aug 01 2023 at 21:19):Also there is a way of helping corec‘s tactics by providing some additional simp rules via an attribute (forgot the name, corec_simps or the like; this is hopefully also mentioned in the tutorial). Maybe adding option.rel_eq as a simp rule would help here.
The tutorial mentions the friend_of_corec_simps attribute. Assigning it to option.rel_eq doesn’t help, but this doesn’t seem surprising to me, since friend_of_corec_simps is only about friendship, while my problem seems to have nothing to do with friendship.
I‘ll reply properly when I’m back next week.
I’m very much looking forward to this reply. :smile:
Wolfgang Jeltsch (Aug 01 2023 at 21:21):By the way, this problem also occurs with a user-defined datatype isomorphic to option. In fact, this is where I discovered it first (I have a special-purpose datatype that is isomorphic to option), and the above code is only the “minimal example”.
Wolfgang Jeltsch (Aug 03 2023 at 13:07):I figured out that the same problem occurs when using list instead of option. I have the impression that there is a general problem with using type constructors around occurrences of a type parameter. Note that this is not about having bounded natural functors around occurrences of the corecursive type but rather just around a type parameter. Interestingly, this situation does not occur in any of the examples of the corec tutorial.
Dmitriy Traytel (Aug 08 2023 at 05:32):I have replied on the mailing list.
Last updated: May 02 2024 at 12:29 UTC