如何在 agda 中证明 (a | b) 形式的一种类型？

Question

在思考：

In Agda is it possible to define a datatype that has equations?

我正在使用以下数据类型：

data Int : Set where
    Z : Int
    S : Int -> Int
    P : Int -> Int

上面对整数的定义很差，上面的答案可以解决这个问题。但是，可以在上述 Int 类型上定义一个可能有用的归约。

normalize : Int -> Int
normalize Z = Z
normalize (S n) with normalize n
... | P m = m
... | m = S m
normalize (P n) with normalize n
... | S m = m
... | m = P m

需要证明的是：

idempotent : (n : Int) -> normalize n \== normalize (normalize n)

当你展开案例时，你会得到例子

idempotent (P n) = ? 

洞的目标有类型

(normalize (P n) | normalize n) \== normalize (normalize (P n) | normalize n)

我还没有看到这个“|”以前，我也不知道如何生成涉及它们的类型的证明。证明需要进行模式匹配，例如，

idempotent (P n) with inspect (normalize n)
... (S m) with-\== = ?
... m with-\== = ?

但是这里第二种情况的孔仍然有一个“|”在里面。所以我有点困惑。

-------- 编辑 ---------------

证明一个更简单的陈述会很有帮助：

normLemma : (n m : NZ) -> normalize n \== P m -> normalize (S n) \== m

“纸上”证明相当简单。假设归一化 n = P m，考虑

normalize (S n) = case normalize n of
  P k -> k
  x -> S x

但归一化 n 假定为 P m，因此归一化 (S n) = k。然后 k = m，因为归一化 n = P m = P k 这意味着 m = k。因此归一化 (S n) = m。

Answer 1

用户Vitus建议使用普通形式。

如果我们有这两个函数：

normalForm : ∀ n -> NormalForm (normalize n)
idempotent' : ∀ {n} -> NormalForm n -> normalize n ≡ n

那么我们可以很容易地组合它们以获得我们需要的结果：

idempotent : ∀ n -> normalize (normalize n) ≡ normalize n
idempotent = idempotent' ∘ normalForm

这里是范式的定义：

data NormalForm : Int -> Set where
  NZ  : NormalForm Z
  NSZ : NormalForm (S Z)
  NPZ : NormalForm (P Z)
  NSS : ∀ {n} -> NormalForm (S n) -> NormalForm (S (S n))
  NPP : ∀ {n} -> NormalForm (P n) -> NormalForm (P (P n))

