Stream: Beginner Questions

Topic: Proofing measures with simp

view this post on Zulip Salvatore Francesco Rossetta (Jan 27 2024 at 12:48):

Hi, sorry for long question. I have this loop

function loop_divisor ::
    "('a::linorder, 'b) Divisor_Module_Params ⇒ ('a::linorder, 'b) Divisor_Module_Params" where
  "(parties rec = []) ⟹ loop_divisor rec = rec" |
  "¬(parties rec = []) ⟹ loop_divisor rec = loop_divisor (divisor_module rec)"

for which I want to prove termination. rec is a record with a list "parties". divisor_module removes head of this list, which gets shorter, this way: 

fun divisor_module :: "('a::linorder, 'b) Divisor_Module_Params ⇒ ('a::linorder, 'b) Divisor_Module_Params" where
"divisor_module rec =
  (let
    p = hd (parties rec);
    ps = remove_first (parties rec);
    ni = Min (snd (snd (result rec)));
    nrec = ⦇ result = (fst (result rec) ∪ {ni}, {},snd (snd (result rec)) - {ni}),
                    parties = ps, indexes = indexes rec,
                    seats = assign_seat ni p (seats rec),
                    votes = votes rec, fract_votes = update_votes p (seats rec) (indexes rec) (votes rec) (fract_votes rec) (params rec),
                    params = params rec ⦈
  in
    nrec)"

My idea was to write a lemma about the list getting shorter and use it in the termination of the loop above. I already wrote a lemma for remove_first which seems correct to me. 

fun remove_first :: "'a list ⇒ 'a list" where
  "remove_first (x # xs) = xs"

lemma length_remove_first:
  assumes non_empty: "(x # xs) ≠ []"
  shows "length xs < length (x # xs)"
proof -
  from non_empty have "x # xs ≠ []" by simp
  then have "length (x # xs) = Suc (length xs)" by simp
  then show ?thesis by simp
qed

But then trying to prove that in divisor_module "parties nrec" (indeed ps) is shorter than "parties rec"

lemma divisor_module_p_length:
  assumes non_empty_parties: "parties rec ≠ []"
  shows "length (parties (divisor_module rec)) < length (parties rec)"
proof -
  have "length (remove_first (parties rec)) < length (parties rec)"
    using non_empty_parties by (rule length_remove_first)
  then show ?thesis
    by simp
qed

it fails to prove the subgoal. Isn't my first lemma sufficient for this? Also, since I am a beginner in proofing, is the logic behind the proofing correct or I should proceed in another way? Thanks in advance

view this post on Zulip Mathias Fleury (Jan 27 2024 at 13:02):

First your remove_first is exactly tl

view this post on Zulip Mathias Fleury (Jan 27 2024 at 13:08):

Second, you have not provided enough to reproduce the bug.

If the problem is this, then let's see where rule is stuck:

  have "length (remove_first (parties rec)) < length (parties rec)"
    supply [[unify_trace_failure]]
    apply (rule length_remove_first)

(*
Clash: List.list.Cons =/= Scratch.stuff.parties
Failed to apply proof method⌂:
goal (1 subgoal):
 1. length (remove_first (parties rec)) < length (parties rec)
*)

… so it is stuck because it does not why parties rec would be unifiable with "Cons _ _"

view this post on Zulip Mathias Fleury (Jan 27 2024 at 13:09):

Now I strongly suspect that if you had used tl, then simp would actually be able to solve the goal

view this post on Zulip Mathias Fleury (Jan 27 2024 at 13:10):

Here the version I tried without the Divisor_Module_Params that is not part of Main:

datatype stuff = S (parties: ‹nat list›)

fun divisor_module :: "_ ⇒ stuff" where
"divisor_module rec =   S (tl (parties rec))"


function loop_divisor ::
    "stuff ⇒ stuff" where
  "(parties rec = []) ⟹ loop_divisor rec = rec" |
  "¬(parties rec = []) ⟹ loop_divisor rec = loop_divisor (divisor_module rec)"

fun remove_first :: "'a list ⇒ 'a list" where
  "remove_first (x # xs) = xs"

lemma length_remove_first:
  assumes non_empty: "(x # xs) ≠ []"
  shows "length xs < length (x # xs)"
proof -
  from non_empty have "x # xs ≠ []" by simp
  then have "length (x # xs) = Suc (length xs)" by simp
  then show ?thesis by simp
qed

