pt 1 done

src/Homework2.agda

@@ -29,87 +29,34 @@ fromBin12 = refl
 -- to
 -------------------------------------------------------
 
-data Σ (A : Set) (B : A → Set) : Set where
-  ⟨_,_⟩ : (x : A) → B x → Σ A B
+inc : Bin → Bin
+inc O = O I
+inc (w I) = w II
+inc (w II) = (inc w) I
 
-∃ : ∀ {A : Set} (B : A → Set) → Set
-∃ {A} B = Σ A B
+to : ℕ → Bin
+to 0 = O
+to (suc n) with to n
+... | O = O I
+... | w I = w II
+... | w II = (inc w) I
 
-∃-syntax = ∃
-syntax ∃-syntax (λ x → B) = ∃[ x ] B
+to2 : to 2 ≡ O II
+to2 = refl
 
-record Terminating (n : ℕ) : Set where
-  inductive
-  constructor box
-  field
-    call : ∀ {m : ℕ} → m <′ n → Terminating m
-open Terminating
+to3 : to 3 ≡ O I I
+to3 = refl
 
-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
+to4 : to 4 ≡ O I II
+to4 = refl
 
-data Parity : (n m : ℕ) → Set where
-  isEven : ∀ {n m : ℕ} → (m * 2 ≡ n) → Parity n m
-  isOdd : ∀ {n m : ℕ} → (1 + m * 2 ≡ n) → Parity n m
+to5 : to 5 ≡ O II I
+to5 = refl
 
-data LooseParity : (n m : ℕ) → Set where
-  looseEven : ∀ {n m : ℕ} → (m * 2 ≤′ n) → LooseParity n m
-  looseOdd : ∀ {n m : ℕ} → (1 + m * 2 ≤′ n) → LooseParity n m
+-------------------------------------------------------
+-- from∘to
+-------------------------------------------------------
 
--- determine the parity of any given ℕ
-parity? : ∀ (n : ℕ) → ∃[ m ] Parity n m
-parity? zero = ⟨ zero , isEven refl ⟩
-parity? (suc n) with parity? n 
-... | ⟨ m , isEven p ⟩ = ⟨ m , isOdd (cong suc p) ⟩
-... | ⟨ m , isOdd {n} p ⟩ = ⟨ suc m , isEven {n = suc n} {m = suc m} (trans (+-assoc 1 1 (m * 2)) (cong suc p)) ⟩
+from∘to : ∀ n → from (to n) ≡ n
 
-checkParity0 : parity? 0 ≡ ⟨ 0 , isEven refl ⟩
-checkParity0 = refl
-
-checkParity1 : parity? 1 ≡ ⟨ 0 , isOdd refl ⟩
-checkParity1 = refl
-
-checkParity3 : parity? 3 ≡ ⟨ 1 , isOdd refl ⟩
-checkParity3 = refl
-
-checkParity15 : parity? 15 ≡ ⟨ 7 , isOdd refl ⟩
-checkParity15 = refl
-
-checkParity128 : parity? 128 ≡ ⟨ 64 , isEven refl ⟩
-checkParity128 = refl
-
--- need to show that Parity implies LooseParity
-loosen : ∀ {n m : ℕ} → Parity n m → LooseParity n m
-loosen (isEven refl) = looseEven ≤′-refl
-loosen (isOdd refl) = looseOdd ≤′-refl
-
--- show that LooseParity implies Terminating
-postulate
-  looseTerm : ∀ {n m : ℕ} → LooseParity n m → Terminating m
--- looseTerm {n} {m = zero} (looseEven ≤′-refl) .call ()
--- looseTerm {n} {m = suc m₁} (looseEven ≤′-refl) .call p = {! looseTerm {n = n} {m = m₁} (looseEven ≤′-refl)  !}
-
-open import Debug.Trace
-
-postulate
-  makeProofEven : ∀ (n m : ℕ) → m * 2 ≡ n → suc m ≤′ suc n
-  makeProofOdd : ∀ (n m : ℕ) → suc (m * 2) ≡ n → suc m ≤′ suc n
-
-to' : (n : ℕ) → Terminating n → Bin
-to' zero _ = O
-to' (suc n) (box mWit) with parity? n
--- this means n is odd
-... | ⟨ m , isOdd p ⟩ = (to' m (mWit (makeProofOdd n m p))) II
--- this means n is even
-... | ⟨ m , isEven p ⟩ = (to' m (mWit (makeProofEven n m p))) I
-
-to : (n : ℕ) → Bin
-to n = to' n (term n)
-
-toBin0 : to 0 ≡ O
-toBin0 = refl
-
-toBin1 : to 3 ≡ O I I
-toBin1 = refl
+to∘from : ∀ b → to (from b) ≡ b