Re: [isabelle] [Noob] Proof on trees



Very nice explanation Bertram. Thanks a lot!
Em 28/05/2016 22:04, "Bertram Felgenhauer via Cl-isabelle-users" <
cl-isabelle-users at lists.cam.ac.uk> escreveu:

> Alfio Martini wrote:
> > Hi Daniel,
> > ,
> > I am especially also interested in knowing why the structured proofs goes
> > thorugh using just the simplifier and the script fails to succeed.
>
> When faced with proving
>
>   "dfs1 (Node tr1 a tr2) @ xs = dfs2 (Node tr1 a tr2) xs"
>
> the simplifier first unfolds the left-hand side to
>
>   "(dfs1 tr1 @ a # dfs1 tr2) @ xs"
>
> At this point, there are two possibilities:
>
> a) use the induction hypothesis and rewrite that term further to
>
>     "dfs2 tr1 (a # dfs1 tr2) @ xs"
>
>   at which point the simplifier gets stuck; in fact it's hard to
>   make progress from here because the xs is outside of the call
>   "dfs2 tr1 ...", but the right-hand side will expand to
>   "dfs2 tr1 (a # dfs2 tr2 xs)" with the xs inside of the
>   "dfs2 tr1 ..." call.
>
> b) use the associativity of append and its definition to obtain
>
>     "dfs1 tr1 @ a # dfs1 tr2 @ xs"
>
>   and only then apply the induction hypothesis which results in
>
>     "dfs2 tr1 (a # dfs2 tr2 xs)"
>
> Unfortunately, if the induction hypothesis is available for
> simplification, the simplifier prefers a) and the proof fails.
>
> The following works, but looks fragile:
>
>   lemma "dfs1 tr @ xs = dfs2 tr xs"
>   proof (induction tr arbitrary: xs)
>     case Tip
>     show ?case by simp
>   next
>     case (Node tr1 a tr2)
>     show ?case
>       apply simp
>       apply (simp add: Node.IH)
>     done
>   qed
>
> I would prove the symmetric version of the lemma which avoids these
> complications:
>
>   lemma dfs2_dfs1_conv: "dfs2 t xs = dfs1 t @ xs"
>   by (induct t arbitrary: xs) auto
>
> Cheers,
>
> Bertram
>
>



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