Zulip Chat Archive

Stream: lean4

Topic: Rewriting congruent relations

Sébastien Michelland (Oct 04 2022 at 15:18):

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 (Oct 04 2022 at 15:38):

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 (Oct 04 2022 at 16:24):

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 (Oct 04 2022 at 16:36):

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 (Oct 04 2022 at 16:40):

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 (Oct 04 2022 at 18:37):

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 (Oct 04 2022 at 19:46):

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 (Oct 04 2022 at 19:48):

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 (Oct 04 2022 at 21:13):

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 (Oct 05 2022 at 07:22):

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 (Oct 05 2022 at 07:24):

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

Sébastien Michelland (Oct 05 2022 at 07:26):

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 (Oct 05 2022 at 08:46):

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 (Oct 05 2022 at 09:10):

This seems to be the relevant paper.

Sébastien Michelland (Oct 06 2022 at 19:43):

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 (Oct 08 2022 at 14:24):

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 (Oct 08 2022 at 16:53):

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 (Oct 08 2022 at 18:12):

@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 (Oct 10 2022 at 11:38):

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 (Oct 10 2022 at 12:08):

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 (Oct 10 2022 at 12:10):

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

Sébastien Michelland (Oct 10 2022 at 12:38):

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 (Oct 10 2022 at 12:53):

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 (Oct 10 2022 at 14:32):

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 (Oct 10 2022 at 15:18):

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 (Oct 11 2022 at 15:19):

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 (Oct 11 2022 at 15:23):

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 (Oct 11 2022 at 15:59):

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

Jannis Limperg (Oct 11 2022 at 16:00):

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

Sebastian Ullrich (Oct 11 2022 at 16:11):

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 (Oct 15 2022 at 20:00):

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 (Oct 16 2022 at 05:21):

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 (Oct 16 2022 at 07:09):

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 (Oct 16 2022 at 07:18):

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 (Oct 16 2022 at 15:40):

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 (Oct 16 2022 at 15:42):

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 (Oct 16 2022 at 23:02):

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 (Oct 17 2022 at 17:41):

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 (Oct 17 2022 at 18:00):

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 (Oct 17 2022 at 19:20):

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 (Oct 18 2022 at 09:17):

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 (Oct 18 2022 at 09:41):

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

Jannis Limperg (Oct 18 2022 at 09:43):

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

Sébastien Michelland (Oct 18 2022 at 12:24):

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 (Oct 18 2022 at 15:46):

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 (Oct 18 2022 at 17:46):

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 (Oct 18 2022 at 17:50):

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 (Oct 18 2022 at 17:51):

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...

Max Nowak 🐉 (Nov 05 2024 at 23:30):

Has anyone picked this back up, or is there a similar project that was trying to accomplish this?

Jannis Limperg (Nov 05 2024 at 23:35):

I have a master student starting soon who's going to try to port the Coq approach.

Max Nowak 🐉 (Nov 05 2024 at 23:36):

Oh wow that is awesome!

Jannis Limperg (Nov 05 2024 at 23:39):

No promises, it's quite a big project. :sweat_smile:

Max Nowak 🐉 (Nov 05 2024 at 23:39):

Understandably so. I'd still be interested in intermediate and partial results!

Florian Würmseer (Jan 08 2025 at 12:16):

Hi, I'm "the" master student :P and I wanted to update you all. It took me some time to understand the paper. I used both Sébastien Michellands eautoimitation and aesop with a custom reduced ruleset to solve the constraints. I've also been testing rewrites in Arrows and Lambda types and noticed that even instances of a very simple arrow rewrite can be quite difficult to solve.

For instance:

example : ∀ P Q : Prop, (P ↔ Q) → (Q → P) ∧ (Q → P) := by
  intro P Q h
  grewrite [h]
  -- Expected updated goal: (Q → Q) ∧ (Q → Q)

results in 11 MVars in my implementation with the following path of the algorithm:

Algorithm trace

MVars (Lean)

This produces two Proper MVars exactly like Rocqs implementation does with the same example. However in my traces of the Rocq algorithm I see no Subrelation instances which blows up the problem in my Lean implementation. I may trace in the wrong place in Rocq but my current goal is to get the algorithm correct (replicate what Rocq does) for each rule before improving the performance on the proof search.

I also extended Sébastiens set of working examples by a bit.

Julien Marquet-Wagner (Jan 08 2025 at 13:14):

That's great news! I wish you luck on this project :) :rocket:

Would this approach be applicable to rewriting "indexed equalities" ?

inductive IdxEq
  {α : Sort u} {F : α → Sort v}
  : {a b : α} → F a → F b → Prop
where
| refl {a : α} (b : F a) : IdxEq b b

infix:50 " =* " => IdxEq