lemma divisor_module_p_length:
  assumes non_empty_parties: "parties rec ≠ []"
  shows "length (parties (divisor_module rec)) < length (parties rec)"
   using assms by simp

view this post on Zulip Salvatore Francesco Rossetta (Jan 27 2024 at 16:27):

Mathias Fleury said:

Here the version I tried without the Divisor_Module_Params that is not part of Main:

datatype stuff = S (parties: ‹nat list›)

fun divisor_module :: "_ ⇒ stuff" where
"divisor_module rec =   S (tl (parties rec))"


function loop_divisor ::
    "stuff ⇒ stuff" where
  "(parties rec = []) ⟹ loop_divisor rec = rec" |
  "¬(parties rec = []) ⟹ loop_divisor rec = loop_divisor (divisor_module rec)"

fun remove_first :: "'a list ⇒ 'a list" where
  "remove_first (x # xs) = xs"

lemma length_remove_first:
  assumes non_empty: "(x # xs) ≠ []"
  shows "length xs < length (x # xs)"
proof -
  from non_empty have "x # xs ≠ []" by simp
  then have "length (x # xs) = Suc (length xs)" by simp
  then show ?thesis by simp
qed

lemma divisor_module_p_length:
  assumes non_empty_parties: "parties rec ≠ []"
  shows "length (parties (divisor_module rec)) < length (parties rec)"
   using assms by simp

I used tl and also simp in the lemma but it is not working, i think it's the only changes to my code, then to me it looks the same.

record ('a, 'b) Divisor_Module_Params =
  result :: "'a Result"
  parties :: "'b Parties"
  indexes :: "'a set"
  seats :: "('a, 'b) Seats"
  votes :: "'b StructVotes"
  fract_votes :: "'b StructVotes"
  params :: "nat list"

fun divisor_module :: "_ ⇒ ('a::linorder, 'b) Divisor_Module_Params" where
"divisor_module rec =
  (let
    ni = Min (snd (snd (result rec)))
     in ⦇ result = (fst (result rec) ∪ {ni}, {},snd (snd (result rec)) - {ni}),
                    parties = tl (parties rec), indexes = indexes rec,
                    seats = assign_seat ni (hd(parties rec)) (seats rec),
                    votes = votes rec, fract_votes = update_votes (hd(parties rec)) (seats rec) (indexes rec) (votes rec) (fract_votes rec) (params rec),
                    params = params rec ⦈)"

function loop_divisor ::
    "('a::linorder, 'b) Divisor_Module_Params ⇒ ('a::linorder, 'b) Divisor_Module_Params" where
  "(parties rec = []) ⟹ loop_divisor rec = rec" |
  "¬(parties rec = []) ⟹ loop_divisor rec = loop_divisor (divisor_module rec)"

fun remove_first :: "'a list ⇒ 'a list" where
  "remove_first (x # xs) = xs"

lemma length_remove_first:
  assumes non_empty: "(x # xs) ≠ []"
  shows "length xs < length (x # xs)"
proof -
  from non_empty have "x # xs ≠ []" by simp
  then have "length (x # xs) = Suc (length xs)" by simp
  then show ?thesis by simp
qed

lemma divisor_module_p_length:
  assumes non_empty_parties: "parties rec ≠ []"
  shows "length (parties (divisor_module rec)) < length (parties rec)"
 supply [[unify_trace_failure]]
   using assms by simp

The error is always failing to prove the subgoal. Could it be for the record instead of datatype?

view this post on Zulip Mathias Fleury (Jan 27 2024 at 16:36):

  1. Your example is still not working when importing only Main
  2. There is a "by auto" missing after the definition of loop_divisor to prove completeness.
  3. Did you look at the error message? The result after simp is:
 parties rec ≠ [] ⟹
    length
     (parties
       (let ni = Min (snd (snd (result rec))) in ⦇result = (insert ni (fst (result rec)), {}, snd (snd (result rec)) - {ni}), parties = tl (parties rec), indexes = indexes rec, seats = seats rec, votes = votes rec, fract_votes = fract_votes rec, params = params rec⦈))
    < length (parties rec)

which clearly shows that the Let is not unfolded by simp… Therefore you need to Let_def to the simplifier.

view this post on Zulip Salvatore Francesco Rossetta (Jan 27 2024 at 17:02):

thanks, I added Let_def, now it is working

Last updated: Apr 27 2024 at 20:14 UTC