在agda中使用计算函数的值作为证明

Question

我仍然试图围绕agda,所以我写了一个小小的tic-tac-toe游戏类型

data Game : Player -> Vec Square 9 -> Set where
 start : Game x ( - ? - ? - ?
                  - ? - ? - ?
                  - ? - ? - ? [] )
 xturn : {gs : Vec Square 9} -> (n : ?) -> Game x gs -> n < (#ofMoves gs) -> Game o (makeMove gs x n )
 oturn : {gs : Vec Square 9} -> (n : ?) -> Game o gs -> n < (#ofMoves gs) -> Game x (makeMove gs o n )

哪个将保持有效的游戏路径.

这里#ofMoves gs将返回空Squares 的数量, n < (#ofMoves gs)将证明该n移动有效,并makeMove gs x n替换n游戏状态向量中的空方块.

在对自己进行了一些激动人心的游戏后,我决定拍摄一些更棒的东西.我们的目标是创造一个能够吸引x玩家和玩家的功能,并在与死亡的史诗般战斗中相互对抗.

--two programs enter, one program leaves
gameMaster : {p : Player } -> {gs : Vec Square 9} --FOR ALL
 -> ({gs : Vec Square 9} -> Game x gs -> (0 < (#ofMoves gs)) -> Game o (makeMove gs x _ )) --take an x player
 -> ({gs : Vec Square 9} -> Game o gs -> (0 < (#ofMoves gs)) -> Game x (makeMove gs o _ )) --take an o player
 -> ( Game p gs)  --Take an initial configuration
 -> GameCondition --return a winner
gameMaster {_} {gs} _ _ game with (gameCondition gs)
... | xWin = xWin
... | oWin = oWin
... | draw = draw
... | ongoing  with #ofMoves gs
... | 0 = draw --TODO: really just prove this state doesn't exist, it will always be covered by gameCondition gs = draw
gameMaster {x} {gs} fx fo game | ongoing | suc nn = gameMaster (fx) (fo) (fx game (s?s z?n)) -- x move
gameMaster {o} {gs} fx fo game | ongoing | suc nn = gameMaster (fx) (fo) (fo game (s?s z?n)) -- o move

这里(0 < (#ofMoves gs))是"手短"的一个证据,证明该游戏正在进行中, gameCondition gs将返回了比赛状态,你会期望(之一xWin,oWin,draw,或ongoing)

我想证明有有效的动作(s?s z?n部分).这应该是可能的,因为suc nn<= #ofMoves gs.我不知道如何在agda中完成这项工作.

Answer 1

我会尝试回答你的一些问题,但我不认为你从正确的角度来看这个问题.虽然您当然可以使用显式证明使用有界数字,但您很可能会更成功地使用数据类型.

对于你makeMove(我已经move在答案的其余部分重命名),你需要一个由可用的自由方块限定的数字.也就是说,当你有4个自由方格时,你希望能够move只用0,1,2和3 调用.有一个非常好的方法来实现它.

看一下Data.Fin,我们发现这个有趣的数据类型:

data Fin : ? ? Set where
  zero : {n : ?} ? Fin (suc n)
  suc  : {n : ?} (i : Fin n) ? Fin (suc n)

Fin 0是空的(既zero和suc构造Fin n为n大于或小于1相等).Fin 1只有zero,Fin 2有zero和suc zero,等等.这正是我们所需要的:一个数字限制的数字n.您可能已经在安全向量查找的实现中看到过这种情况:

lookup : ? {a n} {A : Set a} ? Fin n ? Vec A n ? A
lookup zero    (x ? xs) = x
lookup (suc i) (x ? xs) = lookup i xs

的lookup _ []情况下是不可能的,因为Fin 0没有任何元素!

如何很好地应用这个问题？首先,我们必须跟踪我们有多少个空方格.这允许我们证明gameMaster确实是终止函数(空方块的数量总是在减少).让我们写一个变体,Vec它不仅跟踪长度,还跟踪空方块:

data Player : Set where
  x o : Player

data SquareVec : (len : ?) (empty : ?) ? Set where
  []  :                                        SquareVec 0 0
  -?_ : ? {l e}              ? SquareVec l e ? SquareVec (suc l) (suc e)
  _?_ : ? {l e} (p : Player) ? SquareVec l e ? SquareVec (suc l) e

请注意,我摆脱了Square数据类型; 相反,空方块直接烘焙到-?_构造函数中.而不是- ? rest我们拥有-? rest.

我们现在可以编写这个move函数了.它的类型应该是什么？好吧,它需要一个SquareVec至少有一个空方格,一个Fin e(e空方格的数量)和一个Player.在Fin e保证我们,这个函数总能找到合适的空方:

move : ? {l e} ? Player ? SquareVec l (suc e) ? Fin (suc e) ? SquareVec l e
move             p (  -? sqs) zero     = p  ? sqs
move {e = zero}  p (  -? sqs) (suc ())
move {e = suc e} p (  -? sqs) (suc fe) =   -? move p sqs fe
move             p (p? ? sqs) fe       = p? ? move p sqs fe

请注意,此函数为我们提供了一个SquareVec正好填充的空方块.这个功能根本不能填充多个或没有空方块!

我们沿着向量走向寻找一个空的广场; 一旦我们找到它,Fin争论告诉我们这是否是我们要填写的方格.如果是zero,我们填写玩家; 如果不是,我们继续搜索向量的其余部分,但数字较小.

现在,游戏代表.感谢我们之前做的额外工作,我们可以简化Game数据类型.该move-p构造函数只是告诉我们,此举发生的地点,这就是它!Player为简单起见,我摆脱了索引; 但它可以正常使用它.

data Game : ? {e} ? SquareVec 9 e ? Set where
  start  :                                             Game empty
  move-p : ? {e} {gs} p (fe : Fin (suc e)) ? Game gs ? Game (move p gs fe)

哦,什么empty？这是你的捷径- ? - ? ...:

empty : ? {n} ? SquareVec n n
empty {zero}  = []
empty {suc _} = -? empty

现在,各州.我将状态分为可能正在运行的游戏状态和结束游戏的状态.再次,您可以使用您的原始GameCondition:

data State : Set where
  win   : Player ? State
  draw  :          State
  going :          State

data FinalState : Set where
  win  : Player ? FinalState
  draw :          FinalState

对于以下代码,我们需要这些导入:

open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality

并且有一个确定游戏状态的功能.填写您的实际实施; 这个让玩家玩,直到电路板完全充满.

-- Dummy implementation.
state : ? {e} {gs : SquareVec 9 e} ? Game gs ? State
state {zero}  gs = draw
state {suc _} gs = going

接下来,我们需要证明的是,State不能going在没有空方块:

zero-no-going : ? {gs : SquareVec 9 0} (g : Game gs) ? state g ? going
zero-no-going g ()

再次,这是假人state的证明,你实际实施的证据将是非常不同的.

现在,我们拥有了实施所需的所有工具gameMaster.首先,我们必须决定它的类型.就像你的版本中,我们将两个函数代表了AI,一个用于o和其他的x.然后我们将采取游戏状态并制作FinalState.在这个版本中,我实际上正在返回最终的棋盘,以便我们可以看到游戏的进展情况.

现在,AI功能将返回他们想要的转弯,而不是返回整个新的游戏状态.这更容易使用.

支撑自己,这是我想到的类型签名:

AI : Set
AI = ? {e} {sqv : SquareVec 9 (suc e)} ? Game sqv ? Fin (suc e)

gameMaster : ? {e} {sqv : SquareVec 9 e} (sp : Player)
  (x-move o-move : AI) ? Game sqv ?
  FinalState × (?[ e? ? ? ] ?[ sqv? ? SquareVec 9 e? ] Game sqv?)

请注意,AI函数采用至少有一个空方块的游戏状态并返回一个移动.现在进行实施.

gameMaster sp xm om g with state g
... | win p = win p , _ , _ , g
... | draw  = draw  , _ , _ , g
... | going = ?

因此,如果当前状态是win或draw,我们将返回相应的FinalState和当前的板.现在,我们必须处理going此案.我们将模式匹配e(空方格的数量)以确定游戏是否在最后:

gameMaster {zero}  sp xm om g | going = ?
gameMaster {suc e} x  xm om g | going = ?
gameMaster {suc e} o  xm om g | going = ?

这种zero情况不可能发生,我们事先证明,当空方数为零时state无法返回going.如何在这里申请证明？

我们有匹配的模式state g,我们现在知道state g ? going; 但遗憾的是阿格达已经忘记了这些信息.这就是Dominique Devriese所暗示的:inspect机器允许我们保留证据!

而不仅仅是模式匹配state g,我们还将模式匹配inspect state g:

gameMaster sp xm om g with state g | inspect state g
... | win p | _ = win p , _ , _ , g
... | draw  | _ = draw  , _ , _ , g
gameMaster {zero}  sp xm om g | going | [ pf ] = ?
gameMaster {suc e} x  xm om g | going | _      = ?
gameMaster {suc e} o  xm om g | going | _      = ?

pf现在证明state g ? going,我们可以提供给zero-no-going:

gameMaster {zero}  sp xm om g | going | [ pf ]
  = ?-elim (zero-no-going g pf)

另外两种情况很简单:我们只应用AI函数并递归地应用于gameMaster结果:

gameMaster {suc e} x  xm om g | going | _ 
  = gameMaster o xm om (move-p x (xm g) g)
gameMaster {suc e} o  xm om g | going | _
  = gameMaster x xm om (move-p o (om g) g)

我写了一些愚蠢的AI,第一个填充了第一个可用的空方块; 第二个填充最后一个.

player-lowest : AI
player-lowest _ = zero

max : ? {e} ? Fin (suc e)
max {zero}  = zero
max {suc e} = suc max

player-highest : AI
player-highest _ = max

现在,让我们的比赛player-lowest对player-lowest!在Emacs中,键入C-c C-n gameMaster x player-lowest player-lowest start <RET>:

draw ,
0 ,
x ? (o ? (x ? (o ? (x ? (o ? (x ? (o ? (x ? [])))))))) ,
move-p x zero
(move-p o zero
 (move-p x zero
  (move-p o zero
   (move-p x zero
    (move-p o zero
     (move-p x zero
      (move-p o zero
       (move-p x zero start))))))))

我们可以看到所有正方形都被填充,它们在x和之间交替o.匹配player-lowest与player-highest给我们:

draw ,
0 ,
x ? (x ? (x ? (x ? (x ? (o ? (o ? (o ? (o ? [])))))))) ,
move-p x zero
(move-p o (suc zero)
 (move-p x zero
  (move-p o (suc (suc (suc zero)))
   (move-p x zero
    (move-p o (suc (suc (suc (suc (suc zero)))))
     (move-p x zero
      (move-p o (suc (suc (suc (suc (suc (suc (suc zero)))))))
       (move-p x zero start))))))))

如果你真的想使用证明,那么我建议如下表示Fin:

Fin? : ? ? Set
Fin? n = ? ? m ? m < n

fin?fin? : ? {n} ? Fin n ? Fin? n
fin?fin? zero    = zero , s?s z?n
fin?fin? (suc n) = map suc s?s (fin?fin? n)

fin??fin : ? {n} ? Fin? n ? Fin n
fin??fin {zero}  (_     , ())
fin??fin {suc _} (zero  , _)     = zero
fin??fin {suc _} (suc _ , s?s p) = suc (fin??fin (_ , p))

与问题没有严格关联,但inspect使用了相当有趣的技巧,值得一提.要理解这个技巧,我们必须看看它是如何with工作的.

当你with在表达式上使用时expr,Agda会遍历所有参数的类型,并用expr新变量替换任何出现,让我们调用它w.例如:

test : (n : ?) ? Vec ? (n + 0) ? ?
test n v = ?

正如您所料,这里的类型v是Vec ? (n + 0).

test : (n : ?) ? Vec ? (n + 0) ? ?
test n v with n + 0
... | w = ?

然而,一旦我们抽象n + 0,v突然改变的类型Vec ? w.如果您以后想要使用n + 0其类型中包含的内容,则替换不会再次发生 - 这是一次性交易.

在gameMaster函数中,我们应用with到state g和模式匹配,找出它的going.到我们使用时zero-no-going,state g并且going是两个与Agda无关的独立事物.

我们如何保存这些信息？我们不知何故需要得到state g ? state g并且with只state g在任何一方进行替换- 这将为我们提供所需的state g ? going.

inspect它隐藏功能应用程序的作用是什么state g.我们必须写一个函数hide的方式,阿格达不能看到hide state g和state g实际上都是一样的东西.

隐藏某些东西的一种可能方法是使用任何类型的事实A,A并且? ? A是同构的 - 也就是说,我们可以自由地从一个表示到另一个表示而不会丢失任何信息.

但是,我们不能使用?标准库中定义的.稍后我会说明原因,但就目前而言,我们将定义一个新类型:

data Unit : Set where
  unit : Unit

以及隐藏价值意味着什么:

Hidden : Set ? Set
Hidden A = Unit ? A

我们可以reveal通过申请unit来轻松隐藏价值:

reveal : {A : Set} ? Hidden A ? A
reveal f = f unit

我们需要采取的最后一步是hide功能:

hide : {A : Set} {B : A ? Set} ?
       ((x : A) ? B x) ? ((x : A) ? Hidden (B x))
hide f x unit = f x

为什么这不适用?？如果你声明?为记录,Agda可以自己弄清楚这tt是唯一的值.所以,面对时hide f x,Agda不会停在第三个参数(因为它已经知道它必须是什么样子)并自动将它减少到? _ ? f x.使用data关键字定义的数据类型没有这些特殊规则,所以hide f x保持这种方式直到有人reveal和类型检查器无法看到f x内部存在子表达式hide f x.

其余的只是安排东西,以便我们以后可以得到证据:

data Reveal_is_ {A : Set} (x : Hidden A) (y : A) : Set where
  [_] : (eq : reveal x ? y) ? Reveal x is y

inspect : {A : Set} {B : A ? Set}
          (f : (x : A) ? B x) (x : A) ? Reveal (hide f x) is (f x)
inspect f x = [ refl ]

所以你有它:

inspect state g : Reveal (hide state g) is (state g)
-- pattern match on (state g)
inspect state g : Reveal (hide state g) is going

当你那时reveal hide state g,你会得到state g并最终证明state g ? going.