Salvatore Francesco Rossetta (Feb 02 2024 at 17:12): Salvatore Francesco Rossetta (Feb 02 2024 at 17:12):Hi, I wrote this for termination of this function
function loop_divisor_outer ::
"('a::linorder, 'b) Divisor_Module ⇒ ('a::linorder, 'b) Divisor_Module"
where
"ns r = 0 ⟹ loop_divisor_outer r = defer_divisor r" |
"ns r > 0 ⟹ loop_divisor_outer r = loop_divisor_outer (main_function r)"
by auto
termination
proof (relation "measure (λr. ns r)", goal_cases)
case (1)
then show ?case by simp
next
case (2 r)
assume "p r ≠ []"
then have "ns (main_function r) < ns (r)"
using nseats_decreasing_main_function "2" by blast
then show ?case by simp
qed
Where lemma "nseats_decreasing_main_function" proves that "ns (main_function r) < ns r". Here:
fun main_function :: "('a::linorder, 'b) Divisor_Module ⇒
('a::linorder, 'b) Divisor_Module" where
"main_function rec =
assigning_seats (rec⦇p := ( find_max_votes (fv rec) (p rec))⦈)"
lemma nseats_decreasing_main:
assumes non_empty_parties: "p rec ≠ []"
assumes n_positive: "ns rec > 0"
shows "ns (assigning_seats rec) < ns rec"
proof (cases "length (p rec) ≤ ns rec")
case True
then have "ns (assigning_seats rec) = ns rec - length (p rec)"
by (auto simp add: Let_def)
also have "... < ns rec" using True n_positive non_empty_parties
by simp
finally show ?thesis .
next
case False
then have "ns (assigning_seats rec) = 0"
by (auto simp add: Let_def)
also have "... < ns rec" using n_positive
by simp
finally show ?thesis .
qed
lemma nseats_decreasing_main_function:
assumes non_empty_parties: "p rec ≠ []"
assumes n_positive: "ns rec > 0"
shows "ns (main_function rec) < ns rec"
proof -
have "main_function rec = assigning_seats (rec⦇p := find_max_votes (fv rec) (p rec)⦈)"
by simp
also have "ns ( assigning_seats (rec⦇p := find_max_votes (fv rec) (p rec)⦈)) < ns rec" using non_empty_parties n_positive
by (simp add: Let_def)
finally show ?thesis
using assms nseats_decreasing_main nseats_decreasing by auto
qed
But on the first termination proof, after "show", I get this
picking this:
ns (main_function r) < ns r
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(0 < ns ?r2) ⟹ (p ?r2 ≠ []) ⟹ (main_function ?r2, ?r2) ∈ measure ns
if it is picking my lemma how can it not proof the thesis? maybe mistake is on variables because of that "r2" but I don't know exactly how to fix. Or maybe the above lemmas are not correct somehow? Thanks in advance
Lukas Stevens (Feb 05 2024 at 15:48):Maybe you need show ?thesis instead of show ?case?
Salvatore Francesco Rossetta (Feb 05 2024 at 16:10):Lukas Stevens said:
Maybe you need
show ?thesisinstead ofshow ?case?
if i change it i get this error, i think because from a case i cannot prove the full thesis
proof (chain)
picking this:
ns (main_function r) < ns r
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(0 < ns ?r2) ⟹ (p ?r2 ≠ []) ⟹ (0 < ns ?r2) ⟹ All loop_divisor_outer_dom
Never put an assume if you have a case
Mathias Fleury (Feb 05 2024 at 16:25):Never
Mathias Fleury (Feb 05 2024 at 16:26):(yes it sometimes work. In the best case it is useless but bad taste. In the worst case, it leads to an error like here)
Salvatore Francesco Rossetta (Feb 05 2024 at 17:03):Mathias Fleury said:
Never put an assume if you have a case
So how should I proceed? Because if I remove assms the error I get is about "simp" unrolling all the functions inside while I am looking for something "simpler", because looking back at my code it seems the last step is enough to prove the thesis
Mathias Fleury (Feb 05 2024 at 17:09):I don't know. But you cannot add assumptions out of thin air. This is not how proof work.
Mathias Fleury (Feb 05 2024 at 17:10):Otherwise just assume False and every proof will be trivial
Mathias Fleury (Feb 05 2024 at 17:10):or do a case distinction whether the list is empty or not
Last updated: Apr 28 2024 at 08:19 UTC