[math-classes] Some proofs are notation-dependent

[langston-barrett]

I recently encountered an issue on the following lemma:

  Lemma mult_munit : forall c : R, sm c mon_unit = mon_unit.
    intro c.
    rewrite <- right_identity.
    assert (intermediate : mon_unit = c · mon_unit & - (c · mon_unit)) by
      now rewrite right_inverse.
    rewrite intermediate at 2.
    rewrite associativity.
    rewrite <- distribute_l.
    rewrite right_identity. (* evaluation would stop here *)
    apply right_inverse.
  Qed.

I found that if I changed the instance of Proper for scalar multiplication to use the dot (·) notation and the statement of the lemma to the following, this proof worked exactly as expected:

  Lemma mult_munit : forall c : R, c · mon_unit = mon_unit.

I encountered a similar error with this lemma:

(* Subspaces are specified as a constraint on a vectorspace *)
Class Subspace (K V : Type) 
   {Ke Kplus Kmult Kzero Kone Knegate Krecip} (* scalar operations *)
   {Ve Vop Vunit Vnegate}                     (* vector operations *)
   {sm : ScalarMult K V}
 :=
   { subspace_vectorspace  :>> @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate Krecip
                                            Ve Vop Vunit Vnegate sm
   ; constraint : V -> Prop
   ; closed_under_sg_op    : forall u v, constraint u -> constraint v ->
                           constraint (u & v)
   ; closed_under_sm       : forall c v, constraint v -> constraint sm c v
   (* We don't include that the zero vector is in the subspace, it follows
      from the closure under scalar multiplication.
    *)
   }.

Section Subspace_Lemmas.
  Context `{VectorSpace K V}.

  Definition zero_prop (vec : V) : Prop := vec = mon_unit.

  Instance zero_subspace : Subspace K V.
  Proof.
    split with (constraint := zero_prop); eauto; intros; unfold zero_prop in * |- *.
    { (* Closure under & *)
      rewrite H0, H1.
      now rewrite left_identity.
    }
    { (* Closure under sm *)
      rewrite H0. (* This step would fail with UNDEFINED_EVARS *)
    }
  Qed.
End Subspace_Lemmas.

But if I changed the closure condition to use the dot notation, everything proceeded just fine.

   ; closed_under_sm       : forall c v, constraint v -> constraint (c · v)

My expectation would be that the notation should be irrelevant in proofs. Is there a good reason that it is not? Is this a bug, or are my expectations not in line with typeclass functionality?

For a little more context, see my question on StackOverflow.

[aa755]

Notation are indeed irrelevant for Coq's logic and tactic machinery. Coq's first step is to turn notations into actual objects. You can see those actual objects by doing "Set Printing All." (or View -> Display all low level content in CoqIDE). In particular c . v is parsed (@scalar_mult K V sm c v). So, the real problem that you are witnessing is that Coq's typeclass-inference/unification behaves differently when using (@scalar_mult K V sm c v) vs sm c v, even though the former computes to the latter. I think that for efficiency, typeclass-inference/unification is not designed to fully explore those computational equivalences (aka definitional equalities).

By consistently using only (.) everywhere, you are reducing the need for Coq's inference mechanism to compute to be able to unify things. Nevertheless, there will be cases where despite all those tricks, the inference mechanism will fail. However, when apply/rewrite fails, you can help typeclass inference by manually providing some of the typeclass instances. If you read all of [1], you will see that typeclass instances are just implicit arguments that you can manually provide. For example, you can do rewrite (@closed_under_sm _ _ _ _ _ _ _ xxx). To see the types of xxx and the dashes, do Check @closed_under_sm.

[1] : http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf

[langston-barrett]

@aa755 I have read the tutorial, it's very good 😄 I guess I was just confused about the fact that/why the unifier wouldn't explore all definitional equalities. Thanks for clarifying!