即只有像 S (S ... (S Z)... 和 P (P ... (P Z)...) 这样的词是正常形式的。

而且证明相当简单：

normalForm : ∀ n -> NormalForm (normalize n)
normalForm  Z    = NZ
normalForm (S n) with normalize n | normalForm n
... | Z    | nf     = NSZ
... | S  _ | nf     = NSS nf
... | P ._ | NPZ    = NZ
... | P ._ | NPP nf = nf
normalForm (P n) with normalize n | normalForm n
... | Z    | nf     = NPZ
... | S ._ | NSZ    = NZ
... | S ._ | NSS nf = nf
... | P  _ | nf     = NPP nf

idempotent' : ∀ {n} -> NormalForm n -> normalize n ≡ n
idempotent'  NZ     = refl
idempotent'  NSZ    = refl
idempotent'  NPZ    = refl
idempotent' (NSS p) rewrite idempotent' p = refl
idempotent' (NPP p) rewrite idempotent' p = refl

完整代码：https://gist.github.com/flickyfrans/f2c7d5413b3657a94950#file-another-one

Answer 2

idempotent : (n : Int) -> normalize (normalize n) ≡ normalize n
idempotent  Z    = refl
idempotent (S n) with normalize n | inspect normalize n
... | Z   |   _   = refl
... | S m | [ p ] = {!!}
... | P m | [ p ] = {!!}

第一个洞的上下文是

Goal: (normalize (S (S m)) | (normalize (S m) | normalize m)) ≡
      S (S m)
————————————————————————————————————————————————————————————
p : normalize n ≡ S m
m : Int
n : Int

(normalize (S (S m)) | (normalize (S m) | normalize m)) ≡ S (S m) 只是normalize (S (S m)) 的扩展版本。所以我们可以稍微重写一下上下文：

Goal: normalize (S (S m)) ≡ S (S m)
————————————————————————————————————————————————————————————
p : normalize n ≡ S m
m : Int
n : Int

由于normalize函数的定义

normalize (S n) with normalize n
... | P m = m
... | m = S m

normalize (S n) ≡ S (normalize n)，如果normalize n 不包含Ps。

如果我们有一个像normalize n ≡ S m 这样的方程，那么m 已经被规范化并且不包含Ps。但是如果m 不包含Ps，那么和normalize m。所以我们有normalize (S m) ≡ S (normalize m)。

让我们证明一个更一般的引理：

normalize-S : ∀ n {m} -> normalize n ≡ S m -> ∀ i -> normalize (m ‵add‵ i) ≡ m ‵add‵ i

‵add‵在哪里

_‵add‵_ : Int -> ℕ -> Int
n ‵add‵  0      = n
n ‵add‵ (suc i) = S (n ‵add‵ i)

normalize-S 声明，如果m 不包含Ps，那么这成立：

normalize (S (S ... (S m)...)) ≡ S (S ... (S (normalize m))...)

这是一个证明：

  normalize-S : ∀ n {m} -> normalize n ≡ S m -> ∀ i -> normalize (m ‵add‵ i) ≡ m ‵add‵ i
  normalize-S  Z    ()    i
  normalize-S (S n) p     i with normalize n | inspect normalize n
  normalize-S (S n) refl  i | Z       |   _   = {!!}
  normalize-S (S n) refl  i | S m     | [ q ] = {!!}
  normalize-S (S n) refl  i | P (S m) | [ q ] = {!!}
  normalize-S (P n) p     i with normalize n | inspect normalize n
  normalize-S (P n) ()    i | Z       |   _     
  normalize-S (P n) refl  i | S (S m) | [ q ] = {!!}
  normalize-S (P n) ()    i | P _     |   _

第一个洞的上下文是

Goal: normalize (Z ‵add‵ i) ≡ Z ‵add‵ i
————————————————————————————————————————————————————————————
i  : ℕ
.w : Reveal .Data.Unit.Core.hide normalize n is Z
n  : Int

即normalize (S (S ... (S Z)...)) ≡ S (S ... (S Z)...)。我们可以很容易地证明它：

normalize-add : ∀ i -> normalize (Z ‵add‵ i) ≡ Z ‵add‵ i
normalize-add  0      = refl
normalize-add (suc i) rewrite normalize-add i with i
... | 0     = refl
... | suc _ = refl

所以我们可以用normalize-add i 填充第一个洞。

第二个洞的上下文是

Goal: normalize (S m ‵add‵ i) ≡ S m ‵add‵ i
————————————————————————————————————————————————————————————
i : ℕ
q : .Data.Unit.Core.reveal (.Data.Unit.Core.hide normalize n) ≡ S m
m : Int
n : Int

虽然normalize-S n q (suc i) 有这种类型：

(normalize (S (m ‵add‵ i)) | normalize (m ‵add‵ i)) ≡ S (m ‵add‵ i)

或者，很快，normalize (S (m ‵add‵ i)) ≡ S (m ‵add‵ i)。所以我们需要将S m ‵add‵ i替换为S (m ‵add‵ i)：

inj-add : ∀ n i -> S n ‵add‵ i ≡ S (n ‵add‵ i)
inj-add n  0      = refl
inj-add n (suc i) = cong S (inj-add n i)

现在我们可以写了

  normalize-S (S n) refl  i | S m | [ q ] rewrite inj-add m i = normalize-S n q (suc i)

第三个洞的上下文是

Goal: normalize (m ‵add‵ i) ≡ m ‵add‵ i
————————————————————————————————————————————————————————————
i : ℕ
q : .Data.Unit.Core.reveal (.Data.Unit.Core.hide normalize n) ≡
    P (S m)
m : Int
n : Int

normalize-P n q 0 给我们normalize (S m) ≡ S m，其中normalize-P 是normalize-S 的对偶并且具有这种类型：

  normalize-P : ∀ n {m} -> normalize n ≡ P m -> ∀ i -> normalize (m ‵sub‵ i) ≡ m ‵sub‵ i

我们可以将normalize-S 应用于具有normalize (S m) ≡ S m 类型的东西：normalize-S (S m) (normalize-P n q 0) i。这个表达式正是我们想要的类型。所以我们可以写

  normalize-S (S n) refl  i | P (S m) | [ q ] = normalize-S (S m) (normalize-P n q 0) i

第四洞与第三洞类似：

  normalize-S (P n) refl  i | S (S m) | [ q ] = normalize-S (S m) (normalize-S n q 0) i

这个漏洞有一个问题：Agda 看不到normalize-S (S m) _ _ 终止，因为S m 在语法上并不小于S n。但是，可以通过使用有根据的递归来说服 Agda。

拥有所有这些东西，我们可以轻松地证明idempotent 定理：

idempotent : (n : Int) -> normalize (normalize n) ≡ normalize n
idempotent  Z    = refl
idempotent (S n) with normalize n | inspect normalize n
... | Z   |   _   = refl
... | S m | [ p ] = normalize-S n p 2
... | P m | [ p ] = normalize-P n p 0
idempotent (P n) with normalize n | inspect normalize n
... | Z   |   _   = refl
... | S m | [ p ] = normalize-S n p 0
... | P m | [ p ] = normalize-P n p 2

这里是代码：https://gist.github.com/flickyfrans/f2c7d5413b3657a94950 有两个版本：带有{-# TERMINATING #-} pragma 和不带。

编辑

idempotent简直就是

idempotent : ∀ n -> normalize (normalize n) ≡ normalize n
idempotent n with normalize n | inspect normalize n
... | Z   |   _   = refl
... | S _ | [ p ] = normalize-S n p 1
... | P _ | [ p ] = normalize-P n p 1