[Agda] ℕ <--iso--> Bin⁺ ∩ HasLast1if
mechvel at botik.ru
Tue Nov 26 19:00:46 CET 2013
as an exercise in Agda, I provide
-- my own proof in Agda for suc - isomorphism between ℕ and its
-- an addition to Standard library lib-0.7.
1. It uses the binary code (Bin⁺) representation in which
0 <--> , and a binary code either is  or ends with 1b
(as the higher bit).
This higher bit condition is expressed as HasLast1if, HasLast1.
2. It is proved in Bin.agda that
ℕ <--suc-isomorphic--> Bin⁺ ∩ HasLast1if,
suc corresponds to addCarryToBitList.
3. For this aim, we re-implement toDigits in the form of
toBDigits : (n : ℕ) → ∃ \ (bs : Bin⁺) →
fromDigits bs ≡ n × HasLast1if bs
(for base = 2 only)
- because it is easier for us to compose proofs for such.
4. The main parts are
- injectiveness of fromDigits on Bin⁺ ∩ HasLast1if.
5. My question is:
can this be proved in a simpler/shorter (nicer) way?
(for example, injective-fromDigits looks lengthy).
6. The program consists of the two modules and is tested under
Agda-2.3.3-pre Malonzo, lib-0.7
- both of the development version of November 24, 2013.
(the 126.96.36.199 version, or lower ones, will not do).
I hope it will also work under any later version.
More information about the Agda