Bizarre `simp` error

Stream: lean4

[Artie Khovanov]

Reduced to this Mathlib-free version:

structure Struct (n : Nat) : Prop where

def Struct.data {n} (s : Struct n) : Nat := n

variable (m : Nat)

structure Extend m extends Struct m

@[simp]
theorem fact (h : Extend m) : h.data = m := rfl

set_option pp.all true in
set_option trace.Meta.Tactic.simp true in
example (h : Extend m) : h.data = m := by simp only [fact]
/-
[Meta.Tactic.simp.discharge] fact discharge ❌️
      Extend m
[Meta.Tactic.simp.unify] eq_self.{u_1}:1000, failed to unify
      @Eq.{?u.151} ?α ?a ?a
    with
      @Eq.{1} Nat (@Struct.data m (@Extend.toStruct m h)) m
-/

[Artie Khovanov]

I don't understand why simp can't prove the example

[Henrik Böving]

I would expect because simp doesn't fill in propositional arguments on its own in this situation so you need to do simp only [fact, h].

[Artie Khovanov]

hm, that's frustrating
I lifted (what I've reduced to) Struct to Prop to avoid DTT hell, but apparently that breaks simp!
I understand why it doesn't fill in Prop-valued hypotheses, but why can't it fill in Prop-valued holes in the LHS it's matching on?

[Henrik Böving]

I'm not quite sure, I believeisDefEq should assign the mvar that h becomes on the left but it does not AFAICT. For some reason this defeq query:

 @Struct.data ?m (@Extend.toStruct ?m ?h) =?= @Struct.data m (@Extend.toStruct m h)

only assigns ?m and not ?h.

[Henrik Böving]

I think it is at least worth opening an issue in core over, make sure to point out the defeq issue, that is the reason it doesn't work.

[Aaron Liu]

Is it because Extend.toStruct is a theorem

[Henrik Böving]

Ah that would make sense yes, but it still feels to me like the simp part should morally work.

[Artie Khovanov]

I don't really understand the issue still. Does it only break for structure extensions, or for anything of this form?

[Artie Khovanov]

OK it breaks for anything. Reduced it further:

def p1 : Prop := sorry

def p2 : Prop := sorry

theorem imp : p2 → p1 := sorry

def data (h : p1) := 0

@[simp]
theorem fact (h : p2) : data (imp h) = 0 := rfl

set_option pp.all true in
set_option trace.Meta.Tactic.simp true in
example (h : p2) : data (imp h) = 0 := by simp only [fact]
/-
[Meta.Tactic.simp.discharge] fact discharge ❌️
      p2
[Meta.Tactic.simp.unify] eq_self.{u_1}:1000, failed to unify
      @Eq.{?u.116} ?α ?a ?a
    with
      @Eq.{1} Nat (data (imp h)) (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))
-/

[Artie Khovanov]

I don't understand what you mean by IsDefEq being an issue. Does that appear somewhere in some trace I can print?

[Henrik Böving]

You can inspect the defeq trace with trace.Meta.isDefEq. When simp's term index suggests a theorem to try [ in this case fact] simp will take the LHS of that theorem with all of its parameters replaced with meta variables. It then uses isDefEq to unify the theorem pattern with the term it is trying to rewrite. During this unfication process it only assigns ?m but not ?h. This in turn causes the h hypothesis to remain open which is why simp wants it to be filled by additional reasoning.

[Artie Khovanov]

Thanks! But I can't seem to find this in the IsDefEq trace.

[Henrik Böving]

Henrik Böving said:

I'm not quite sure, I believeisDefEq should assign the mvar that h becomes on the left but it does not AFAICT. For some reason this defeq query:

 @Struct.data ?m (@Extend.toStruct ?m ?h) =?= @Struct.data m (@Extend.toStruct m h)

only assigns ?m and not ?h.

This query from above is from the defeq trace

[Henrik Böving]

image.png

[Artie Khovanov]

Oh OK!
In my simplified version I see
[Meta.isDefEq] ✅️ data (imp ?h) =?= data (imp h)
with no dropdown

[Henrik Böving]

Yeah because no meta variable is being assigned

[Artie Khovanov]

I'm really sorry I think this is a bit beyond me. I understood that line as saying ?h is being assigned to h?

[Henrik Böving]

No, that line is asking the unification problem

data (imp ?h) =?= data (imp h)

the unifier (isDefEq) can then attempt to use a first order heuristic whereby if you have a problem of the shape

f x =?= g y

and f =?= g and x =?= y it's solved (if this fails it would try a bit harder with higher order approaches). So in this situation it identifies okay data =?= data and then it ries to solve (imp ?h) =?= (imp h).

Now the way that defeq presumably solves this problem is that because imp h is a proof, it is guaranteed to be equal to any other proof of the same fact. So defeq can conclude without traversing into the terms further that they are equal (after all they have the same type) and close the problem.

Because of this behavior the meta variable ?h does not end up getting assigned (the unifier never even sees it). Not traversing into proof terms is an (important) performance optimization that should certainly remain active in the general case. Regardless I still think it makes sense to at least keep this issue in our issue tracker in case someone finds a nice solution or even just to make it easier for other users to discover what is going wrong.

[Artie Khovanov]

Right I see. I will confess I'm not really sure what exactly to say in the issue so I will leave that to others if they would like to. But this seems like something that isn't changing anytime soon?

[Artie Khovanov]

Thanks for your patience with the explanations!

[Henrik Böving]

But this seems like something that isn't changing anytime soon?

Yes

[Artie Khovanov]

I suppose this is actually really easy to work around. By proof irrelevance, any proof of (h : p2) → data (imp h) = 0 is a proof of (h' : p1) → data h' = 0.

[Artie Khovanov]

So really it's a question of me writing a not-general-enough simp lemma.

[Henrik Böving]

That's true yes, it would still be nice if we could make it work or at least have simp throw an error when you mark the theorem.

[Kyle Miller]

Yeah, please create an issue — it might be worth special casing projections.

If writing a more general simp lemma works for you, then great.

Other workarounds:

1. You might also consider using a Type-valued structure anyway and relying on eta-for-structures, which should reduce DTT issues (structures with only proof fields should be defeq, even if the structure is in Type).
2. You might have the same field re-defined on substructures, to avoid this nested projection issue from preventing unification.

[Henrik Böving]

https://github.com/leanprover/lean4/issues/11798

[Artie Khovanov]

Thanks so much!