时间戳

首页 > 解决方案 > 非平凡列表函数的归纳

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

问题描述

这是一个数学练习（取自第 2 页- 俄语）：

共有 100 枚在视觉上无法区分的硬币，分为三种类型：金、银和铜（每种类型至少出现一次）。众所周知，金各重3克，银各重2克，铜各重1克。如何在不带砝码的两盘秤上称量不超过 101 次的所有硬币的类型？

（注：我猜这个练习是错误的，最多需要102个称重。不过没关系）

解决方法如下：

  1. 从硬币列表中逐个取出硬币并将每个硬币与前一个硬币进行比较
    • 如果硬币的重量相同，那么我们将它们分配到一组并继续进一步称重
    • 如果我们发现比前一个更重的硬币 c j，则转到步骤 2
    • 如果我们找到一个比前一个更轻的硬币 c i，那么继续称量硬币，试图找到一个比 c i重的硬币 c j
      • 如果我们找到更轻的硬币，那么 c 0 > c i > c j并且我们知道这些硬币的重量：3 > 2 > 1。转到步骤 3
  2. 继续比较硬币
    • 如果我们发现硬币 c k比 c j重，则 c i < c j < c k（权重为 1 < 2 < 3）
    • 如果我们发现 c k比 c j更轻，那么比较 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 次重量）

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

c 0   c i     c j   c k
3 3 2 2 2 3 3 1 1 2 1 3
|_| |___| |_|
 伊克

这是 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 + 2n

标签： isabelletheorem-proving

解决方案

一些一般提示：

您有三个递归函数：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 最多调用weigh101 次，并且该策略无法了解有关硬币的任何信息，除了传递给 continuation 的比较结果Weigh。

推荐阅读