sbp / idris-bi Goto Github PK

Coq defines its types in Numbers.BinNums which seems a little strange to me. It may be because they modularise [NPZ]Arith over so many files and they found that it's better to import the types into each file rather than do chained exporting.

On the other hand, in idris-bi we're keeping everything in the files Bip.idr, Bin.idr, and Biz.idr. It might be a good idea to move Bip into Bip.idr and so on. That way we would eliminate the Bi.idr file entirely. Who's really going to import Data.Bi without importing one of the other files?

In some places it's b*q+r, in others it's q*b+r; would be nice to choose a single style (personally I like q*b+r more) to avoid extra mulComms.

Whilst I only envisaged porting the P, N, and Z arithmetics from Coq, it might be nice to go for full-on completion and port QArith too. I'm not sure what the type should be, but probably something like this:

record Biq where
  constructor Ratio
  numerator: Biz
  denominator: Bip

The constructor could be Rational instead of Ratio, though by convention it should really be MkBiq. Coq uses num and den for the field names. I don't like "num", but perhaps n and d, or numer and denom would be okay.

Reproducible with Nix:

$ nix-build https://github.com/nixos/nixpkgs/archive/a8c7103.tar.gz -A idrisPackages.bi
these derivations will be built:
  /nix/store/3cjip6k9ndqlsmdv1x3xmx7j5hqc79qk-bi-2018-01-17.drv
building '/nix/store/3cjip6k9ndqlsmdv1x3xmx7j5hqc79qk-bi-2018-01-17.drv'...
unpacking sources
unpacking source archive /nix/store/ngky5q8yzgghzfppb2sg1fzwyxzzj6r2-source
source root is source
patching sources
configuring
no configure script, doing nothing
building
Entering directory `./src'
Type checking ./Data/Bi.idr
Type checking ./Data/Util.idr
Type checking ./Data/Bip.idr
Type checking ./Data/Bip/AddMul.idr
Type checking ./Data/Bip/Iter.idr
./Data/Bip/Iter.idr:86:1-32:
   |
86 | iterInvariant f Inv  U    g x ix = g x ix
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking left hand side of iterInvariant:
When checking argument Inv to Data.Bip.Iter.iterInvariant:
        Inv is not a valid name for a pattern variable
builder for '/nix/store/3cjip6k9ndqlsmdv1x3xmx7j5hqc79qk-bi-2018-01-17.drv' failed with exit code 1
error: build of '/nix/store/3cjip6k9ndqlsmdv1x3xmx7j5hqc79qk-bi-2018-01-17.drv' failed

Might be quite useful to link Bip/Bin/Biz to un/signed machine words, perhaps by making a covering function for Data.Bits.

If we define bipMinus as

bipMinusHelp : Bim -> Bip
bipMinusHelp (BimP c) = c
bipMinusHelp _        = U

bipMinus : (a, b: Bip) -> Bip
bipMinus a b = bipMinusHelp (bimMinus a b)

then the proof of subSuccR simplifies a lot, since now we can use rewrite:

subSuccR : (p, q: Bip) -> bipMinus p (bipSucc q) = bipPred (bipMinus p q)
subSuccR p q = rewrite subMaskSuccR p q in 
               rewrite subMaskCarrySpec p q in 
               aux (bimMinus p q)
  where
  aux : (m : Bim) -> bipMinusHelp (bimPred m) = bipPred (bipMinusHelp m) 
  aux  BimO        = Refl
  aux (BimP  U   ) = Refl
  aux (BimP (O _)) = Refl
  aux (BimP (I _)) = Refl
  aux  BimM        = Refl

So I propose to redefine all case-using functions (bipMinus, bipMin, bipMax, bipSqrtRemStep etc) to this form, at least until idris-lang/Idris-dev#4001 is fixed.

Another inconvenience is that we can't put these helpers under where, as there currently is no way to refer to them (see idris-lang/Idris-dev#3991).

Or replace-heavy ones.

Example: https://github.com/ahmadsalim/desc-n-crunch/blob/master/src/Interfaces.idr

For now I've been simply converting snake_case to camelCase in proof names, but I think once Bip proofs are done, we should go through them and rename to reflect the names of actual Bip functions (e.g., subMask* -> bimMinus* etc).

I suspect many of the proofs here in theory could be simplified using https://github.com/FranckS/RingIdris

The question of course is how usable that library is :)

Should we bring back trivial proofs, i.e. ones provable with a single Refl? I've been leaving them out as they're useless as lemmas due to Idris's strong normalization, but maybe they're still useful as simple sanity checks?

Inequalities:

• Have a set of inductive inequality definitions (http://www.reddit.com/r/Idris/comments/6ya7jg/unification_problems_associated_with_totality/), and bijections to the witness-style ones currently used?
• Reduce code duplication for ltGt, leTrans and others: interfaces, elaborator macros?
• Fix order of arguments in Bin and Biz versions of addCompareMonoR

We seem to have two versions of those: in Bip, to define bipAnd/bipDiff/bipXor, and in Bin proper as binDPO/binD. As we don't have any proofs of bipAnd etc in Bip, might as well move those to Bin to avoid duplication?