时间戳

首页 > 解决方案 > 如何转换结果？

pattern-matching - 如何转换结果？

问题描述

我有这个 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}

问题出在倒数第二行：它抱怨oneis not ℕ⁺ m，但是我必须p在那里证明它们确实是。

我怎样才能做到这一点？如果我想证明的实际上是一个相等，我知道该怎么做（好吧，p在这种情况下只是通过），但我不知道如何使用p将泛型转换ℕ⁺ m为ℕ⁺ (suc zero).

标签： pattern-matchingequalityagda

解决方案

等式类型_≡_在 Agda 中没有特殊含义。到 Agdaone看起来像一个值类型ℕ⁺ (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，因为它不需要。）

推荐阅读