Email Gateway (Aug 22 2022 at 13:04): Email Gateway (Aug 22 2022 at 13:04):From: Lars Hupel <hupel@in.tum.de>
(This is not an April Fool's joke ...)
Dear list,
I have a weird fold combinator, let's call it "fold-left-right". Here's
its definition:
fun foldlr where
"foldlr f [] init = init" |
"foldlr f (x # xs) init = f init x (foldlr f xs)"
In order to use it in functions, I stated a congruence rule:
lemma foldlr_cong[fundef_cong]:
assumes "init1 = init2" "xs1 = xs2"
assumes "⋀acc x. x ∈ set xs1 ⟹ f acc x = g acc x"
shows "foldlr f xs1 init1 = foldlr g xs2 init2"
I started the proof as follows:
using assms
apply (induction f xs1 init1 arbitrary: init2 xs2 rule: foldlr.induct)
apply auto
... but got stuck and well, tried 'try0', which offered me to try
'presburger' (and nothing else!). What is it about 'presburger' that it
can solve that goal, but other provers can't?
Can anyone suggest a more elegant proof?
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:05):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Lars,
nice April Fool’s joke ;-)
Not sure if it is nicer than (auto, presburger) but the following also works:
apply (auto simp: fun_eq_iff intro!: arg_cong[of _ _ "g _ _”])
Dmitriy
Last updated: Nov 21 2024 at 12:39 UTC