Unification does not backtrack

Stream: mathlib4

[Gareth Ma]

Is this a known issue? Is this even an issue/bug?

import Mathlib.Data.Set.Defs
import Mathlib.Order.Notation

example {X : Type*} {f g : Set X → Prop} {a : Set X}
    (h : aᶜᶜ = a) (h' : f aᶜᶜ ↔ g aᶜ) : f a ↔ g aᶜ :=
  -- this fails: h ▸ h'
  (congrArg f h).symm.to_iff.trans h'

[Gareth Ma]

It seems the unification for \t does not backtrack when it fails... or something

[Gareth Ma]

Also, are there set_option trace options to debug unification? I can't seem to find it

[Gareth Ma]

Eq.subst h h' (motive := fun x ↦ f x ↔ g aᶜ)

this works

[Gareth Ma]

example {X : Type} {f g : X → Prop} {c : X → X} {a : X}
    (h : c (c a) = a) (h' : f (c (c a)) ↔ g (c a)) : f a ↔ g (c a) :=
  h ▸ h'

Doesn't depend on Mathlib version

[AG]

Gareth Ma said:

Also, are there set_option trace options to debug unification? I can't seem to find it

Try this! set_option trace.Meta.isDefEq true

[Kyle Miller]

h ▸ e is complicated by the way. It's sort of like by have e' := e; first | rw [h]; exact e | rw [<- h]; exact e | rw [h] at e'; exact e' | rw [<- h] at e'; exact e', though I don't know the exact order of what it tries.

[Joachim Breitner]

It first tries to rewrite the expected type, and only if it can’t rewrite there, tries other things.

[Gareth Ma]

I doubt it does rw [h] first, since if it does then it would have succeeded, right?

[Gareth Ma]

example {X : Type*} {f g : Set X → Prop} {a : Set X}
    (h : aᶜᶜ = a) (h' : f aᶜᶜ ↔ g aᶜ) : f a ↔ g aᶜ := by
  rw [h] at h'
  exact h'

This works (obviously?)

[Gareth Ma]

AG said:

set_option trace.Meta.isDefEq true

Okay it's weird, since the first line of the trace is

[Meta.isDefEq] ✅ f a ↔ g aᶜ =?= f a ↔ g aᶜ

Shouldn't it just end there?

[Kyle Miller]

Looking at trace.Meta.isDefEq is not the full story. The \t operator is not handled by unification. It has a whole elaborator implementing it (see docs#Lean.Elab.Term.elabSubst)

[Kyle Miller]

The source code does show that it tries rewriting the expected type first (and Joachim would likely know, I think he was the last to touch this elaborator)

[Kyle Miller]

Though maybe it's doing rw [<- h] first? That would explain the failure, since then the expected type would be f aᶜᶜ ↔ g aᶜᶜᶜ

[Gareth Ma]

Even if so, if that fails it should fall back to the other cases right? I will try my best to have a look when I get back

[Kyle Miller]

I just checked what the exact error message was in your example. That shows

type mismatch
  h'
has type
  f aᶜᶜ ↔ g aᶜ : Prop
but is expected to have type
  f aᶜᶜ ↔ g aᶜᶜᶜ : Prop

which is consistent with it doing rw [<- h] first and committing to it.

[Kyle Miller]

@Joachim Breitner Maybe subst notation should be implemented using backtracking, rather than committing to a particular rewrite?

[Gareth Ma]

Kyle Miller said:

I just checked what the exact error message was in your example. That shows

type mismatch
  h'
has type
  f aᶜᶜ ↔ g aᶜ : Prop
but is expected to have type
  f aᶜᶜ ↔ g aᶜᶜᶜ : Prop

which is consistent with it doing rw [<- h] first and committing to it.

Hmm but h.symm ▸ h' still doesn't work

[Kyle Miller]

That's weird.

At least if you make the expected type inaccessible it works:

example {X : Type*} {f g : Set X → Prop} {a : Set X}
    (h : aᶜᶜ = a) (h' : f aᶜᶜ ↔ g aᶜ) : f a ↔ g aᶜ :=
  (h ▸ h' :)

[Joachim Breitner]

Kyle Miller said:

Joachim Breitner Maybe subst notation should be implemented using backtracking, rather than committing to a particular rewrite?

If you ask me it should be implemented simpler, not trickier :-). It is too innocently looking for such a complicated notation.

It does backtrack, so to say, if rw [ <- h] in the expected type doesn't work, it tries something else. But it doesn't backtrack other later failures. I'm wairy of such backtracking, can't it lead to even harder to understand effects at a distance? You make a change somewhere and suddenly the notation rewrites the other direction?

[Kyle Miller]

Right now it's basically

by
  first
    | first | rw [h] | rw [<- h]
      exact e
    | have e' := e
      first | rw [h] at e' | rw [<- h] at e'
      exact e'

and my backtracking question is whether it should be

by
  have e' := e
  first
    | rw [h]; exact e
    | rw [<- h]; exact e
    | rw [h] at e'; exact e'
    | rw [<- h] at e'; exact e'

[Joachim Breitner]

Hmm, I don’t have opinions either way here.