Lemma usage in other lemmas · Beginner Questions

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"

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.

Mathias Fleury (Mar 28 2024 at 14:40):

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…

Salvatore Francesco Rossetta (Apr 03 2024 at 08:38):

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

Mathias Fleury (Apr 03 2024 at 09:56):

Salvatore Francesco Rossetta (Apr 03 2024 at 10:24):

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.

Salvatore Francesco Rossetta (Apr 03 2024 at 10:38):

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"

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 ? ? ?

Mathias Fleury (Apr 03 2024 at 12:14):

Salvatore Francesco Rossetta (Apr 03 2024 at 12:18):

Mathias Fleury (Apr 03 2024 at 15:32):

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

Salvatore Francesco Rossetta (Apr 03 2024 at 15:40):

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

Mathias Fleury (Apr 03 2024 at 16:03):

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

Stream: Beginner Questions

Topic: Lemma usage in other lemmas

Salvatore Francesco Rossetta (Mar 28 2024 at 08:24):