search

sbp / idris-bi

Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq
https://github.com/idris-lang/Idris-dev/issues/3976
36 stars 5 forks source link

WIP: BIP: The Final Proofs #12

Closed clayrat closed 7 years ago

clayrat commented 7 years ago

I'm almost done with gcdn_greatest and then it's basically ggcd_greatest remaining.

clayrat commented 7 years ago

Ok, so I have ported everything under Module Pos. After that there's a bunch of syntax definitions and some "compatibility facts", do you think we need those as well?

clayrat commented 7 years ago

Oh, seems there also are some proofs in Pnat.v, we probably need those too?

sbp commented 7 years ago

Yep, it would be nice to certify the interpretation of Bip as Nat as Pnat.v allows. I think this is especially important because toNatBip works in a different way to the current implementation in Coq.PArith.BinPosDef. I think I was using an old version of the code when I ported that.