Add some "verified" implementations #4848
Conversation
|
I added a small module for group homomorphisms. It might be too specialized to be included here, but the proofs are pretty cool, and the alternative is leaving them in the void that is my |
nickdrozd
force-pushed
the
implementations
branch
2 times, most recently
from
553abe6 to
942a2c7
Compare
|
I added a module for cyclic groups along with more cool proofs, and some more minor changes. |
There was a problem hiding this comment.
You definitely moved around a lot of code. It makes it difficult to work out, which parts are added and which are just moved. Also it's difficult to see whether moved code has been changed or not. For that reason I believe that moving things around should probably be done in separate PRs for clarity's sake.
Besides, moving interfaces and implementations is a breaking change and I'm not sure if it's proper to do it with Idris2 just around the corner. Probably better make these changes there?
| ||| + Inverse for `<+>`: | ||
| ||| forall a, a <+> inverse a == neutral | ||
| ||| forall a, inverse a <+> a == neutral | ||
| interface Group a => AbelianGroup a where { } |
There was a problem hiding this comment.
While I understand (and agree with) the idea of this change, it'll break third-party code if it depends on this interface structure. Therefore I would be very careful with it and only introduce it on a major version change.
There was a problem hiding this comment.
Has AbelianGroup actually be implemented anywhere outside of this repo? My guess is that it has not, although I would be interested to see any examples in the wild.
There was a problem hiding this comment.
I certainly implemented it once or twice. Probably still have the code somewhere on my disk. ;) But I understand your point. It's probably right.
| rewrite semigroupOpIsAssociative b c d in | ||
| rewrite abelianGroupOpIsCommutative b c in | ||
| rewrite sym $ semigroupOpIsAssociative c b d in | ||
| semigroupOpIsAssociative a c (b <+> d) |
There was a problem hiding this comment.
These kinds of rearrangements are painful. There's this discrepancy between how we intuitively think about addition (actually about all operations that are simultaneously commutative and associative) as a list of terms, where exact sequencing does not matter. On the other hand in the AST it's represented as a tree, rather than a list, which makes moving terms around much more, well not exactly difficult, but troublesome I'd say. I've been dreaming for some time now of a view (i.e. specific type) allowing to express such lengthy sums (or products, or whatever) as a list of terms. I tried to do it myself once, but I got stuck on the way of proving properties of such views. Maybe you'd like to try doing it? Having such a type, we could even devise some syntax sugar to make such rearrangements even more intuitive…
There was a problem hiding this comment.
It would be nice to have something like that, but I don't know how. I've just been grinding through on a case-by-case basis.
There was a problem hiding this comment.
I imagine it would be a type containing a List (or Vect) of terms, with a proof that folding it is the same as a regular use of the function you fold with. It should only require associativity I guess? Then you can implement transformations on the List, proving they still don't change the result (this is where commutativity will be required. I have tried something like this:
data Sum : Type -> Type where
MkSum : Monoid a => List a -> Sum a
eval : Sum a -> a
terms : Sum a -> List a
evalEquvalentToFold : Monoid s => (s : Sum a) -> eval s = fold (<+>) Algebra.neutral (terms s)
Unfortunately proving anything about fold is difficult due to the way it's implemented. Probably a slightly different approach would be required, but I think this is the right direction.
| -- rewrite inverseNeutralIsNeutral {t=t} in | ||
| -- rewrite monoidNeutralIsNeutralL a in | ||
| -- rewrite monoidNeutralIsNeutralL x in | ||
| -- Refl |
There was a problem hiding this comment.
Unfortunately I don't know the answer to your question.
However, I'm definitely against committing commented-out code to the master. If it does not work, for whatever reason, it shouldn't be committed. Perhaps you could propose it as a separate PR after this one is done, so that every one can pull the branch in question and investigate more easily?
There was a problem hiding this comment.
I cut the code, but left the implementation line commented out as a clue for the future.
| mtimesTimes x Z m = sym $ monoidNeutralIsNeutralR $ mtimes' m x | ||
| mtimesTimes x (S k) m = | ||
| rewrite mtimesTimes x k m in | ||
| semigroupOpIsAssociative x (mtimes' k x) (mtimes' m x) |
There was a problem hiding this comment.
This property is called distributivity. Maybe mtimesDistributesOverGroupOp?
There was a problem hiding this comment.
I suppose that is technically true, but the spirit of the operation is that it's exponentiation when the group op is interpreted as multiplication, or multiplication when it's interpreted as addition.
There was a problem hiding this comment.
I can't see, how does it matter. Exponentiation does indeed distribute over multiplication. But mtimesDistributesOverGroupOp mentions neither addition nor multiplication explicitly, so it should be ok.
| gtimesCommutes x n m = | ||
| rewrite sym $ gtimesTimes x n m in | ||
| rewrite plusCommutativeZ n m in | ||
| gtimesTimes x m n |
There was a problem hiding this comment.
Isn't this just a special case of commutativity of ZZ addition? I mean plusCommutativeZ (gtimes n x) (gtimes m x) has exactly this type, doesn't it?
There was a problem hiding this comment.
No, gtimes n x produces an instance of the group type, not a ZZ.
This way a module can import Verified without importing implementations, avoiding circular dependencies in some cases. It would be nicer to put the implementations in with their types.
I suggest looking at the commits one by one. Github seems to have put them slightly out of order, but it should still clarify what is getting moved and what is getting added. The problem with the current algebra module arrangement is that all sorts of implementations are included along with the interfaces, and it quickly becomes difficult to change anything without running into circular imports. It's also the case that the existing arrangement was basically set up as a temporary dump, and doesn't have much to recommend it. I don't personally care much about the release schedule, but these things need to get sorted out at some point. Since I'm trying to add things that basically can't be added without rearranging things, I figured I would do it all at once. |
I was running into some weird import issues, and this seems to solve them. Interfaces.Verified as a module probably ought to be abolished, as it really isn't very useful as a grouping.
Every cyclic group is abelian, so also replace AbelianGroup implementations with CyclicGroup implementations where possible.
AbelianGroup doesn't add anything syntactically, so there really isn't any point to maintaining the plain / verified split.
nickdrozd
force-pushed
the
implementations
branch
from
942a2c7 to
0fd6d50
Compare
|
I imagine it would be a type containing a List (or Vect) of terms, with a
proof that folding it is the same as a regular use of the function you fold
with. It should only require associativity I guess? Then you can implement
transformations on the List, proving they still don't change the result
(this is where commutativity will be required. I have tried something like
this:
This seems to be an example of proof by reflection. I think the description
in CPDT is pretty good: http://adam.chlipala.net/cpdt/html/Reflection.html
|
This PR adds in some proofs from #4841 without the major interface changes (there are some minor changes having to do with module organization). One big frustrating problem is that the proofs at https://github.com/idris-lang/Idris-dev/pull/4841/files#diff-5f4f002b8c0e9f0c582eea71e165f6b3R236 don't seem to work in the "verified" context. Does anybody know why??? @Sventimir @ziman