Rewriting congruent relations

Stream: lean4

[Sébastien Michelland]

A common pattern in Coq to rewrite over custom relations is to prove congruence for certain functions with the Proper typeclass, and then use rewrite to rewrite their arguments.

I've been digging around for a similar mechanism in Lean 4, but I couldn't come up with anything substantial. The notion of Setoid looks related but it only really works for equivalence relations. I saw that simp has a notion of "congruence lemmas" mentioned a few times in the code, but most of the info went back to Lean 3.

Is this kind of rewriting possible? If so how would one go about it?

[Jannis Limperg]

No, "generalised rewriting" is not implemented in Lean. You can sometimes achieve a similar effect by quotienting with an equivalence relation and then rewriting with propositional equality, but this is far from a full replacement.

Several people have expressed interest in this mechanism recently, but it's a significant amount of coding effort. More than one good master thesis, I would guesstimate.

[Sébastien Michelland]

I see. The project I'm working on only uses a few such relations, so I'm wondering whether a proof-of-concept for it could work out.

But I guess the hard part is handling all the context... and it can't be as simple as looking up a congruence proof for each function call on the way up.

[Jannis Limperg]

Conceptually, I don't think there's anything particularly difficult about it. If anyone wants to work on this, I'd be happy to help. A minimum viable version could be restricted to equivalence relations and respectful morphisms. Coq's design generalises in multiple directions, but these generalisations could be added later (and are more niche anyway).

[Sébastien Michelland]

Alright, maybe I can give this a try in a limited setting. I've worked on extensions to Coq's congruence tactic at some point so I should be able to make some basic cases work t least... the harder part for me is doing the Lean metaprogramming side I think.

[Andrés Goens]

That sounds pretty interesting, I'd be happy to help on the Lean metaprogramming side @Sébastien Michelland (and I've been wanting to test some of the rewrite stuff on that particular project anyway)

[Sébastien Michelland]

Jannis Limperg said:

A minimum viable version could be restricted to equivalence relations and respectful morphisms.

Quick note: equivalence relations are not closed under the respectful morphism construction so we actually have to start at PERs. It's mostly the same, fortunately.

[Sébastien Michelland]

Andrés Goens said:

That sounds pretty interesting, I'd be happy to help on the Lean metaprogramming side Sébastien Michelland (and I've been wanting to test some of the rewrite stuff on that particular project anyway)

Your help is more than welcome! Even on the theoretical side, where I have broad ideas about how to tackle the problem but no real expert knowledge to back it up.

[Sébastien Michelland]

I pushed some basic definitions along with a trivial example where the goal is only applications. This should at least show what general process I have in mind.

There are already difficult questions in terms of finding Proper instances. I'm not sure if I can make the typeclass engine find all solutions for a query. I'm tempted to just ask Proper ?R f for some function f at hand, and then check what ?Rs are found by making it an outParam. I'm not anticipating to have a large number of instances for a specific function, so it could work out for a start.

[Andrés Goens]

that's a cool start (makes it more concrete and easier to understand)! I'm a bit confused by the example though, you can't prove Rβ (fαβ a) x for that arbitrary x. Did you mean to prove Rβ (fαβ a) x ↔ Rβ (fαβ a') x, i.e. your h₂, where ideally the whole proof would go with a simple by [h]?

[Andrés Goens]

or I don't really understand the example :shrug: what is the idea behind it @Sébastien Michelland ?

[Sébastien Michelland]

Oh the goal is indeed not provable. I made it this way to avoid Lean proving it automatically with a hypothesis or something. The "demo" ends after the rewrite.

[Sébastien Michelland]

I added some tests handling subrelations, which is often necessary because non-rewritten arguments get an Eq in the respectful relation while in general Proper instances will be declared with more general types.

Unsurprisingly, encoding the subrelation rules in this naive way already blows up TC resolution, even without the transitivity rule for Subrel. I'm guessing the proper way to do this would be to solve with a specialized algorithm or to write the typeclasses in a smart way to avoid the engine branching so much. Any insight here?

