Add Algebra interfaces and laws

[nickdrozd]

This PR ports over some Algebra stuff from Idris 1. It is mostly similar: the interfaces are split into syntactic versions and verified versions. The latter are named like VMonoid etc. That can be changed, but I think it's the most ergonomic name.

Many of the theorems are stated but not proved. They can all be proved in Idris 1 [1], but the proofs don't work here. I would expect them all to work. There seem to be a few different bugs involved, but I don't understand the details.

[1] See https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Control/Algebra/Laws.idr and idris-lang/Idris-dev#4848

[nickdrozd]

I've included commented-out the proofs that I would expect to work, but don't. In some cases, the mirror image of the proof does work. For instance, this works:

cancelLeft : VGroup ty => (x, y, z : ty) ->
  x <+> y = x <+> z -> y = z
cancelLeft x y z p =
  rewrite sym $ monoidNeutralIsNeutralR y in
    rewrite sym $ groupInverseIsInverseR x in
      rewrite sym $ semigroupOpIsAssociative (inverse x) x y in
        rewrite p in
      rewrite semigroupOpIsAssociative (inverse x) x z in
    rewrite groupInverseIsInverseR x in
  monoidNeutralIsNeutralR z

But this doesn't:

cancelRight : VGroup ty => (x, y, z : ty) ->
  y <+> x = z <+> x -> y = z
cancelRight x y z p =
  rewrite sym $ monoidNeutralIsNeutralL y in
    rewrite sym $ groupInverseIsInverseL x in
      rewrite semigroupOpIsAssociative y x (inverse x) in
        rewrite p in
      rewrite sym $ semigroupOpIsAssociative z x (inverse x) in
    rewrite groupInverseIsInverseL x in
  monoidNeutralIsNeutralL z

[rgrover]

In essence:

• some of the commented sections may be un-necessary.
• Idris2 appears to be unable to normalize straightforward equalities in some cases.
  I'm sorry I didn't go further with the proofs. I feel this is a valuable addition. All the best.

[rgrover]

same as above. this can be uncommented.

[nickdrozd]

Control/Algebra/Laws.idr:45:7--48:1:While processing right hand side of inverseCommute at Control/Algebra/Laws.idr:39:1--48:1:
While processing right hand side of inverseCommute,prop at Control/Algebra/Laws.idr:41:3--48:1:
Rewriting by neutral <+> ?ty x y p (\{rwarg:1434} => (rwarg = x <+> y)) (sym (semigroupOpIsAssociative x y (x <+> y))) (\{rwarg:1451} => (x <+> rwarg = x <+> y)) (semigroupOpIsAssociative y x y) (\{rwarg:1459} => (x <+> (rwarg <+> y) = x <+> y)) p = ?ty x y p (\{rwarg:1434} => (rwarg = x <+> y)) (sym (semigroupOpIsAssociative x y (x <+> y))) (\{rwarg:1451} => (x <+> rwarg = x <+> y)) (semigroupOpIsAssociative y x y) (\{rwarg:1459} => (x <+> (rwarg <+> y) = x <+> y)) p did not change type x <+> (neutral <+> y) = x <+> y

[rgrover]

Using Idris2 from 4aa1c1f, this definition, when uncommented, compiles for me.

[nickdrozd]

Using 6898965:

Control/Algebra/Laws.idr:33:7--35:1:While processing right hand side of selfSquareId at Control/Algebra/Laws.idr:28:1--35:1:
Can't solve constraint between:
	neutral
and
	inverse x <+> x

[rgrover]

can be uncommented (see above)

[nickdrozd]

Control/Algebra/Laws.idr:53:33--53:57:While processing right hand side of groupInverseIsInverseL at Control/Algebra/Laws.idr:52:1--55:1:
Can't solve constraint between:
	Constraint (Monoid ty) (Constraint (MonoidV ty) conArg)
and
	Constraint (Monoid ty) (Constraint (Group ty) conArg)

[rgrover]

Idris2 isn't able to use x' = inverse x in its normalization. The following also reproduces the issue (the copiler complains about prf):

let x' = inverse x
    prf = the (x' = inverse x) Refl
 in ...

[rgrover]

Based on what @edwinb suggested, we could aid Idris2 in the equality between x' and inverse x using a local function like:

||| -(-x) = x
public export
inverseSquaredIsIdentity : VGroup ty => (x : ty) ->
  inverse (inverse x) = x
inverseSquaredIsIdentity x =
  let
    lemma : (x' : ty) -> (x' = inverse x) -> inverse (inverse x) = x
    lemma x' prf =
      uniqueInverse
        x'
        (inverse (inverse x))
        x
        (rewrite sym prf in groupInverseIsInverseR x')
        (rewrite prf in groupInverseIsInverseR x)
   in lemma (inverse x) Refl

[nickdrozd]

I suggest we avoid leaning on workarounds like this. As a user, I don't want to have to work around quirks in the type system. Ideally I would be able to express what I want to express without feeling like I have to walk on eggshells to satisfy the typechecker.

Especially in this particular case, the existing proof is clean and elegant, and this change obscures that.

[edwinb]

Thanks for these. I'd like to take a look at the ones which fail before merging this, just to avoid having things with types but no definitions in the library.

Also some bikeshedding - I'm not sure about having the V as a prefix, my preference would be for a suffix for tab completion reasons. I expect there's as many opinions on naming as there are people, however...

[edwinb]

Actually it looks as if @rgrover has worked out all the problems, thanks for that! The let one is decribed here: https://idris2.readthedocs.io/en/latest/updates/updates.html#let-bindings

It's an annoyance, but better for overall consistency, with the core language as it stands.

[nickdrozd]

@edwinb I changed VMonoid to MonoidV, etc.

[nickdrozd]

@rgrover I wasn't able to get any of the proofs to go through locally. I uncommented the proofs and pushed to see how the CI would react. It has failed, but I can't see the output.

[nickdrozd]

I got rid of all the let bindings and uncommented the proofs (except for inverseOfSum, which I couldn't get to go through). There are no holes left, so unless anyone has any objections this should be good to go.

[edwinb]

Sorry, this has been lingering for a while - everything looks fine to me though. Thanks for the contribution!