Моя история довольно длинная, и мой код того, что я на самом деле хотел сделать, также довольно длинный.Итак, сначала я опишу то, что я пробовал с формулой в заголовке, а затем я опишу, как я столкнулся с чем-то подобным на практике, поместив мой фактический код в самый низ.
Я понимаю, что, возможно, яЯ должен был делать то, что хочу, совершенно по-другому: у меня нет опыта работы с Изабель (или даже большого опыта работы с функциональными языками программирования, такими как Haskell), поэтому мой код, вероятно, не идиоматичен.
ЧтоЯ сделал с этим
Во-первых, я понимаю, что все в разделе можно доказать с помощью by presburger (как мне сказал try).Это не работает с моей реальной проблемой, хотя и, вероятно, не должно, потому что там я имею дело с пользовательскими типами данных, содержащими целые числа, а не сами целые числа.
В попытках свести это к минимальной полной проверяемостиНапример, я заметил, что даже простые формулы, такие как "∃(x::nat). (x ≠ 2)", трудно доказать Изабель.Однако я подумал, что может помочь что-то конкретное, например x = 1.Действительно,
lemma "∃(x::nat). (x ≠ 2 ∧ x = 1)"
by auto
работал легко, но
lemma "∃(x::nat). (x ≠ 2 ∧ (x ≠ 2 ⟶ x = 1))"
by auto
по-прежнему не работает.Я подумал, что, возможно, мне следует сначала поставить бетонную часть, но когда я попытался
lemma "∃(x::nat). ((x ≠ 2 ⟶ x = 1) ∧ x ≠ 2)"
by auto
, линия by auto осталась пурпурной в jEdit, что, как я считаю, указывает на бесконечный цикл.
КакЯ столкнулся с этим
Я пытаюсь использовать Изабель, чтобы сделать модель для Сёги , и в конечном итоге доказать уникальность решения некоторых проблем сёги.Когда я попытался доказать, что простая конфигурация является матом, Изабель застряла (для контекста, у меня было datatype coord = Coord int int):
∃dst. dst ≠ Coord 5 3 ∧
(dst ≠ Coord 5 3 ⟶
dst ≠ Coord 5 2 ∧
(dst ≠ Coord 5 2 ⟶
(dst = Coord 5 1 ⟶
(∃src. src ≠ Coord 5 3 ∧ (src ≠ Coord 5 3 ⟶ src = Coord 5 2))) ∧
dst = Coord 5 1))
Я знаю, это выглядит как беспорядок.Позвольте мне немного изменить отступ, чтобы облегчить анализ человеческих глаз.
∃dst. dst ≠ Coord 5 3 ∧
(
dst ≠ Coord 5 3 ⟶
dst ≠ Coord 5 2 ∧
(
dst ≠ Coord 5 2 ⟶
(
dst = Coord 5 1 ⟶
(∃src. src ≠ Coord 5 3 ∧ (src ≠ Coord 5 3 ⟶ src = Coord 5 2))
) ∧ dst = Coord 5 1
)
)
Надеюсь, можно увидеть, что src = Coord 5 2 соответствует одной строке с src, а затем dst = Coord 5 1 удовлетворяетвсе это.
Я пытался представить это как лемму и доказать это by auto --- конечно, это не работает.Я наконец попробовал by try, и он сказал мне:
"cvc4": Try this: by (smt coord.inject) (866 ms)
ОК, это сработало.Но я действительно сбит с толку, потому что я даже не знаю, что такое smt.
Несмотря на это, этот метод (после применения auto) успешно доказал, что игрок 2 находится под контролем.Я пытался использовать тот же метод, чтобы доказать, что это мат (который, по крайней мере, равносилен доказательству того, что в нескольких конфигурациях Player 2 все еще проверяется), но это также привело к ошибке:
Solver z3: Solver "z3" failed -- enable tracing using the "smt_trace" option for details
Даже sledgehammer мне не помогли.
Поскольку проверки и маты находятся в самых основных правилах проблем сёги, я думаю, что мне нужно иметь возможность распознавать их автоматически, прежде чем я смогу сделать что-нибудь нетривиальное,Я открыт для того, чтобы записывать и доказывать несколько лемм вручную, но теперь я считаю, что я могу делать что-то принципиально неправильное.
Мой код
Если есть что-то, что мне нужно уточнитьПожалуйста, спросите в комментариях.
theory Shogi
imports Main "HOL-Library.Multiset"
begin
datatype coord = Coord int int
datatype vector = Vector int int
datatype piece_type = King | Gold
datatype move = Move coord coord | Drop piece_type coord
datatype player = Sente | Gote
type_synonym on_board = "(coord, player * piece_type) map"
datatype board = Board on_board "(player * piece_type) multiset" player
fun opponent :: "player ⇒ player" where
"opponent Sente = Gote" |
"opponent Gote = Sente"
fun diff :: "coord ⇒ coord ⇒ vector" where
"diff (Coord x1 y1) (Coord x0 y0) = Vector (x1 - x0) (y1 - y0)"
fun negate :: "vector ⇒ vector" where
"negate (Vector x y) = (Vector (-x) (-y))"
fun to_hand :: "(player * piece_type) option ⇒ (player * piece_type) multiset" where
"to_hand None = {#}" |
"to_hand (Some (owner, piece)) = {#((opponent owner), piece)#}"
fun make_move :: "board ⇒ move ⇒ board" where
"make_move (Board on_board in_hand to_move) (Move src dst) =
(Board
(on_board(src := None, dst := (on_board src)))
(in_hand + (to_hand (on_board dst)))
(opponent to_move)
)" |
"make_move (Board on_board in_hand to_move) (Drop piece pos) =
(Board
(on_board(pos := Some (to_move, piece)))
(in_hand - {#(to_move, piece)#})
(opponent to_move)
)"
fun is_on_board :: "coord ⇒ bool" where
"is_on_board (Coord file rank) = (1 ≤ file ∧ file ≤ 9 ∧ 1 ≤ rank ∧ rank ≤ 9)"
fun movement_vector :: "piece_type ⇒ vector ⇒ bool" where
"movement_vector King (Vector x y) = ((x, y) ∈ {
(1, -1), (0, -1), (-1, -1),
(1, 0), (-1, 0),
(1, 1), (0, 1), (-1, 1)})" |
"movement_vector Gold (Vector x y) = ((x, y) ∈ {
(1, -1), (0, -1), (-1, -1),
(1, 0), (-1, 0),
(0, 1) })"
fun negated_movement_vector :: "piece_type ⇒ vector ⇒ bool" where
"negated_movement_vector piece vector = movement_vector piece (negate vector)"
fun absolute_movement_vector :: "player ⇒ piece_type ⇒ vector ⇒ bool" where
"absolute_movement_vector Sente = movement_vector" |
"absolute_movement_vector Gote = negated_movement_vector"
fun is_legal_for_piece :: "(player * piece_type) option ⇒ player ⇒ on_board
⇒ coord ⇒ coord ⇒ bool" where
"is_legal_for_piece None _ _ _ _ = False" |
"is_legal_for_piece (Some (owner, piece)) to_move on_board src dst =
(owner = to_move ∧ absolute_movement_vector owner piece (diff dst src))"
fun get_owner :: "(player * piece_type) option ⇒ player option" where
"get_owner None = None" | "get_owner (Some (owner, piece)) = Some owner"
fun is_legal_physically :: "board ⇒ move ⇒ bool" where
"is_legal_physically (Board on_board in_hand to_move) (Move src dst) =
(
(is_on_board dst) ∧
(get_owner (on_board dst)) ≠ Some to_move ∧
(is_legal_for_piece (on_board src) to_move on_board src dst)
)" |
"is_legal_physically (Board on_board in_hand to_move) (Drop piece pos) =
((is_on_board pos) ∧ ((on_board pos) = None))"
fun is_in_check :: "on_board ⇒ player ⇒ bool" where
"is_in_check on_board player =
(∃dst src.
(on_board dst) = Some (player, King) ∧
(is_legal_for_piece (on_board src) (opponent player) on_board src dst)
)"
fun is_legal_board :: "board ⇒ bool" where
"is_legal_board (Board on_board in_hand to_move) =
(¬(is_in_check on_board (opponent to_move)))"
fun is_legal :: "board ⇒ move ⇒ bool" where
"is_legal board move =
(
(is_legal_physically board move) ∧
(is_legal_board (make_move board move))
)"
fun is_mate :: "board ⇒ bool" where "is_mate board = (¬(∃move. (is_legal board move)))"
fun is_checkmate :: "board ⇒ bool" where
"is_checkmate (Board on_board in_hand to_move) = (
(is_mate (Board on_board in_hand to_move)) ∧ (is_in_check on_board to_move))"
abbreviation board1 :: on_board where "board1 ≡ (map_of [
((Coord 5 1), (Gote, King)),
((Coord 5 2), (Sente, Gold)),
((Coord 5 3), (Sente, King))
])"
lemma "∃dst. dst ≠ Coord 5 3 ∧
(dst ≠ Coord 5 3 ⟶
dst ≠ Coord 5 2 ∧
(dst ≠ Coord 5 2 ⟶
(dst = Coord 5 1 ⟶
(∃src. src ≠ Coord 5 3 ∧ (src ≠ Coord 5 3 ⟶ src = Coord 5 2))) ∧
dst = Coord 5 1))"
by (smt coord.inject)
lemma "is_in_check board1 Gote"
apply auto
apply (smt coord.inject)
done
lemma "is_checkmate (Board board1 {#} Gote)"
apply auto
apply sledgehammer (* Both "cvc4" and "vampire" timed out *)
apply (smt coord.inject) (* Solver z3: Solver "z3" failed -- enable tracing using the "smt_trace" option for details *)
apply presburger (* Failed to apply proof method *)
end