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



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


> 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?
> 
> Cheers
> Lars
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.