pattern-matching - 在 Agda 中，如何证明 with-abstracts 中匹配模式的属性？

Question

进口:

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 的值是多少”模式匹配的结果”。但我不确定这是否是一个相关的差异。

Answer 1

如果你定义这样的隐式函数，你的生活将会变得一团糟。为什么不让 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

请注意，我的答案本质上是如何被迫创建一个与 b 等效的函数 f 的？可能还有一些复杂的方法可以使用 with 和 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