I guess this is equivalent to equality in Σ (a : α), F a, but it this formulation I'd expect the dependency to be problematic, as there are morally two levels, that of α and that of F which is "over α", whereas equivalence relations only appear "on one level".
Maybe in the space of possible generalizations of rewriting techniques, the direction of equivalence relations is orthogonal to the direction of indexed equalities? (If so, there should be an even more general problem for "indexed relations".)

The context is that such types appear when working with displayed categories and more generally with so-called "displayed algebras" (I believe this term was coined by András Kovács, it's very useful when tacking questions of representation of type theory within type theory).

Markus de Medeiros (Jan 08 2025 at 13:59):

Awesome! I'm glad someone is working on this :)

To throw another example at you, the "Proof" section of the README for iris-lean project describes some places where they want generalized rewriting. I could probably help come up with concrete examples, if you wanted to test your implementation.

Florian Würmseer (Jan 08 2025 at 18:59):

@Markus de Medeiros that would be great! Having more examples will definitely help me assert the performance and see what's possible. I don't have a strong intuition yet which Proper and respectful instances are required for the more complex structures. So I really appreciate your offer to find/extract "real world" examples from the iris port and their respective instances as a strong foundation for the algorithm and proof search.

This would also help me answer @Julien Marquet-Wagner s question and whether the instances work with the different levels and how the algorithm would behave.

Florian Würmseer (Jan 19 2025 at 09:49):

Hi, another update on my journey. I consulted the author Mattieu about the differences from the paper :tada: . He got back to me with some differences that are very crucial for the performance on nested cases:

Ok, I see what's happening I think. Taking the declarative system literaly produces a lot of constraints indeed. The implementation is based on section 2.3.2 and has a few refinements that might not be apparent in the paper. We treat application as binary somehow, so that when you rewrite with H : P <-> Q in Q -> P treated as impl Q P, the constraint is simply (Proper (iff => ?ev) (impl Q)) . I.e. if a rewrite does not apply in (impl Q) we do not decompose it. This is done by keeping a Success | Identity status for recursive calls to rewriting. To still be complete w.r.t. the declarative system, we add the partial instance that allows to create a relation evar ?ev8 for the argument Q and your Proper ?ev8 Q constraint. So this is done lazily during resolution, only if needed. Another aspect is that by default we do not allow rewriting on morphisms (only setoid_rewrite activates that, not rewrite IIRC), so we do not generate the Proper _ and and Proper _ impl and associated subrelation constraints but rather directly a Proper (?ev10 => ev0) (and Q). Finally for subrelation, we also apply it lazily: when going top-down in the term, we propagate the expected relation for the rewrite of a given subterm (generating evars when we can't know it). If a rewrite happens with a concrete relation (typically the atom case), and it's not equal to the constraint, we insert a subrelation coercion, otherwise we don't. Again to keep completeness we have a somewhat tricky typeclass instance proper_subrelation that allows to apply at the root of a Proper constraint the proper_subrelation instance, but only once to avoid loops. This is the purpose of the do_subrelation hypotheses: they are consumed by the tactic that applies proper_subrelation so that it applies only once per constraint. Hope this helps!

Since the actual Coq implementation includes lot's of technicalities that would be different in Lean's meta programming I'll try to find the bridge between the actual Coq implementation and the above named changes to the algorithm in the paper. And importantly get a better intuition for the Proper and respectful definitions as core for arbitrary rewrites. Also Jannis and Henrik suggested that the setoid_rewrite approach in Coq may not be relevant for Lean due to the Quotient type utilities.

Sébastien Michelland (Jan 19 2025 at 09:54):

I'm glad to see this being picked up again! I haven't looked at it since starting my PhD in a different sub-field but I had a lot of fun trying it at first. @Florian Würmseer I hope it's the same for you too!

The constraints you have in the basic arrow example seem "correct" with respect to my implementation which was very naive following the paper. Matthieu's explanations match my moral understanding of what the tactic wants to do, and I think the not decomposing apps where no rewrite happens is something I considered. The rest of the technical details are beyond what I knew at the time I made my attempt, so you're already headed beyond the basics I setup.

Looking back, I would have thought that matching the constraint set of the Rocq implementation would be too optimistic due to implementation details, but now I'm not sure anymore. If you can match it at least on simple examples that'd be a fantastic way to validate.

Florian Würmseer (Jan 19 2025 at 10:02):

Thank you! You're right. Comparing the constraints in Coq may be feasible when starting with basic cases and progressing to nested cases following the ideas from the paper/implementation. And for the completeness of the above example here the constraints I log in Coq for that conjunction:

[my_rewrite_debug]
  [P Q H (do_subrelation:=Morphisms.do_subrelation) |-
    Morphisms.Proper (?r ==> ?r0 ==> Basics.flip Basics.impl) and]
    (internal placeholder).[P Q H (do_subrelation:=Morphisms.do_subrelation)
                             |-
                             Morphisms.Proper (iff ==> ?r0) (Basics.impl Q)]
                             (internal placeholder).
  [P Q H |- relation Prop] (internal placeholder).
  [P Q H (do_subrelation:=Morphisms.do_subrelation) |-
    Morphisms.Proper (iff ==> ?r) (Basics.impl Q)] (internal placeholder).
  [P Q H |- relation Prop] (internal placeholder).

