John Park (Sep 05 2024 at 18:01): John Park (Sep 05 2024 at 18:01):I want to prove an inequality with transitive chains:
lemma "a >= 0"
proof -
have "a >= x" sorry
also have "... >= y" sorry
also have "... >= 0" sorrry
finally have ?thesis .
qed
But this doesn't work, since "..." abbreviates LHS instead of RHS of its previous expression, due to Isabelle/HOL's way of defining >= and <=.
I don't want to rephrase the proposition into "0 <= a" and reverse the proof chain, since it would be quite artificial to prove "0 <= y" first, where y comes from no where.
Is there any way to use the "..." syntax for chained proof of >= inequalities?
Mathias Fleury (Sep 05 2024 at 19:23):Besides naming it explicitly, no:
lemma "a >= 0"
proof -
have "a >= x" (is "_ >= ?x") sorry
also have "?x >= y" (is "_ >= ?x") sorry
also have "?x >= 0" sorrry
finally have ?thesis .
qed
Another option, if you do not mind a local definition and using "moreover, ultimate":
lemma
fixes a x y :: "'a :: {zero, linorder}"
shows "0 ≤ a"
proof-
define greater_or_equal (infix "geq" 50)
where "(x1::'a) geq x2 ≡ x2 ≤ x1"
have "a geq x"
sorry
moreover have "... geq y"
sorry
moreover have "... geq 0"
sorry
ultimately show "a geq 0"
sorry
qed
that's a nice trick!
Mathias Fleury (Sep 09 2024 at 08:30):yeah but it breaks the entire automation (you have to unfold it each time)
Yong Kiam (Sep 09 2024 at 08:32):would putting [simp] work?
Jonathan Julian Huerta y Munive (Sep 09 2024 at 08:44):It depends. I had to reshape the definition but simp unfolds it, if written as below:
lemma
fixes a x y :: "'a :: {zero, linorder}"
shows "0 ≤ a"
proof-
define greater_or_equal (infix "geq" 50)
where geq_def[simp]: "greater_or_equal ≡ (λ(x1::'a) x2. x2 ≤ x1)"
have "a geq x"
apply simp
sorry
moreover have "... geq y"
sorry
moreover have "... geq 0"
sorry
ultimately show "a geq 0"
sorry
qed
You can also avoid the lambda with for:
define greater_or_equal (infix "geq" 50)
where geq_def[simp]: "greater_or_equal x1 x2 ≡ (x2 ≤ x1)" for x1 x2 :: ‹'a :: ord›
and yes simp works, but it could negatively impact sledgehammer (because there is one more symbol, although it probably does not matter too much)
John Park (Sep 09 2024 at 15:38):Based on @Mathias Fleury 's first solution:
lemma "(a::int) >= 0"
proof -
note order_trans[rotated, trans]
have "a >= xxx" (is "_ >= ?rhs") sorry
also have "?rhs >= yyy" (is "_ >= ?rhs") sorry
also have "?rhs >= 0" sorry
finally have ?thesis .
qed
Last updated: Dec 21 2024 at 16:20 UTC