has it (DecTotalOrder Bin) ?

[mechvel]

has it (DecTotalOrder Bin) ?

[MatthewDaggitt]

Can you elaborate a bit more? Do you mean Fin instead of Bin?

[mechvel]

I see `strictTotalOrder : StrictTotalOrder _ _ _` in `Data.Bin`, but I do not find there `decTotalOrder : decTotalOrder _ _ _` Probably it has sense to add such.

…

------ Sergei

On Thu, 2017-06-22 at 15:21 -0700, MatthewDaggitt wrote: Can you elaborate a bit more? Do you mean Fin instead of Bin? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[MatthewDaggitt]

Correct me if I'm wrong, but _<_ in Data.Bin is not a total order or even a preorder because it is a strict inequality and therefore is not reflexive...

[mechvel]

On Mon, 2017-06-26 at 05:27 -0700, MatthewDaggitt wrote: Correct me if I'm wrong, but _<_ in Data.Bin is not a total order or even a preorder because it is a strict inequality and therefore is not reflexive... — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

Data.Bin defines and exports StrictTotalOrder for _<_. And similarly, it is also desirable to have there DecTotalOrder for _≤_ for Bin. Such is possible to define, but I do not find such.

…

----- Segei

[MatthewDaggitt]

Ah, well at the moment the relation _≤_ isn't even defined in Data.Bin. Adding such a definition would probably mean that the existing definition of _<_ would want to be reworked in terms of it and that would entail making large changes to the rest of the file.

As it's a fairly niche part of the library and a reasonably large piece of work, I don't think that it's likely it'll be done any time soon. However if you need this and have already written the necessary code then please do feel free to submit a pull request with it!

[mechvel]

On Mon, 2017-06-26 at 08:18 -0700, MatthewDaggitt wrote: Ah, well at the moment the relation _≤_ isn't even defined in Data.Bin. Adding such a definition would probably mean that the existing definition of _<_ would want to be reworked in terms of it and that would entail making large changes to the rest of the file. As it's a fairly niche part of the library and a reasonably large piece of work, I don't think that it's likely it'll be done any time soon. However if you need this and have already written the necessary code then please do feel free to submit a pull request with it!

I have its code inside DoCon-A-0.04.1. I am going to separate it and to suggest for Standard, may be, in July 2017. Also, please, consider ftp://ftp.botik.ru/pub/local/Mechveliani/agdaNotes/bin2.zip (of February 2013 !). This is a very essential addition to Bin. Threre are proved some properties from the list that constitutes the _correctness_ of the binary coding. Correctness of the binary coding means that (1) this coding is a bijective map, (2) it preserves the operations _+_, _*_. Without this correctness proof, Bin is not a proved program. This bin2.zip contains a proof for that the binary coding is injective and that it preserves suc <--> addC, may be something else. But I am not sure that I am the only one who proved things on Bin in Agda. The e-mail archive may contain the related announcements from other people (they may be in the segment of 2012 -- 2015). It may have sense to directly ask the Agda email list.

…

------ Sergei

[mechvel]

Please, take a fresh version from there:
ftp://ftp.botik.ru/pub/local/Mechveliani/agdaNotes/bin2.zip

Ii is tested under Agda 2.6.0-207bde6.

[mechvel]

Also
ftp://ftp.botik.ru/pub/local/Mechveliani/agdaNotes/bin3.zip

includes the items of bin2.zip + the instance of DecTotalOrder for Bin
for
x ≤ y defined on Bin as x < y ⊎ x ≡ y.

[MatthewDaggitt]

Thank you for your contribution! It would be great if you could submit some of it as a pull request rather than a zip file. If you need any pointers on creating a pull request please feel free to ask!

As for the ordering x ≤ y = x < y ⊎ x ≡ y, defining _≤_ in terms of _<_ is backwards with respect to the rest of the standard library. I'm reluctant to accept it as I feel its likely to cause confusions for users and further problems down the line. As I mentioned before, I'd be much more comfortable rewriting the implementation of _<_ in terms of a new native _≤_ relation.

[mechvel]

On Wed, 2017-07-05 at 09:59 +0000, MatthewDaggitt wrote: Thank you for your contribution! It would be great if you could submit some of it as a pull request rather than a zip file. If you need any pointers on creating a pull request please feel free to ask!

Please, how to make a pull request in this my particular case? I have done a fork from the project 'Standard library'. In this fork I enter into scr/Data/Bin/ I have the files Bin2.agda Nat2.agda readme.agda to pull, where readme.agda contains a general description and comment. I set "Create new branch", click "Upload files", and "Choose your files". This brings me to the files on my computer. I click at Nat2.agda on my computer. This returns me to the repository, and nothing happens, no message of any file being uploaded. Please, how to improve?