[Jannis Limperg]

This seems to be the relevant paper.

[Sébastien Michelland]

Thanks for digging it up. I've started to look at it, and I'm hopeful I can grasp it well enough. Writing the Lean code is another matter, but I'm sure I can get plenty of help here. :)

Anyway, just to answer my previous question: handling subrelations is done in the main algorithm which is not typeclass driven; they eliminate it early to avoid searching and keep recursing on syntax (§2.3.2); and they assume the set of instances is transitive to never chain such rules. So that all checks out. I shall try and imitate that.

[Sébastien Michelland]

Quick update: I've started implementing the first algorithm which traverses the goal and generates a set of intermediate relations, Proper instances and subrelation instances as metavariables. This is going pretty well, although I'm not quite sure if and how the context gets updated during the monadic code compared to what the paper expects.

After that, it's all typeclass inference in the paper, but I don't know whether we can just solve a set of typeclass queries that share metavariables.

[Sébastien Michelland]

Reading the Coq source code, it also turns out that a fair amount of typeclass resolution is customized by using the fact that the typeclass resolution engine is a variant of eauto. By using hints that call into custom tactics, a number of instances are applied selectively and not put into the instance database, to avoid combinatorial explosions.

[Sébastien Michelland]

@Jannis Limperg I'm ending up with this kind of typeclass problem:

[Meta.Tactic.grewrite] Constraints to solve:
  ?m.455: relation (relation α)
  ?m.459: Proper ?m.455 Rα
  ?m.462: relation (α → Prop)
  ?m.478: Subrel ?m.455 (Rα ==> ?m.462)
  ?m.480: relation α
  ?m.484: Proper ?m.480 x
  ?m.486: relation Prop
  ?m.496: Subrel ?m.462 (?m.480 ==> ?m.486)
  ?m.508: Subrel ?m.486 (flip impl)

How can I solve/work towards solving this set of queries?

[Jannis Limperg]

I've never looked into typeclass resolution much, but I'm not aware of any use of typeclasses in Lean 4 where we synthesise a set of interdependent instances all at once. So this may be difficult. We could try to solve each constraint in turn (in some sensible order) with backtracking, but (a) Lean's typeclass inference does not assign metavariables (except those it generates itself) and (b) I don't think we can get typeclass inference to give us multiple possible solutions. I don't really have another idea at the moment, short of implementing a custom search algorithm for this sort of problem. @Anne Baanen, as our resident typeclass tsar, do you maybe have an idea? (This is Lean 4, but the fundamentals are hopefully similar enough.)

We definitely don't have support for extending typeclass inference with custom tactics, which, as you say, seems to be necessary to constrain the search. I've seen comments in the Lean 4 source code indicating that this feature is on the roadmap, but probably not any time soon.

[Sébastien Michelland]

So the part about extending typeclass search with tactics is probably fine - I can write custom tactics that call into the typeclass engine manually instead. For the instances that I've seen it almost feels straightforward.

For the set of instances, one approach maybe is to see that all the dependencies are on relations, so once these are chosen all of the instances can be solved for individually and in any order. I'm considering some kind of "informed bruteforcing" on that front, although I'm not quite sure how to discover the relations to use apart from enumerating Propers and Subrels - which, apparently, is not possible either. :thinking:

[Sebastian Ullrich]

Do you have an example where in-order, no-backtracking solving is not sufficient?

[Sébastien Michelland]

Yes. Consider a rewrite of Rα a a' into the goal Pα a : Prop. This gives you the following constraints:

[Meta.Tactic.grewrite] Constraints to solve:
  ?m.449: relation (α → Prop)
  ?m.453: Proper ?m.449 Pα
  ?m.455: relation Prop
  ?m.465: Subrel ?m.449 (Rα ==> ?m.455)
  ?m.477: Subrel ?m.455 (flip impl)

