Add Everything (#34)

Numbers/BinaryNaturals/Addition.agda

@@ -0,0 +1,198 @@
+{-# OPTIONS --warning=error --safe --without-K #-}
+
+open import LogicalFormulae
+open import Functions
+open import Lists.Lists
+open import Numbers.Naturals
+open import Groups.GroupDefinition
+open import Numbers.BinaryNaturals.Definition
+
+module Numbers.BinaryNaturals.Addition where
+
+-- Define the monoid structure, and show that it's the same as ℕ's
+
+_+Binherit_ : BinNat → BinNat → BinNat
+a +Binherit b = NToBinNat (binNatToN a +N binNatToN b)
+
+_+B_ : BinNat → BinNat → BinNat
+[] +B b = b
+(x :: a) +B [] = x :: a
+(zero :: xs) +B (y :: ys) = y :: (xs +B ys)
+(one :: xs) +B (zero :: ys) = one :: (xs +B ys)
+(one :: xs) +B (one :: ys) = zero :: incr (xs +B ys)
+
++BCommutative : (a b : BinNat) → a +B b ≡ b +B a
++BCommutative [] [] = refl
++BCommutative [] (x :: b) = refl
++BCommutative (x :: a) [] = refl
++BCommutative (zero :: as) (zero :: bs) rewrite +BCommutative as bs = refl
++BCommutative (zero :: as) (one :: bs) rewrite +BCommutative as bs = refl
++BCommutative (one :: as) (zero :: bs) rewrite +BCommutative as bs = refl
++BCommutative (one :: as) (one :: bs) rewrite +BCommutative as bs = refl
+
++BIsInherited[] : (b : BinNat) (prB : b ≡ canonical b) → [] +Binherit b ≡ [] +B b
++BIsInherited[] [] prB = refl
++BIsInherited[] (zero :: b) prB = t
+  where
+    refine : (b : BinNat) → zero :: b ≡ canonical (zero :: b) → b ≡ canonical b
+    refine b pr with canonical b
+    refine b pr | x :: bl = ::Inj pr
+    t : NToBinNat (0 +N binNatToN (zero :: b)) ≡ zero :: b
+    t with orderIsTotal 0 (binNatToN b)
+    t | inl (inl pos) = transitivity (doubleIsBitShift (binNatToN b) pos) (applyEquality (zero ::_) (transitivity (binToBin b) (equalityCommutative (refine b prB))))
+    t | inl (inr ())
+    ... | inr eq with binNatToNZero b (equalityCommutative eq)
+    ... | u with canonical b
+    t | inr eq | u | [] = exFalso (bad b prB)
+      where
+        bad : (c : BinNat) → zero :: c ≡ [] → False
+        bad c ()
+    t | inr eq | () | x :: bl
++BIsInherited[] (one :: b) prB = ans
+  where
+    ans : NToBinNat (binNatToN (one :: b)) ≡ one :: b
+    ans = transitivity (binToBin (one :: b)) (equalityCommutative prB)
+
+-- Show that the monoid structure of ℕ is the same as that of BinNat
+
++BIsInherited : (a b : BinNat) (prA : a ≡ canonical a) (prB : b ≡ canonical b) → a +Binherit b ≡ a +B b
++BinheritLemma : (a : BinNat) (b : BinNat) (prA : a ≡ canonical a) (prB : b ≡ canonical b) → incr (NToBinNat ((binNatToN a +N binNatToN b) +N ((binNatToN a +N binNatToN b) +N zero))) ≡ one :: (a +B b)
+
++BIsInherited' : (a b : BinNat) → a +Binherit b ≡ canonical (a +B b)
+
++BinheritLemma a b prA prB with orderIsTotal 0 (binNatToN a +N binNatToN b)
++BinheritLemma a b prA prB | inl (inl x) rewrite doubleIsBitShift (binNatToN a +N binNatToN b) x = applyEquality (one ::_) (+BIsInherited a b prA prB)
++BinheritLemma a b prA prB | inr x with sumZeroImpliesOperandsZero (binNatToN a) (equalityCommutative x)
++BinheritLemma a b prA prB | inr x | fst ,, snd = ans2
+  where
+    bad : b ≡ []
+    bad = transitivity prB (binNatToNZero b snd)
+    bad2 : a ≡ []
+    bad2 = transitivity prA (binNatToNZero a fst)
+    ans2 : incr (NToBinNat ((binNatToN a +N binNatToN b) +N ((binNatToN a +N binNatToN b) +N zero))) ≡ one :: (a +B b)
+    ans2 rewrite bad | bad2 = refl
+
++BIsInherited [] b _ prB = +BIsInherited[] b prB
++BIsInherited (x :: a) [] prA _ = transitivity (applyEquality NToBinNat (additionNIsCommutative (binNatToN (x :: a)) 0)) (transitivity (binToBin (x :: a)) (equalityCommutative prA))
++BIsInherited (zero :: as) (zero :: b) prA prB with orderIsTotal 0 (binNatToN as +N binNatToN b)
+... | inl (inl 0<) rewrite additionNIsCommutative (binNatToN as) 0 | additionNIsCommutative (binNatToN b) 0 | equalityCommutative (additionNIsAssociative (binNatToN as +N binNatToN as) (binNatToN b) (binNatToN b)) | additionNIsAssociative (binNatToN as) (binNatToN as) (binNatToN b) | additionNIsCommutative (binNatToN as) (binNatToN b) | equalityCommutative (additionNIsAssociative (binNatToN as) (binNatToN b) (binNatToN as)) | additionNIsAssociative (binNatToN as +N binNatToN b) (binNatToN as) (binNatToN b) | additionNIsCommutative 0 ((binNatToN as +N binNatToN b) +N (binNatToN as +N binNatToN b)) | additionNIsAssociative (binNatToN as +N binNatToN b) (binNatToN as +N binNatToN b) 0 = transitivity (doubleIsBitShift (binNatToN as +N binNatToN b) (identityOfIndiscernablesRight _ _ _ _<N_ 0< (additionNIsCommutative (binNatToN b) _))) (applyEquality (zero ::_) (+BIsInherited as b (canonicalDescends as prA) (canonicalDescends b prB)))
++BIsInherited (zero :: as) (zero :: b) prA prB | inl (inr ())
+... | inr p with sumZeroImpliesOperandsZero (binNatToN as) (equalityCommutative p)
++BIsInherited (zero :: as) (zero :: b) prA prB | inr p | as=0 ,, b=0 rewrite as=0 | b=0 = exFalso ans
+  where
+    bad : (b : BinNat) → (pr : b ≡ canonical b) → (pr2 : binNatToN b ≡ 0) → b ≡ []
+    bad b pr pr2 = transitivity pr (binNatToNZero b pr2)
+    t : b ≡ canonical b
+    t with canonical b
+    t | x :: bl = ::Inj prB
+    u : b ≡ []
+    u = bad b t b=0
+    nono : {A : Set} → {a : A} → {as : List A} → a :: as ≡ [] → False
+    nono ()
+    ans : False
+    ans with inspect (canonical b)
+    ans | [] with≡ x rewrite x = nono prB
+    ans | (x₁ :: y) with≡ x = nono (transitivity (equalityCommutative x) (transitivity (equalityCommutative t) u))
++BIsInherited (zero :: as) (one :: b) prA prB rewrite additionNIsCommutative (binNatToN as +N (binNatToN as +N zero)) (succ (binNatToN b +N (binNatToN b +N zero))) | additionNIsCommutative (binNatToN b +N (binNatToN b +N zero)) (binNatToN as +N (binNatToN as +N zero)) | equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN b)) = +BinheritLemma as b (canonicalDescends as prA) (canonicalDescends b prB)
++BIsInherited (one :: as) (zero :: bs) prA prB rewrite equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = +BinheritLemma as bs (canonicalDescends as prA) (canonicalDescends bs prB)
++BIsInherited (one :: as) (one :: bs) prA prB rewrite additionNIsCommutative (binNatToN as +N (binNatToN as +N zero)) (succ (binNatToN bs +N (binNatToN bs +N zero))) | additionNIsCommutative (binNatToN bs +N (binNatToN bs +N zero)) (2 *N binNatToN as) | equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) | +BinheritLemma as bs (canonicalDescends as prA) (canonicalDescends bs prB) = refl
+
++BIsInherited'[] : (b : BinNat) → [] +Binherit b ≡ canonical ([] +B b)
++BIsInherited'[] [] = refl
++BIsInherited'[] (zero :: b) with inspect (canonical b)
++BIsInherited'[] (zero :: b) | [] with≡ pr rewrite binNatToNZero' b pr | pr = refl
++BIsInherited'[] (zero :: b) | (x :: bl) with≡ pr rewrite pr = ans
+  where
+    contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
+    contr {l1 = []} p1 ()
+    contr {l1 = x :: l1} () p2
+    ans : NToBinNat (binNatToN b +N (binNatToN b +N zero)) ≡ zero :: x :: bl
+    ans with inspect (binNatToN b)
+    ans | zero with≡ th rewrite th = exFalso (contr (binNatToNZero b th) pr)
+    ans | succ th with≡ blah rewrite blah | doubleIsBitShift' th = applyEquality (zero ::_) (transitivity (equalityCommutative u) pr)
+      where
+        u : canonical b ≡ incr (NToBinNat th)
+        u = transitivity (equalityCommutative (binToBin b)) (applyEquality NToBinNat blah)
++BIsInherited'[] (one :: b) with inspect (binNatToN b)
+... | zero with≡ pr rewrite pr = applyEquality (one ::_) (equalityCommutative (binNatToNZero b pr))
+... | (succ bl) with≡ pr = ans
+  where
+    u : NToBinNat (2 *N binNatToN b) ≡ zero :: canonical b
+    u with doubleIsBitShift' bl
+    ... | t = transitivity (identityOfIndiscernablesLeft _ _ _ _≡_ t (applyEquality (λ i → NToBinNat (2 *N i)) (equalityCommutative pr))) (applyEquality (zero ::_) (transitivity (applyEquality NToBinNat (equalityCommutative pr)) (binToBin b)))
+    ans : incr (NToBinNat (binNatToN b +N (binNatToN b +N zero))) ≡ one :: canonical b
+    ans = applyEquality incr u
+
++BIsInherited' [] b = +BIsInherited'[] b
++BIsInherited' (zero :: a) [] with inspect (binNatToN a)
++BIsInherited' (zero :: a) [] | zero with≡ x rewrite x | binNatToNZero a x = refl
++BIsInherited' (zero :: a) [] | succ y with≡ x rewrite x | additionNIsCommutative (y +N succ (y +N 0)) 0 = transitivity (doubleIsBitShift' y) (transitivity (applyEquality (λ i → (zero :: NToBinNat i)) (equalityCommutative x)) (transitivity (applyEquality (λ i → zero :: i) (binToBin a)) (canonicalAscends' {zero} a bad)))
+  where
+    bad : canonical a ≡ [] → False
+    bad pr with transitivity (equalityCommutative x) (transitivity (equalityCommutative (binNatToNIsCanonical a)) (applyEquality binNatToN pr))
+    bad pr | ()
++BIsInherited' (one :: a) [] with inspect (binNatToN a)
++BIsInherited' (one :: a) [] | 0 with≡ x rewrite x | binNatToNZero a x = refl
++BIsInherited' (one :: a) [] | succ n with≡ x rewrite x | doubleIsBitShift' n = applyEquality incr {_} {zero :: canonical a} (transitivity {x = _} {NToBinNat (2 *N succ n)} bl (transitivity (doubleIsBitShift' n) (applyEquality (zero ::_) (transitivity (applyEquality NToBinNat (equalityCommutative x)) (binToBin a)))))
+  where
+    bl : incr (NToBinNat ((n +N succ (n +N 0)) +N 0)) ≡ NToBinNat (succ (n +N succ (n +N 0)))
+    bl rewrite equalityCommutative x | additionNIsCommutative (n +N succ (n +N 0)) 0 = refl
++BIsInherited' (zero :: as) (zero :: bs) rewrite equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = ans
+  where
+    ans : NToBinNat (2 *N (binNatToN as +N binNatToN bs)) ≡ canonical (zero :: (as +B bs))
+    ans with inspect (binNatToN as +N binNatToN bs)
+    ans | zero with≡ x with sumZeroImpliesOperandsZero (binNatToN as) x
+    ... | as=0 ,, bs=0 rewrite as=0 | bs=0 = foo
+      where
+        u : canonical (as +Binherit bs) ≡ []
+        u rewrite as=0 | bs=0 = refl
+        foo : [] ≡ canonical (zero :: (as +B bs))
+        foo = transitivity (transitivity b (applyEquality (λ i → canonical (zero :: i)) (+BIsInherited' as bs))) (canonicalAscends'' {zero} (as +B bs))
+          where
+            b : [] ≡ canonical (zero :: (as +Binherit bs))
+            b rewrite u = refl
+    ans | succ y with≡ x rewrite x | doubleIsBitShift' y = transitivity (applyEquality (λ i → zero :: NToBinNat i) (equalityCommutative x)) ans2
+      where
+        u : 0 <N binNatToN (as +B bs)
+        u rewrite equalityCommutative (binNatToNIsCanonical (as +B bs)) | equalityCommutative (+BIsInherited' as bs) | x | nToN (succ y) = succIsPositive y
+        ans2 : zero :: NToBinNat (binNatToN as +N binNatToN bs) ≡ canonical (zero :: (as +B bs))
+        ans2 rewrite +BIsInherited' as bs = canonicalAscends (as +B bs) u
++BIsInherited' (zero :: as) (one :: bs) rewrite additionNIsCommutative (2 *N binNatToN as) (succ (2 *N binNatToN bs)) | additionNIsCommutative (2 *N binNatToN bs) (2 *N binNatToN as) | equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = ans2
+  where
+    ans2 : incr (NToBinNat (2 *N (binNatToN as +N binNatToN bs))) ≡ one :: canonical (as +B bs)
+    ans2 with inspect (binNatToN as +N binNatToN bs)
+    ans2 | zero with≡ x with sumZeroImpliesOperandsZero (binNatToN as) x
+    ans2 | zero with≡ x | as=0 ,, bs=0 rewrite as=0 | bs=0 = applyEquality (one ::_) (transitivity t (+BIsInherited' as bs))
+      where
+        t : [] ≡ as +Binherit bs
+        t rewrite as=0 | bs=0 = refl
+    ans2 | succ y with≡ x rewrite x | doubleIsBitShift' y = applyEquality (one ::_) (transitivity (applyEquality NToBinNat (equalityCommutative x)) (+BIsInherited' as bs))
++BIsInherited' (one :: as) (zero :: bs) rewrite equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = ans
+  where
+    ans : incr (NToBinNat (2 *N (binNatToN as +N binNatToN bs))) ≡ one :: canonical (as +B bs)
+    ans with inspect (binNatToN as +N binNatToN bs)
+    ans | zero with≡ x with sumZeroImpliesOperandsZero (binNatToN as) x
+    ... | as=0 ,, bs=0 rewrite as=0 | bs=0 = applyEquality (one ::_) (transitivity t (+BIsInherited' as bs))
+      where
+        t : [] ≡ NToBinNat (binNatToN as +N binNatToN bs)
+        t rewrite as=0 | bs=0 = refl
+    ans | succ y with≡ x rewrite x | doubleIsBitShift' y = applyEquality (one ::_) (transitivity (applyEquality NToBinNat (equalityCommutative x)) (+BIsInherited' as bs))
++BIsInherited' (one :: as) (one :: bs) rewrite additionNIsCommutative (2 *N binNatToN as) (succ (2 *N binNatToN bs)) | additionNIsCommutative (2 *N binNatToN bs) (2 *N binNatToN as) | equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = ans
+  where
+    ans : incr (incr (NToBinNat (2 *N (binNatToN as +N binNatToN bs)))) ≡ canonical (zero :: incr (as +B bs))
+    ans with inspect (binNatToN as +N binNatToN bs)
+    ... | zero with≡ x with sumZeroImpliesOperandsZero (binNatToN as) x
+    ans | zero with≡ x | as=0 ,, bs=0 rewrite as=0 | bs=0 = bar
+      where
+        u' : canonical (as +Binherit bs) ≡ []
+        u' rewrite as=0 | bs=0 = refl
+        u : canonical (as +B bs) ≡ []
+        u rewrite equalityCommutative (+BIsInherited' as bs) = transitivity (NToBinNatIsCanonical (binNatToN as +N binNatToN bs)) u'
+        t : canonical (incr (as +B bs)) ≡ one :: []
+        t rewrite incrPreservesCanonical' (as +B bs) | u = refl
+        bar : zero :: one :: [] ≡ canonical (zero :: incr (as +B bs))
+        bar rewrite t = refl
+    ans | succ y with≡ x rewrite x | doubleIsBitShift' y = transitivity (applyEquality (λ i → zero :: incr (NToBinNat i)) (equalityCommutative x)) ans2
+      where
+        ans2 : zero :: incr (as +Binherit bs) ≡ canonical (zero :: incr (as +B bs))
+        ans2 rewrite +BIsInherited' as bs | equalityCommutative (incrPreservesCanonical' (as +B bs)) | canonicalAscends' {zero} (incr (as +B bs)) (incrNonzero (as +B bs)) = refl

Numbers/BinaryNaturals/Definition.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --warning=error --safe #-}
+{-# OPTIONS --warning=error --safe --without-K #-}
 
 open import LogicalFormulae
 open import Functions
@@ -16,7 +16,8 @@ module Numbers.BinaryNaturals.Definition where
   BinNat = List Bit
 
   ::Inj : {xs ys : BinNat} {i : Bit} → i :: xs ≡ i :: ys → xs ≡ ys
-  ::Inj refl = refl
+  ::Inj {i = zero} refl = refl
+  ::Inj {i = one} refl = refl
 
   nonEmptyNotEmpty : {a : _} {A : Set a} {l1 : List A} {i : A} → i :: l1 ≡ [] → False
   nonEmptyNotEmpty {l1 = l1} {i} ()
@@ -136,18 +137,6 @@ module Numbers.BinaryNaturals.Definition where
   binToBin : (x : BinNat) → NToBinNat (binNatToN x) ≡ canonical x
   binToBin x = transitivity (NToBinNatIsCanonical (binNatToN x)) (binNatToNInj (NToBinNat (binNatToN x)) x (nToN (binNatToN x)))
 
--- Define the monoid structure, and show that it's the same as ℕ's
-
-  _+Binherit_ : BinNat → BinNat → BinNat
-  a +Binherit b = NToBinNat (binNatToN a +N binNatToN b)
-
-  _+B_ : BinNat → BinNat → BinNat
-  [] +B b = b
-  (x :: a) +B [] = x :: a
-  (zero :: xs) +B (y :: ys) = y :: (xs +B ys)
-  (one :: xs) +B (zero :: ys) = one :: (xs +B ys)
-  (one :: xs) +B (one :: ys) = zero :: incr (xs +B ys)
-
   doubleIsBitShift' : (a : ℕ) → NToBinNat (2 *N succ a) ≡ zero :: NToBinNat (succ a)
   doubleIsBitShift' zero = refl
   doubleIsBitShift' (succ a) with doubleIsBitShift' a
@@ -157,87 +146,11 @@ module Numbers.BinaryNaturals.Definition where
   doubleIsBitShift zero ()
   doubleIsBitShift (succ a) _ = doubleIsBitShift' a
 
-  +BCommutative : (a b : BinNat) → a +B b ≡ b +B a
-  +BCommutative [] [] = refl
-  +BCommutative [] (x :: b) = refl
-  +BCommutative (x :: a) [] = refl
-  +BCommutative (zero :: as) (zero :: bs) rewrite +BCommutative as bs = refl
-  +BCommutative (zero :: as) (one :: bs) rewrite +BCommutative as bs = refl
-  +BCommutative (one :: as) (zero :: bs) rewrite +BCommutative as bs = refl
-  +BCommutative (one :: as) (one :: bs) rewrite +BCommutative as bs = refl
-
-  +BIsInherited[] : (b : BinNat) (prB : b ≡ canonical b) → [] +Binherit b ≡ [] +B b
-  +BIsInherited[] [] prB = refl
-  +BIsInherited[] (zero :: b) prB = t
-    where
-      refine : (b : BinNat) → zero :: b ≡ canonical (zero :: b) → b ≡ canonical b
-      refine b pr with canonical b
-      refine b pr | x :: bl = ::Inj pr
-      t : NToBinNat (0 +N binNatToN (zero :: b)) ≡ zero :: b
-      t with orderIsTotal 0 (binNatToN b)
-      t | inl (inl pos) = transitivity (doubleIsBitShift (binNatToN b) pos) (applyEquality (zero ::_) (transitivity (binToBin b) (equalityCommutative (refine b prB))))
-      t | inl (inr ())
-      ... | inr eq with binNatToNZero b (equalityCommutative eq)
-      ... | u with canonical b
-      t | inr eq | u | [] = exFalso (bad b prB)
-        where
-          bad : (c : BinNat) → zero :: c ≡ [] → False
-          bad c ()
-      t | inr eq | () | x :: bl
-  +BIsInherited[] (one :: b) prB = ans
-    where
-      ans : NToBinNat (binNatToN (one :: b)) ≡ one :: b
-      ans = transitivity (binToBin (one :: b)) (equalityCommutative prB)
-
   canonicalDescends : {a : Bit} (as : BinNat) → (prA : a :: as ≡ canonical (a :: as)) → as ≡ canonical as
   canonicalDescends {zero} as pr with canonical as
   canonicalDescends {zero} as pr | x :: bl = ::Inj pr
   canonicalDescends {one} as pr = ::Inj pr
 
--- Show that the monoid structure of ℕ is the same as that of BinNat
-
-  +BIsInherited : (a b : BinNat) (prA : a ≡ canonical a) (prB : b ≡ canonical b) → a +Binherit b ≡ a +B b
-  +BinheritLemma : (a : BinNat) (b : BinNat) (prA : a ≡ canonical a) (prB : b ≡ canonical b) → incr (NToBinNat ((binNatToN a +N binNatToN b) +N ((binNatToN a +N binNatToN b) +N zero))) ≡ one :: (a +B b)
-
-  +BIsInherited' : (a b : BinNat) → a +Binherit b ≡ canonical (a +B b)
-
-  +BinheritLemma a b prA prB with orderIsTotal 0 (binNatToN a +N binNatToN b)
-  +BinheritLemma a b prA prB | inl (inl x) rewrite doubleIsBitShift (binNatToN a +N binNatToN b) x = applyEquality (one ::_) (+BIsInherited a b prA prB)
-  +BinheritLemma a b prA prB | inr x with sumZeroImpliesOperandsZero (binNatToN a) (equalityCommutative x)
-  +BinheritLemma a b prA prB | inr x | fst ,, snd = ans2
-    where
-      bad : b ≡ []
-      bad = transitivity prB (binNatToNZero b snd)
-      bad2 : a ≡ []
-      bad2 = transitivity prA (binNatToNZero a fst)
-      ans2 : incr (NToBinNat ((binNatToN a +N binNatToN b) +N ((binNatToN a +N binNatToN b) +N zero))) ≡ one :: (a +B b)
-      ans2 rewrite bad | bad2 = refl
-
-  +BIsInherited [] b _ prB = +BIsInherited[] b prB
-  +BIsInherited (x :: a) [] prA _ rewrite +BCommutative (x :: a) [] | additionNIsCommutative (binNatToN (x :: a)) (binNatToN []) = +BIsInherited[] (x :: a) prA
-  +BIsInherited (zero :: as) (zero :: b) prA prB with orderIsTotal 0 (binNatToN as +N binNatToN b)
-  ... | inl (inl 0<) rewrite additionNIsCommutative (binNatToN as) 0 | additionNIsCommutative (binNatToN b) 0 | equalityCommutative (additionNIsAssociative (binNatToN as +N binNatToN as) (binNatToN b) (binNatToN b)) | additionNIsAssociative (binNatToN as) (binNatToN as) (binNatToN b) | additionNIsCommutative (binNatToN as) (binNatToN b) | equalityCommutative (additionNIsAssociative (binNatToN as) (binNatToN b) (binNatToN as)) | additionNIsAssociative (binNatToN as +N binNatToN b) (binNatToN as) (binNatToN b) | additionNIsCommutative 0 ((binNatToN as +N binNatToN b) +N (binNatToN as +N binNatToN b)) | additionNIsAssociative (binNatToN as +N binNatToN b) (binNatToN as +N binNatToN b) 0 = transitivity (doubleIsBitShift (binNatToN as +N binNatToN b) (identityOfIndiscernablesRight _ _ _ _<N_ 0< (additionNIsCommutative (binNatToN b) _))) (applyEquality (zero ::_) (+BIsInherited as b (canonicalDescends as prA) (canonicalDescends b prB)))
-  +BIsInherited (zero :: as) (zero :: b) prA prB | inl (inr ())
-  ... | inr p with sumZeroImpliesOperandsZero (binNatToN as) (equalityCommutative p)
-  +BIsInherited (zero :: as) (zero :: b) prA prB | inr p | as=0 ,, b=0 rewrite as=0 | b=0 = exFalso ans
-    where
-      bad : (b : BinNat) → (pr : b ≡ canonical b) → (pr2 : binNatToN b ≡ 0) → b ≡ []
-      bad b pr pr2 = transitivity pr (binNatToNZero b pr2)
-      t : b ≡ canonical b
-      t with canonical b
-      t | x :: bl = ::Inj prB
-      u : b ≡ []
-      u = bad b t b=0
-      nono : {A : Set} → {a : A} → {as : List A} → a :: as ≡ [] → False
-      nono ()
-      ans : False
-      ans with inspect (canonical b)
-      ans | [] with≡ x rewrite x = nono prB
-      ans | (x₁ :: y) with≡ x = nono (transitivity (equalityCommutative x) (transitivity (equalityCommutative t) u))
-  +BIsInherited (zero :: as) (one :: b) prA prB rewrite additionNIsCommutative (binNatToN as +N (binNatToN as +N zero)) (succ (binNatToN b +N (binNatToN b +N zero))) | additionNIsCommutative (binNatToN b +N (binNatToN b +N zero)) (binNatToN as +N (binNatToN as +N zero)) | equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN b)) = +BinheritLemma as b (canonicalDescends as prA) (canonicalDescends b prB)
-  +BIsInherited (one :: as) (zero :: bs) prA prB rewrite equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = +BinheritLemma as bs (canonicalDescends as prA) (canonicalDescends bs prB)
-  +BIsInherited (one :: as) (one :: bs) prA prB rewrite additionNIsCommutative (binNatToN as +N (binNatToN as +N zero)) (succ (binNatToN bs +N (binNatToN bs +N zero))) | additionNIsCommutative (binNatToN bs +N (binNatToN bs +N zero)) (2 *N binNatToN as) | equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) | +BinheritLemma as bs (canonicalDescends as prA) (canonicalDescends bs prB) = refl
-
 --- Proofs
 
   parity : (a b : ℕ) → succ (2 *N a) ≡ 2 *N b → False
@@ -425,94 +338,6 @@ module Numbers.BinaryNaturals.Definition where
   ... | [] with≡ pr = exFalso (incrNonzero xs pr)
   ... | (_ :: _) with≡ pr rewrite pr = applyEquality (zero ::_) (transitivity (equalityCommutative pr) (incrPreservesCanonical' xs))
 
-  +BIsInherited'[] : (b : BinNat) → [] +Binherit b ≡ canonical ([] +B b)
-  +BIsInherited'[] [] = refl
-  +BIsInherited'[] (zero :: b) with inspect (canonical b)
-  +BIsInherited'[] (zero :: b) | [] with≡ pr rewrite binNatToNZero' b pr | pr = refl
-  +BIsInherited'[] (zero :: b) | (x :: bl) with≡ pr rewrite pr = ans
-    where
-      contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
-      contr {l1 = []} p1 ()
-      contr {l1 = x :: l1} () p2
-      ans : NToBinNat (binNatToN b +N (binNatToN b +N zero)) ≡ zero :: x :: bl
-      ans with inspect (binNatToN b)
-      ans | zero with≡ th rewrite th = exFalso (contr (binNatToNZero b th) pr)
-      ans | succ th with≡ blah rewrite blah | doubleIsBitShift' th = applyEquality (zero ::_) (transitivity (equalityCommutative u) pr)
-        where
-          u : canonical b ≡ incr (NToBinNat th)
-          u = transitivity (equalityCommutative (binToBin b)) (applyEquality NToBinNat blah)
-  +BIsInherited'[] (one :: b) with inspect (binNatToN b)
-  ... | zero with≡ pr rewrite pr = applyEquality (one ::_) (equalityCommutative (binNatToNZero b pr))
-  ... | (succ bl) with≡ pr = ans
-    where
-      u : NToBinNat (2 *N binNatToN b) ≡ zero :: canonical b
-      u with doubleIsBitShift' bl
-      ... | t = transitivity (identityOfIndiscernablesLeft _ _ _ _≡_ t (applyEquality (λ i → NToBinNat (2 *N i)) (equalityCommutative pr))) (applyEquality (zero ::_) (transitivity (applyEquality NToBinNat (equalityCommutative pr)) (binToBin b)))
-      ans : incr (NToBinNat (binNatToN b +N (binNatToN b +N zero))) ≡ one :: canonical b
-      ans = applyEquality incr u
-
-  +BIsInherited' [] b = +BIsInherited'[] b
-  +BIsInherited' (x :: a) [] rewrite +BCommutative (x :: a) [] | additionNIsCommutative (binNatToN (x :: a)) 0 = binToBin (x :: a)
-  +BIsInherited' (zero :: as) (zero :: bs) rewrite equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = ans
-    where
-      ans : NToBinNat (2 *N (binNatToN as +N binNatToN bs)) ≡ canonical (zero :: (as +B bs))
-      ans with inspect (binNatToN as +N binNatToN bs)
-      ans | zero with≡ x with sumZeroImpliesOperandsZero (binNatToN as) x
-      ... | as=0 ,, bs=0 rewrite as=0 | bs=0 = foo
-        where
-          u : canonical (as +Binherit bs) ≡ []
-          u rewrite as=0 | bs=0 = refl
-          foo : [] ≡ canonical (zero :: (as +B bs))
-          foo = transitivity (transitivity b (applyEquality (λ i → canonical (zero :: i)) (+BIsInherited' as bs))) (canonicalAscends'' {zero} (as +B bs))
-            where
-              b : [] ≡ canonical (zero :: (as +Binherit bs))
-              b rewrite u = refl
-      ans | succ y with≡ x rewrite x | doubleIsBitShift' y = transitivity (applyEquality (λ i → zero :: NToBinNat i) (equalityCommutative x)) ans2
-        where
-          u : 0 <N binNatToN (as +B bs)
-          u rewrite equalityCommutative (binNatToNIsCanonical (as +B bs)) | equalityCommutative (+BIsInherited' as bs) | x | nToN (succ y) = succIsPositive y
-          ans2 : zero :: NToBinNat (binNatToN as +N binNatToN bs) ≡ canonical (zero :: (as +B bs))
-          ans2 rewrite +BIsInherited' as bs = canonicalAscends (as +B bs) u
-  +BIsInherited' (zero :: as) (one :: bs) rewrite additionNIsCommutative (2 *N binNatToN as) (succ (2 *N binNatToN bs)) | additionNIsCommutative (2 *N binNatToN bs) (2 *N binNatToN as) | equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = ans2
-    where
-      ans2 : incr (NToBinNat (2 *N (binNatToN as +N binNatToN bs))) ≡ one :: canonical (as +B bs)
-      ans2 with inspect (binNatToN as +N binNatToN bs)
-      ans2 | zero with≡ x with sumZeroImpliesOperandsZero (binNatToN as) x
-      ans2 | zero with≡ x | as=0 ,, bs=0 rewrite as=0 | bs=0 = applyEquality (one ::_) (transitivity t (+BIsInherited' as bs))
-        where
-          t : [] ≡ as +Binherit bs
-          t rewrite as=0 | bs=0 = refl
-      ans2 | succ y with≡ x rewrite x | doubleIsBitShift' y = applyEquality (one ::_) (transitivity (applyEquality NToBinNat (equalityCommutative x)) (+BIsInherited' as bs))
-  +BIsInherited' (one :: as) (zero :: bs) rewrite equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = ans
-    where
-      ans : incr (NToBinNat (2 *N (binNatToN as +N binNatToN bs))) ≡ one :: canonical (as +B bs)
-      ans with inspect (binNatToN as +N binNatToN bs)
-      ans | zero with≡ x with sumZeroImpliesOperandsZero (binNatToN as) x
-      ... | as=0 ,, bs=0 rewrite as=0 | bs=0 = applyEquality (one ::_) (transitivity t (+BIsInherited' as bs))
-        where
-          t : [] ≡ NToBinNat (binNatToN as +N binNatToN bs)
-          t rewrite as=0 | bs=0 = refl
-      ans | succ y with≡ x rewrite x | doubleIsBitShift' y = applyEquality (one ::_) (transitivity (applyEquality NToBinNat (equalityCommutative x)) (+BIsInherited' as bs))
-  +BIsInherited' (one :: as) (one :: bs) rewrite additionNIsCommutative (2 *N binNatToN as) (succ (2 *N binNatToN bs)) | additionNIsCommutative (2 *N binNatToN bs) (2 *N binNatToN as) | equalityCommutative (productDistributes 2 (binNatToN as) (binNatToN bs)) = ans
-    where
-      ans : incr (incr (NToBinNat (2 *N (binNatToN as +N binNatToN bs)))) ≡ canonical (zero :: incr (as +B bs))
-      ans with inspect (binNatToN as +N binNatToN bs)
-      ... | zero with≡ x with sumZeroImpliesOperandsZero (binNatToN as) x
-      ans | zero with≡ x | as=0 ,, bs=0 rewrite as=0 | bs=0 = bar
-        where
-          u' : canonical (as +Binherit bs) ≡ []
-          u' rewrite as=0 | bs=0 = refl
-          u : canonical (as +B bs) ≡ []
-          u rewrite equalityCommutative (+BIsInherited' as bs) = transitivity (NToBinNatIsCanonical (binNatToN as +N binNatToN bs)) u'
-          t : canonical (incr (as +B bs)) ≡ one :: []
-          t rewrite incrPreservesCanonical' (as +B bs) | u = refl
-          bar : zero :: one :: [] ≡ canonical (zero :: incr (as +B bs))
-          bar rewrite t = refl
-      ans | succ y with≡ x rewrite x | doubleIsBitShift' y = transitivity (applyEquality (λ i → zero :: incr (NToBinNat i)) (equalityCommutative x)) ans2
-        where
-          ans2 : zero :: incr (as +Binherit bs) ≡ canonical (zero :: incr (as +B bs))
-          ans2 rewrite +BIsInherited' as bs | equalityCommutative (incrPreservesCanonical' (as +B bs)) | canonicalAscends' {zero} (incr (as +B bs)) (incrNonzero (as +B bs)) = refl
-
   NToBinNatSucc zero = refl
   NToBinNatSucc (succ n) with NToBinNat n
   ... | [] = refl

Numbers/BinaryNaturals/Multiplication.agda

@@ -6,6 +6,7 @@ open import Lists.Lists
 open import Numbers.Naturals
 open import Groups.GroupDefinition
 open import Numbers.BinaryNaturals.Definition
+open import Numbers.BinaryNaturals.Addition
 
 module Numbers.BinaryNaturals.Multiplication where
 

Numbers/Integers.agda

@@ -2,9 +2,10 @@
 
 open import LogicalFormulae
 open import Numbers.Naturals
+open import Numbers.NaturalsWithK -- TODO: remove this dependency, it's baked into ZSimple
 open import Groups.Groups
 open import Groups.GroupDefinition
-open import Rings.RingDefinition
+open import Rings.Definition
 open import Functions
 open import Orders
 open import Setoids.Setoids

Numbers/Naturals.agda

@@ -1,4 +1,4 @@
-{-# OPTIONS --warning=error --safe #-}
+{-# OPTIONS --warning=error --safe --without-K #-}
 
 open import LogicalFormulae
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
@@ -810,14 +810,6 @@ module Numbers.Naturals where
   aIsNotSuccA zero pr = naughtE pr
   aIsNotSuccA (succ a) pr = aIsNotSuccA a (succInjective pr)
 
-  <NRefl : {a b : ℕ} → (p1 p2 : a <N b) → (p1 ≡ p2)
-  <NRefl {a} {.(succ (p1 +N a))} (le p1 refl) (le p2 proof2) = help p1=p2 proof2
-    where
-      p1=p2 : p1 ≡ p2
-      p1=p2 = equalityCommutative (canSubtractFromEqualityRight {p2} {a} {p1} (succInjective proof2))
-      help : (p1 ≡ p2) → (pr2 : succ (p2 +N a) ≡ succ (p1 +N a)) → le p1 refl ≡ le p2 pr2
-      help refl refl = refl
-
   ℕTotalOrder : TotalOrder ℕ
   PartialOrder._<_ (TotalOrder.order ℕTotalOrder) = _<N_
   PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) = lessIrreflexive

Numbers/NaturalsWithK.agda

@@ -0,0 +1,18 @@
+{-# OPTIONS --warning=error --safe #-}
+
+open import LogicalFormulae
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import WellFoundedInduction
+open import Functions
+open import Orders
+open import Numbers.Naturals
+
+module Numbers.NaturalsWithK where
+
+<NRefl : {a b : ℕ} → (p1 p2 : a <N b) → (p1 ≡ p2)
+<NRefl {a} {.(succ (p1 +N a))} (le p1 refl) (le p2 proof2) = help p1=p2 proof2
+  where
+    p1=p2 : p1 ≡ p2
+    p1=p2 = equalityCommutative (canSubtractFromEqualityRight {p2} {a} {p1} (succInjective proof2))
+    help : (p1 ≡ p2) → (pr2 : succ (p2 +N a) ≡ succ (p1 +N a)) → le p1 refl ≡ le p2 pr2
+    help refl refl = refl

Numbers/Rationals.agda

@@ -5,7 +5,7 @@ open import Numbers.Naturals
 open import Numbers.Integers
 open import Groups.Groups
 open import Groups.GroupDefinition
-open import Rings.RingDefinition
+open import Rings.Definition
 open import Fields.Fields
 open import PrimeNumbers
 open import Setoids.Setoids

Numbers/RationalsLemmas.agda

@@ -7,7 +7,7 @@ open import Numbers.Rationals
 open import Groups.Groups
 open import Groups.GroupsLemmas
 open import Groups.GroupDefinition
-open import Rings.RingDefinition
+open import Rings.Definition
 open import Fields.Fields
 open import PrimeNumbers
 open import Setoids.Setoids
@@ -16,7 +16,7 @@ open import Functions
 open import Fields.FieldOfFractions
 open import Fields.FieldOfFractionsOrder
 open import Rings.IntegralDomains
-open import Rings.RingLemmas
+open import Rings.Lemmas
 
 module Numbers.RationalsLemmas where