Comment prouver que les équations de définition du récurseur de N sont propositionnelles en utilisant le principe d'induction de N dans Agda?

Question

Ceci est un exercice du livre Homotopy Type Theory. Voici ce que j'ai:

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 ? 

Je ne sais pas comment prouver que recℕ z f (succ n) ≡ f n (recℕ z f n). Je dois prouver:

(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)) 

En anglais, étant donné un nombre naturel n et l'hypothèse d'induction prouvent la conséquence.

L'opérateur infixe _∘_ est la composition de fonction normale. Les _≡_ et _×_ types de données sont définies comme suit:

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

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

J'ai pensé à une solution pour un certain temps, mais je ne peux pas comprendre comment résoudre ce problème.

Answer 1

Obtenons l'aide de Agda mode pour 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 = {!!} 

Si on normalise le contexte dans le trou en tapant C-u C-u C-c C-, (chaque fois que je sens que je suis en train d'invoquer la fatalité dans Mortal Kombat) , nous verrons (je nettoyais vos définitions un peu)

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)) 

Les deuxièmes arguments à f sont égaux des deux côtés, de sorte que nous pouvons écrire

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

où

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

Maintenant, l'objectif est

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

qui est un lemme simple

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

Alors

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.