Email Gateway (Aug 22 2022 at 17:50): Email Gateway (Aug 22 2022 at 17:50):From: Wenda Li <wl302@cam.ac.uk>
Hi Jose,
Here are some tips from my experience.
As your goal does not have division, we can consider “algebra_simps” (otherwise we may need “field_simps” or “divide_simps”). Also, I usually consider
“x - y = 0” when “x<y” and x y are of type “nat”
as an “anomaly" when reasoning about natural numbers in Isabelle, so I will try to prove “x >= y” first (or do some case analysis here).
Therefore, I first tried “(simp add:algebra_simps)” on your target, and the tactic got stuck at the step “k + (k * k + a * (k * 2) - k) = k * k + a * (k * 2)”. To resolve the “anomaly”, I proved "k * k + a * (k * 2) ≥ k” first, and the problem was then gone:
lemma "(k::nat)(k+2a-1) + 2(a + k) = (Suc k)((Suc k)+2*a-1)"
proof -
have "k * k + a * (k * 2) ≥ k"
by (simp add: trans_le_add1)
then show ?thesis by (simp add:algebra_simps)
qed
where “by (simp add: trans_le_add1)” has been found by sledgehammer, and “a>=1” in your previous email turns out to be an unnecessary assumption.
Hope this helps,
Wenda
Email Gateway (Aug 22 2022 at 17:50):From: Peter Lammich <lammich@in.tum.de>
Hi Jose,
a canonical way would be to "convert" both sides to real, and then
"push in" the conversion until the variables. When giving it the lemma
"of_nat_diff" the simplifier can do the non-underflow proof for the
subtraction automatically.
lemma HDGFHFnat: "a≥1 ⟹ (k::nat)(k+2a-1) + 2*(a + k) =
(k+1)((k+1)+2a-1)"
apply (rule of_nat_eq_iff[where 'a=real,THEN iffD1])
apply (simp add: of_nat_diff)
by argo
Last updated: Apr 26 2024 at 16:20 UTC