John Hughes (Jan 28 2025 at 12:48): John Hughes (Jan 28 2025 at 12:48):Following up on Moritz R's question from a while back, I tried to use "presume" in a "it suffices to prove that..." kind of way.
I started with this proof that x^2 + xy + y^2 >= 0 for real x and y:
theory Scratch
imports Main Complex_Main
begin
lemma squareNN:
fixes x::real
shows "x^2 ≥ 0"
proof -
show ?thesis by simp
qed
lemma twoSquares:
fixes x::real and y::real
shows "0 ≤ x^2 + y^2"
proof-
show ?thesis using squareNN by simp
qed
lemma
fixes x::real and y::real
shows "x^2 + x*y + y^2 ≥ 0"
proof -
have 1: "4*x^2 +4* x*y + 4*y^2 = (4*x^2 + 4*x*y + (y^2)) + 3*y^2" by simp
have 2: "(4*x^2 + 4*x*y + y^2) = (2*x + y)^2" by (simp add: power2_sum)
have 3: "4*x^2 +4* x*y + 4*y^2 = (2*x + y)^2 + 3*y^2" using 1 2 by simp
have 4: "0 ≤ (2*x + y)^2 + 3*y^2" using 3 twoSquares [of "(2*x +y)" "y" ] by simp
have 5: "0 ≤ 4*x^2 +4* x*y + 4*y^2" using 3 4 by presburger
show ?thesis using 5 by auto
end
As you can see, I prove something about 4 times the quantity of interest, and then get to the thesis at the very end. I wanted to invert this to say "to prove the original, it suffices to show that 0 ≤ 4*x^2 +4* xy + 4y^2, and then go about proving that. So I wrote
lemma
fixes x::real and y::real
shows "x^2 + x*y + y^2 ≥ 0"
proof -
presume 0: "0 ≤ 4*x^2 + 4*x*y + 4*y^2"
show ?thesis using 0 by auto
have 1: "4*x^2 +4* x*y + 4*y^2 = (4*x^2 + 4*x*y + (y^2)) + 3*y^2" by simp
have 2: "(4*x^2 + 4*x*y + y^2) = (2*x + y)^2" by (simp add: power2_sum)
have 3: "4*x^2 +4* x*y + 4*y^2 = (2*x + y)^2 + 3*y^2" using 1 2 by simp
have 4: "0 ≤ (2*x + y)^2 + 3*y^2" using 3 twoSquares [of "(2*x +y)" "y" ] by simp
have 5: "0 ≤ 4*x^2 + 4*x*y + 4*y^2" using 4 3 by presburger
show ?thesis using 5 by blast (* FAILS *)
end
When I got to that "next to last" line , the proof-state shows that "this" and the "goal" are identical, but I cannot figure out how to close things out. The "show ?thesis" ends up using the original thesis (x^2 + xy + y^2 >= 0), so that's obviously wrong. Can someone suggest the correct final line to this proof?
Balazs Toth (Jan 28 2025 at 15:10):It's actually the first time that I hear of presume, but I think I figured out how to use it. This should be the typical pattern on how to use it:
lemma
assumes "A" "A ⟹ B"
shows "B"
proof-
presume A: "A"
then show ?thesis
using assms(2)
by simp
next
show "A"
using assms(1)
by simp
qed
Hmm. It's a little disappointing to have to explicitly restate "A" rather than having a name for it (akin to ?thesis), but thanks...that gets me past the place where I was stuck.
Last updated: Feb 01 2025 at 20:19 UTC