isabelle - 非平凡列表函数的归纳

Question

这是一个数学练习(取自 page 2 - 俄语):

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?

(注:我猜这个练习是错误的，最多需要称102次。不过没关系)

解决方法如下:

1. 从硬币列表中逐一取出硬币，并将每枚硬币与前一枚进行比较
   • 如果硬币的重量相同，则我们将它们分配到一组并继续进一步称重
   • 如果我们发现比前一枚硬币重的硬币c_j，则转到步骤2
   • 如果我们发现一枚比前一枚硬币轻的硬币 c_i，则继续称重硬币以尝试找到一枚比 c_i 重的硬币 c_j子>
     • 如果我们找到更轻的硬币，则 c₀> c_i> c_j 并且我们知道这些硬币的重量:3 > 2 > 1. 转到第 3 步
2. 不断比较硬币
   • 如果我们找到比 c_j 重的硬币 c_k，则 c_i < c_j < c_k(权重为 1 < 2 < 3)
   • 如果我们找到比 c_j 更轻的硬币 c_k，然后比较 c_i 和 c_k
     • 如果c_i < c_k，则c_i, c_j, c_的权重>k 是 1, 3, 2
     • 如果c_i> c_k，则c_i, c_j, c_的权重>k 是 2, 3, 1
     • 如果 c_i = c_k，则比较 c_i + c_k 和 c _j
       • 如果c_i + c_k < c_j，则c_i的权重，c_j, c_k 分别是 1, 3, 1 (本例中我们没有银币，所以在第 3 步和第 4 步我们将使用两个铜币代替)
       • 如果c_i + c_k> c_j，则c_i、c_的权重>j, c_k 分别为 2, 3, 2
       • 如果c_i + c_k = c_j，则c_i的权重，c_j, c_k 为 1, 2, 1
3. 将其余硬币与银币(或两枚铜币)进行比较
   • 打火机硬币是铜
   • 同样的硬币是银
   • 较重的硬币是黄金
4. 如果在第 1 步中我们首先找到较轻的硬币而不是较重的硬币，那么我们需要将第一个较重的硬币与银币进行比较以确定它们的重量(根据硬币组的不同，可能是第 102 次称重)<

这是一个硬币列表的例子:

c0  ci    cj  ck3 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)))"

我可以证明解决方案对具体案例有效:

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)

但是我不知道如何在一般情况下证明它:

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

我不能对 cs 进行归纳，因为我需要证明这一点

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

它不成立。我可以为 [CC, SC, GC] 确定权重，但不能为 [SC, GC] 确定权重。

另一种方法是针对特殊情况证明这些引理:

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

然后证明案例列表是详尽无遗的。

例如:

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]

但是我连这个引理都无法证明。

问题是:

1. 您能否建议如何证明这样的引理或如何重新表述函数以使引理可证明？
2. 如何制定weigh 函数在算法中最多使用n + 2 次的引理，其中n 是硬币？

Answer 1

一些一般提示:

您有三个递归函数:determine_weights、find_heavier、weigh_coins。

对于每个递归函数，尝试在不使用递归(而是使用量词)的情况下表达输入和结果之间的关系。您为前面的函数证明的属性必须足够强大以证明后面的函数的属性。此外，该属性不应修复任何参数。例如，find_heavier 最初总是使用 j = 0 调用，但该属性应该适用于 j 的所有值，以便它可以在期间使用归纳法。

同时尝试在您的描述中制定和证明高级步骤:例如表明此函数找到一枚银币或两枚铜币。

关于问题2:

我会尝试以不可能作弊的方式陈述问题。例如:

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"

这里 runStrategy 最多调用 weigh 101 次，除了传递给 Weigh 的比较结果外，该策略无法学习任何关于硬币的信息。