Chengsong Tan (Feb 07 2024 at 15:21): Chengsong Tan (Feb 07 2024 at 15:21):How to finish a proof like this?
lemma empty_list_switching: "a = [True] ∧ b = [] ∧ c = [] ⟹ length ((tl a @ (hd a) # b @ c)) ≤ 1 ∧ length (a @ b @ c) ≤ 1"
(is "?a ∧ ?b ∧ ?c ⟹ ?l")
proof -
assume "?a ∧ ?b ∧ ?c" thus ?thesis
proof -
have "length (a @ b @ c) ≤ 1"
by (simp add: ‹a = [True] ∧ b = [] ∧ c = []›)
then show ?thesis proof -
have "tl a = []" sorry
have "hd a = True" sorry
have "b = []" sorry
have "c = []" sorry
hence ?thesis
sorry
qed
qed
Isabelle says "failed to finish proof" on the first qed, and if I just say hence ?thesis then I can go on and on forever. What's the method of saying "please finish the entire proof by piecing together the facts I have provided" in Isar?
Please excuse me for this slightly weird example (made up to get a MWE), which comes from my current project while learning Isar, in which I was proving something like this where P, Q etc. are quite large:
lemma empty_list_switching: "P∧ Q ∧ R ⟹ f(P', Q', R')"
(is "?P ∧ ?Q ∧ ?R ⟹ ?f")
proof -
assume "?P ∧ ?Q ∧ ?R" thus ?thesis
proof -
have fact1 about f
<proof for this>
then show ?thesis proof -
have fact 2 about P' sorry
have fact 3 about Q' sorry
have fact 4 about R' sorry
hence ?thesis
sorry
qed
qed
It told you failed to finish proof because you used hence rather than thus. Here is how I would write the proof:
lemma empty_list_switching: "a = [True] ∧ b = [] ∧ c = [] ⟹ length ((tl a @ (hd a) # b @ c)) ≤ 1 ∧ length (a @ b @ c) ≤ 1"
(is "?a ∧ ?b ∧ ?c ⟹ ?l")
proof -
assume *: "?a ∧ ?b ∧ ?c"
then have "length (tl a @ hd a # b @ c) ≤ 1"
by simp
moreover from * have "length (a @ b @ c) ≤ 1"
by simp
ultimately show ?thesis
by simp
qed
I think it's considered bad style to use keywords hence and thus, I'd probably just stick to "then have" and "then show"
Mathias Fleury (Feb 07 2024 at 16:15):Christian Pardillo Laursen said:
I think it's considered bad style to use keywords hence and thus, I'd probably just stick to "then have" and "then show"
Makarius is a strong advocate against thus/hence. But there is no consensus that is is bad style.
Mathias Fleury (Feb 07 2024 at 16:17):My personal experience is that they often end up being expanded when refactoring a proof.
Chengsong Tan (Feb 08 2024 at 01:36):Christian Pardillo Laursen said:
It told you failed to finish proof because you used hence rather than thus. Here is how I would write the proof:
lemma empty_list_switching: "a = [True] ∧ b = [] ∧ c = [] ⟹ length ((tl a @ (hd a) # b @ c)) ≤ 1 ∧ length (a @ b @ c) ≤ 1" (is "?a ∧ ?b ∧ ?c ⟹ ?l") proof - assume *: "?a ∧ ?b ∧ ?c" then have "length (tl a @ hd a # b @ c) ≤ 1" by simp moreover from * have "length (a @ b @ c) ≤ 1" by simp ultimately show ?thesis by simp qed
Thank you Christian! This style is much nicer to work with.
Last updated: Apr 28 2024 at 16:17 UTC