如何在 Agda 中使用 N 的归纳原理证明 N 的递归定义方程命题成立？

Question

这是 Homotopy Type Theory 书中的练习。这是我拥有的：

data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ

iter : {C : Set} → C → (C → C) → ℕ → C
iter z f  zero    = z
iter z f (succ n) = f (iter z f n)

succℕ : {C : Set} → (ℕ → C → C) → ℕ × C → ℕ × C
succℕ f (n , x) = (succ n , f n x)

iterℕ : {C : Set} → C → (ℕ → C → C) → ℕ → ℕ × C
iterℕ z f = iter (zero , z) (succℕ f)

recℕ : {C : Set} → C → (ℕ → C → C) → ℕ → C
recℕ z f = _×_.proj₂ ∘ iterℕ z f

indℕ : {C : ℕ → Set} → C zero → ((n : ℕ) → C n → C (succ n)) → (n : ℕ) → C n
indℕ z f  zero    = z
indℕ z f (succ n) = f n (indℕ z f n)

recℕzfzero≡z : {C : Set} {z : C} {f : ℕ → C → C} → recℕ z f zero ≡ z
recℕzfzero≡z = refl

recℕzfsuccn≡fnrecℕzfn : {C : Set} {z : C} {f : ℕ → C → C} (n : ℕ) →
                        recℕ z f (succ n) ≡ f n (recℕ z f n)
recℕzfsuccn≡fnrecℕzfn = indℕ refl ?

我不知道如何证明recℕ z f (succ n) ≡ f n (recℕ z f n)。我需要证明：

(n : ℕ) → recℕ z f (succ n) ≡ f n (recℕ z f n)
        → recℕ z f (succ (succ n)) ≡ f (succ n) (recℕ z f (succ n))

在英语中，给定一个自然数n，归纳假设证明结果。

中缀运算符_∘_是正常的函数组合。 _≡_ 和 _×_ 数据类型定义为：

data _≡_ {A : Set} : A → A → Set where
    refl : {x : A} → x ≡ x

record _×_ (A B : Set) : Set where
    constructor _,_
    field
        _×_.proj₁ : A
        _×_.proj₂ : B

我想了很久的解决方案，但我想不出如何解决这个问题。

Answer 1

让我们从 Agda-mode for emacs 获得一些帮助：

recℕzfsuccn≡fnrecℕzfn : {C : Set} {z : C} {f : ℕ → C → C} (n : ℕ) →
                        recℕ z f (succ n) ≡ f n (recℕ z f n)
recℕzfsuccn≡fnrecℕzfn {f = f} n = {!!}

如果我们通过输入 C-u C-u C-c C-, 来规范化漏洞中的上下文（每次我觉得我试图在真人快打中调用死亡），我们会看到（我稍微清理了你的定义)

Goal: f
      (proj₁
       (iter (0 , .z) (λ nx → succ (proj₁ nx) , f (proj₁ nx) (proj₂ nx))
        n))
      (proj₂
       (iter (0 , .z) (λ nx → succ (proj₁ nx) , f (proj₁ nx) (proj₂ nx))
        n))
      ≡
      f n
      (proj₂
       (iter (0 , .z) (λ nx → succ (proj₁ nx) , f (proj₁ nx) (proj₂ nx))
        n))

f的第二个参数两边相等，所以我们可以写成

recℕzfsuccn≡fnrecℕzfn {f = f} n = cong (λ m -> f m (recℕ _ f n)) {!!}

哪里

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

现在的目标是

Goal: proj₁ (iter (zero , .z) (succℕ f) n) ≡ n

这是一个简单的引理

lem : {C : Set} {z : C} {f : ℕ → C → C} (n : ℕ)
    → proj₁ (iter (zero , z) (succℕ f) n) ≡ n
lem = indℕ refl (λ _ -> cong succ)

所以

recℕzfsuccn≡fnrecℕzfn : {C : Set} {z : C} {f : ℕ → C → C} (n : ℕ) →
                        recℕ z f (succ n) ≡ f n (recℕ z f n)
recℕzfsuccn≡fnrecℕzfn {f = f} n = cong (λ m -> f m (recℕ _ f n)) (lem n)

The whole code.

如何在 Agda 中使用 N 的归纳原理证明 N 的递归定义方程命题成立？

How to prove that the defining equations of the recursor for N hold propositionally using the induction principle for N in Agda?

functional-programming

agda

dependent-type

type-theory

homotopy-type-theory