Email Gateway (Aug 22 2022 at 11:03): Email Gateway (Aug 22 2022 at 11:03):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I'm having trouble defining this function:
datatype ('T0) List0 =
dCons0: cCons0 (sh0: "'T0") (st2: "'T0 List0") |
dNil0: cNil0
fun length0 where
"length0 xs0 = case_List0
(λfresh fresha. Let fresha
(let x0 = fresh in (λxs1. Numeral1 + length0 xs1)))
0 xs0"
The function package complains:
Unfinished subgoals:
(a, 1, <):
1. ⋀x12 xb. size xb < Suc (size x12)
(a, 1, <=):
1. ⋀x12 xb. size xb ≤ Suc (size x12)
When I change my definition to 'function (sequential)', it turns out that
the recursive call appears to be in no relation with the argument. Now,
I'm wondering if there's some congruence rule missing? Because, if I
unfold 'Let_def' manually and define it like this:
fun length1 where
"length1 xs0 = (case xs0 of cCons0 fresh fresha ⇒ Numeral1 +
length1 fresha | cNil0 ⇒ 0)"
... it is accepted.
Note that the above is auto-generated code produced from some (trusted)
code and hence -- for soundness reasons -- I want to keep pre-processing
at a minimum.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:03):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Lars,
while I do not yet fully understand the reasons, it seems that this
behavior is caused by the unused let-binding "let x0 = fresh in ...". If
we proof a (ad-hoc) congruence rule for such situations, the function
definition is accepted:
lemma [fundef_cong]:
assumes "a = b"
and "⋀x. x = b ⟹ f a = g b"
shows "Let a (Let u (λu. f)) = Let b (Let u (λu. g))"
using assms by auto
However, I didn't think much about it. So there are most likely much
better solutions.
cheers
chris
Email Gateway (Aug 22 2022 at 11:03):From: Christian Sternagel <c.sternagel@gmail.com>
A simpler variant:
lemma [fundef_cong]:
assumes "x = y" and "f y = g y"
shows "Let u (λ_. f) x = Let v (λ_. g) y"
using assms by auto
Email Gateway (Aug 22 2022 at 11:03):From: Lars Hupel <hupel@in.tum.de>
Hi Chris,
while I do not yet fully understand the reasons, it seems that this
behavior is caused by the unused let-binding "let x0 = fresh in ...".
you seem to be on the right track. When I modify my original program to
not bind any unused variables, the problem disappears. I still think
it's rather confusing.
As for the additional congruence rules, I have no idea what the possible
implications could be when adding those. Don't they overwrite the
existing rules? (At least, that's what the simp-cong rules do.)
Cheers
Lars
Last updated: Apr 30 2024 at 04:19 UTC