这里是一个数学练习（取自page 2-俄语）：
有100种在视觉上无法区分的金币，分为三种类型：金，银和铜（每种类型至少出现一次）。众所周知，金重3克，银重2克，铜重1克。如何在不带砝码的两板秤上确定不超过101磅的所有硬币的类型？
（（注：我想这个练习是错误的，最多需要进行102称重。但这没关系）
解决方案如下：
c
0
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]
但是我什至不能证明这个引理。问题是：
weigh函数在算法中最多使用n + 2次的引理，其中n是硬币数？您具有三个递归函数：determine_weights，find_heavier，weigh_coins。