issue !4#1458: `apply_rules` in the `symm` + `only` confi...

Stream: triage

[Random Issue Bot]

Today I chose issue 1458 for discussion!

apply_rules in the symm + only configuration
Created by @Heather Macbeth (@hrmacbeth) on 2023-01-10
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Eric Rodriguez]

I think whilst investigating this, I uncovered another issue: if you put this in Mathlib/test/solve_by_elim/basic.lean, it will fail:

example : (5 : ℕ) = 7 := by
  solve_by_elim (config := {symm := true}) [show (7 : ℕ) = 5 from sorry]

On the other hand, the current issue does still seem to exist; will dig into why later. Hopefully I'll close it today anyways, but solve_by_elim is now in Std; should this issue be moved?

[Eric Rodriguez]

I'm really confused by this, it seems to me that the sections that deal with only and symm are completely separate, and shouldn't at all be affected by each other. Still looking into this, if anyone has any ideas please let me know:)

[Eric Rodriguez]

OK, I'm closer to having some idea, but now really struggling with turning this option on to see any trace messages!

image.png

set_option trace.Meta.Tactic.solveByElim true and set_option trace.Std.Tactic.Meta.Tactic.solveByElim true both neither work

[Kim Morrison]

Hmm, it should be the first of those set_options. #mwe?

[Eric Rodriguez]

import Lean.Util.Trace

initialize Lean.registerTraceClass `Foo

set_option trace.Foo true

[Eric Rodriguez]

Oh, I see, it can't be turned on in the same file...

[Eric Rodriguez]

This seems like an annoying issue because it's often harder to debug multiple-file scenarios

[Eric Rodriguez]

I've found the source of the error: it's line 379 in the file. If this is replaced with the case for not only (i.e. l381), then it is fine. (One way to see this quickly without editing the code is by changing h to * in a mwe such as:

attribute [symm] Eq.symm
example (h : a = b) : b = a := by solve_by_elim only [h]

However, I'm not sure what I should be putting into there instead. I tried (← getLocalHyps).toList.bagInter (← add.mapM elab'), but this doesn't seem to work, and I don't know why, which leads me onto my second question: how can I see what's in here?

If I replace 379 with:

    let l := (← getLocalHyps).toList.bagInter (← add.mapM elab')
    println! l
    pure l

I get some expression involving _uniqs printed, which makes sense to me, these will be fvars and there's no context here to be printing them. I tried passing the goal in order to see (at the current moment I'm only focusing on fixing the single-goal case, not solve_by_elim*) and instead do goal.withContext (do println! l), but that also doesn't work and gives the same thing. I then tried goal.withContext (do let x := l.mapM ppExpr; println! (← x)) as a last-ditch guess and variations and it doesn't seem right. I think I am just blindly prodding and hoping without understanding everything well (still working through MPIL) - what is the correct way to do these things?

[Kim Morrison]

Sorry @Eric Rodriguez, I'm not too sure what you're trying to do here. Could you #xy a bit, and show me the apply_rules behaviour that needs fixing?

[Eric Rodriguez]

I'm trying to fix the bug reported in the description of this thread, specifically that symm doesn't seem to trigger with only. This is because (and I don't fully understand the root cause here, just observationally) the locals array is set to empty for the case of only (with no *). I'm trying to figure out the right expression for this, and (a) I can't figure it out, and (b) I can't understand how to debug and see what is in the array in a way that doesn't just print _uniqs at me.

[Eric Rodriguez]

The second code block in my last message is a mwe (sorry, would copy paste but on mobile)

[Kim Morrison]

Okay. The reason symm and only don't interact well is that we deal with symm by adding additional hypotheses. e.g. if h is a hypothesis to which we can apply a @[symm] lemma, then we add the new hypothesis h_symm. Of course, even if h was in the only list, h_symm will not be.

[Kim Morrison]

A bigger issue than #1458 is that we rebuild all these h_symm hypotheses every time we want to apply a lemma. This is insane, and surely a performance problem in solve_by_elim.

I made a PR to change that: std4#547, but it wasn't sufficiently tested and broke Mathlib. I was in a hurry so reverted it in std4#559, but this needs to be addressed.

[Eric Rodriguez]

Oh, I was going to say that the list of lemmas is made in mkAssumptionSet, which is before symmSaturate is run, but that actually returns a TermElabM, so that's not actually run until we want to get the list of lemmas, I guess?

[Kim Morrison]

That's right.

[Eric Rodriguez]

I'm still not sure how I'd be able to debug in a way that shows the names of these fvars easily.

[Kim Morrison]

I think in the combination of symm and only, perhaps the right thing to do is just to add h_symm to the set of names for every h in the set of names, and then make sure that we don't fail if those aren't actually present in the local context. It is a bit hacky.

[Kim Morrison]

(I don't think we need to debug anything: we know why the symmetric versions aren't used, we need to change the design so they can be used.)

[Eric Rodriguez]

Yeah, that's what I was thinking. I will try something of the like soon; the question about debugging and seeing the names was more for educational reasons as opposed to "needed for this task", if that makes sense.

[Kim Morrison]

It's very late here, I can try to be more helpful on the debugging side tomorrow. :-)

[Eric Rodriguez]

Many thanks Scott!

[Eric Rodriguez]

Scott, could the right approach for this be to change the goal state into one that _only_ has the right lemmas (i.e. clear anything not mentioned), and then run symmSaturate? That way we don't have to keep the list of lemmas around, either.

[Eric Rodriguez]

Considering we even have symm_saturate as a normal tactic, we could also turn solve_by_elim only [...] expand into have ...; clear ...; symm_saturate; solve_by_elim [*] (where the have step deals with any non-fvars)

[Random Issue Bot]

Today I chose issue 1458 for discussion!

apply_rules in the symm + only configuration
Created by @Heather Macbeth (@hrmacbeth) on 2023-01-10
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue #1458 for discussion!

apply_rules in the symm + only configuration
Created by @Heather Macbeth (@hrmacbeth) on 2023-01-10
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?