Email Gateway (Aug 18 2022 at 10:37): Email Gateway (Aug 18 2022 at 10:37):From: Gregory Kulczycki <gregwk@vt.edu>
I've been experimenting with the Isabelle prover and have reached a point in
a proof where I have the following subgoal:
/\ xs ys zs. [| hd xs = hd ys; tl xs @ zs = tl ys |] ==> xs @ zs = ys
This looks obvious to me (since xs @ zs = ys is equivalent to hd xs # tl xs
@ zs = hd ys # tl ys for non-empty xs) , but I don't know how to proceed.
Any suggestions?
Thanks,
Greg
Email Gateway (Aug 18 2022 at 10:38):From: Tobias Nipkow <nipkow@in.tum.de>
Your goal is not provable. You need the assumptions that both xs and ys
are non-empty --- see your own proof. If you have those, you can convert
from xs ~= [] to EX a as. xs = a#as (similarly for ys) by simplifying
with neq_Nil_conv. The rest is done by auto.
Tobias
Gregory Kulczycki schrieb:
Email Gateway (Aug 18 2022 at 10:38):From: Amine Chaieb <chaieb@in.tum.de>
Gregory,
I don't think it is provable for xs and ys empty.
lemma assumes xs0: "xs ~= []" and ys0: "ys ~= []" and hd: "hd xs = hd
ys" and tl: "tl xs @ zs = tl ys"
shows "xs @ zs = ys"
proof-
from xs0 ys0 obtain xsh xst ysh yst
where xs: "xs = xsh#xst" and ys: "ys = ysh#yst" apply (cases xs, auto)
apply (cases ys, auto) done
with hd have xsh: "xsh = ysh" by simp
have "ys = xsh#(tl ys)" by (simp add: ys xsh)
also have "... = xsh # xst @ zs" by (simp add: tl[symmetric] xs)
finally show ?thesis by (simp add: xs)
qed
Amin.
Gregory Kulczycki wrote:
Email Gateway (Aug 18 2022 at 10:38):From: Gregory Kulczycki <gregwk@vt.edu>
Since my original lemma said "hd xs = c and hd ys = c" I wrongly assumed
that this implied that xs and ys were non-empty. The neq_Nil_conv lemma
worked well for this proof. Also, the cases method answered a question I had
about another proof.
Thanks!
Greg
Last updated: Nov 21 2024 at 12:39 UTC