Initial

two.agda

@@ -0,0 +1,124 @@
+data _≡_ {A : Set} : A → A → Set where
+  refl : {a : A} → a ≡ a
+
+context : {A B : Set} → {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
+context f refl = refl
+
+trans : {A : Set} → {a b c : A} → a ≡ b → b ≡ c → a ≡ c
+trans refl refl = refl
+
+data ⊥ : Set where
+
+¬ : Set → Set
+¬ A = A → ⊥
+
+_≢_ : {A : Set} → A -> A -> Set
+_≢_  a b = ¬ (a ≡ b)
+
+data _∧_ (A B : Set) : Set where
+  _∧ᵢ_ : A → B → A ∧ B
+
+infixr 19 _∧_ 
+infixr 19 _∧ᵢ_ 
+
+data ℕ : Set where
+  zero : ℕ
+  succ : ℕ → ℕ
+{-# BUILTIN NATURAL ℕ #-}
+
+_+_ : ℕ → ℕ → ℕ
+n + 0 = n
+n + succ m = succ (n + m)
+
+data _<_ : ℕ → ℕ → Set where
+  z<sn : (n : ℕ) → 0 < succ n
+  s<s : (n m : ℕ) → n < m → succ n < succ m
+
+data _≤_ : ℕ → ℕ → Set where
+  z≤n : ∀ (n : ℕ) -> 0 ≤ n
+  s≤s : ∀ (n m : ℕ) -> n ≤ m -> succ n ≤ succ m
+
+-- Task 2
+data ℤ : Set where
+  pos : ℕ → ℤ
+  negsucc : ℕ → ℤ -- -n - 1 alternatively - (n + 1)
+
+recN : {A : Set} → ℕ → A → (ℕ → A → A) → A
+recN 0     d e = d
+recN (succ x) d e = e x (recN x d e)
+
+addℕ : ℕ → ℕ → ℕ
+addℕ n m = recN m n (λ _ x → succ x)
+
+prfadd : (n m : ℕ) → (n + m) ≡ (addℕ n m)
+prfadd n 0 = refl
+prfadd n (succ m) = context succ (prfadd n m)
+
+-- Task 3
+zrec : {A : Set} → ℤ → (ℕ → A) → (ℕ → A) → A
+zrec (pos     n) f _ = f n
+zrec (negsucc n) _ g = g n
+
+addOne : ℤ → ℤ
+addOne a = zrec a (λ x → pos (succ x)) (λ x → recN x (pos x) (λ n _ → negsucc n))
+
+subOne : ℤ → ℤ
+subOne a = zrec a (λ x → recN x (negsucc x) (λ n _ → pos n)) (λ x → negsucc (succ x))
+
+prfℤ₁ : (z : ℤ) → subOne (addOne z) ≡ z
+prfℤ₁ (pos x) = refl
+prfℤ₁ (negsucc 0) = refl
+prfℤ₁ (negsucc (succ x)) = refl
+
+prfℤ₂ : (z : ℤ) → addOne (subOne z) ≡ z
+prfℤ₂ (pos 0) = refl
+prfℤ₂ (pos (succ x)) = refl
+prfℤ₂ (negsucc x) = refl
+
+-- Task 4
+
+data Vec (A : Set) : ℕ → Set where
+  nil : Vec A 0
+  _,_ : {n : ℕ} → Vec A n → (a : A) → Vec A (succ n)
+
+infixl 20 _,_
+
+index : {A : Set} {n : ℕ} → Vec A n → (i : ℕ) → (0 ≤ i ∧ i < n) → A
+index (xs , a) 0 (z≤n n ∧ᵢ z<sn n₁) = a
+index (xs , a) (succ i) (z≤n n ∧ᵢ s<s i m i<m) = index xs i (z≤n i ∧ᵢ i<m)
+  
+data PRF : ℕ → Set where
+  zero : PRF 0
+  succ : PRF 1
+  proj : {n : ℕ}   → (i : ℕ)     → 0 ≤ i ∧ i < n        → PRF n
+  comp : {n m : ℕ} → (f : PRF m) → (gs : Vec (PRF n) m) → PRF n
+  rec  : {n : ℕ}   → (f : PRF n) → (g : PRF (succ (succ n))) → PRF (succ n)
+
+⟦_⟧ : {n : ℕ} → PRF n → (Vec ℕ n) → ℕ
+⟦ zero ⟧        nil         = 0
+⟦ succ ⟧       (nil , n)    = succ n
+⟦ proj i prf ⟧  ρ           = index ρ i prf
+⟦ rec f g ⟧    (ρ , 0)      = ⟦ f ⟧ ρ
+⟦ rec f g ⟧    (ρ , succ n) = ⟦ g ⟧ ((ρ , n , ⟦ rec f g ⟧ (ρ , n)))
+⟦ comp f gs ⟧   ρ           = ⟦ f ⟧ (⟦ gs ⟧* ρ)
+  where
+    ⟦_⟧* : {n m : ℕ} → Vec (PRF m) n → (Vec ℕ m) → Vec ℕ n
+    ⟦ nil ⟧*    ρ = nil
+    ⟦ fs , f ⟧* ρ =  (⟦ fs ⟧* ρ , ⟦ f ⟧ ρ)
+
+
+addProg : PRF 2
+addProg =
+  rec
+    (proj 0 (z≤n 0 ∧ᵢ z<sn 0))
+    (comp succ (nil , proj 0 (z≤n 0 ∧ᵢ z<sn 2)))
+
+add : ℕ → ℕ → ℕ
+add n m = ⟦ addProg ⟧ (nil , n , m)
+
+prfProg : (n m : ℕ) → (add n m) ≡ (n + m)
+prfProg n 0 = refl
+prfProg n (succ m) = context succ (prfProg n m)
+
+prfProg2 : (n m : ℕ) → (add n m) ≡ (addℕ n m)
+prfProg2 n m = trans (prfProg n m) (prfadd n m)