An induction for a non-trivial list function

Question

Here is a math exercise (taken from page 2 - in Russian):

There are 100 visually indistinguishable coins of three types: gold, silver and copper (each type occurs at least once). It is known that gold weighs 3 grams each, silver weighs 2 grams each, copper weighs 1 gram each. How can I determine the type of all coins in no more than 101 weighings on two-plate scales without weights?

(Note: I guess that the exercise is wrong and at most 102 weighings are required. However it doesn't matter)

The solution is as follows:

1. Take coins one by one from a list of coins and compare each coin with a previous one
   • If the coins have the same weight, then we assign them to one group and continue to weigh further
   • If we found a heavier coin c_j than the previous one, then go to step 2
   • If we found a lighter coin c_i than the previous one, then keep weighing coins trying to find a coin c_j heavier than c_i
     • If we found a lighter coin instead, then c₀ > c_i > c_j and we know weights of these coins: 3 > 2 > 1. Go to step 3
2. Keep comparing coins
   • If we found a heavier coin c_k than c_j, then c_i < c_j < c_k (and weights are 1 < 2 < 3)
   • If we found a lighter coin c_k than c_j, then compare c_i and c_k
     • If c_i < c_k, then weights of c_i, c_j, c_k are 1, 3, 2
     • If c_i > c_k, then weights of c_i, c_j, c_k are 2, 3, 1
     • If c_i = c_k, then compare c_i + c_k with c_j
       • If c_i + c_k < c_j, then weights of c_i, c_j, c_k are 1, 3, 1 (in this case we don't have a sliver coin, so we will use two copper coins instead on steps 3 and 4)
       • If c_i + c_k > c_j, then weights of c_i, c_j, c_k are 2, 3, 2
       • If c_i + c_k = c_j, then weights of c_i, c_j, c_k are 1, 2, 1
3. Compare rest coins with the silver coin (or two copper coins)
   • Lighter coins are copper
   • Same coins are silver
   • Heavier coins are gold
4. If on step 1 we found a lighter coin first instead of a heavier one, then we need to compare first heavy coins with a silver coin to determine their weight (it could be a 102th weighing depending on a coin set)

Here is an example of a coin list:

c0  ci    cj  ck
3 3 2 2 2 3 3 1 1 2 1 3
|_| |___| |_|
 i    j    k

Here is a solution in Isabelle HOL:

datatype coin = GC | SC | CC

datatype comp = LT | EQ | GT

primrec coin_weight :: "coin ⇒ nat" where
  "coin_weight CC = 1"
| "coin_weight SC = 2"
| "coin_weight GC = 3"

primrec sum_list where
  "sum_list f [] = 0"
| "sum_list f (x # xs) = f x + sum_list f xs"

definition weigh :: "coin list ⇒ coin list ⇒ comp" where
  "weigh xs ys = (
    let xw = sum_list coin_weight xs in
    let yw = sum_list coin_weight ys in
    if xw < yw then LT else
    if xw > yw then GT else EQ)"

definition std_weigh :: "coin list ⇒ coin ⇒ nat" where
  "std_weigh xs ys ≡ (case weigh xs [ys] of LT ⇒ 3 | GT ⇒ 1 | EQ ⇒ 2)"

definition gen_weights :: "coin list ⇒ coin ⇒ coin list ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat list" where
  "gen_weights cs c⇩0 std i j k w⇩j w⇩k w ≡
    ― ‹Optional heavy coins (\<^term>‹c⇩0›...)›
    replicate i (std_weigh std c⇩0) @
    ― ‹Light coins (\<^term>‹c⇩i›...)›
    replicate j w⇩j @
    ― ‹Heavy coins (\<^term>‹c⇩j›...)›
    replicate k w⇩k @
    ― ‹A light coin (\<^term>‹c⇩k›)›
    [w] @
    ― ‹Rest coins›
    map (std_weigh std) cs"

primrec determine_weights where
  "determine_weights [] c⇩0 c⇩i c⇩j i j k = None"
| "determine_weights (c⇩k # cs) c⇩0 c⇩i c⇩j i j k = (
    case weigh [c⇩j] [c⇩k]
      of LT ⇒ Some (gen_weights cs c⇩0 [c⇩j] i j (Suc k) 1 2 3)
       | GT ⇒ Some (
          case weigh [c⇩i] [c⇩k]
            of LT ⇒ gen_weights cs c⇩0 [c⇩k] i j (Suc k) 1 3 2
             | GT ⇒ gen_weights cs c⇩0 [c⇩i] i j (Suc k) 2 3 1
             | EQ ⇒ (
                case weigh [c⇩i, c⇩k] [c⇩j]
                  of LT ⇒ gen_weights cs c⇩0 [c⇩i, c⇩k] i j (Suc k) 1 3 1
                   | GT ⇒ gen_weights cs c⇩0 [c⇩k] i j (Suc k) 2 3 2
                   | EQ ⇒ gen_weights cs c⇩0 [c⇩j] i j (Suc k) 1 2 1))
       | EQ ⇒ determine_weights cs c⇩0 c⇩i c⇩j i j (Suc k))"

