Additions to Data.Bin

[MatthewDaggitt]

No description provided.

[MatthewDaggitt]

Okay @mechvel, we've finally made the pull request, well done for getting this far! We'll now try and get your code into the right shape to be added to the standard library.

Let's first look at your additions to Data.Nat.Properties. There are a few general guidelines you should adhere to when writing code for the standard library:

1. Don't perform renaming unless it's absolutely necessary. We like to keep things named the same throughout the library to make it easier for users to read the code. For example:

   • Line 26: you rename the standard syntax for ≡-Reasoning. Instead you should change your code to use the standard syntax.
   • Lines 945-948: you rename various record types. Instead just use the names directly.
   • Line 954: for half just use ⌊_/2⌋ directly.

2. Don't reprove things that are already in the standard library. The aim is always to add the minimum number of changes to the standard library to prove what you need to. e.g.

   • Line 970: 1* already exists as *-left-identity
   • Line 986: n≤suc-n already exists as n≤1+n
   • Lines 1011, 1014, 1030: <→≤, <→≢ and ≤,≢-then< already exist as <⇒≤, <⇒≢ and ≤+≢⇒<
   • Line 1035: <-antisym exists as <-asym

3. Don't create proofs that are "too small" and whose contents can just be written directly. For example

   • Line 964: +cong₁ and +cong₂ can simply be replaced by cong (_+ y) and cong (x +_)
   • Line 977: suc>0 can be replaced with s≤s z≤n
   • Line 989: suc-n>n can be replaced with ≤-refl

The examples above aren't a complete list. See if you can spot other instances of them as well in your code. As we've discussed you can make changes to the pull request by simply repeating the steps detailed in #65. After pushing your new changes to your repository, they'll automatically show up here.

Let me know when you've pushed your changes improving on the style points above!

[mechvel]

Thank you for your notes.
Please, respond to my arguments for (1), (2), (3).
If you insist, then I would follow your suggestion.

(1) The denotation suc>0 is clear to everyone who knows what is suc.
And (s≤s z≤n) is something special, the reader would take an effort to understand the meaning.

