Stream: Beginner Questions

Topic: Foldr invariant on permutations

Salvatore Francesco Rossetta (Feb 05 2024 at 09:52):

Hi, I want to prove that my function "calculate_votes_for_election" is invariant under permutations of list of parties.

fun count_votes :: "'b ⇒ 'b Profile ⇒ 'b Votes
                                      ⇒ 'b Votes" where
  "count_votes party profile_list votes =
  (let n_votes = foldr (λpref acc. if card (above pref party) = 0
                                      then acc+1
                                  else acc) profile_list 0
   in votes(party := n_votes))"

fun empty_votes :: "('b ⇒ rat)" where
  "empty_votes b = 0"

fun calculate_votes_for_election :: "'b list ⇒ 'b Profile ⇒ 'b Votes" where
  "calculate_votes_for_election parties prof =
      (let v = empty_votes in (if parties = [] then empty_votes else
      (foldr (λparty acc_votes.
              count_votes party prof acc_votes)
              parties v)))"

For the moment i rewrote count_votes without the foldr but in recursion way

fun count_votes :: "'b ⇒ 'b Profile ⇒ 'b Votes ⇒ rat
                                      ⇒ 'b Votes" where
  "count_votes party [] votes n = votes(party:= n)" |
  "count_votes party (px # p) votes n =
   count_votes party p votes (if card (above px party) = 0
                                      then n+1
                                  else n)"

thinking that in this way it may be easier to proof. Any help or suggestion? Should i rewrite also calculate_votes_for_election in recursive way to write my proof? Thanks in advance

Mathias Fleury (Feb 05 2024 at 09:54):

Do you need to work on lists? The natural data structure would be multisets…

Mathias Fleury (Feb 05 2024 at 09:56):

Otherwise the natural way would be to interprete the function as comp_fun_commute in the proofs.

Salvatore Francesco Rossetta (Feb 05 2024 at 11:03):

Mathias Fleury said:

Do you need to work on lists? The natural data structure would be multisets…

I chose lists because I need to extract one element from it and in the theory about multisets I found nothing to extract a single element without knowing in advance the element itself, I only found Min but in my case it's not a linorder type.

Salvatore Francesco Rossetta (Feb 05 2024 at 12:22):

Update: I tried to do it with multisets without succeeding so I am trying with lists.

fun calculate_votes :: "'b list ⇒ 'b Profile ⇒'b Votes ⇒ 'b Votes" where
  "calculate_votes [] profile_list votes = votes" |
  "calculate_votes (px # p) profile_list votes =
      calculate_votes p profile_list (count_votes px profile_list empty_votes 0)"

lemma calculate_votes_permutation:
  fixes
    p1 :: "'b Parties" and
    p2 ::"'b Parties" and
    profile ::"'b Profile" and
    votes::"'b Votes"
  shows "∀p1 p2 profile votes. p1 <~~> p2 ⟶ calculate_votes p1 profile votes = calculate_votes p2 profile votes"
proof (cases)
  assume "p1 = []"
  assume "p1 <~~> p2"
  then have "p2 = []" using perm_empty_imp
    by (simp add: ‹p1 = []›)
  hence "calculate_votes p1 profile votes =
         calculate_votes p2 profile votes"
  by (simp add: ‹p1 = []›)
  then show ?thesis by simp
next

I managed to write something like this and it is not working, even though it seems to "pick" the thesis

proof (chain)
picking this:
  calculate_votes p1 profile votes = calculate_votes p2 profile votes
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (p1 = []) ⟹
  (mset p1 = mset p2) ⟹
  ∀p1 p2 profile votes.
     mset p1 = mset p2 ⟶ calculate_votes p1 profile votes = calculate_votes p2 profile votes

How should I change my proof? Or again is there any way to do it with multisets?

Mathias Fleury (Feb 05 2024 at 12:42):

Salvatore Francesco Rossetta said:

Mathias Fleury said:

Do you need to work on lists? The natural data structure would be multisets…

I chose lists because I need to extract one element from it and in the theory about multisets I found nothing to extract a single element without knowing in advance the element itself, I only found Min but in my case it's not a linorder type.

You must have missed fold_mset

Mathias Fleury (Feb 05 2024 at 12:43):

