Getting started with math-classes

[langston-barrett]

Hi there,

I'm trying to do some basic linear algebra proofs. I was using the coq algebra contrib, but discovered math-classes and decided to give it a try!

One thing that's stopping me right now is that the algebra distribution includes some very basic proofs about immediate consequences of the structure laws that I'm not sure how to begin replicating with math-classes. For instance, algebra includes the following lemma:

Lemma MODULE_absorbant_l :
 forall x : Mod, Equal (module_mult (monoid_unit R) x) (monoid_unit Mod).
intros x; try assumption.
apply GROUP_reg_left with (module_mult (monoid_unit R) x); auto with algebra.
apply
 Trans with (module_mult (sgroup_law R (monoid_unit R) (monoid_unit R)) x);
 auto with algebra.
apply Trans with (module_mult (monoid_unit R) x); auto with algebra.
Qed.

Which I believe corresponds to the following statement in math-classes:

  Lemma module_absorbant_l `{Module R M} : forall x : M, sm Rzero x = Munit.

However, I'm not sure how to go about providing a proof for this statement (especially without an auto with algebra analogue). Can you give me some pointers on proving such basic theorems?

[spitters]

Corn is geared towards analysis, especially computable analysis. Analysis needs algebra of course, so we have quite an extensive algebra library. However, if it is just linear algebra you are interested in, perhaps have a look at math-components.

Having said that, did you have a look at the corresponding theorems for rings? Where do you get stuck?

[langston-barrett]

Well, one possible first step in this proof is the assertion that sm 0 x = sm (0 + 0) x. I've tried everything in the comments:

(* 0x = (0+0)x *)
Lemma H1 `{Module R M} : forall x : M, sm 0 x = sm (0 + 0) x.
  intros.
  (* rewrite monoid_left_id *).
  (* rewrite plus_0_r. *)
  (* rewrite plus_0_l. *)
  (* rewrite (monoid_left_id (Aop := Rplus) (Aunit := 0)). *)

Sorry if this is a basic problem, I'm very new to coq 😄

edit: I've gotten a little further, but I'm still struggling:

(* 0x = (0+0)x *)
Lemma H1 `{Module R M} : forall x : M, sm 0 x = sm (0 + 0) x.
  intros.
  assert (H0 : Rzero = 0 + 0).
  {
    rewrite plus_0_r.
    reflexivity.
  }
  rewrite H0. (* this step fails with a crazy error *)

error (truncated):

Error:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X307==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H x H0
          |- relation R] (internal placeholder) {?r}
 ?X308==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H x H0
          (do_subrelation:=do_subrelation)
          |- Proper

As another intermediary step, I tried proving the following lemma, only to encounter another such error message. It seems rewriting generally results in this sort of error.

Lemma lemma4 `{Module R M} : forall (x y : R) (z : M), x = y -> sm x z = sm y z.
  intros.
  rewrite H0. (* this step fails *)

[aa755]

Surprisingly, the Class Module does not require scalar multiplication to respect the equivalence in the type R. rewrite works after adding that assumption. Note that in MathClasses, = does not denote the syntactic equality relation (Coq.Init.Logic.eq), and can be an arbitrary equivalence relation. Chapter 3 of the following tutorial may help in understanding why the additional assumption was needed: http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf

Require Import Coq.Classes.Morphisms.
Open Scope signature_scope.
Lemma H1 `{Module R M} 
  {h: Proper (equiv ==> equiv  ==> equiv) sm}: forall x : M, sm 0 x = sm (0 + 0) x.
  intros. 
  rewrite plus_0_l.
  reflexivity.
Qed.

[langston-barrett]

@aa755 Thanks for the pointer to that tutorial, looks like it will be very useful!

Is this a bug in math-classes? It doesn't match my intuition (or my linear algebra textbook - Lay - which gives that lemma 😄).

[langston-barrett]

@aa755 A quick question about syntax: is it possible to include that hypothesis e.g. at the beginning of a Section?

I've tried

Section Module_Lemmas.
  Hypothesis sm_prop `{Module R M} : Proper (equiv ==> equiv ==> equiv) sm.

but I get a syntax error. The tutorial you linked me to seems to indicate that it might be possible to hypothesize an instance of a class (see Section TwoMonoids), but I tried the following only to be sent down the rabbit hole of hypothesizing the whole algebraic hierarchy:

Section Module_Lemmas.
  Variable M : Module.
  Hypothesis sm_prop : Proper (equiv ==> equiv ==> equiv) sm.

[spitters]

Yes, I think it's a bug (Thanks). If you send a pull-request, I'll merge it.

I think you want Context instead of Hypothesis.

[langston-barrett]

@spitters I'll send in a PR soon. Thank you so much for your help, everyone! The coq community is amazingly newcomer-friendly 😁 I hope to provide more valuable contributions as I become more proficient.

[langston-barrett]

PR is open in math-classes!