Hi, I wrote this lemma
lemma assign_seats_not_winner_mantains_seats:
fixes
rec::"('a::linorder, 'b) Divisor_Module"
defines "winners ≡ get_winners (fv rec) (p rec)"
defines "i1 ≡ get_index_upd (hd winners) (p rec)"
assumes "i1 ≠ i2"
assumes "i2 < length (sl rec)"
shows "(sl rec) ! i2 = (sl (assign_seats rec)) ! i2"
and I used it in another lemma
lemma assign_seats_concordant:
fixes
rec::"('a::linorder, 'b) Divisor_Module" 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 "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"
proof(cases "length winners ≤ ns rec")
case True
then show ?thesis
proof(cases "party1 = hd winners")
case True
have "sl (assign_seats rec) ! i1 = (sl rec) ! i1 + 1"
using ‹length winners ≤ ns rec› True assign_seats_seats_increased assms(8) assms(11)
i1_def winners_def by blast
also have "sl (assign_seats rec) ! i2 = (sl rec) ! i2"
using True assign_seats_not_winner_mantains_seats assms
i1_def winners_def by metis <-------
then show ?thesis
using assms(8) calculation by linarith
next
case False
then show ?thesis
proof(cases "party2 = hd winners")
case True
...
next
case False
obtain partyW iW where "partyW = hd winners"
"iW = get_index_upd partyW (p rec)" by simp
have "party2 ≠ partyW"
using ‹partyW = hd winners› False by simp
then have "i2 = get_index_upd party2 (p rec)"
using assms by simp
also have "sl (assign_seats rec) ! i2 = (sl rec) ! i2"
using False assign_seats_not_winner_mantains_seats assms i2_def i1_def
winners_def by ? ? ?
then show ?thesis sorry
qed
qed
next
case False
...
qed
but it is not working. I tried to introduce with obtains a "winner" different from party2 to help the first lemma but i don't know if it's helpful.
As you can see, I used it earlier where there is the arrow but I cannot use it in later subcase (? ? ?), why if assumptions are (or at least looks) the same in both cases?
P.S: Since it's all about assms and lemmas I don't think I should provide functions code, also sorry if I didn't manage to simplify the example.
Usually in those cases I instantiate by hand with assign_seats_not_winner_mantains_seats[of winners rec i2]
and apply auto
. Usually the remaining (unproven) assumptions of the theorems shows what is wrong…
Mathias Fleury said:
Usually in those cases I instantiate by hand with
assign_seats_not_winner_mantains_seats[of winners rec i2]
andapply auto
. Usually the remaining (unproven) assumptions of the theorems shows what is wrong…
What do you mean "instantiate by hand"? Should I write this inside my proof or write it in another lemma and then use it? I tried something but it doesn't work, for example writing it
case False
have "sl (assign_seats rec) ! i2 = (sl rec) ! i2"
using False assms i2_def i1_def
winners_def assign_seats_not_winner_mantains_seats[of winners rec i2] by simp
then show ?thesis sorry
No I mean exactly that. The question is now why/what is not working
Mathias Fleury said:
No I mean exactly that. The question is now why/what is not working
The error is More instantiations than variables in theorem
, so I thought about removing "winners" because it is not in the thesis of the lemma i want to use (but maybe it's completely wrong step, just my idea)
using False assms i2_def i1_def
winners_def assign_seats_not_winner_mantains_seats[of rec i2] apply auto by simp
and it is giving a failed subgoal, which is the same I get if I would not use the lemma at all.
May it be because in my first lemma in the assumptions I explicitely wrote that i2 is different from the winner this way
defines "i1 ≡ get_index_upd (hd winners) (p rec)"
assumes "i1 ≠ i2"
so I know that i2 ≠ get_index_upd (hd winners) (p rec)
while in my later lemma this is not explicitely an assumption but more a case to prove, something like this?
have "party2 ≠ hd winners" using False by simp
then have "i2 ≠ get_index_upd (hd winners) (p rec)" using by ? ? ?
and therefore I can use the lemma above because this assm is true?
Salvatore Francesco Rossetta said:
Mathias Fleury said:
No I mean exactly that. The question is now why/what is not working
The error is
More instantiations than variables in theorem
, so I thought about removing "winners" because it is not in the thesis of the lemma i want to use (but maybe it's completely wrong step, just my idea)using False assms i2_def i1_def winners_def assign_seats_not_winner_mantains_seats[of rec i2] apply auto by simp
and it is giving a failed subgoal, which is the same I get if I would not use the lemma at all.
My guess is that the error comes from i1 being unfolded in the theorem version
Mathias Fleury said:
My guess is that the error comes from i1 being unfolded in the theorem version
And how could I manage to solve this? By avoiding that i1 is unfolded?
First get the instantiations right, trying assign_seats_not_winner_mantains_seats[of rec]
, assign_seats_not_winner_mantains_seats[of i2]
until all instantiations are done
Mathias Fleury said:
First get the instantiations right, trying
assign_seats_not_winner_mantains_seats[of rec]
,assign_seats_not_winner_mantains_seats[of i2]
until all instantiations are done
I had already tried earlier, the [of rec]
one doesn't give any errors (but still i get subgoal error) and the [of i2]
one gives a type mismatch because it's expecting rec, not i2
So instantiate all variables. Then run apply auto
. Then look at the goal. One of the assumptions should exactly be your lemma. It probably has some assumptions that auto cannot prove. Find it and try to find out why not
Last updated: Dec 30 2024 at 16:22 UTC