Potential Bug in symm tactic

Stream: mathlib4

[zbatt]

On line 166 of FinEnum.lean it used to say symm which I replaced with apply Eq.symm. I realized this morning that seemed off so I went and double checked. If you replace apply Eq.symm with symm you get an error

symmetry lemmas only apply to binary relations, not
  s = s \ {xs_hd}

Is this a bug?

[Kevin Buzzard]

Mathlib.Init.Core has attribute [symm] Eq.symm so this is indeed unexpected (to me, at least) behaviour.

[Siddhartha Gadgil]

I am investigating this.

[zbatt]

This is strange, logging the representation with logInfo (repr tgt) in Symm.lean tells us that the goal is Lean.Expr.mvar (Lean.Name.mkNum _uniq 45724), but if you first do suffices s = s\ {xs_hd} from this then the symm works fine

[Kyle Miller]

I'm not sure if this is relevant, but this reminded me that in the Lean 3 implementation there's a step where it instantiates the mvars of the target before proceeding.

[Kevin Buzzard]

I'm finding this really hard to minimise.

[zbatt]

@Kyle Miller
I just tried that locally and it didn't immediately work. That being said this is my first time doing anythin with tactic debugging so someone else should double check

Update: I'm realizing I put it in the wrong place, so I'm checking again now. Hopefully it'll fix this time.

[Siddhartha Gadgil]

@Kyle Miller I am testing if that is the solution here.

[Siddhartha Gadgil]

Last time I was debugging symm and trans I just made the errors much more verbose temporarily. I will try that again if the above does not work (the build is slow now so each step takes a while).

[zbatt]

yep it worked!

[Siddhartha Gadgil]

What is "it"?

[zbatt]

Specifcally, replace line 102 with g.symmAux (← instantiateMVars (← g.getType)) fun lem args body g => do

/-- Apply a symmetry lemma (i.e. marked with `@[symm]`) to a metavariable. -/
def symm (g : MVarId) : MetaM MVarId := do
  g.symmAux (← instantiateMVars (← g.getType)) fun lem args body g => do
    let .true ← isDefEq (← g.getType) body | failure
    g.assign (mkAppN lem args)
    return args.back.mvarId!

[zbatt]

I don't know enough about tactics to know if this is correct to do, but I thought I should point out that the same lack of instantiateMVars appears on line 75. Should this be changed too?

[Siddhartha Gadgil]

I am trying a line inserted after line 37:

let targetTy ← instantiateMVars targetTy

It is still building. Let me see if it works.

[Siddhartha Gadgil]

Actually my change probably fixes nothing as it is when the attribute is being added. I believe @zbatt is right on both counts: the correct fix here and the same should be done on line 75.

[zbatt]

should I PR these changes?

[Siddhartha Gadgil]

@zbatt maybe it is best if you make both changes, build everything and make a PR. Is that fine?

[Siddhartha Gadgil]

Our lines crossed.

[zbatt]

will do! (just give me a minute to submit some homework :p)

[zbatt]

PR'd

[Siddhartha Gadgil]

Just an alert - a lot of the code of ext is also common with symm and trans (my initial implementation of symm and transwas heavily modelled on ext). It may be worth checking if the same issue is there too.

[Parth Shastri]

ext it seems uses getType', which includes instantiateMVars.

[zbatt]

Also trans apppears to use getMainTarget so I don't think it should have the same issue.