As for the ordering x ≤ y = x < y ⊎ x ≡ y, defining _≤_ in terms of _<_ is backwards with respect to the rest of the standard library. I'm reluctant to accept it as I feel its likely to cause confusions for users and further problems down the line. As I mentioned before, I'd be much more comfortable rewriting the implementation of _<_ in terms of a new native _≤_ relation.

This is a further question to consider.

…

------ Sergei

[MatthewDaggitt]

Please, how to make a pull request in this my particular case?

1. In a suitable directory, on the command line call git clone https://github.com/mechvel/agda-stdlib stdlib-clone. This will copy the standard library into a new folder called stdlib-clone.
2. Make the changes you want to in the files Data.Bin and Data.Bin.Properties within stdlib-clone, (including updating CHANGELOG.md with the changes you've made)
3. Whilst in the top level of the directory stdlib-clone, run the command make test from the command line to check that your changes haven't broken anything.
4. Add the files you've made changes to using the commands git add src/Data/Bin.agda, git add src/Data/Bin/Properties.agda, git add CHANGELOG.md etc.
5. Commit the files you've added using git commit.
6. Push all your changes to your fork on github using git push origin master
7. Go to https://github.com/mechvel/agda-stdlib and there should be a button to create a pull request from your new commit.

[mechvel]

I put Nat2.agda into the folder Data/Nat/,
and put Bin2.agda into Data/Bin

And module Data.Bin.Bin2
imports items from ``Data.Nat.Nat2''.

And ``make test" reports

---

cabal clean && cabal install
cleaning...
Resolving dependencies...
Configuring lib-0.13...
Building lib-0.13...
Preprocessing executable 'GenerateEverything' for lib-0.13...
[1 of 1] Compiling Main ( GenerateEverything.hs, dist/build/GenerateEverything/GenerateEverything-tmp/Main.o )
Linking dist/build/GenerateEverything/GenerateEverything ...
Preprocessing executable 'AllNonAsciiChars' for lib-0.13...
[1 of 1] Compiling Main ( AllNonAsciiChars.hs, dist/build/AllNonAsciiChars/AllNonAsciiChars-tmp/Main.o )
Linking dist/build/AllNonAsciiChars/AllNonAsciiChars ...
Installing executable(s) in /home/mechvel/.cabal/bin
Installed lib-0.13
cabal exec -- GenerateEverything
GenerateEverything: src/Data/Bin/Bin2.agda is malformed

I reduce this module to two lines (by commenting out all the rest):

module Data.Bin.Bin2 where -- ℕ <--> Bin⁺ isomorphism

open import Level using () renaming (zero to 0ℓ)

and still it is reported "malformed".

I wonder what might this mean.

[mechvel]

As for the ordering x ≤ y = x < y ⊎ x ≡ y, defining ≤ in terms of < is backwards with respect
to the rest of the standard library. I'm reluctant to accept it as I feel its likely to cause confusions
for users and further problems down the line. As I mentioned before, I'd be much more
comfortable rewriting the implementation of < in terms of a new native ≤ relation.

Currently, Bin has the following implementation to _<_ :

data _<_ (b₁ b₂ : Bin) : Set where
less : (lt : (Nat._<_ on toℕ) b₁ b₂) → b₁ < b₂

Do you suggest to replace this with

data _≤__ (b₁ b₂ : Bin) : Set where
leq : (le : (Nat._≤__ on toℕ) b₁ b₂) → b₁ ≤_b₂

and then, to define _<_ as
x < y = x ≤ y × x ≢ y
?

[MatthewDaggitt]

I put Nat2.agda into the folder Data/Nat/ and put Bin2.agda into Data/Bin

So the changes that you're making shouldn't be put inside their own files. They should be incorporated into the existing Data.Bin and Data.Bin.Properties files. This should bypass your current problem with the tests.

Currently, Bin has the following implementation to <:

data < (b₁ b₂ : Bin) : Set where
less : (lt : (Nat.< on toℕ) b₁ b₂) → b₁ < b₂

Do you suggest to replace this with

data ≤_ (b₁ b₂ : Bin) : Set where
leq : (le : (Nat.≤_ on toℕ) b₁ b₂) → b₁ ≤_b₂

and then, to define < as
x < y = x ≤ y × x ≢ y

That certainly seems better. In fact, as we're reworking the implementation and the changes aren't going to be backwards compatible anyway, I might be tempted to copy the style of _≤_ in Data.Fin and get rid of the data declaration entirely so that it reads as follows:

_≤_ : Rel Bin Set
x ≤ y = toℕ x Nat.≤ toℕ y

_<_ : Rel Bin Set
x < y = x ≤ y × x ≢ y

The notes say that the existing data declaration is to aid in pattern matching. It might be worth experimenting with the two different definitions of _≤_: your new version and mine and see which is easier to work with.