patrick/agdaproofs
1
0
Fork 0
mirror of https://github.com/Smaug123/agdaproofs synced 2025-10-13 07:38:40 +00:00
Code Issues Packages Projects Releases Wiki Activity

Complete the proof that monoid structure is shared between N and BinNat (#31)

Browse Source
This commit is contained in:
Patrick Stevens
2019-07-29 18:45:29 +01:00
committed by GitHub
parent 226f1ad0f7
commit ff5ede3fa8
1 changed files with 10 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
Numbers/BinaryNaturals.agda
View File

@@ -91,12 +91,11 @@ module Numbers.BinaryNaturals 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)
_+BinheritC_ : Canonicalised → Canonicalised → Canonicalised
(a , prA) +BinheritC (b , prB) = NToBinNatC (binNatToN a +N binNatToN b)
_+B_ : BinNat → BinNat → BinNat
[] +B b = b
(x :: a) +B [] = x :: a
@@ -104,11 +103,14 @@ module Numbers.BinaryNaturals where
(one :: xs) +B (zero :: ys) = one :: (xs +B ys)
(one :: xs) +B (one :: ys) = zero :: incr (xs +B ys)
-- Still not sure of the right way to go about this one. Should we go via canonical, even though it's a big waste in almost all cases?
doubleIsBitShift' : (a : ℕ) → NToBinNat (2 *N succ a) ≡ zero :: NToBinNat (succ a)
doubleIsBitShift' zero = refl
doubleIsBitShift' (succ a) with doubleIsBitShift' a
... | bl rewrite additionNIsCommutative a (succ (succ (a +N 0))) | additionNIsCommutative (succ (a +N 0)) a | additionNIsCommutative a (succ (a +N 0)) | additionNIsCommutative (a +N 0) a | bl = refl
doubleIsBitShift : (a : ℕ) → (0 <N a) → NToBinNat (2 *N a) ≡ zero :: NToBinNat a
doubleIsBitShift zero ()
doubleIsBitShift (succ a) _ with inspect (NToBinNat (a +N succ (a +N 0)))
doubleIsBitShift (succ a) _ | t = {!!}
doubleIsBitShift (succ a) _ = doubleIsBitShift' a
+BCommutative : (a b : BinNat) → a +B b ≡ b +B a
+BCommutative [] [] = refl
@@ -147,6 +149,8 @@ module Numbers.BinaryNaturals where
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)