finished hwk2!

src/Homework2.agda

@@ -16,14 +16,8 @@ data Bin : Set where
 
 from : Bin → ℕ
 from O = 0
-from (b I) = 2 * (from b) + 1
+from (b I) = 1 + (from b) * 2
-from (b II) = 2 * (from b) + 2
+from (b II) = 2 + (from b) * 2
-
-fromBin3 : from (O I I) ≡ 3
-fromBin3 = refl
-
-fromBin12 : from (O II I II) ≡ 12
-fromBin12 = refl
 
 -------------------------------------------------------
 -- to
@@ -31,32 +25,53 @@ fromBin12 = refl
 
 inc : Bin → Bin
 inc O = O I
-inc (w I) = w II
+inc (b I) = b II
-inc (w II) = (inc w) I
+inc (b II) = (inc b) I
 
 to : ℕ → Bin
 to 0 = O
-to (suc n) with to n
+to (suc n) = inc (to n)
-... | O = O I
-... | w I = w II
-... | w II = (inc w) I
-
-to2 : to 2 ≡ O II
-to2 = refl
-
-to3 : to 3 ≡ O I I
-to3 = refl
-
-to4 : to 4 ≡ O I II
-to4 = refl
-
-to5 : to 5 ≡ O II I
-to5 = refl
 
 -------------------------------------------------------
 -- from∘to
 -------------------------------------------------------
 
+from-inc : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
+from-inc O = refl
+from-inc (n I) = refl
+from-inc (n II) = cong suc (cong (_* 2) (from-inc n))
+
 from∘to : ∀ n → from (to n) ≡ n
+from∘to zero = refl
+from∘to (suc n) = trans (from-inc (to n)) (cong suc (from∘to n))
+
+-------------------------------------------------------
+-- to∘from
+-------------------------------------------------------
+
+toI : ∀ (n : ℕ) → to (1 + n * 2) ≡ (to n) I
+toI zero = refl
+toI (suc n) = cong inc (cong inc (toI n))
 
 to∘from : ∀ b → to (from b) ≡ b
+to∘from O = refl
+to∘from (n I) =
+  begin
+    to (1 + (from n) * 2)
+  ≡⟨ toI (from n) ⟩
+    (to (from n)) I
+  ≡⟨ cong _I (to∘from n) ⟩
+    n I
+  ∎
+to∘from (n II) =
+  begin
+    to (from (n II))
+  ≡⟨⟩
+    to (2 + (from n) * 2)
+  ≡⟨⟩
+    inc (to (1 + (from n) * 2))
+  ≡⟨ cong inc (toI (from n)) ⟩
+    inc ((to (from n)) I)
+  ≡⟨ cong inc (cong _I (to∘from n)) ⟩
+    n II
+  ∎