Stream: Beginner Questions

Topic: using lemma in later proof

view this post on Zulip Salvatore Francesco Rossetta (Mar 25 2024 at 12:33):

Hi, I have this function

fun assign_seats :: "('a::linorder, 'b) Divisor_Module
                        ⇒ ('a::linorder, 'b) Divisor_Module" where
"assign_seats rec = (
      let winners = get_winners (fv rec) (p rec) in
      if length winners ≤ ns rec then
        let rec' =  (divisor_module [hd winners] rec) in
                    ⦇res = (res rec'), p = (p rec'), i = (i rec'),  s = (s rec'),
                         ns = ((ns rec') - 1), v = (v rec'), fv = (fv rec'), sl = (sl rec'),  d = (d rec')
                        ⦈
      else
         let rec'' = (break_tie winners rec) in
                       ⦇res = (res rec''),  p = (p rec''),
                         i = (i rec''), s = (s rec''),
                         ns = 0, v = (v rec''), fv = (fv rec''), sl = (sl rec''), d = (d rec'')
                        ⦈)"

for which i want to prove this lemma

lemma assign_seats_seats_increased:
   fixes
  rec::"('a::linorder, 'b) Divisor_Module"
defines "winners ≡ get_winners (fv rec) (p rec)"
defines "party ≡ hd winners"
defines "index ≡ get_index_upd party (p rec)"
defines "rec' ≡ (divisor_module [hd winners] rec)"
assumes "length winners ≤ ns rec"
assumes "index < length (sl rec)"
shows "sl (assign_seats rec) ! index = sl rec ! index + 1"
proof -
  have "sl (assign_seats rec) =  sl (⦇res = (res rec'),
                         p = (p rec'),
                         i = (i rec'),
                         s = (s rec'),
                         ns = ((ns rec') - 1),
                         v = (v rec'),
                         fv = (fv rec'),
                         sl = (sl rec'),
                         d = (d rec')
                        ⦈)"
    using assms assign_seats_update by metis
  then have "sl (assign_seats rec) ! index = (sl rec') ! index"
    by simp
  then have "... = sl (divisor_module [hd winners] rec) ! index" using assms by simp
  then have "... = (list_update (sl rec) index ((sl rec) ! index + 1))
                   ! index" using assms divisor_module_sl_update
    by (metis list.sel(1))
  then have "... = sl rec ! index + 1"
    using nth_list_update_eq assms by simp
  then have "sl (assign_seats rec) ! index = sl rec ! index + 1" by simp
  then show ?thesis using ‹sl (assign_seats rec) ! index = sl rec ! index + 1›
  by simp
qed

The step then have "sl (assign_seats rec) ! index = sl rec ! index + 1" by simp is not working (failed to finish subgoal). How is that possible, if I spent the previous steps proving this equivalence? Is there something I am missing? All the previous steps are working, so I don't think it's necessary to share also code about previous functions or lemmas.

view this post on Zulip Mathias Fleury (Mar 25 2024 at 12:38):

finally not then

view this post on Zulip Mathias Fleury (Mar 25 2024 at 12:39):

then threads only the last used fact, while you want to have all of then combined…

view this post on Zulip Manuel Eberl (Mar 25 2024 at 13:30):

The first string of thens should be alsos; the last one a finally.

view this post on Zulip Salvatore Francesco Rossetta (Mar 25 2024 at 18:09):

Manuel Eberl said:

The first string of thens should be alsos; the last one a finally.

Thank you, since Isabelle was not giving any error I thought it was legit. Not it works.

Last updated: Apr 28 2024 at 16:17 UTC