piazza-checkpoint

src/Homework2.agda

@@ -19,8 +19,11 @@ from O = 0
 from (b I) = 2 * (from b) + 1
 from (b II) = 2 * (from b) + 2
 
-fromBin : from (O II I II) ≡ 12
+fromBin3 : from (O I I) ≡ 3
-fromBin = refl
+fromBin3 = refl
+
+fromBin12 : from (O II I II) ≡ 12
+fromBin12 = refl
 
 -------------------------------------------------------
 -- to
@@ -68,6 +71,9 @@ 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
 
@@ -88,16 +94,16 @@ postulate
 open import Debug.Trace
 
 postulate
-  makeProofEven : ∀ (n m : ℕ) → m * 2 ≡ n → suc m ≤′ suc n
+  makeProofEven : ∀ (n m : ℕ) → m * 2 ≡ n → suc m ≤′ n
-  makeProofOdd : ∀ (n m : ℕ) → suc (m * 2) ≡ n → suc m ≤′ suc n
+  makeProofOdd : ∀ (n m : ℕ) → suc (m * 2) ≡ n → suc m ≤′ n
 
 to' : (n : ℕ) → Terminating n → Bin
-to' 0 _ = O
+to' zero _ = O
-to' (suc n) (box caller) with parity? n
+to' n (box mWit) with parity? n
--- this means (n - 1) is even, aka n is odd
+-- this means n is odd
-... | ⟨ m , isEven p ⟩ = (to' m (caller (makeProofEven n m p))) I
+... | ⟨ m , isOdd p ⟩ = (to' m (mWit (makeProofOdd n m p))) I
--- this means (n - 1) is odd, aka n is even
+-- this means n is even
-... | ⟨ m , isOdd p ⟩ = (to' m (caller (makeProofOdd n m p))) II
+... | ⟨ m , isEven p ⟩ = (to' m (mWit (makeProofEven n m p))) II
 
 to : (n : ℕ) → Bin
 to n = to' n (term n)
@@ -105,5 +111,5 @@ to n = to' n (term n)
 toBin0 : to 0 ≡ O
 toBin0 = refl
 
-toBin1 : to 1 ≡ O I
+toBin1 : to 3 ≡ O I I
 toBin1 = refl

src/OtherShit.agda

@@ -4,7 +4,27 @@ open import Relation.Binary.PropositionalEquality
 open ≡-Reasoning
 open import Data.Nat
 open import Data.Nat.Properties
+open import Data.Unit
+open import Data.Empty
 
-postulate
+data Bin : Set where
-  x : ∀ (a b c : ℕ) → a + b ≡ b + a
+  O : Bin
+  _I : Bin → Bin
+  _II : Bin → Bin
 
+data Bool : Set where
+  true : Bool
+  false : Bool
+
+T : Bool → Set
+T true = ⊤
+T false = ⊥
+
+T→≡ : ∀ (b : Bool) → T b → b ≡ true
+T→≡ true tt = refl
+T→≡ false ()
+
+data parity : ℕ → Set → Set where
+  zero : parity zero
+  oddSuc : ∀ {n : ℕ} → parity n → parity (evenSuc n)
+  evenSuc  : ∀ {n : ℕ} → parity n → parity (oddSuc n)