Salvatore Francesco Rossetta (Apr 03 2024 at 16:09): Salvatore Francesco Rossetta (Apr 03 2024 at 16:09):I have this function
fun fx::"fxrec ⇒ fxrec"
where "fx r = ⦇cnt = cnt r - 1, x = x r - 1, y = y r - 1⦈"
lemma fx_lemma:
assumes "x r ≥ y r"
shows "x (fx r) ≥ y (fx r)"
proof -
show ?thesis
using assms by simp
qed
function fx_loop::"fxrec ⇒ fxrec" where
"cnt r = 0 ⟹ fx_loop r = r" |
"cnt r > 0 ⟹ fx_loop r = fx_loop (fx r)"
by auto
lemma fx_loop_lemma:
fixes
r::"fxrec"
assumes "x r > y r"
shows "x (fx_loop r) ≥ y (fx_loop r)"
I want to prove that the lemma holds for the loop, since it is only applying the first function more times. I think the best way is by induction on cnt, but if I induct on cnt how could I use the IH to prove my goal? Trying I just end up in a recursive calling that brings me nowhere.
Mathias Fleury (Apr 03 2024 at 16:15):you have missing the termination proof. Then you also get the proper induction principle
termination sorry
lemma fx_loop_lemma:
fixes
r::"fxrec"
assumes "x r > y r"
shows "x (fx_loop r) ≥ y (fx_loop r)"
using assms
by (induction r rule:fx_loop.induct)
auto
Mathias Fleury said:
you have missing the termination proof. Then you also get the proper induction principle
termination sorry lemma fx_loop_lemma: fixes r::"fxrec" assumes "x r > y r" shows "x (fx_loop r) ≥ y (fx_loop r)" using assms by (induction r rule:fx_loop.induct) auto
It works, but when I try to apply it to my real case, even if I have the same assumptions (copy and pasted), I still have some failed subgoal.
lemma lemma1:
fixes
rec::"('a::linorder, 'b) Divisor_Module" and
m::"rat" and
party1::"'b" and party2::"'b" and parties::"'b Parties"
assumes "v1 > v2"
assumes "party1 ≠ party2"
defines "i1 ≡ get_index_upd party1 (p rec)"
defines "i2 ≡ get_index_upd party2 (p rec)"
defines "fv1 ≡ v1 / (d rec) ! ((sl rec) ! i1)"
defines "fv2 ≡ v2 / (d rec) ! ((sl rec) ! i2)"
defines "winners ≡ get_winners (fv rec) (p rec)"
assumes "sl rec ! i1 ≥ sl rec ! i2"
assumes "i1 ≠ i2"
assumes "i1 < length (sl rec)"
assumes "i2 < length (sl rec)"
shows "sl (assign_seats rec) ! i1 ≥ sl (assign_seats rec) ! i2"
sorry
function loop_o ::
"('a::linorder, 'b) Divisor_Module ⇒ ('a::linorder, 'b) Divisor_Module"
where
"ns r = 0 ⟹ loop_o r = r" |
"ns r > 0 ⟹ loop_o r = loop_o (assign_seats r)"
by auto
termination by (relation "measure (λr. ns r)")
(auto simp add: Let_def nseats_decreasing)
lemma [code]: ‹loop_o r = (if ns r = 0 then r else loop_o (assign_seats r))›
by (cases r) auto
lemma loop_o_concordant:
/* same assms as lemma1 */
shows "sl (loop_o rec) ! i1 ≥ sl (loop_o rec) ! i2"
using assms lemma1
by (induction rec rule:loop_o.induct)
auto
Isn't the "skeleton" of the function and of the lemmas the same as the example I provided in the question?
Mathias Fleury (Apr 03 2024 at 19:12):Without error message or full example, no clue what the error message
Salvatore Francesco Rossetta (Apr 03 2024 at 19:27):Mathias Fleury said:
Without error message or full example, no clue what the error message
the error message is a failing of both subgoals (the two cases of the loop above) and is unfolding all the code, so it's just really long. I will try to recreate the error without having to paste the full example.
Mathias Fleury (Apr 03 2024 at 19:32):I can also run the full example…
Salvatore Francesco Rossetta (Apr 04 2024 at 05:39):Mathias Fleury said:
I can also run the full example…
Thank you, I put everything in a file and cleaned some useless parts not related to this, at the end there is the lemma with the finished subgoals (and slightly above the example we talked about that works).
Mathias Fleury (Apr 04 2024 at 05:52):So I started with:
apply (induction rec rule:loop_o.induct)
subgoal for r
using lemma1[of v2 v1 party1 party2 r]
apply (auto simp: Let_def split: if_splits simp del: assign_seats.simps)
(I just use subgoal to focus on the first case, using Isar would be better but for exploration, I just use subgoal)
Mathias Fleury (Apr 04 2024 at 05:55):From the look of the subgoal, I think I instantiated lemma1 wrong, but I don not have enough context (and enough time to think it)
Mathias Fleury (Apr 04 2024 at 06:03):This is were I would start from here: find the right instantiation so that the conclusion of the assumption matches to conclusion of the theorem
Mathias Fleury (Apr 04 2024 at 06:04):Then look at the assumption, so currently in (sl r ! get_index_upd party2 (p r) ≤ sl r ! get_index_upd party1 (p r) ⟹
sl (assign_seats r) ! get_index_upd party2 (p r)
≤ sl (assign_seats r) ! get_index_upd party1 (p r)), you want the conclusion sl (assign_seats r) ! get_index_upd party2 (p r)
≤ sl (assign_seats r) ! get_index_upd party1 (p r)) to match sl r ! get_index_upd party2 (p r) ≤ sl r ! get_index_upd party1 (p r)
Mathias Fleury (Apr 04 2024 at 06:04):then the question is why is the assumption not discharged (sl r ! get_index_upd party2 (p r) ≤ sl r ! get_index_upd party1 (p r)
Mathias Fleury (Apr 04 2024 at 06:04):once it will be discharged, the theorem should go through
Salvatore Francesco Rossetta (Apr 06 2024 at 09:39):Mathias Fleury said:
Then look at the assumption, so currently in
(sl r ! get_index_upd party2 (p r) ≤ sl r ! get_index_upd party1 (p r) ⟹ sl (assign_seats r) ! get_index_upd party2 (p r) ≤ sl (assign_seats r) ! get_index_upd party1 (p r)), you want the conclusionsl (assign_seats r) ! get_index_upd party2 (p r) ≤ sl (assign_seats r) ! get_index_upd party1 (p r))to matchsl r ! get_index_upd party2 (p r) ≤ sl r ! get_index_upd party1 (p r)
I am trying to solve this and in meantime I changed the code (to prove the first lemma I use that here I skipped with sorry). Now when I use induction provided by the function and instantiating the lemma I am using, auto is running without ending (it's highlighted). Instead, when I focus on the subgoal as you did it is giving me "No subgoals!". Shouldn't this mean that all the subgoals have been proved? Then why the induction proof is not working?
Mathias Fleury (Apr 08 2024 at 04:54):"no subgoal" means that the subgoal was proven and you can go to the next one with the keyword done
Mathias Fleury (Apr 08 2024 at 04:54):and given your description, it is probably the second goal that is looping
Salvatore Francesco Rossetta (Apr 08 2024 at 05:59):Mathias Fleury said:
"no subgoal" means that the subgoal was proven and you can go to the next one with the keyword
done
I did and I rearranged variables in [of r party1 party v1 v2] because of some type errors, later I have been looking at the second case and I get a failed subgoal. I understand there is some problem with the assms but since loop_o does not appear in any of the assms I do not know how to proceed. Should I prove some lemma halfway between the loop and the function I am using in it? Here is the code, I think it's better than pasting the failed subgoal.
Mathias Fleury (Apr 08 2024 at 18:52):If you look at the goal you have:
0 < ns r ⟹
(
index (p r) party1 = index (p (assign_seats r)) party1 ⟹
... ⟹
sl (loop_o (assign_seats r)) ! index (p (assign_seats r)) party2
≤ sl (loop_o (assign_seats r)) ! index (p (assign_seats r)) party1
) ⟹
i1 = index (p r) party1 ⟹
... .⟹
sl (loop_o (assign_seats r)) ! index (p r) party2 ≤ sl (loop_o (assign_seats r)) ! index (p r) party1
So I expect that that either the instantiation are wrong (p (assign_seats r) vs p r) or that it should simplify but it does not
Salvatore Francesco Rossetta (Apr 08 2024 at 21:26):Mathias Fleury said:
So I expect that that either the instantiation are wrong (
p (assign_seats r)vsp r) or that it should simplify but it does not
So I tried to add an assumption p rec = p (assign_seats rec) but it was working the opposite way, instead of simplifying it was "adding" another assign_seats. Then I tried to free "p rec" just instantiating a normal variable independent of recursion and I have the two matched like this
sl (loop_o (assign_seats r)) ! index parties party2
≤ sl (loop_o (assign_seats r)) ! index parties party1)
but it is still not working.
Mathias Fleury (Apr 09 2024 at 07:18):I am not sure to get what you did. You should add p (assign_seats rec) = p rec as assumption to your goal (which probably involves going to Isar instead of continuing with subgoal).
Salvatore Francesco Rossetta (Apr 09 2024 at 07:48):Mathias Fleury said:
I am not sure to get what you did. You should add
p (assign_seats rec) = p recas assumption to your goal (which probably involves going to Isar instead of continuing with subgoal).
Yes, yesterday in my messy message I wrote that I added p rec = p (assign_seats rec) because it seemed the right thing to do but it still does not work. I get
1. 0 < ns r ⟹
(fv r ! index (p r) party1 =
v1 / rat_of_nat (d (assign_seats r) ! (sl (assign_seats r) ! index (p r) party1)) ⟹
... ⟹
sl (loop_o (assign_seats r)) ! index (p r) party2
≤ sl (loop_o (assign_seats r)) ! index (p r) party1) ⟹
... ⟹
sl (loop_o (assign_seats r)) ! index (p r) party2
≤ sl (loop_o (assign_seats r)) ! index (p r) party1
So now these two match and it should work. Yet it does not
Mathias Fleury (Apr 09 2024 at 07:52):Now is the point to look at the assumptions like fv r ! index (p r) party1 =
v1 / rat_of_nat (d (assign_seats r) ! (sl (assign_seats r) ! index (p r) party1)), because auto is not able to discharge them. Does that hold? If so why? My guess is that it is again an issue with assign_seats r vs r and that you add simp rules to simplify them, but I am not sure
Salvatore Francesco Rossetta (Apr 09 2024 at 08:31):Mathias Fleury said:
Now is the point to look at the assumptions like
fv r ! index (p r) party1 = v1 / rat_of_nat (d (assign_seats r) ! (sl (assign_seats r) ! index (p r) party1)), because auto is not able to discharge them. Does that hold? If so why? My guess is that it is again an issue withassign_seats rvsrand that you add simp rules to simplify them, but I am not sure
Well it does not hold, because it should hold this way instead fv (assign_seats r) ! index (p r) party1 = .... If you look back at my code, I used a define fv1 = fv rec ! index (p r) party1 and then subsequently I assumed fv1 = .... So, if I understood correctly, while with the assumes "rec" is changing to "assign_seats rec" during induction, the defines stays at fv1 = fv rec, while I want it to change to fv1 = fv (assign_seats rec) and for this I should move this define to the assumptions, right?
Mathias Fleury (Apr 09 2024 at 12:00):The definition are already included in assms. You can force the unfolding with:
using assms(6-) assign_seats_concordant unfolding assms(1-5)
apply (induction rec rule:loop_o.induct)
subgoal for r
using assign_seats_concordant[of r party1 party2 v1 v2]
apply (auto simp: Let_def split: if_splits simp del: assign_seats.simps)
done
subgoal for r
using assign_seats_concordant[of r party1 party2 v1 v2]
by (auto simp: Let_def split: if_splits simp del: assign_seats.simps)
but I have not spent enough trying to understand why it does not work (that is your job, not mine!)
Salvatore Francesco Rossetta (Apr 09 2024 at 16:05):I cleaned my code and corrected some mistakes, now the first subgoal is working, while the second is missing one subgoal that is starting with this
1. ns r = 0 ⟹
0 < ns ra_ ⟹ ...
What is this ra_ refering to? I do not understand what case Isabelle is talking about concretely
Salvatore Francesco Rossetta (Apr 09 2024 at 16:09):It should mean it cannot prove the subgoal ns r = 0, right? But how, if this case is
"ns r = 0 ⟹ loop_o r = r"
in my code?
Mathias Fleury (Apr 09 2024 at 17:38):the first goal is the case ns r = 0.
Mathias Fleury (Apr 09 2024 at 17:42):for ra_ it could be that subgoal for r should be subgoal for x r (you name the variables, so make sure that you give the names you expect). Otherwise search for all occurrences, maybe auto split a variable and you have r = Suc ra_ or something.
Salvatore Francesco Rossetta (Apr 09 2024 at 19:57):Mathias Fleury said:
the first goal is the case
ns r = 0.
Yes, I noticed and worked on it today, now I am working with assumptions and I see that if I write using assms only the base case works but if I write unfolding assms then only the step case is working. Is there something in between I can use to solve?
Last updated: May 06 2024 at 20:16 UTC