Salvatore Francesco Rossetta (Jan 18 2024 at 22:31): Salvatore Francesco Rossetta (Jan 18 2024 at 22:31):Hi, sorry for long question, I have this function
function loop_divisor_outer ::
"'a::linorder Result × ('a::linorder, 'b) Divisor_Module_Params × 'a::linorder Termination_Condition × nat ⇒ ('a::linorder, 'b) Divisor_Module_Params"
where
"loop_divisor_outer (r, p, t, n) =
(if n ≤ 0 then defer_divisor p
else let (n', p') = main_function (r, p, t, n) in loop_divisor_outer (r, p', t, n'))"
by pat_completeness auto
I would like to prove that it reaches an end (n = 0) proving that n' < n for every iteration. i "know" this because in main_function i calculate n' as n' = n - length max_votes_parties, which is a non empty list.
code for reference:
fun main_function :: "('a::linorder Result × ('a::linorder, 'b) Divisor_Module_Params × 'a::linorder Termination_Condition × nat) ⇒
(nat × ('a::linorder, 'b) Divisor_Module_Params)" where
"main_function (r, p, t, n::nat) =
(let (result, parties, indexes, s, votes, v, ps) = p;
(ass, rej, def) = result;
max_votes_parties = find_max_votes v parties
in
if max_votes_parties = [] then
(0, (result, parties, indexes, s, votes, v, ps))
else
if (length max_votes_parties) ≤ n then
let
n = n - length max_votes_parties;
res_params = loop_divisor_composition (max_votes_parties,
(r, max_votes_parties, indexes, s,
votes, v, ps));
res = fst(res_params)
in
(n, res_params)
else
let (res, seats) = divisor_module_for_tie_breaking (ass, rej, def) max_votes_parties s
in
(0, (res, parties, indexes, seats, votes, v, ps)))"
Isabelle cannot automatically prove that this value (n/n') will decrease until it gets to zero. That's why when I write termination for loop this way
termination
proof (relation "measure (\<lambda>(_, _, _, n). n)", goal_cases)
case 1
then show ?case by auto
next
case 2
then show ?case by auto
qed
of course case 2 (when n will decrease) is not proven with auto, so I have to do it manually. what's the cleanest way to prove it? can i do some assumptions? should i start proving functions inside this? thanks in advance
Mathias Fleury (Jan 19 2024 at 05:55):You should have already all the assumption in the '2' case
Salvatore Francesco Rossetta (Jan 19 2024 at 09:11):Mathias Fleury said:
You should have already all the assumption in the '2' case
Do you mean my code should already work? Because at the moment there's a failed subgoal prove:
show ((r_, y_, t_, xa_), r_, p_, t_, n_) ∈ measure (λ(uu_, uu_, uu_, n). n)
Successful attempt to solve goal by exported rule:
(¬ ?n3 ≤ 0) ⟹
(?x3 = main_function (?r3, ?p3, ?t3, ?n3)) ⟹
((?xa3, ?y3) = ?x3) ⟹
((?r3, ?y3, ?t3, ?xa3), ?r3, ?p3, ?t3, ?n3) ∈ measure (λ(uu_, uu_, uu_, n). n)
proof (state)
this:
((r_, y_, t_, xa_), r_, p_, t_, n_) ∈ measure (λ(uu_, uu_, uu_, n). n)
goal:
No subgoals!
Failed to finish proof⌂:
goal (1 subgoal):
1. 0 < n_ ⟹
x_ =
(case p_ of
(result, parties, indexes, s, votes, v, ps) ⇒
let max_votes_parties = find_max_votes v parties
in if max_votes_parties = [] then (0, result, parties, indexes, s, votes, v, ps)
else if length max_votes_parties ≤ n_
then let n = n_ - length max_votes_parties;
res_params =
loop_divisor_composition
(max_votes_parties, r_, max_votes_parties, indexes, s, votes, v, ps);
res = fst res_params
in (n, res_params)
else let (res, seats) =
divisor_module_for_tie_breaking result max_votes_parties s
in (0, res, parties, indexes, seats, votes, v, ps)) ⟹
(xa_, y_) =
(case p_ of
(result, parties, indexes, s, votes, v, ps) ⇒
let max_votes_parties = find_max_votes v parties
in if max_votes_parties = [] then (0, result, parties, indexes, s, votes, v, ps)
else if length max_votes_parties ≤ n_
then let n = n_ - length max_votes_parties;
res_params =
loop_divisor_composition
(max_votes_parties, r_, max_votes_parties, indexes, s, votes, v, ps);
res = fst res_params
in (n, res_params)
else let (res, seats) =
divisor_module_for_tie_breaking result max_votes_parties s
in (0, res, parties, indexes, seats, votes, v, ps)) ⟹
xa_ < n_
The error is on the "by auto" of the second case
Mathias Fleury (Jan 19 2024 at 09:13):No, I mean that there is no need to add an assumption…
Mathias Fleury (Jan 19 2024 at 09:14):From the goal, I would try a auto split: prod.splits simp: Let_def… but you have not provided any context to help you much.
Mathias Fleury (Jan 19 2024 at 09:15):Mathias Fleury said:
No, I mean that there is no need to add an assumption…
BTW, you question currently boils down to: "How do I do a proof?"
Salvatore Francesco Rossetta (Jan 19 2024 at 13:40):Mathias Fleury said:
Mathias Fleury said:
No, I mean that there is no need to add an assumption…
BTW, you question currently boils down to: "How do I do a proof?"
Actually it's the very first time I ever try to write a proof ever, that's why I may seem confused, I still have to understand clearly all the steps to write a proof. Thanks for the help anyway
Mathias Fleury (Jan 19 2024 at 13:47):Then I would suggest starting with the tutorial at: https://isabelle.in.tum.de/doc/prog-prove.pdf
Mathias Fleury (Jan 19 2024 at 13:47):The page seem to be currently down, but in the documentation panel in Isabelle/jEdit > prog-prove
Last updated: Apr 27 2024 at 20:14 UTC