(2) ≡-Reasoning has a very strange parenthesis. It looks like ( but is not (.
I think that my denotation is easier to operate with.
(3) 1* is much easier to read/understand in proofs than *-left-identity

[MatthewDaggitt]

The denotation suc>0 is clear to everyone who knows what is suc. And (s≤s z≤n) is something special, the reader would take an effort to understand the meaning.

Okay I agree that it's more meaningful semantically. Please could you rename it to 0<1+n to follow the conventions in the Data.Nat.Properties.

≡-Reasoning has a very strange parenthesis. It looks like ( but is not (. I think that my denotation is easier to operate with.

I think that is a problem with the font that you are using. In most fonts it comes out as an angled bracket which is clearly distinguishable from a curved bracket.

1* is much easier to read/understand in proofs than *-left-identity

I think that's a matter of opinion, to me it looks like an identity function 1*_! I'm afraid that, for better or worse, the proof already exists in the standard library and so you'll need to use the standard name.

[WolframKahl]

-- Commit Summary -- * Committer: Sergei Meshveliani ***@***.***>

Is it possible to change this to the e-mail address Sergei's preferred address <[email protected]> ? (Would this be helped in the future by Sergei changing either an address in his github account, or some local setting on his machines?)

[WolframKahl]

3. Don't create proofs that are "too small" and whose contents can just be written directly. For example - Line 964: `+cong₁` and `+cong₂` can simply be replaced by `cong (_+ y)` and `cong (x +_)`

`+cong₁` and `+cong₂` have less than half the characters compared with those expansions. As long as I need combinators like these at all, I very strongly want to use their shorter names. If the standard library does not proved these short names, I have to provide them for myself, and Sergei has to provide them for himself, and possibly similar for some other users... (And that is not even counting the fact that `x` and `y` may not be that short.)

[mechvel]

1* is much easier to read/understand in proofs than *-left-identity

I think that's a matter of opinion, to me it looks like an identity function 1*_!

It is only in the proof part, so it cannot be undedrstood as id.

I'm afraid that, for better or worse, the proof already exists in the standard library and so you'll
need to use the standard name.

If you insist, then all right.

Do I and Wolfram convince you about +cong₁ and such?
The matter is that cong (_+ y)
often occurs like this: cong (_+ ((x1 * x2 + a) * 2)).
And I write this as +cong₁ by using hidden argument
(though in abut half of the cases Agda forces me to set the hidden argument).
Proofs are difficult to read when large expressions are copied from LHS to the part of
≡⟨ ... ⟩.

[mechvel]

suc-n>n can be replaced with ≤-refl

1. I succeed only with ≤-refl PE.refl.
2. Similar as with 0<1+n, can you agree wih that
   n<1+n is easier to understand than (≤-refl PE.refl)
   ?

[gallais]

I would expect +cong₂ to be cong₂ _+_ given that cong₂ is already an existing notion in the standard library. Using exponent ˡ and ʳ seems more appropriate here.

Also, if (x1 * x2 + a) * 2 can be inferred then cong (_+ ((x1 * x2 + a) * 2)) can simply be written cong (_+ _). If it can't then the shorthand won't bring anything to the table.

[mechvel]

I would expect +cong₂ to be cong₂ + given that cong₂ is already an existing notion in the
standard library. Using exponent ˡ and ʳ seems more appropriate here.

Also, if (x1 * x2 + a) * 2 can be inferred then cong (+ ((x1 * x2 + a) * 2)) can simply be written
cong (+ _). If it can't then the shorthand won't bring anything to the table.

This all looks reasonable.
Concerning the cong denotations, I am going to try to follow Matthew's solution, and then, to see.

[MatthewDaggitt]

I succeed only with ≤-refl PE.refl

Well the library version of ≤-refl doesn't take any arguments, so you must still be using your own version. You'll need to switch to the library version.

Similar as with 0<1+n, can you agree with that n<1+n is easier to understand than (≤-refl PE.refl)

Okay, there is a tension between filling the library up with copies of redundant lemmas and increasing the readability of proofs. I agree that n<1+n does have some merit. However (and I can see this argument coming) the proof 2+n>1 falls on the wrong side of this! Otherwise people will be asking to have 3+n>2, 4+n>3 etc. Would you remove it in favour of something like s≤s 0<1+n.

Also, if (x1 * x2 + a) * 2 can be inferred then cong (+ ((x1 * x2 + a) * 2)) can simply be written
cong (+ _). If it can't then the shorthand won't bring anything to the table.

I agree with @gallais completely. In many cases the implicit arguments to +cong₁ and +cong₂ cannot be inferred and therefore, following standard library conventions, they should be made explicit. In which case nothing is gained over cong (_ +_).

[mechvel]

Also, if (x1 * x2 + a) * 2 can be inferred then cong (+ ((x1 * x2 + a) * 2)) can simply be written
cong (+ _). If it can't then the shorthand won't bring anything to the table.

For example, my commited code (in the end of Data.Nat.DivMod) includes the line

n=q*2 = P.trans n=rN+q*2 (+cong₁ rN=0)

The lib-conservative stile makes it
n=q*2 = P.trans n=rN+q*2 (cong (_+ (q * 2)) rN=0)

Replacing (q * 2) with _ leads to "unsolved metas".
And with +congˡ , it is written as
n=q*2 = P.trans n=rN+q*2 (+congˡ rN=0).

Here Agda allows to omit a hidded argument for +congˡ
(and in about half of another cases it would not allow).
As it often occur larger expresssions in place of (q * 2), I introduce

+congˡ :  {y : ℕ} → (_+ y) Preserves _≡_ ⟶ _≡_
+congˡ {y} =  PE.cong (_+ y)

If the lib maintainer insists, then I shall remove +congˡ and +congʳ denotation from the commit.

[mechvel]

It looks like I have satisfied all the requirements for the code.
But I fail with updating the pull request. See my letter on the Agda mail list.
I put the proposal to

http://www.botik.ru/pub/local/Mechveliani/agdaNotes/bin2.zip

There are 7 files, including CHANGELOG.md and Readme.txt.
Can this stand for pull-requst?

Remarks are welcome.

[MatthewDaggitt]

With the announcement of @mechvel's new library Binary 3.0, I think users interested in binary computation can use that library directly, and so I'm going to close this pull request.