Commonly, you will do this when Pα is proper for Rα ==> iff, and thus you're aiming for:

  ?m.449 := Rα ==> iff
  ?m.453: Proper (Rα ==> iff) Pα -- the main instance at play
  ?m.455 := iff
  ?m.465: Subrel (Rα ==> iff) (Rα ==> iff) -- trivial
  ?m.477: Subrel iff (flip impl) -- standard

Now assume you solve in the listing order. There is a valid instance of ?m.453 in Proper Eq Pα, which will cause ?m.465 to fail because the respectful relation is not reflexive. You need to guess the correct relation ?m.449 for that to succeed. Not only do you have to solve both queries that involve ?m.449, but really the entire set because the first Subrel ties it to ?m.455, the other relation that you have to guess.

The core problem is that you need to guess a relation for every codomain of an application in the goal, so someone has to explore.

[Sebastian Ullrich]

I suppose it might be possible to combine all contraints into a single instance problem by basically building a tree instead of a set, but I'm not sure if typeclasses are really the best solution here in Lean

[Jannis Limperg]

Sébastien Michelland said:

So the part about extending typeclass search with tactics is probably fine - I can write custom tactics that call into the typeclass engine manually instead. For the instances that I've seen it almost feels straightforward.

Only if the custom logic is at the top level. If you need custom logic every time an instance is considered during typeclass search, this is not currently possible afaik. (I haven't looked at the paper carefully enough to see whether we need this.)

For the set of instances, one approach maybe is to see that all the dependencies are on relations, so once these are chosen all of the instances can be solved for individually and in any order. I'm considering some kind of "informed bruteforcing" on that front, although I'm not quite sure how to discover the relations to use apart from enumerating Propers and Subrels - which, apparently, is not possible either. :thinking:

I would frame it like this: discovering the relations by enumerating Propers and Subrels is exactly what Coq's typeclass inference does, using unification.

Maybe the solution really is to implement an approximation of typeclasses eauto. In principle, this should be no problem; we have nice backtrackable data structures. But I suspect the devil is very much in the details.

[Anne Baanen]

I agree with Jannis' assessment that this is going to be difficult with the standard synthesis algorithm. The only thing I can figure out right now is to bundle everything together into one huge class (with judicious use of out_params?) and hope this is expressive enough to capture what you're looking for. But indeed a custom synthesis algorithm seems more practical at this point.

[Sébastien Michelland]

Thanks for the input! After some consideration I shall try to write a custom algorithm. I'm afraid contorting the standard typeclass search for this would just result in a wild hack, and the generalized rewriting approach so far seems clean enough that I can imagine it being polished and merged in the future. I would like to keep it that way.

I pushed some outline, but essentially my idea is to make a naive imitation of eauto, in the sense that:

• It would solve multiple goals by trying different hints (let's say theorems/instances for now), recursively, with backtracking.
• It would unify metavariables and, if needed, allow introducing new ones as temporaries.

I believe I can make it work nicely by first focusing on getting instances from context (hypotheses) rather than typeclass search. This will both help me split debugging efforts, and act as a fallback to keep the tactic usable whenever the custom typeclass search inevitably fails to find relevant instances.

[Sébastien Michelland]

Some practical questions straight away:

• How can I obtain a goal with a metavariable in an interactive proof? For instance Proper ?R fαβ. I tried exists R, Proper R fαβ then refine ⟨?R, ?_⟩ but then the goal is just some ?m.806 ?R and it doesn't unify with eg. Proper (Rα ==> Rβ) fαβ. (Edit: the goal also no longer contains Proper. How does this work? Is ?m.806 delayed-assigned?)

• Attempting to unify instances with the goal will assign metavariables. How do I save/split the context so that I can roll back the assignment in case the current instance is not satisfactory?

[Jannis Limperg]

For the second question, look at this chapter of the metaprogramming book.

[Jannis Limperg]

Basically, you can use the MonadBacktrack interface to store the current MetavarContext and roll back to it.

[Sebastian Ullrich]

By the way, the current lack of generalized rewriting in Lean also was an issue for the Iris port, which Lars fixed via an ad-hoc implementation https://github.com/larsk21/iris-lean/blob/master/src/Iris/Std/Rewrite.lean. But crucially, there was no need for backtracking in this specific case.

[Sébastien Michelland]

Progress on this is coming along. With some help for Jannis, I now have a basic imitation of eauto that can close goals with backtracking:

example (P₁ P₂: α → Prop) (f: forall (a: α), P₁ a → P₂ a → β)
        (a: α) (ha₁: P₁ a)
        (a': α) (ha'₁: P₁ a') (ha'₂: P₂ a'): β := by
  eauto

The search for this one looks like this:

[Meta.Tactic.eauto] goal[0]: β ▼
  [hints] applying hypothesis: f: (a : α) → P₁ a → P₂ a → β
  [hints] subgoals: P₁ ?a, P₂ ?a, α
  [] goal[1]: P₁ ?a ▼
    [hints] applying hypothesis: ha₁: P₁ a
    [hints] subgoals:
    [] goal[1]: P₂ a ▼
      [] failed to close the goal
    [hints] applying hypothesis: ha'₁: P₁ a'
    [hints] subgoals:
    [] goal[1]: P₂ a' ▼
      [hints] applying hypothesis: ha'₂: P₂ a'
      [hints] subgoals:

[Meta.Tactic.eauto] final proof: f a' ha'₁ ha'₂

The fact that several goals of depth 1 are nested might look counter-intuitive, but since the witness for P₁ ?a unifies away ?a this also affects the other goal P₂ ?a, so the nesting is in fact correct.

This is all very basic but that should be enough resolution power to get started on the typeclass problems for generalized rewriting. Next is trying these problems with local hypotheses, then wiring up lower-level routines of the typeclass synthesizer to query instances that unify with the goal.

[Scott Morrison]

That sort of example is handled by solve_by_elim in mathlib3. I'm a bit confused as to why the minimal solve_by_elim in mathlib4 is failing on it, actually!

[Sébastien Michelland]

I haven't tried, because I didn't know about this tactic! Thanks for bringing it up. Considering it was not recommended to me before, I'm suspecting it would not be able to handle the other two aspects of Coq's typeclasses eauto that I want/need to approximate : (1) querying typeclasses without synthesizing instances, instead leaving them as subgoals (apply in Lean4 does not support it currently), and (2) external hints in the form of using custom tactics when certain types of goals appear.

[Scott Morrison]

It doesn't do (1), but the mathlib3 version does have a discharger option which will run a custom tactic on each subgoal.

[Sébastien Michelland]

I've made some good progress on this.

• I added a variant of apply that does not synthesize implicit instance arguments. It seems to me that it could be an option of the original apply, let me know if that's worth discussing. typeclasses_eauto uses it.
• This allowed me to start using normal instance declarations during the search (provided they're in context), and thus solve some basic generalized-rewriting queries.
• I added basic infrastructure to register hints, which should work across different files. Hint databases can be specified in the command, which allows me do to things like:

eauto_hint Subrel_respectful: test_eauto
eauto_hint Reflexive.refl: test_eauto
eauto_hint Reflexive_Subrel: test_eauto
eauto_hint Subrel_Iff_flip_impl: test_eauto

example {α β: Type _} {Rα: relation α} {Pα: α → Prop}
  (h₁: Proper (Rα ==> Iff) Pα)
  (goal: forall (R₁: relation (α → Prop)) (R₂: relation Prop),
     Proper R₁ Pα →
     Subrel R₁ (Rα ==> R₂) →
     Subrel R₂ (flip impl) → β): β := by
  typeclasses_eauto with test_eauto

which is an actual typeclass query for the simplest generalized rewriting instance.

[Sébastien Michelland]

I imagine that hints could be better integrated with the rest of Lean by using attributes. But there's still the question of extern hints that apply "tactic expressions" based on some pattern match. They didn't seem to fit, so I did the basic Coq imitation for now. Suggestions are welcome.

[Sébastien Michelland]

I got the simplest generalized rewrite to work! It looks underwhelming, but it was a long way in the making. :sweat_smile:

In the context, we have Pα: α → Prop which is Proper (Rα ==> Iff), allowing us to rewrite:

example (h: Rα a a') : Pα a := by
  grewrite h -- turns into Pα a'
  sorry

The full log is as follows. First, the generalized rewriting algorithm traverses the term to find occurrences and generate Proper and Subrel instances to apply along the way:

[Meta.Tactic.grewrite] skeleton: Pα a ▼
  [] type_f = α → Prop
  [] using rule: APP
  [] skeleton: Pα ▼
    [] using rule: ATOM
  [] skeleton: a ▼
    [] using rule: UNIFY

This generates a set of constraints involving intermediate relations that needs to be guessed (here ?m.438: relation (α → Prop) and ?m.457: relation Prop). The flip impl comes from the top-level, it is the relation that we can apply on the goal to make progress. (We could similarly rewrite on hypotheses by targeting impl).

[Meta.Tactic.grewrite] constraints to solve:
      Proper ?m.438 Pα
      Subrel ?m.438 (Rα ==> ?m.457)
      Subrel ?m.457 (flip impl)

Then the problem gets solved using typeclasses_eauto with grewrite. This runs the basic eauto imitation, with hints from the grewrite theorems (for all applicable theorems that are not typeclass instances), and also uses instances that the typeclass engine says unifies with the goal.

[Meta.Tactic.eauto] goal[0]: Proper ?m.438 Pα ▼
  [hints] applying hypothesis: Proper_Rα: Proper (Rα ==> Iff) Pα
  [] goal[0]: Subrel (Rα ==> Iff) (Rα ==> ?m.457) ▼
    [hints] [grewrite] applying hint: Reflexive.refl: ∀ {α : Type u_1} {R : relation α} [self : Reflexive R] (x : α), R x x
    [hints] subgoals: Reflexive Subrel
    [] goal[1]: Reflexive Subrel ▼
      [hints] applying instance: @Equiv.toReflexive: {α : Type u_1} → {R : relation α} → [self : Equiv R] → Reflexive R
      [hints] subgoals: Equiv Subrel
      [] goal[2]: Equiv Subrel ▼
        [] failed to close the goal
      [hints] applying instance: @Reflexive_Subrel: {α : Type u_1} → Reflexive Subrel
      [] goal[0]: Subrel Iff (flip impl) ▼
        [hints] applying instance: Subrel_Iff_flip_impl: Subrel Iff (flip impl)

Note how we apply hypotheses (Proper_Rα), database hints (Reflexive.refl), and instances from the typeclass engine (@Reflexive_Subrel) all for this problem. There is also a bit of backtracking because the first instance we get is a false lead.

There's still a bunch of bugs and none of the other tests work yet, but I'm happy with this first result. :smiley:

[Sébastien Michelland]

I fixed a couple of bugs this morning, then followed up with performance tweaks which mean that we have reasonable examples starting to work now!

For instance, assuming we have f: α → β which is Proper (Rα ==> Rβ) where Rβ is a PER, then we can rewrite this goal:

example (h: Rα a a') (finish: Rβ (fαβ a') x): Rβ (fαβ a) x := by
  grewrite h
  exact finish

The set of instances and hints behind the constraint solving is still very unpolished, but the infrastructure is clearly getting there!

[Jannis Limperg]

As you scale up to bigger hint databases, probably the biggest performance improvement will be to put the hints in a DiscrTree. However, this also means that hints will be applied with reducible rather than default transparency (which is probably fine, but is an observable change).

[Sébastien Michelland]

So far I've only been looking at the search tree, and for that I think the lowest-hanging fruit is avoiding super-general instances and prioritizing hints properly.

But I do have some concerns about the pattern of commitIfNoEx followed by applying a hypothesis which doesn't unify, then a rollback. In my examples I have ~15 elements in my local context + hint databases, so that's basically 15 rollbacks for every goal and subgoal, which surely can't be ideal. I considered doing that only for hints that unify, but unification already has side effects so it doesn't work; I guess that's why Coq's version is also based on the root symbol.

So maybe DiscrTree is gonna help with that! I had no idea where to go for such a structure but it seems to be mostly cooked already so that's cool.

[Jannis Limperg]

Yes, DiscrTree is precisely the data structure you need. It's essentially an expression trie which enables efficient lookup of expressions that may unify with the goal, up to reducible transparency. Afaict from the docs, Coq uses the same approach when you create your hint database with the discriminated option, which would be the default if not for compatibility concerns. Lean 4 also uses DiscrTrees for simp lemmas and typeclasses.

[Jannis Limperg]

Btw, I just came across docs4#Lean.sanitizeName, which you could use to prettify the tracing of local hints.

[Jannis Limperg]

Ah never mind, this function is for making hygienic names, not for displaying them.

[Sébastien Michelland]

Thanks, I can look at that in the future. For now, I'm trying to implement occurrence selection (which essentially already works) and scaling things up.

One problem I'm having is that the backtracking code catches all exceptions, and I failed to realize that I was hitting the heartbeat limit on some uncontrolled instance searches. I already have an easily-catchable internal exception for eauto failures, but there are also exceptions in apply that I don't control. So far I "fixed" the problem by pre-testing unification to throw my internal exception instead of just a message, and thus every message exception is bubbled back to the top-level. Is there a better way of achieving that?

[Jannis Limperg]

I don't see a good solution. Maybe the redundant isDefEq is least bad, though it's obviously not ideal.

Does anyone else have opinions on this? (Tl;dr of the question: how do we distinguish whether an apply call failed because the types do not unify or because of a fatal error, e.g. hitting the heartbeat limit?) Now that I think about it, I'm sure I have similar problems in Aesop.

[Sébastien Michelland]

I'll stick to that for now, as in the worst case I can always internalize apply - it would just be some 40 more lines of code since I already have a variation of it.

[Sébastien Michelland]

Following deeper reflections on constraint ordering I realized the natural order was best if arguments are solved before functions. This allowed me to scale my occurrence selection, and now under Proper (Rα ==> Prop) Pα we have:

example (h: Rα a a') (finish: Pα a'): Pα a ∧ Pα a ∧ Pα a ∧ Pα a ∧ Pα a ∧ Pα a := by
  have h₁: Proper (Iff ==> Iff ==> Iff) And := ⟨fun _ _ hx _ _ hy => by simp [hx, hy]⟩
  have h₂: Proper (Eq ==> Eq) Pα := ⟨fun _ _ hx => by simp [hx]⟩
  grewrite h at 5 -- Pα a  ∧ Pα a  ∧ Pα a  ∧ Pα a  ∧ Pα a' ∧ Pα a
  grewrite h at 5 -- Pα a  ∧ Pα a  ∧ Pα a  ∧ Pα a  ∧ Pα a' ∧ Pα a'
  grewrite h at 1 -- Pα a' ∧ Pα a  ∧ Pα a  ∧ Pα a  ∧ Pα a' ∧ Pα a'
  grewrite h at 3 -- Pα a' ∧ Pα a  ∧ Pα a  ∧ Pα a' ∧ Pα a' ∧ Pα a'
  grewrite h at 1 -- Pα a' ∧ Pα a' ∧ Pα a  ∧ Pα a' ∧ Pα a' ∧ Pα a'
  grewrite h at 1 -- Pα a' ∧ Pα a' ∧ Pα a' ∧ Pα a' ∧ Pα a' ∧ Pα a'
  repeat (constructor; assumption)
  assumption

For the extra have: the instance of And is just not registered yet, and I'm lacking properties on extensional equality so I had to provide that Proper (Eq ==> Eq) which is always true. Using have is always a safety as well as an option to guide the search since it tries local declarations early.

[Sébastien Michelland]

I'm slowly running out of time to spend on this, so I'll be trying to wrap up and polish these basic use cases, with documentation and everything. Hopefully this can be expanded on in the future...