a

src/Homework2.agda

@@ -35,25 +35,75 @@ data Σ (A : Set) (B : A → Set) : Set where
 ∃-syntax = ∃
 syntax ∃-syntax (λ x → B) = ∃[ x ] B
 
-data Parity : (n : ℕ) → Set where
+record Terminating (n : ℕ) : Set where
-  isEven : (n : ℕ) → (m : ℕ) → (m * 2 ≡ n) → Parity n
+  inductive
-  isOdd : (n : ℕ) → (m : ℕ) → (1 + m * 2 ≡ n) → Parity n
+  constructor box
+  field
+    call : ∀ {m : ℕ} → m <′ n → Terminating m
+open Terminating
 
-parity? : ∀ (n : ℕ) → Parity n
+term : ∀ (n : ℕ) → Terminating n
-parity? zero = isEven zero zero refl
+term 0 .call ()
+term (suc n) .call ≤′-refl = term n
+term (suc n) .call (≤′-step sm≤n) = term n .call sm≤n
+
+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
+
+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
+
+-- determine the parity of any given ℕ
+parity? : ∀ (n : ℕ) → ∃[ m ] Parity n m
+parity? zero = ⟨ zero , isEven refl ⟩
 parity? (suc n) with parity? n 
-... | isEven _ m p = isOdd (suc n) m (cong (1 +_) p)
+... | ⟨ m , isEven p ⟩ = ⟨ m , isOdd (cong suc p) ⟩
--- p is proof that 1 + m * 2 ≡ n
+... | ⟨ m , isOdd {n} p ⟩ = ⟨ suc m , isEven {n = suc n} {m = suc m} (trans (+-assoc 1 1 (m * 2)) (cong suc p)) ⟩
--- 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
+checkParity0 : parity? 0 ≡ ⟨ 0 , isEven refl ⟩
--- to zero = O
+checkParity0 = refl
--- 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
+checkParity1 : parity? 1 ≡ ⟨ 0 , isOdd refl ⟩
--- toBin = refl
+checkParity1 = 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' 0 _ = O
+to' (suc n) (box caller) with parity? n
+-- this means (n - 1) is even, aka n is odd
+... | ⟨ m , isEven p ⟩ = (to' m (caller (makeProofEven n m p))) I
+-- this means (n - 1) is odd, aka n is even
+... | ⟨ m , isOdd p ⟩ = (to' m (caller (makeProofOdd n m p))) II
+
+to : (n : ℕ) → Bin
+to n = to' n (term n)
+
+toBin0 : to 0 ≡ O
+toBin0 = refl
+
+toBin1 : to 1 ≡ O I
+toBin1 = refl

src/OtherShit.agda

@@ -0,0 +1,10 @@
+module OtherShit where
+
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+open import Data.Nat
+open import Data.Nat.Properties
+
+postulate
+  x : ∀ (a b c : ℕ) → a + b ≡ b + a
+