Florian Würmseer (Jan 24 2025 at 08:58):

Hi, I was able to recreate a part of the constraint generation algorithm in Coq and wrote a bunch of tests to check whether Coqs constraints equal mine. However, there is one thing I still don't understand considering the second part of Matthieus message above. @Sébastien Michelland or someone else on this thread may have an idea considering the constraints here. Let's say for a problem:

example : ∀ P Q : Prop, (P ↔ Q) → Q ∧ (P → Q) := by
  intros P Q H
  grewrite [H]

I get constraints like:

P Q : Prop
H : P ↔ Q
⊢ Proper (?m.41534 ⟹ flip impl) (And Q) -- ?m.41534 : relation Prop
P Q : Prop
H : P ↔ Q
⊢ ProperProxy ?m.41536 Q -- ?m.41536 : relation Prop
P Q : Prop
H : P ↔ Q
⊢ Proper (Iff ⟹ ?m.41536 ⟹ ?m.41534) impl

Now eventually I want to end up with something Subrel ?x (flip impl) or impl respectively to get an implication (Q /\ (P -> Q)) <- (Q /\ (Q -> Q) assuming we want to rw in the goal. Looking at Matthieus answer I still don't understand where I would place Subrels here and what the Subrel args would be. For reference, Coqs constraints look like this:

  [P Q H (do_subrelation:=Morphisms.do_subrelation) |-
    Morphisms.Proper (?r ==> Basics.flip Basics.impl) (and Q)]
    (internal placeholder).[P Q H |- Morphisms.ProperProxy ?r0 Q]
                             (internal placeholder).
  [P Q H (do_subrelation:=Morphisms.do_subrelation) |-
    Morphisms.Proper (Basics.iff ==> ?r0 ==> ?r) Basics.impl] (internal placeholder).
  [P Q H |- relation Prop] (internal placeholder).
  [P Q H |- relation Prop] (internal placeholder).

I'm still looking for an answer to what those do_subrelation:=Morphism.do_relation mean in Coq and what kind of Subrel chain I need in general for the modified algorithm.

Sébastien Michelland (Jan 24 2025 at 11:18):

@Florian Würmseer As far as I can tell (not 100% sure!), the (do_subrelation:=Morphism.do_subrelation) in the context part of the goal just indicates a let-binding which then happens to be unused. I suspect there is no subrelation in the constraint set generated by Rocq in this case. If there were one it should almost certainly appear in the RHS of a judgment.

Florian Würmseer (Feb 07 2025 at 12:02):

Another update. I was able to implement the Coq algorithm for constraint generation in Lean and wrote a couple more tests where I compared the proofs, constraints, and types of a rewrite with Coq. My current focus for the thesis is to show that the two algorithms (the paper one and the one implemented in Coq) always lead to the same rewrite proofs. I'm also optimizing Sébastien's EAuto for the new constraints. @Sébastien Michelland I'm a bit puzzled by how the ProperProxy TC in coq leads to a performance gain. I see that ProperProxy implements some different TC instances than Proper but I don't see how that speeds up the proof search. Do you recall what's so special about ProperProxy? I saw you left a TODO or comment about that in your code.
The Coq algorithm examines apps not just by the topmost binary app but unrolls them for some optimized Proper - respectful constraints. A rewrite on x with r x x' in f x y z x for instance will treat y and z as id (no unification) and generate something like Proper (r ==> ?y ==> ?z ==> r ==> (<-)) f with two ProperProxy instances for ?y and ?z: ProperProxy ?y y, ProxerProxy ?z z. I don't see how that is better than using Proper in this case. Do you have an intuition for this?

Florian Würmseer (Feb 07 2025 at 12:29):

PS: the proof for this rw (f x y z x) <- (f x' y z x') is: Proper.proper x x' h y y ProperProxy.proxy z z ProperProxy.proxy x x' h with h : r x x'

Sébastien Michelland (Feb 08 2025 at 10:39):

@Florian Würmseer For the proxy part, you can find some info in the code: https://coq.inria.fr/doc/V8.20.0/stdlib/Coq.Classes.Morphisms.html

From my understanding the idea is that ProperProxyhas hints with well-chosen priorities, so that instance search for ProperProxy first attempts basic matches like equality and iff before it goes into Proper, and might not do so if the target is left as an evar. The point is that the "other" instances are defined outside the generalized rewriting code and would not behave well either priority-wise or by enumerating too many options for the evars, leading to long searches.

As far as I'm aware the satisfiability of ProperProxy is equivalent to that of Proper (or at least when you have a non-evar relation)

Last updated: May 02 2025 at 03:31 UTC