進口：
open import Data.Nat using (?; zero; suc)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open import Data.List using (List; _∷_; [])
示例 1：
postulate
a : ?
p : a ≡ zero
b : ?
b with a
... | zero = zero
... | _ = suc zero
q : b ≡ zero
q = ?
這是一個最小的作業示例。如果要證明q，應該怎么填坑？
我不知道的部分是如何在 的證明中推理 中q發生的模式匹配b。我不知道有什么語法可以讓我這樣做（我對 Agda 不是很熟悉）。
示例 2（稍微復雜一些）：
postulate
a : List ?
p : a ≡ zero ∷ []
b : List ?
b with a
... | zero ∷ ns = ns
... | _ = []
q : b ≡ []
q = ?
再說一次，如果我要證明q，我應該怎么填坑呢？
示例1和示例2的區別：示例1中我們只關心“with-abstraction中的哪個分支被輸入”，而示例2中我們還關心“ns模式匹配的結果是什么”。我不確定這是否是一個相關的差異。
uj5u.com熱心網友回復：
如果你定義這樣的隱式函式，你將讓你的生活變得一團糟。為什么不做b一個實際的功能a呢？另外，不完整案例的推理也更難。但這是您第一個難題的解決方案：
b : ?
b with a
... | zero = zero
... | suc _ = suc zero -- first change
q : b ≡ zero
q = Eq.trans (Eq.sym (f≡b a Eq.refl)) (r a p)
where
f : ? → ?
f zero = zero
f (suc _) = suc zero
r : (x : ?) → x ≡ zero → f x ≡ zero
r .zero Eq.refl = Eq.refl
f≡b : ? x → x ≡ a → f x ≡ b
f≡b .a Eq.refl with a
... | zero = Eq.refl
... | suc x = Eq.refl
請注意我的回答基本上是如何被迫創建一個f等同于b? with也可能有一些復雜的方法可以用and來做到這一點inspect，但我不太明白。
要在同一檔案中作業，您的問題是：
postulate
a′ : List ?
p′ : a′ ≡ zero ∷ []
c : List ?
c with a′
... | zero ∷ ns = ns
... | suc _ ∷ _ = []
... | [] = []
qq : c ≡ []
qq = {!!}
這根本不值得。相反，比較一下這是多么容易：
cc : List ? → List ?
cc [] = []
cc (zero ∷ ns) = ns
cc ((suc _) ∷ _) = []
qqq : (x : List ?) → x ≡ zero ∷ [] → cc x ≡ []
qqq .(zero ∷ []) Eq.refl = Eq.refl
轉載請註明出處，本文鏈接：https://www.uj5u.com/net/536816.html
下一篇：如何撰寫帶有兩個引數的型別簽名？