Email Gateway (Aug 01 2023 at 17:27): Email Gateway (Aug 01 2023 at 17:27):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hello!
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 sort of 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.
I don’t see a convincing reason why the first example shouldn’t work as
well. Am I missing something important or is this behavior not intended?
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.
All the best,
Wolfgang
Email Gateway (Aug 08 2023 at 05:37):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Wolfgang,
Thank you for the report. Indeed one of corec’s tactics was not powerful enough to finish the proof. I have amended the tactic in the development repository (isabelle/e72f8009a4f0) and your minimal example should work in the forthcoming release candidates. Please let me know if the actual, non-minimal example also works.
@Jasmin: you may want to have a look at my change. I’m never entirely sure of what invariants I might be violating in corec. But my patch fixes Wolfgang’s example and does not break existing corec examples.
Best wishes,
Dmitriy
Email Gateway (Aug 08 2023 at 13:16):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hi, Dmitriy!
Thanks a lot for the improvement. Yes, the respective error messages are
gone also for the real code.
That said, there are more error messages, which I had seen already
before but considered to perhaps come from the same problem. The
following code exemplifies these:
codatatype ('m, 'r) process =
Return ‹'r› |
Send ‹'m
option› |
Receive ‹'m ⇒ ('m, 'r) process›
corec nothing where
"nothing = Return ()"
The following error messages are shown:
Tactic failed
The error(s) above occurred for the goal statement⌂:
rel_fun (rel_sum R2 (rel_sum (=) (rel_fun (=) R1))) (rel_pre_process R2 R1) Abs_process_pre_process Abs_process_pre_process
Tactic failed
The error(s) above occurred for the goal statement⌂:
rel_fun (rel_pre_process R2 R1) (rel_sum R2 (rel_sum (=) (rel_fun (=) R1))) Rep_process_pre_process Rep_process_pre_process
The above example seems to be minimal. When trying to shrink it further,
I tripped over another error message. I tried the following code:
codatatype ('m, 'r) process =
Return ‹'r› |
Send ‹'m option› |
Receive ‹'m ⇒ unit›
corec nothing where
"nothing = Return ()"
This resulted in the following error message:
exception Option raised (line 83 of "General/basics.ML")
Sorry for bothering you with so many error messages. :wink: Any chance to
overcome the issues behind them?
All the best,
Wolfgang
Email Gateway (Aug 08 2023 at 14:07):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Wolfgang,
Thanks for these examples. I have another patch now running on testboard (https://ci.isabelle.systems/jenkins/job/testboard/930/), that should improve the tactic failures for theorems involving Abs/Rep. The resolution is the same as in the previous case, but this time two different tactics are involved. I will push it if the testboard run goes through.
The other error message is funnier. If you remove the Receive constructor you will see a user-friendlier error message that explains why this cannot work:
Noncorecursive codatatypes are not supported (try "definition" instead of "corec”)
I’m not sure why the nice error message is replaced with the low-level error, but since this is not supposed to work anyway, I guess this is not as urgent.
Best wishes,
Dmitriy
Email Gateway (Aug 09 2023 at 13:30):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Am Dienstag, dem 08.08.2023 um 14:07 +0000 schrieb Dmitriy Traytel:
Hi Wolfgang,
Hello, hello! :smile:
Thanks for these examples. I have another patch now running on
testboard (https://ci.isabelle.systems/jenkins/job/testboard/930/),
that should improve the tactic failures for theorems involving
Abs/Rep. The resolution is the same as in the previous case, but this
time two different tactics are involved. I will push it if the
testboard run goes through.
Great! Thanks a lot. Could you ping us on the mailing list once your
patch is pushed and also tell us its ID?
The other error message is funnier. If you remove the Receive
constructor you will see a user-friendlier error message that explains
why this cannot work:Noncorecursive codatatypes are not supported (try "definition" instead of "corec”)
Oh, indeed I accidentally removed the last occurrence of actual
corecursion. :sweat_smile:
Best wishes,
Dmitriy
All the best,
Wolfgang
Email Gateway (Aug 09 2023 at 13:33):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Wolfgang,
It is pushed as isabelle/da437a9f2823.
Best wishes,
Dmitriy
Email Gateway (Aug 09 2023 at 21:22):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
My real code now works. Great! Thanks a lot for making this happen.
All the best,
Wolfgang
Last updated: Apr 28 2024 at 16:17 UTC