如何转换结果？

Question

我有这个 Agda 程序：

data ℕ⁺ : ℕ → Set where
  one : ℕ⁺ (suc zero)
  suc⁺ : {n : ℕ} → ℕ⁺ (suc n)

lemma : ∀ (m n : ℕ) → m ≡ suc n → ℕ⁺ m
lemma m zero p = one
lemma m (suc n) p  = suc⁺ {suc n}

问题出在倒数第二行：它抱怨 one 不是 ℕ⁺ m，但我有 p 来证明它们确实是。

我该怎么做？我知道如果我想证明的实际上是相等的（好吧，在这种情况下只需传递 p ），但我不知道如何使用 p 转换通用 ℕ⁺ m 到 ℕ⁺ (suc zero).

Answer 1

相等类型_≡_在Agda中没有特殊意义。对于 Agda one 看起来像 ℕ⁺ (suc zero) 类型的值，它需要 ℕ⁺ m。 transport 应该有帮助。

transport : forall {A : Set} {B : A → Set} {x y : A} → x ≡ y → B x → B y
transport refl bx = bx

comm : forall {A : Set} {x y : A} → x ≡ y → y ≡ x
comm {x = x} p = transport {B = _≡ x} p refl

lemma : ∀ (m n : ℕ) → m ≡ suc n → ℕ⁺ m
lemma _ _ p  = transport {B = \k → ℕ⁺ k} (comm p) suc⁺

（这里我删除了one，因为它不需要。）

Answer 2

如果您在 p 上进行模式匹配，它会将 m 细化为 .(suc n):

lemma : ∀ (m n : ℕ) → m ≡ suc n → ℕ⁺ m
lemma .(suc n) zero    refl = one
lemma .(suc n) (suc n) refl = suc⁺

（免责声明：这是从 non-HoTT/CTT 的角度出发；如果没有，这可能行不通。）

如何转换结果？

How do I convert the result?

equality

pattern-matching

agda