primrec find_heavier where
  "find_heavier [] c⇩0 c⇩i i j alt = None"
| "find_heavier (c⇩j # cs) c⇩0 c⇩i i j alt = (
    case weigh [c⇩i] [c⇩j]
      of LT ⇒ determine_weights cs c⇩0 c⇩i c⇩j i (Suc j) 0
       | GT ⇒ alt cs c⇩j (Suc j)
       | EQ ⇒ find_heavier cs c⇩0 c⇩i i (Suc j) alt)"

primrec weigh_coins where
  "weigh_coins [] = Some []"
| "weigh_coins (c⇩0 # cs) =
    find_heavier cs c⇩0 c⇩0 0 0
      (λcs c⇩i i. find_heavier cs c⇩0 c⇩i i 0
        (λcs c⇩j j. Some (gen_weights cs c⇩0 [c⇩i] 0 i j 3 2 1)))"

I can prove that the solution is valid for a concrete case:

definition "coins ≡ [GC, GC, SC, SC, SC, GC, GC, CC, CC, SC, CC, GC]"

value "weigh_coins coins"

lemma weigh_coins_ok:
  "cs = coins ⟹
   weigh_coins cs = Some ws ⟹
   ws = map coin_weight cs"
  by (induct cs; auto simp: coins_def weigh_def gen_weights_def std_weigh_def)

lemma weigh_coins_length_ok:
  "cs = coins ⟹
   weigh_coins cs = Some ws ⟹
   length cs = length ws"
  by (induct cs; auto simp: coins_def weigh_def gen_weights_def std_weigh_def)

However I have no idea how to prove it for a general case:

lemma weigh_coins_ok:
  "weigh_coins cs = Some ws ⟹
   ws = map coin_weight cs"
proof (induct cs)
  case Nil
  then show ?case by simp
next
  case (Cons c cs)
  then show ?case

qed

I can't induct over cs because I'll need to prove that

weigh_coins (c # cs) = Some ws ⟹ ∃ws. weigh_coins cs = Some ws

It doesn't hold. I can determine weights for [CC, SC, GC], but can't do it for [SC, GC].

An alternative approach is to prove these lemmas for a special cases:

[CC, CC, ...] @ [SC, SC, ...] @ [GC, GC, ...] @ ...
[CC, CC, ...] @ [GC, GC, ...] @ [SC, SC, ...] @ ...
[SC, SC, ...] @ [GC, GC, ...] @ [CC, CC, ...] @ ...
...

And then to prove that the list of cases is exhaustive.

For example:

lemma weigh_coins_length:
  "cs = [CC] @ replicate n CC @ [SC, GC] ⟹
   weigh_coins cs = Some ws ⟹
   length cs = length ws"
  apply (induct n arbitrary: cs ws)
  apply (auto simp: weigh_def gen_weights_def std_weigh_def)[1]

However I can't prove even this lemma.

The questions are:

1. Could you suggest how such a lemmas can be proven or how to reformulate the functions to make the lemmas provable?
2. How to formulate the lemma that weigh function is used at most n + 2 times in the algorithm, where n is the number of coins?

Answer 1

Some general hints:

You have three recursive functions: determine_weights, find_heavier, weigh_coins.

For each recursive function, try to express a relation between the inputs and results without using recursion (instead use quantifiers). The property you prove for the earlier functions must be strong enough to prove the properties for the later ones. Also, the property should not fix any of the parameters. For example find_heavier is always initially called with j = 0, but the property should work for all values of j so that it can be used during induction.

Also try to formulate and prove the high level steps in your description: For example show that this function finds a silver coin or two copper coins.

Regarding question 2:

I would try to state the problem in a way where it is not possible to cheat. For example:

datatype strategy =
    Return "coin list"
  | Weigh "nat list" "nat list" "comp ⇒ strategy"  ― ‹Weigh coins based on positions›

definition "select indexes coins ≡ map (nth coins) indexes"

fun runStrategy where
  "runStrategy coins _ (Return r) = Some r"
| "runStrategy coins 0 _ = None"
| "runStrategy coins (Suc n) (Weigh xs ys cont) = (
      if distinct xs ∧ distinct ys ∧ set xs ∩ set ys = {} then 
        runStrategy coins n (cont (weigh (select xs coins) (select ys coins)))
      else None)"

lemma "∃strategy. ∀coins. 
    length coins = 100 ∧ (∀c. c ∈ set coins)
    ⟶ runStrategy coins 101 strategy = Some coins"

Here runStrategy calls weigh at most 101 times and the strategy cannot learn anything about the coins, except for the comparison result passed into the continuation of Weigh.