29 lines
757 B
Agda
29 lines
757 B
Agda
module hwk1 where
|
||
|
||
open import Data.Nat
|
||
open import Relation.Binary.PropositionalEquality as Eq
|
||
open Eq.≡-Reasoning
|
||
|
||
natrec : {C : Set} → (a : ℕ) → (d : C) → (e : ℕ → C → C) → C
|
||
natrec zero d e = d
|
||
natrec (suc b) d e = e b (natrec b d e)
|
||
|
||
⊕ : ℕ → ℕ → ℕ
|
||
⊕ x y = natrec x y (λ u v → suc v)
|
||
|
||
problem2-lemma : (x : ℕ) → natrec x 0 (λ u v → suc v) ≡ x
|
||
problem2-lemma zero = refl
|
||
problem2-lemma (suc x) = cong suc (problem2-lemma x)
|
||
|
||
-- (λ u v → suc v) x (natrec x 0 (λ u v → suc v))
|
||
-- suc (natrec x 0 (λ u v → suc v))
|
||
|
||
problem2 : (x : ℕ) → ⊕ x 0 ≡ x
|
||
problem2 x = problem2-lemma x
|
||
-- begin
|
||
-- ⊕ x 0
|
||
-- ≡⟨⟩
|
||
-- natrec x 0 (λ u v → suc v)
|
||
-- ≡⟨ {! !} ⟩
|
||
-- x
|
||
-- ∎ |