在 agda 中使用计算函数的值进行证明 [英] Using the value of a computed function for a proof in agda

查看：35 发布时间：2021/9/7 19:26:45 tic-tac-toe proof agda

本文介绍了在 agda 中使用计算函数的值进行证明的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

我仍在尝试围绕 agda 进行思考，所以我写了一个小井字游戏类型

data Game : Player ->维克广场 9 ->设置在哪里开始:游戏 x ( - ∷ - ∷ - ∷- ∷ - ∷ - ∷- ∷ - ∷ - ∷ [] )xturn : {gs : Vec Square 9} ->(n: ℕ) ->游戏 x gs ->≤(#ofMoves gs) ->游戏 o (makeMove gs x n )反过来:{gs:Vec Square 9} ->(n: ℕ) ->游戏 o gs ->≤(#ofMoves gs) ->游戏 x (makeMove gs on n )

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

这里 #ofMoves gs 将返回空 Square 的数量，<代码>n <(#ofMoves gs) 将证明第 n 步是有效的，makeMove gs x n 替换游戏状态向量中的第 n 个空方块.

在与自己进行了几场刺激的比赛后，我决定尝试一些更棒的东西.目标是创建一个函数，让 x 玩家和 o 玩家在史诗般的战斗中相互对抗.

--两个程序进入，一个程序离开gameMaster : {p : Player } ->{gs : Vec Square 9} --FOR ALL->({gs : Vec Square 9} -> Game x gs -> (0 < (#ofMoves gs)) -> Game o (makeMove gs x _ )) -- 拿一个 x 玩家->({gs : Vec Square 9} -> Game o gs -> (0 < (#ofMoves gs)) -> Game x (makeMove gs o _ )) -- 选择一个玩家->( 游戏 p gs) -- 进行初始配置->GameCondition -- 返回一个赢家gameMaster {_} {gs} _ _ game with (gameCondition gs)... |xWin = xWin... |oWin = oWin... |画 = 画... |正在进行#ofMoves gs... |0 = draw --TODO: 真的只是证明这个状态不存在，它会一直被gameCondition覆盖 gs = drawgameMaster {x} {gs} 外汇游戏 |正在进行 |suc nn = gameMaster (fx) (fo) (fx game (s≤s z≤n)) -- x 移动gameMaster {o} {gs} 外汇游戏 |正在进行 |suc nn = gameMaster (fx) (fo) (fo game (s≤s z≤n)) -- o 移动

这里 (0 < (#ofMoves gs)) 是证明游戏正在进行的简写"，gameCondition gs 将按照您的预期返回游戏状态(xWin、oWin、draw 或 <代码>正在进行)

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

解决方案

我会尝试回答您的一些问题，但我认为您的角度不正确.虽然您当然可以使用显式证明处理有界数，但使用数据类型很可能会更成功.

对于您的 makeMove(我在答案的其余部分将其重命名为 move)，您需要一个以可用自由方块为界的数字.也就是说，当您有 4 个空闲方块时，您希望能够仅使用 0、1、2 和 3 调用 move.有一种非常好的方法可以实现这一点.

查看 Data.Fin，我们发现这个有趣的数据类型:

data Fin : ℕ → 设置位置零 : {n : ℕ} → Fin (suc n)suc : {n : ℕ} (i : Fin n) → Fin (suc n)

Fin 0 为空(zero 和 suc 为 n 构造 Fin n代码> 大于或等于 1).Fin 1 只有 zero，Fin 2 有 zero 和 suc zero，并且很快.这正是我们所需要的:一个以 n 为界的数字.您可能已经在安全向量查找的实现中看到了这一点:

lookup : ∀ {a n} {A : Set a} → Fin n → Vec A n → A查找零 (x ∷ xs) = x查找 (suc i) (x ∷ xs) = 查找 i xs

lookup _ [] 情况是不可能的，因为 Fin 0 没有元素！

如何将其很好地应用于您的问题?首先，我们必须跟踪我们有多少空方块.这让我们可以证明 gameMaster 确实是一个终止函数(空方块的数量一直在减少).让我们编写一个 Vec 的变体，它不仅跟踪长度，还跟踪空方块:

data Player : 设置位置x o : 玩家data SquareVec : (len : ℕ) (empty : ℕ) → Set where[]:SquareVec 0 0-∷_ : ∀ {le e} → SquareVec l e → SquareVec (suc l) (suc e)_∷_ : ∀ {le e} (p : Player) → SquareVec l e → SquareVec (suc l) e

注意我去掉了 Square 数据类型；相反，空方块被直接烘焙到 -∷_ 构造函数中.代替 - ∷ rest 我们有 -∷ rest.

我们现在可以编写move 函数.它的类型应该是什么?好吧，它需要一个 SquareVec 至少有一个空方块，一个 Fin e(其中 e 是空方块的数量)和播放器.Fin e 保证我们这个函数总能找到合适的空方块:

move : ∀ {le e} → Player → SquareVec l (suc e) → Fin (suc e) → SquareVec l e移动 p ( -∷ sqs) 零 = p ∷ sqs移动 {e = 零} p ( -∷ sqs) (suc ())移动 {e = suc e} p ( -∷ sqs) (suc fe) = -∷ 移动 p sqs fe移动 p (p′ ∷ sqs) fe = p′ ∷ 移动 p sqs fe

请注意，此函数为我们提供了一个 SquareVec，其中正好填充了一个空方块.此函数不能填充超过一个或根本没有空方块！

我们沿着向量走下去寻找一个空方块；一旦我们找到它，Fin 参数告诉我们它是否是我们想要填充的方块.如果它是 0，我们填充玩家；如果不是，我们继续搜索向量的其余部分，但使用较小的数字.

现在，游戏代表.由于我们之前所做的额外工作，我们可以简化 Game 数据类型.move-p 构造函数只是告诉我们移动发生的位置，仅此而已！为了简单起见，我去掉了 Player 索引；但它会很好用.

data Game : ∀ {e} → SquareVec 9 e → 设置 where开始:游戏为空move-p : ∀ {e} {gs} p (fe : Fin (suc e)) → Game gs → Game (move p gs fe)

哦，什么是空?这是您的 - ∷ - ∷ ... 的快捷方式:

empty : ∀ {n} → SquareVec n n空 {零} = []空 {suc _} = -∷ 空

现在，各州.我将状态分为可能正在运行的游戏状态和已结束游戏的状态.同样，您可以使用您原来的 GameCondition:

data State : 设置位置胜利:玩家→状态绘制:状态去:状态data FinalState : 设置位置获胜:玩家 → FinalState绘制:最终状态

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

打开导入 Data.Empty打开导入 Data.Product打开导入 Relation.Binary.PropositionalEquality

还有一个确定游戏状态的函数.填写您的实际实施；这个只是让玩家玩到棋盘完全填满为止.

-- 虚拟实现.状态 : ∀ {e} {gs : SquareVec 9 e} → 游戏 gs → 状态状态 {零} gs = 绘制状态 {suc _} gs = 去

接下来需要证明State在没有空方块的情况下不能going:

zero-no-going : ∀ {gs : SquareVec 9 0} (g : Game gs) → state g ≢ going零不去 g ()

同样，这是虚拟state的证明，您实际实现的证明将大不相同.

现在，我们拥有了实现 gameMaster 所需的所有工具.首先，我们必须确定它的类型是什么.与您的版本非常相似，我们将采用两个表示 AI 的函数，一个用于 o，另一个用于 x.然后我们将获取游戏状态并生成 FinalState.在这个版本中，我实际上返回了最终版，以便我们了解游戏的进展情况.

现在，AI 函数将只返回他们想要的回合，而不是返回全新的游戏状态.这更容易使用.

振作起来，这是我想到的类型签名:

AI : 设置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) → 游戏 sqv →FinalState × (Σ[ e′ ∈ ℕ ] Σ[ sqv′ ∈ SquareVec 9 e′ ] 游戏 sqv′)

请注意，AI 函数采用至少有一个空方格的游戏状态并返回一个移动.现在开始实施.

gameMaster sp xm om g 状态为 g... |赢 p = 赢 p , _ , _ , g... |画 = 画, _ , _ , g... |去 = ?

因此，如果当前状态是win 或draw，我们将返回相应的FinalState 和当前的棋盘.现在，我们必须处理 going 的情况.我们将对 e(空方块的数量)进行模式匹配，以确定游戏是否结束:

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

zero 的情况不会发生，我们之前证明了state 在空方块数为零时不能返回going.如何在此处应用该证明?

我们在state g上匹配了模式，我们现在知道state g ≡ going；但遗憾的是 Agda 已经忘记了这些信息.这就是 Dominique Devriese 所暗示的:inspect 机制允许我们保留证据！

除了在 state g 上进行模式匹配之外，我们还将在 inspect state g 上进行模式匹配:

gameMaster sp xm om g 状态为 g |检查状态 g... |赢p |_ = 赢 p , _ , _ , g... |画 |_ = 画, _ , _ , ggameMaster {零} sp xm om g |去|[ pf ] = ?gameMaster {suc e} x xm om g |去|_ = ?gameMaster {suc e} o xm om g |去|_ = ?

pf 现在是 state g ≡ going 的证明，我们可以将其提供给 zero-no-going:

gameMaster {zero} sp xm om g |去|[ pf ]= ⊥-elim(零不去 g pf)

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

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

<小时>

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

player-lowest : AI玩家最低的 _ = 零max : ∀ {e} → Fin (suc e)最大{零} = 零最大 {suc e} = 最大玩家最高:AI玩家最高 _ = 最大

现在，让我们将 player-lowest 与 player-lowest 进行匹配！在 Emacs 中，输入 C-c C-n gameMaster x player-lowest player-lowest start :

draw ,0 ,x ∷ (o ∷ (x ∷ (x ∷ (o ∷ (x ∷ (o ∷ (x ∷ (o ∷ (x ∷ [])))))))) ,移动-p x 零(move-p o 零(移动-p x 零(move-p o 零(移动-p x 零(move-p o 零(移动-p x 零(move-p o 零(move-p x 零开始)))))))))

我们可以看到所有的方块都被填满了，它们在 x 和 o 之间交替.将 player-lowest 与 player-highest 匹配给我们:

draw ,0 ,x ∷ (x ∷ (x ∷ (x ∷ (x ∷ (x ∷ (o ∷ (o ∷ (o ∷ (o ∷ [])))))))) ,移动-p x 零(move-p o (suc 零)(移动-p x 零(move-p o (suc (suc (suc 零)))(移动-p x 零(move-p o (suc (suc (suc (suc (suc zero)))))(移动-p x 零(move-p o (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))(move-p x 零开始)))))))))

<小时>

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

Fin₂ : ℕ → 设置Fin₂ n = ∃ λ m → m

<小时>

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

当你在表达式 expr 上使用 with 时，Agda 会检查所有参数的类型并用一个新的替换任何出现的 expr变量，我们称之为 w.例如:

test : (n : ℕ) → Vec ℕ (n + 0) → ℕ测试 n v = ?

这里，v 的类型是 Vec ℕ (n + 0)，正如你所期望的那样.

test : (n : ℕ) → Vec ℕ (n + 0) → ℕ用 n + 0 测试 n v... |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 - 这将为我们提供所需的 <代码>状态 g ≡ 运行.

inspect 的作用是隐藏函数应用state g.我们必须以一种Agda 看不到的方式编写hide 函数，hide state g 和state g 实际上是一回事.>

隐藏某些东西的一种可能方法是利用以下事实:对于任何类型 A，A 和 ⊤ → A 都是同构的 - 即也就是说，我们可以自由地从一种表示转到另一种表示，而不会丢失任何信息.

然而，我们不能使用标准库中定义的⊤.稍后我将说明原因，但现在，我们将定义一个新类型:

data Unit : 设置位置单位 : 单位

隐藏值意味着什么:

隐藏:设置→设置隐藏 A = 单位 → A

通过应用unit，我们可以很容易地揭示隐藏的值:

reveal : {A : Set} → Hidden A → A显示 f = f 单位

我们需要采取的最后一步是hide函数:

hide : {A : Set} {B : A → Set} →((x : A) → B x) → ((x : A) → 隐藏 (B x))隐藏 f x 单位 = f x

为什么这不适用于 ⊤?如果将 ⊤ 声明为记录，Agda 可以自行确定 tt 是唯一的值.所以，当面对 hide fx 时，Agda 不会停在第三个参数上(因为它已经知道它必须是什么样子)并自动将其缩减为 λ _ → fx.用 data 关键字定义的数据类型没有这些特殊规则，所以 hide fx 保持这种方式，直到有人 reveals 它和类型检查器无法看到 hide fx 中有一个 fx 子表达式.

剩下的就是整理一些东西，以便我们以后可以得到证明:

data Reveal_is_ {A : Set} (x : Hidden A) (y : A) : Set where[_] : (eq : 揭示 x ≡ y) → 揭示 x 是 y检查:{A:设置} {B:A→设置}(f : (x : A) → B x) (x : A) → Reveal (hide f x) is (f x)检查 f x = [ refl ]

所以，你有它:

inspect state g : Reveal (hide state g) is (state g)-- 模式匹配(状态 g)检查状态 g : Reveal (hide state g) is going

当你然后 reveal hide state g 时，你会得到 state g 和最后证明 state g ≡ go.

I'm still trying to wrap my head around agda, so I wrote a little tic-tac-toe game Type

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 )

Which will hold a valid game path.



Here #ofMoves gs would return the number of empty Squares,
n < (#ofMoves gs) would prove that the nth move is valid,
and makeMove gs x n replaces the nth empty Square in the game state vector.

After a few stimulating games against myself, I decided to shoot for something more awesome.  The goal was to create a function that would take an x player and an o player and pit them against each other in an epic battle to the death.
--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
Here (0 < (#ofMoves gs)) is "short hand" for a proof that that the game is ongoing,
gameCondition gs will return the game state as you would expect (one of xWin, oWin, draw, or ongoing)

I want to prove that there are valid moves (the s≤s z≤n part).  This should be possible since suc nn <= #ofMoves gs.  I have no idea how how to make this work in agda.
 解决方案 
I'll try to answer some of your questions, but I don't think you're apporaching this from the right angle. While you certainly can work with bounded numbers using explicit proofs, you'll most likely be more successful with data type instead.

For your makeMove (I've renamed it to move in the rest of the answer), you need a number bounded by the available free squares. That is, when you have 4 free squares, you want to be able to call move only with 0, 1, 2 and 3. There's one very nice way to achieve that.

Looking at Data.Fin, we find this interesting data type:
data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)
Fin 0 is empty (both zero and suc construct Fin n for n greater or equal than 1). Fin 1 only has zero, Fin 2 has zero and suc zero, and so on. This represents exactly what we need: a number bounded by n. You might have seen this used in the implementation of safe vector lookup:
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
The lookup _ [] case is impossible, because Fin 0 has no elements!

How to apply this nicely to your problem? Firstly, we'll have to track how many empty squares we have. This allows us to prove that gameMaster is indeed a terminating function (the number of empty squares is always decreasing). Let's write a variant of Vec which tracks not only length, but also the empty squares:
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
Notice that I got rid of the Square data type; instead, the empty square is baked directly into the -∷_ constructor. Instead of - ∷ rest we have -∷ rest.

We can now write the move function. What should its type be? Well, it'll take a SquareVec with at least one empty square, a Fin e (where e is the number of empty squares) and a Player. The Fin e guarantees us that this function can always find the appropriate empty square:
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
Notice that this function gives us a SquareVec with exactly one empty square filled. This function couldn't have filled more than one or no empty squares at all!

We walk down the vector looking for an empty square; once we find it, the Fin argument tells us whether it's the square we want to fill in. If it's zero, we fill in the player; if it isn't, we continue searching the rest of the vector but with a smaller number.

Now, the game representation. Thanks to the extra work we did earlier, we can simplify the Game data type. The move-p constructor just tells us where the move happened and that's it! I got rid of the Player index for simplicity; but it would work just fine with it.
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)
Oh, what's empty? It's shortcut for your - ∷ - ∷ ...:
empty : ∀ {n} → SquareVec n n
empty {zero}  = []
empty {suc _} = -∷ empty
Now, the states. I separated the states into a state of a possibly running game and a state of an ended game. Again, you can use your original GameCondition:
data State : Set where
  win   : Player → State
  draw  :          State
  going :          State

data FinalState : Set where
  win  : Player → FinalState
  draw :          FinalState
For the following code, we'll need these imports:
open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality
And a function to determine the game state. Fill in with your actual implementation; this one just lets players play until the board is completly full.
-- Dummy implementation.
state : ∀ {e} {gs : SquareVec 9 e} → Game gs → State
state {zero}  gs = draw
state {suc _} gs = going
Next, we need to prove that the State cannot be going when there are no empty squares:
zero-no-going : ∀ {gs : SquareVec 9 0} (g : Game gs) → state g ≢ going
zero-no-going g ()
Again, this is the proof for the dummy state, the proof for your actual implementation will be very different.

Now, we have all the tools we need to implement gameMaster. Firstly, we'll have to decide what its type is. Much like your version, we'll take two functions that represent the AI, one for o and other for x. Then we'll take the game state and produce FinalState. In this version, I'm actually returning the final board so we can see how the game progressed.

Now, the AI functions will return just the turn they want to make instead of returning whole new game state. This is easier to work with.

Brace yourself, here's the type signature I conjured up:
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′)
Notice that the AI functions take a game state with at least one empty square and return a move. Now for the implementation.
gameMaster sp xm om g with state g
... | win p = win p , _ , _ , g
... | draw  = draw  , _ , _ , g
... | going = ?
So, if the current state is win or draw, we'll return the corresponding FinalState and the current board. Now, we have to deal with the going case. We'll pattern match on e (the number of empty squares) to figure out whether the game is at the end or not:
gameMaster {zero}  sp xm om g | going = ?
gameMaster {suc e} x  xm om g | going = ?
gameMaster {suc e} o  xm om g | going = ?
The zero case cannot happen, we proved earlier that state cannot return going when the number of empty squares is zero. How to apply that proof here?

We have pattern matched on state g and we now know that state g ≡ going; but sadly Agda already forgot this information. This is what Dominique Devriese was hinting at: the inspect machinery allows us to retain the proof!

Instead of pattern matching on just state g, we'll also pattern matching on 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 is now the proof that state g ≡ going, which we can feed to zero-no-going:
gameMaster {zero}  sp xm om g | going | [ pf ]
  = ⊥-elim (zero-no-going g pf)
The other two cases are easy: we just apply the AI function and recursively apply gameMaster to the result:
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)




I wrote some dumb AIs, the first one fills the first available empty square; the second one fills the last one.
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
Now, let's match player-lowest against player-lowest! In the Emacs, type 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))))))))
We can see that all squares are filled and they alternate between x and o. Matching player-lowest with player-highest gives us:
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))))))))