Salvatore Francesco Rossetta said:

Update: I tried to do it with multisets without succeeding so I am trying with lists.

fun calculate_votes :: "'b list ⇒ 'b Profile ⇒'b Votes ⇒ 'b Votes" where
  "calculate_votes [] profile_list votes = votes" |
  "calculate_votes (px # p) profile_list votes =
      calculate_votes p profile_list (count_votes px profile_list empty_votes 0)"

lemma calculate_votes_permutation:
  fixes
    p1 :: "'b Parties" and
    p2 ::"'b Parties" and
    profile ::"'b Profile" and
    votes::"'b Votes"
  shows "∀p1 p2 profile votes. p1 <~~> p2 ⟶ calculate_votes p1 profile votes = calculate_votes p2 profile votes"
proof (cases)
  assume "p1 = []"
  assume "p1 <~~> p2"
  then have "p2 = []" using perm_empty_imp
    by (simp add: ‹p1 = []›)
  hence "calculate_votes p1 profile votes =
         calculate_votes p2 profile votes"
  by (simp add: ‹p1 = []›)
  then show ?thesis by simp
next

I managed to write something like this and it is not working, even though it seems to "pick" the thesis

proof (chain)
picking this:
  calculate_votes p1 profile votes = calculate_votes p2 profile votes
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (p1 = []) ⟹
  (mset p1 = mset p2) ⟹
  ∀p1 p2 profile votes.
     mset p1 = mset p2 ⟶ calculate_votes p1 profile votes = calculate_votes p2 profile votes

How should I change my proof? Or again is there any way to do it with multisets?

That is not a valid proof. You are doing cases of variables under forall-quantors. So obviously it does not work

Salvatore Francesco Rossetta (Feb 05 2024 at 13:20):

Mathias Fleury said:

That is not a valid proof. You are doing cases of variables under forall-quantors. So obviously it does not work

I know, I pasted only the first case because that is not working, the other one is simply a "sorry" for now, so it should not be a problem?

proof (cases)
  assume "p1 = []"
  assume "p1 <~~> p2"
  then have "p2 = []" using perm_empty_imp
    by (simp add: ‹p1 = []›)
  then show ?thesis by (simp add: ‹p1 = []›)
next
  assume "¬(p1 = [])"
  then show ?thesis sorry
qed

Mathias Fleury (Feb 05 2024 at 13:22):

The p1 in your fixes has NOTHING to do with the p1 in your goal

Mathias Fleury (Feb 05 2024 at 13:22):

(except having the same name)

Mathias Fleury (Feb 05 2024 at 13:22):

Therefore, the case distinction on p1 is meaningless for the goal

Mathias Fleury (Feb 05 2024 at 13:23):

This is most likely what you want:

lemma calculate_votes_permutation:
  fixes
    p1 :: "'b Parties" and
    p2 ::"'b Parties" and
    profile ::"'b Profile" and
    votes::"'b Votes"
  assumes "p1 <~~> p2"
  shows "calculate_votes p1 profile votes = calculate_votes p2 profile votes"

Mathias Fleury (Feb 05 2024 at 13:23):

and then the proof should actually work

Salvatore Francesco Rossetta (Feb 05 2024 at 13:31):

Mathias Fleury said:

and then the proof should actually work

it does not, there is the same error as before. today i will try to do it with multisets through fold_mset, but at this point i am just curious to know why it still does not work.

Mathias Fleury (Feb 05 2024 at 13:42):

You removed the assume "p1 <~~> p2" right?

Salvatore Francesco Rossetta (Feb 05 2024 at 17:51):

Mathias Fleury said:

You removed the assume "p1 <~~> p2" right?

Thank you, I did and changing some details it worked. I slightly rewrote it cleaner and now I am working on the second case

proof (cases "p1 = []")
  case True
  with assms show ?thesis by (simp add: perm_empty_imp)
