Re: [isabelle] A congruence rule proven by 'presburger'?
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 _ _â])
> On 01 Apr 2016, at 20:51, Lars Hupel <hupel at in.tum.de> wrote:
> (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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and