If you really want to work with the proofs, then I suggest the following representation of 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))




Not strictly related to the question, but inspect uses rather interesting trick which might be worth mentioning. To understand this trick, we'll have to take a look at how with works.

When you use with on an expression expr, Agda goes through the types of all arguments and replaces any occurence of expr with a fresh variable, let's call it w. For example:
test : (n : ℕ) → Vec ℕ (n + 0) → ℕ
test n v = ?
Here, the type of v is Vec ℕ (n + 0), as you would expect.
test : (n : ℕ) → Vec ℕ (n + 0) → ℕ
test n v with n + 0
... | w = ?
However, once we abstract over n + 0, the type of v suddenly changes to Vec ℕ w. If you later want to use something which contains n + 0 in its type, the substitution won't take place again - it's a one time deal.

In the gameMaster function, we applied with to state g and pattern matched to find out it's going. By the time we use zero-no-going, state g and going are two separate things which have no relation as far as Agda is concerned.

How do we preserve this information? We somehow need to get state g ≡ state g and have the with replace only state g on either side - this would give us the needed state g ≡ going.

What the inspect does is that it hides the function application state g. We have to write a function hide in a way that Agda cannot see hide state g and state g are in fact the same thing.

One possible way to hide something is to use the fact that for any type A, A and ⊤ → A are isomorphic - that is, we can freely go from one representation to the other without losing any information.

