Как преобразовать результат?
У меня есть эта программа 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).
Ответы 2
Тип равенства _≡_ не имеет особого значения в Агде. Для 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, так как он не нужен.)
(В стандартной библиотеке transport называется subst, а comm называется sym. Оба определены в Relation.Binary.PropositionalEquality.)
Если вы сопоставите шаблон на p, он уточнит m в .(suc n):
lemma : ∀ (m n : ℕ) → m ≡ suc n → ℕ⁺ m
lemma .(suc n) zero refl = one
lemma .(suc n) (suc n) refl = suc⁺
(отказ от ответственности: это не с точки зрения HoTT/CTT; вероятно, это не сработает без аксиома К.)
Спасибо! Я догадался об этой подписи, но не знал, что ее определение настолько простое.