next
  case False
  then obtain x p1' where "p1 = x # p1'"
    by (meson list.exhaust)
  then obtain p2' where "p2 <~~> x # p2'"
    using assms by metis
  then have "p2' <~~> p1'"
  using ‹p1 = x # p1'› assms by auto
  then have "calculate_votes p1 profile votes = calculate_votes (x # p1') profile votes"
    using assms
  by (simp add: ‹p1 = x # p1'›)
  also have "... = calculate_votes p1' profile (count_votes x profile empty_votes 0)"
    by simp
  also have "... = calculate_votes p2' profile (count_votes x profile empty_votes 0)"
    using assms by simp
  also have "... = calculate_votes p2 profile votes"
    using ‹p2 <~~> x # p2'› by simp
  finally show ?thesis .
qed

I wrote the first steps and they work perfectly but the "... = calculate_votes p2' profile (count_votes x profile empty_votes 0)" step does not work, I think related to the "step n" for which I assume the lemma works in the induction proofs. So I should add this somewhere? but not as an assumption, for what I understood.

Mathias Fleury (Feb 05 2024 at 19:40):

step contain all the theorem (IH + all assumptions). Therefore, using step may be what you are missing.

Salvatore Francesco Rossetta (Feb 06 2024 at 08:33):

Mathias Fleury said:

step contain all the theorem (IH + all assumptions). Therefore, using step may be what you are missing.

it's still not working, also the error is the same:

have calculate_votes p1' profile (count_votes x profile empty_votes 0) =
     calculate_votes p2' profile (count_votes x profile empty_votes 0)
proof (state)
this:
  calculate_votes p1' profile (count_votes x profile empty_votes 0) =
  calculate_votes p2' profile (count_votes x profile empty_votes 0)

goal (1 subgoal):
 1. p1 ≠ [] ⟹ calculate_votes p1 profile votes = calculate_votes p2 profile votes
Failed to apply initial proof method⌂:
using this:
    mset p1 = mset p2
    ?x ∈ ccpo_class.iterates ?f ⟹ ?f ?x ∈ ccpo_class.iterates ?f
goal (1 subgoal):
 1. calculate_votes p1' profile (count_votes x profile empty_votes 0) =
    calculate_votes p2' profile (count_votes x profile empty_votes 0)

It is really weird, since this step should be solved by IH

Mathias Fleury (Feb 06 2024 at 08:37):

I am lost in the proof you are actually running, but where are you doing induction? Currently I see only a case distinction cases

Salvatore Francesco Rossetta (Feb 06 2024 at 08:42):

Mathias Fleury said:

I am lost in the proof you are actually running, but where are you doing induction? Currently I see only a case distinction cases

Currently this is my code

fun calculate_votes :: "'b list ⇒ 'b Profile ⇒'b Votes ⇒ 'b Votes" where
  "calculate_votes [] profile_list votes = votes" |
  "calculate_votes (px # p) profile_list votes =
      calculate_votes p profile_list (count_votes px profile_list empty_votes 0)"


lemma calculate_votes_permutation:
  fixes
    p1 :: "'b Parties" and
    p2 ::"'b Parties" and
    profile ::"'b Profile" and
    votes::"'b Votes"
  assumes "p1 <~~> p2"
  shows "calculate_votes p1 profile votes = calculate_votes p2 profile votes"
proof (cases "p1 = []")
  case True
  with assms show ?thesis by (simp add: perm_empty_imp)
next
  case False
  then obtain x p1' where "p1 = x # p1'"
    by (meson list.exhaust)
  then obtain p2' where "p2 <~~> x # p2'"
    using assms by metis
  then have "p2' <~~> p1'"
  using ‹p1 = x # p1'› assms by auto
  then have "calculate_votes p1 profile votes = calculate_votes (x # p1') profile votes"
    using assms
  by (simp add: ‹p1 = x # p1'›)
  also have "... = calculate_votes p1' profile (count_votes x profile empty_votes 0)"
    by simp
  also have "... = calculate_votes p2' profile (count_votes x profile empty_votes 0)"
    using step by simp
  also have "... = calculate_votes p2 profile votes"
    using ‹p2 <~~> x # p2'› by simp
  finally show ?thesis .
qed

The True case works, I am in the False one, stuck in the step where I use "step" as you suggested. The only thing I can think of is that I define p2 as a permutation of x # p2' and not as being itself p2 = x # p2', so maybe the IH does not work as expected?

Last updated: Apr 28 2024 at 12:28 UTC