2

这是同伦类型理论书中的一个练习。这是我所拥有的：

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

我一直在想一个解决方案，但我不知道如何解决这个问题。

4

1 回答 1

4

让我们从 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)

整个代码。

于 2016-02-13T17:28:30.397 回答