Agda 定义中带 with 的函数的归纳：with inspect 和 ⊥ 的使用

Posted on Edited on In

Abstract. 写 Agda 大作业的时候遇到的傻逼问题，解决过程中用到了一些深刻的东西。感觉搞清楚之后对 Pattern Matching 的理解提高了一些。

Introduction

在证明 mss ≡ mss-fast 的时候，我们使用到了 tails 函数（求一个序列的所有后缀）。在标准库当中这个函数有一个优美的递归写法：

1
2
3
tails : ∀ {A : Set} → List A → List (List A)
tails [] = [] ∷ []
tails (x ∷ xs) = (x ∷ xs) ∷ (tails xs)

但是在作业中下发的 Specification 中，采用了一种看似简短实际上很垃圾的定义：

1
2
tails' : ∀ {A : Set} → List A → List (List A)
tails' = scanr _++_ [] ∘ map [_]

为了后面的 Horner’s Rule 等可以方便地证明，我们应当先证明如下引理

1
2
3
tails-lemma : ∀ {A : Set} → tails' {A} ≡ tails {A}
tails-lemma = extensionality tails-lemma' where
  tails-lemma' : ∀ {A : Set} → (x : List A) → tails' x ≡ tails x

正常来说这里我们需要 induction with x，但是 tails 中用到了 scanr，scanr 的定义是

1
2
3
4
5
scanr : (A → B → B) → B → List A → List B
scanr f e []       = e ∷ []
scanr f e (x ∷ xs) with scanr f e xs
... | []     = []                -- dead branch
... | y ∷ ys = f x y ∷ y ∷ ys

对于空序列，证明是显然的。

对于非空序列，这里用了一个 with 来做 pattern matching，其中有一个是 dead branch，因此情况比较棘手。

首先我们尝试进行一些 equational reasoning，在 tails' 的定义和结论之间挖一个 hole。

1
2
3
4
5
tails-lemma' (y ∷ ys) = begin
    scanr _++_ [] (map [_] (y ∷ ys))
  ≡⟨ {!   !} ⟩
    tails (y ∷ ys)
  ∎

进行类型检查之后可以发现这个 hole 是要证明

1
2
3
(scanr _++_ [] ([ y ] ∷ map [_] ys)
       | scanr _++_ [] (map [_] ys))
      ≡ (y ∷ ys) ∷ tails ys

中间这个 | 是要求你使用一个 with 进行模式匹配。

With inspect 的使用

我们 with 一个和 scanr 定义中一样的东西，然后挖两个 hole

1
2
3
tails-lemma' (x ∷ xs) with scanr _++_ [] (map [_] xs)
    ... | []       = {!   !}
    ... | (y ∷ ys) = {!   !}

此时的两个 hole 的 goal 分别是

1
2
[] ≡ (x ∷ xs) ∷ tails xs
(x ∷ y) ∷ y ∷ ys ≡ (x ∷ xs) ∷ tails xs

这两个 goal 看起来很奇怪，其中第一个甚至是一个永假命题。第二个只要证明 y ≡ xs，但是给定的信息下我们完全无从下手。

事实上将这两个 goal 和已知信息联系起来的桥梁分别是：

  • 进入第一个 branch 的条件：scanr _++_ [] (map [_] xs) ≡ []。而第一个 branch 是一个 dead branch，也就是说这个情况永远不会出现。
  • 进入第二个 branch 的条件：scanr _++_ [] (map [_] xs) ≡ (y ∷ ys)。

这两个进入分支的条件，可以用两种方法提取：

  1. with … in p

    用如下的代码

    1
    2
    3
    * with f x in p
    ... | f1 = {!   !}
    ... | f2 = {!   !}

    这样一来，在第一个 hole 当中你会得到一个定理 p : f x ≡ f1，在第二个 hole 当中你会得到一个定理 p : f x ≡ f2。

  2. with … inspect …

    用如下的代码

    1
    2
    3
    * with f x | inspect f x
    ... | f1 | [ fx≡f1 ] = {!   !}
    ... | f2 | [ fx≡f2 ] = {!   !}

    这样一来在第一个 hole 中你会得到 fx≡f1 : f x ≡ f1，在第二个 hole 当中你会得到 fx≡f2 : f x ≡ f2

