我的故事很长，我真正想做的代码也很长。所以首先我将描述我用标题中的公式尝试过的事情，然后我将描述我在实践中是如何遇到这样的事情的，将我的实际代码放在最底部。
我知道也许我应该以完全不同的方式完成我想做的事情：我之前没有使用 Isabelle 的经验（甚至没有使用 Haskell 等函数式编程语言的丰富经验），所以我的代码可能不是惯用的。
我用它做了什么
首先，我知道本节中的所有内容都可以用by presburger（try告诉我的）来证明。不过，这不适用于我的实际问题，而且可能不应该，因为我在那里处理包含整数的自定义数据类型，而不是整数本身。
在尝试将其简化为一个最小的完整可验证示例时，我注意到即使是简单的公式"∃(x::nat). (x ≠ 2)"也很难为 Isabelle 证明。但是，我认为具体的东西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 中保持紫色，我认为这表示无限循环。
我是怎么遇到的
我正在尝试使用 Isabelle 为Shogi制作模型，并最终证明解决某些 Shogi 问题的唯一性。当我试图证明一个简单的配置是一个将死时，伊莎贝尔被困在了（为了上下文，我有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 处于检查状态。我尝试使用相同的方法来证明它是一个将死（至少，这相当于证明在几个配置中玩家 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