discussion of modularity mechanisms

[andres-erbsen]

Here is some lore about abstraction and modularity mechanisms in Coq and Lean which I think may be relevant for setting conventions for stdlib2:

• example of where module functors are not good for defining the algebraic hierarchy: the final theorem of a development quantifies over n and talks about the ring of integers mod n, instantiating a library of lemmas about arbitrary rings with that n. If that library is implemented as a module functor, the top-level theorem of the development would also need to be a module functor. Then every other development would need to be defined using functors when calling that theorem with arguments that in turn depend on universally quantified variables. I hear people find this very inconvenient, and there is also the current limitation that a module functor cannot be instantiated by an Ltac script.

• https://github.com/leanprover/lean/wiki/Refactoring-structures highlights downsides of "bundled" and "unbundled" patters of using typeclasses as modules:

generally, it is relevant in any domain where we have transformations, an identity transformation, a composition operator, and an inverse. It feels weird to tell users that whenever they have a group in their application, they MUST use the constants mul or add. Otherwise, the automation will not work. The list.append and list.nil example emphasizes this issue. It is a monoid, a left_cancel_semigroup, and a right_cancel_semigroup. We want users to be able to use the algebraic normalizer without forcing them to use add for list.append and zero for list.nil.

The unbundled approach doesn't work with the simplifier as is. The problem is that the lemmas are hard to index. For example: the left hand side of the assoc lemma is (?op (?op ?a ?b) ?c)
where ?op, ?a, ?b and ?c are metavariables (aka matching variables). We don't have a single constant that we can use to filter the locations where this lemma can be applied.

mit-plv/fiat-crypto#233 and the RecordImport feature request coq/coq#7808 are my half-baked attempt of working around this dilemma...
For an example of emulating this using current Coq features, see mit-plv/bedrock2#14 (later discussion on that issue comes back to other modularity mechanisms which may be also relevant).

Note that the question of modularity interacts with what kind of unification is expected of tactics. For example, if it is expected that code will contain both @ring_add Zring and Z.add, we will likely want tactics to treat them interchangably, and for performance reasons this will likely need to use some restricted form of unification ("alias unification" using Tarjan's algorithm).

[andres-erbsen]

@gares #14 (comment) how do canonical structures solve these issues? For example, would a well-written tactic that works on semirings defined using canonical structures work on a goal that uses nat or Z, in a syntactic form such that the statement of that goal does not Require the definition of rings? As you say, TC and CS seem equivalent in many ways, so my guess would be that CS have the same issues as TC.

I do not have an expedient proposal of what to do here -- if anything I was hoping that somebody would explain how the issues I have been running into are avoidable. The only way I see out of this morass is to avoid relying on unification hints altogether, and instead rely on non-automatic functor specialization and manual imports to bring appropariate names into scope. Doing this with the current namespace management features of coq is indeed overly painful, so any more easily applicable solution would be appreciated.

[SkySkimmer]

A couple examples to consider when looking at CS vs TC

Axiom nat_comm : forall a b, a + b = b + a. (* I can't be bothered adding a require for it *)

Module Canon.

  Structure Com := { car :> Type; op : car -> car -> car; com : forall a b, op a b = op b a }.
  Arguments op {_} _ _.

  Ltac use_comm := rewrite com.

  Canonical Structure nring := {| car := nat; op := plus; com := nat_comm |}.

  Lemma use : forall n, n + 0 = n.
  Proof.
    intros n.
    (* n + 0 = n *)
    use_comm.
    (* @op nring 0 n = n *)
    reflexivity.
  Qed.
  
End Canon.

Module Class.

  Class Op (A:Type) := op : A -> A -> A.
  Class Comm {A} (o:Op A) := com : forall a b : A, op a b = op b a.

  Ltac use_comm := rewrite com.

  Instance nop : Op nat := plus.
  Instance ncom : Comm plus := nat_comm.

  Lemma use : forall n, n + 0 = n.
  Proof.
    intros n.
    Fail use_comm. (* found no subterm matching "op ? ?" *)
    change (op n 0 = n). use_comm.
    reflexivity.
  Qed.
End Class.

CS do seem to have access to more information than TC. I'm not sure if it's fundamental or if it's a matter of ease of access such that some TC scheme could be made as expressive (the later case would be like bidirectional typechecking vs solving unification problems I think).

[gares]

SSR rewrite does matching up to CS value/projection equivalence, for example. The goal can talk about Z, while the lemma about addition of a commutative group, and things will match.

[spitters]

More experiments here:
https://github.com/coq/stdlib2/wiki/EqClass

[andres-erbsen]

Wow, it does look like canonical structures avoid the issues I brought up for typeclasses. Is there a way to trigger the same matching directly without calling rewrite (e.g. as a replacement ltac match .. with .. end)?

[gares]

No, but it can be surely added. The implementation of rewrite is not particularly efficient either, so having a good FO matching up-to CS projection-value algorithm would probably benefit everybody.

[gares]

Sorry, I was sleeping. The matching facility of ssr is exported to ltac, but is quite primitive.

From Coq Require Import ssrmatching ssreflect.

Structure Add A := { op : A -> A -> A }.
Canonical Add_nat : Add nat := {| op := plus |}.

Lemma foo a b : a + b = 0.
Proof.
ssrpattern (op _ _ _ _).

gives

1 subgoal
a, b : nat
______________________________________(1/1)
let selected := op nat Add_nat a b in selected = 0

and the ltac API very minimal (see https://github.com/coq/coq/blob/master/test-suite/ssr/pattern.v ).
Warning: ssrmatching and polymorphic universe are not exactly working well together (yet).