agda - 如何在 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

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

Answer 1

用户 维特斯 建议使用范式。

如果我们有这两个函数:

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))

IE。只有像 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