Email Gateway (Aug 22 2022 at 16:19): Email Gateway (Aug 22 2022 at 16:19):From: Stefan Berghofer <berghofe@in.tum.de>
Dear all,
I recently came across a strange problem with case expressions involving the unit type.
Trying to prove something like
lemma "(case () of () => x) = x"
using "apply simp" causes the new goal
"(case ?M' of () => x) = x"
with a schematic variable to be generated, while "apply auto" just diverges. This slightly odd
behaviour is caused by the rule old.unit.case_cong_weak, whose premise "?M = ?M'" is directly
simplified to "True", rather than proved by reflexivity, which would eliminate the variable ?M'.
Would it make sense to remove this rule from the simpset?
Of course, the above example has been simplified a little. I actually noticed this problem when trying
to provide case syntax for record types, whose "more" fields usually contain the unit element.
Greetings,
Stefan
Email Gateway (Aug 22 2022 at 16:22):From: Stefan Berghofer <berghofe@in.tum.de>
Hi Jasmin,
thanks for your reply.
On 11/03/2017 10:07 AM, Blanchette, J.C. wrote:
Would it make sense to remove this rule from the simpset?
You probably mean out of the "cong" set. By all means as far as I'm concerned.
declare unit.case_cong_weak[cong del]
Yes, that's exactly what I meant. Sorry for being a bit imprecise. Could you take care of this?
I am not that familiar with the setup of the new datatype package.
(No need for the "old." prefix; we're still in a transition phase but these will go away within a couple of releases.)
We could also change "ctr_sugar.ML" so that it doesn't set the "cong" attribute for types that have a single nullary constructor, but it's probably overkill (and wouldn't catch all cardinality-1 cases).
I agree. The above declare command should be completely sufficient.
Greetings,
Stefan
Last updated: Apr 19 2024 at 16:20 UTC