Вот математическое упражнение (взято с стр. 2 - на русском языке):
Существует 100 визуально неразличимых монет трех типов: золото, серебро и медь (каждая тип встречается хотя бы один раз). Известно, что золото весит 3 грамма каждый, серебро весит 2 грамма каждый, медь весит 1 грамм каждый. Как определить тип всех монет весом не более 101 на двухпластинчатых весах без гирь?
(Примечание. Полагаю, что упражнение неверное и требуется не более 102 взвешиваний). Однако это не имеет значения)
Решение состоит в следующем:
- Возьмите монеты одну из одной из списка монет и сравните каждую монету с предыдущей
- Если монеты имеют одинаковый вес, то мы назначаем их одной группе и продолжаем весить дальше
- Если мы нашли более тяжелую монету c j , чем предыдущая, то go с шагом 2
- Если мы нашли более легкую монету c i , чем предыдущая, продолжайте взвешивать монеты, пытаясь найти монету c j тяжелее c i
- Если вместо этого мы нашли более легкую монету, то c 0 > c i > c j и мы знаем вес этих монет: 3> 2> 1. Go с шагом 3
- Ke еп сравнение монет
- Если мы нашли более тяжелую монету c k , чем c j , то c i j k (и веса 1 <2 <3) </li>
- Если мы нашли более легкую монету c k чем c j , затем сравните c i и c k
- Если c i 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 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
- Сравнить остальные монеты с серебряной монетой (или двумя медными монетами)
- легкие монеты медные
- такие же монеты серебряные
- более тяжелые монеты золотые
- Если на шаге 1 мы сначала нашли более легкую монету вместо более тяжелой, то нам нужно сравнить первые тяжелые монеты с серебряной монетой, чтобы определить их вес (это может быть 102-е взвешивание в зависимости от набора монет)
Вот пример списка монет:
c<sub>0</sub> c<sub>i</sub> c<sub>j</sub> c<sub>k</sub>
3 3 2 2 2 3 3 1 1 2 1 3
|_| |___| |_|
i j k
Вот решение в Изабель 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]
Однако я не могу доказать даже эту лемму.
Вопросы:
- Не могли бы вы предложить, как можно доказать такую лемму или как переформулировать функции, чтобы сделать леммы доказуемыми?
- Как сформулировать лемму о том, что функция
weigh используется самое большее n + 2 раз в алгоритм, где n количество монет?