However, we cannot use the ⊤ as defined in the standard library. In a moment I'll show why, but for now, we'll define a new type:
data Unit : Set where
  unit : Unit
And what it means for a value to be hidden:
Hidden : Set → Set
Hidden A = Unit → A
We can easily reveal the hidden value by applying unit to it:
reveal : {A : Set} → Hidden A → A
reveal f = f unit
The last step we need to take is the hide function:
hide : {A : Set} {B : A → Set} →
       ((x : A) → B x) → ((x : A) → Hidden (B x))
hide f x unit = f x
Why wouldn't this work with ⊤? If you declare ⊤ as record, Agda can figure out on its own that tt is the only value. So, when faced with hide f x, Agda won't stop at the third argument (because it already knows how it must look like) and automatically reduce it to λ _ → f x. Data types defined with the data keyword don't have these special rules, so hide f x remains that way until someone reveals it and the type checker cannot see that there's a f x subexpression inside hide f x.

The rest is just arranging stuff so we can get the proof later:
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 ]
So, there you have it:
inspect state g : Reveal (hide state g) is (state g)
-- pattern match on (state g)
inspect state g : Reveal (hide state g) is going
When you then reveal hide state g, you'll get state g and finally the proof that state g ≡ going.

                        这篇关于在 agda 中使用计算函数的值进行证明的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！


                    
                        查看全文

在 agda 中使用计算函数的值进行证明 [英] Using the value of a computed function for a proof in agda

问题描述

相关文章

其他开发最新文章

热门教程

热门工具

登录关闭

在 agda 中使用计算函数的值进行证明 [英] Using the value of a computed function for a proof in agda

问题描述

相关文章

其他开发最新文章

热门教程

热门工具

登录 关闭

登录关闭