test

src/Extra2.agda

@@ -0,0 +1,34 @@
+module _ where
+
+open import Relation.Binary.PropositionalEquality
+
+record ⊤ : Set where
+  constructor tt
+
+postulate
+  tt′ : ⊤
+
+lemma₀ : tt ≡ tt′
+lemma₀ = refl
+
+open import Data.Nat
+open import Data.Nat.Properties
+
+record Terminating (n : ℕ) : Set where
+  inductive
+  constructor box
+  field
+    call : ∀ {m : ℕ} → m <′ n → Terminating m
+open Terminating
+
+term : ∀ (n : ℕ) → Terminating n
+term 0 .call ()
+term (suc n) .call ≤′-refl = term n
+term (suc n) .call (≤′-step sm≤n) = term n .call sm≤n
+
+postulate
+  _/2 : ℕ → ℕ
+  /2-<′ : ∀ (n : ℕ) → n /2 <′ n
+
+merge : (n : ℕ) → Terminating n → ℕ
+merge n (box caller) = merge (n /2) (caller (/2-<′ n))

src/Extra3.agda

@@ -0,0 +1,87 @@
+module _ where
+
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+open import Function
+open import Data.Nat
+open import Data.Fin hiding (_+_)
+open import Data.Product hiding (map)
+
+-- Functions as Lists
+
+Vec : Set → ℕ → Set
+Vec A n = Fin n → A
+
+map-Vec : {A B : Set} {n : ℕ} → (A → B) → Vec A n → Vec B n
+map-Vec f v = f ∘′ v
+
+map-Vec-compose : {A B C : Set} {n : ℕ} (f : B → C) (g : A → B) (v : Vec A n)
+  → map-Vec (f ∘ g) v ≡ map-Vec f (map-Vec g v)
+map-Vec-compose f g v = refl
+
+List : Set → Set
+List A = Σ ℕ (λ n → Vec A n)
+
+map : {A B : Set} → (A → B) → List A → List B
+map f (n , v) = n , (f ∘′ v)
+
+map-compose : {A B C : Set} (f : B → C) (g : A → B) (l : List A)
+  → map (f ∘ g) l ≡ map f (map g l)
+map-compose f g l = refl
+
+[] : {A : Set} → List A
+[] = 0 , λ ()
+
+_∷_ : {A : Set} → A → List A → List A
+a ∷ (n , v) = (suc n) , λ{ zero → a ; (suc n) → v n }
+
+--- Questions
+
+-- Q1: Instance arguments...
+-- A1: Don't abuse it
+
+-- Q2: Convervativity of the eta rule of sigma types
+-- A2: this is a very interesting question!!!
+--
+-- ETT is conservative with respect to (ITT + K) + function ext, by Martin Hofmann
+
+-- Q3: Differences between judgmental eq, propositional eq, and isomorphisms
+
+-- A3: Judgmental equality is given
+
+_ = 1 + 1 ≡ 2
+_ = refl
+
+-- Propositional equality is a type that can be either
+
+-- 1. the inductive types generated by reflexivity, or
+-- 2. ...
+-- 3. ...
+
+-- Isomorphisms only make sense between two types.
+
+-- Q4: syntax
+
+postulate
+  F : (Set → Set) → (Set → Set)
+
+syntax F (λ x → e) (λ y → f) = e - x - y - f
+
+-- Q5. subtying in kinds
+
+-- Speed coding
+
++-comm : ∀ n m → n + m ≡ m + n
++-comm 0 m = ?
++-comm (suc n) m =
+  begin
+    suc n + m
+  ≡⟨ ? ⟩
+    suc n + m
+  ≡⟨ ? ⟩
+    suc n + m
+  ≡⟨ ? ⟩
+    suc n + m
+  ≡⟨ ? ⟩
+    m + suc n
+  ∎

src/Homework2.agda

@@ -9,3 +9,51 @@ data Bin : Set where
   O : Bin
   _I : Bin → Bin
   _II : Bin → Bin
+
+-------------------------------------------------------
+-- from
+-------------------------------------------------------
+
+from : Bin → ℕ
+from O = 0
+from (b I) = 2 * (from b) + 1
+from (b II) = 2 * (from b) + 2
+
+fromBin : from (O II I II) ≡ 12
+fromBin = refl
+
+-------------------------------------------------------
+-- to
+-------------------------------------------------------
+
+data Σ (A : Set) (B : A → Set) : Set where
+  ⟨_,_⟩ : (x : A) → B x → Σ A B
+
+∃ : ∀ {A : Set} (B : A → Set) → Set
+∃ {A} B = Σ A B
+
+∃-syntax = ∃
+syntax ∃-syntax (λ x → B) = ∃[ x ] B
+
+data Parity : (n : ℕ) → Set where
+  isEven : (n : ℕ) → (m : ℕ) → (m * 2 ≡ n) → Parity n
+  isOdd : (n : ℕ) → (m : ℕ) → (1 + m * 2 ≡ n) → Parity n
+
+parity? : ∀ (n : ℕ) → Parity n
+parity? zero = isEven zero zero refl
+parity? (suc n) with parity? n 
+... | isEven _ m p = isOdd (suc n) m (cong (1 +_) p)
+-- p is proof that 1 + m * 2 ≡ n
+-- thus 1 + (1 + m * 2) ≡ 1 + n
+-- turn it into 2 + m * 2 using +-assoc
+... | isOdd _ m p = isEven (suc n) (suc m) (trans (+-assoc 1 1 (m * 2)) (cong suc p))
+
+-- to : (n : ℕ) → Terminating n → Bin
+-- to zero = O
+-- to (suc n) with parity? n
+-- ... | isEven _ m _ = (to m) I
+-- ... | isOdd _ zero _ = O I
+-- ... | isOdd _ (suc m) _ = (to m) II
+
+-- toBin : to 3 ≡ O I I
+-- toBin = refl