Minghai (Dec 29 2024 at 21:45): Minghai (Dec 29 2024 at 21:45):Hi, I'm trying to prove this theorem from the minif2f dataset:
theorem mathd_numbertheory_35:
fixes k :: nat
assumes "k^2 = 196"
shows "(\<Sum> k \<in> { n ::nat. n dvd k}. k) = (24::nat)"
proof -
fix n::nat
assume Hn0: "n dvd k"
have "(14::nat) ^ 2 = 196" by eval
hence Hk: "k = 14" using assms(1) by (metis bot_nat_0.extremum power2_eq_iff_nonneg)
have Hn1: "n ≤ 14" using Hk Hn0 dvd_imp_le by auto
have Hn2: "n ≥ 1" using Hk Hn0 by (metis One_nat_def dvd_def one_le_mult_iff one_le_numeral)
have "n ∈ {1, 2, 7, 14}" using Hk Hn0 Hn1 Hn2 by try
I want to show that n is in {1, 2, 7, 14} since it is a factor of 14. I tried to prove this using automation because it looks easy, but failed. Then I tried to first derive that n is in {1, 2, 3 ... 14}, and check whether each of them can dvd 14, so I wrote a lemma:
lemma n_range:
fixes n :: nat
assumes "n ≥ 1" "n ≤ 14"
shows "n ∈ {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14}"
using assms by try
But try still failed to prove it. I tried some simpler cases, and I found that it could handle the cases with less than 10 choices, such as assumes "n ≥ 1" "n ≤ 9".
My question is, why does the automation only handle cases with less than 10 choices? Is this due to the depth of proof search? Additionally, is there an easy way to prove facts about a nat with limited choices by enumerating all possible values? e.g., n <= 100, and n satisfies some constrains, then enumerate all nats <= 100 and check if it satisfies the constrains?
irvin (Dec 31 2024 at 13:40):lemma n_range:
fixes n :: nat
assumes "n ≥ 1" "n ≤ 14"
shows "n ∈ {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14}"
using assms
apply simp
try
have "n ∈ {1, 2, 7, 14}"
using Hk Hn0 Hn1 Hn2 n_range
try
this seems to work
Mathias Fleury (Dec 31 2024 at 14:34):Or this version that does the enumeration (without any try, aka unproven goal):
lemma le_iff_minus1: ‹a > 0 ⟹ x ≤ a ⟷ (x ≤ a - 1 ∨ x = a)› for a :: nat
by auto
theorem mathd_numbertheory_35:
fixes k :: nat
assumes "k^2 = 196"
shows "(\<Sum> k \<in> { n ::nat. n dvd k}. k) = (24::nat)"
proof -
fix n::nat
assume Hn0: "n dvd k"
have "(14::nat) ^ 2 = 196" by eval
hence Hk: "k = 14" using assms(1) by (metis bot_nat_0.extremum power2_eq_iff_nonneg)
have Hn1: "n ≤ 14" using Hk Hn0 dvd_imp_le by auto
have Hn2: "n ≥ 1" using Hk Hn0 by (metis One_nat_def dvd_def one_le_mult_iff one_le_numeral)
have "n ∈ {1, 2, 7, 14}" using Hk Hn0 Hn1 Hn2 by (auto simp: le_iff_minus1)
Or here is one of the nice arithmetic tactics:
lemma n_range:
fixes n :: nat
assumes "n ≥ 1" "n ≤ 14"
shows "n ∈ {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14}"
using assms unfolding insert_iff empty_iff by presburger
These proof work well! Thank you guys!
Last updated: Feb 01 2025 at 20:19 UTC