有必要说明一下这里的 [_]，这个东西和 singleton list 不一样，这个是 inspect 实现当中 _·_is_ 运算的 contructor，inspect 实现类似于如下代码[1]：

1
2
3
4
5
6
record MyReveal_·_is_ (f : ℕ → ℕ) (x y : ℕ) : Set where
  constructor [_]
  field eq : f x ≡ y

my-inspect : ∀ f n → MyReveal f · n is (f n)
my-inspect f n = [ refl ]

在第二个参数外面套一个 [_] constructor，直观上理解相当于是 inspect 把定理包在了一个 _·_is_ 里面，用 [_] 可以把他捞出来。

回到原问题，对于第二个 branch 我们进行一些简单的 rewrite 就可以证明，但第一个 dead branch 还没有解决。

⊥ 的使用

⊥ 是 Data.Empty 中的一个类，是一种空的性质。其源代码[2]如下

1
2
3
4
5
6
7
data ⊥ : Set where

------------------------------------------------------------------------
-- Functions

⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()

这个 ⊥-elim 从逻辑上来说，就是 $\vdash \mathrm{F}\rightarrow q$。

有了 ⊥-elim 我们可以做一些举反例的证明，这里就拿一个作业题举例。

定义 init 函数满足 init (x ++ [ a ]) ≡ (x , a)，证明 init 不可能是一个 homomorphism。

可以进行举反例的证明。注意这里 ≢ 的定义是 x ≢ y : (x ≡ y) → ⊥

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
shabi : ∀ {_⊗_} (m : IsSemigroup _⊗_)
  → IsHomomorphism NList-++′-is-semigroup m (init {ℕ}) 
  → [ 1 ] ≡ [ 2 ]
shabi {_⊗_} m H = begin
    init ( [ 1 ]′ ++′ [ 2 ]′ )
  ≡⟨ distrib H [ 1 ]′ [ 2 ]′ ⟩ 
    init ([ 1 ]′) ⊗ init([ 2 ]′)
  ≡⟨ sym (distrib H [ 2 ]′ [ 1 ]′) ⟩ 
    init ( [ 2 ]′ ++′ [ 1 ]′ )
  ∎ 

obviously : [ 1 ] ≢ [ 2 ]
obviously ()

init-is-not-homomorphism : ∀ {_⊗_} (m : IsSemigroup _⊗_)
  → ¬ IsHomomorphism NList-++′-is-semigroup m (init {ℕ})
init-is-not-homomorphism {_⊗_} m H = obviously (shabi m H)

Final Solution

根据上面的理论不难写出以下代码：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
empty-lemma : ∀ {A : Set} → (xs : List A) → tails xs ≡ [] → ⊥
empty-lemma []       ()
empty-lemma (x ∷ xs) ()

first-lemma : ∀ {A : Set} → (xs : List A) (y : List A) (ys : List (List A)) 
  → tails xs ≡ y ∷ ys → y ≡ xs
first-lemma [] y ys refl = refl
first-lemma (x ∷ xs) y ys refl = refl

tails-lemma : ∀ {A : Set} → tails' {A} ≡ tails {A}
tails-lemma = extensionality tails-lemma' where
  tails-lemma' : ∀ {A : Set} → (x : List A) → tails' x ≡ tails x 
  tails-lemma' [] = refl
  tails-lemma' (x ∷ xs) with scanr _++_ [] (map [_] xs) in p 
  ... | []       rewrite tails-lemma' xs = ⊥-elim (empty-lemma xs p)
  ... | (y ∷ ys) rewrite tails-lemma' xs | p | first-lemma xs y ys p = refl
  1. 1.Agda Standard Library, READNE/Inspect.agda ↩
  2. 2.Agda Standard Library, Data/Empty.agda ↩