Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A congruence rule proven by 'presburger'?


view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC