using `Iff` rfl proofs in `dsimp`

Stream: mathlib4

[Thomas Murrills]

Update: this is a little more subtle than I thought. I have an idea for what's wrong, but on second thought, I'm not completely certain about it. I'll think more carefully about this. :)

[Utensil Song]

Thomas Murrills said:

Issue: #2678
Draft PR forthcoming...

It seems to be lean4#2678 actually.

[Thomas Murrills]

Ah, thank you, you're right—I always forget the prefix. Edited. :)

[Thomas Murrills]

So, I believe the issue was that simp preprocesses Iff lemmas by applying propext to them. As such, we can't just look for Iff.rfl and the like when determining if something is a rfl theorem (i.e. is fit for use by dsimp); we need to peel away propext as well. We'll see if this notion holds up after the toolchain compiles and I test it. :)

[Thomas Murrills]

Good news: it works correctly! Bad news: std is now broken.

[Thomas Murrills]

But maybe only a little. :) It looks to be just a single proof (so far). Though I'm a bit worried as to what that means for mathlib...

[Thomas Murrills]

I think I've finally understood the issue with the std breakage. It's interesting!

The offending line is of the form simp [by simpa using foo]. This essentially means "simplify the type of foo, then use it as a simp lemma".

The simp in simpa here (and in general) doesn't include dsimp lemmas in its construction of the term. This PR makes more simp lemmas into dsimp lemmas, so when we elaborate by simpa using foo, we get a term that potentially has fewer lemmas in it. This means that when we now infer the type of that term, we might get one which is not as (d)simplified.

However, this is only the case if we instantiateMVars before inferring the type. Note that elab_type has some extra machinery in it to replicate some of the conditions of elaboration within simp (and this affects the result). (I'm guessing this is because something caches the specific type of the mvar being worked on by by simpa using foo, but I'm not sure; inferType is opaque.)

import Lean
import Std.Tactic.Simpa

open Lean Meta Elab Tactic

elab "elab_type" stx:term : tactic => withMainContext <| withReducible do
  let e ← Term.elabTerm stx none
  Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
  let type ← inferType e
  logInfoAt stx m!"type: {indentD type}"
  let typeOfInstantiated ← inferType <|← instantiateMVars e
  logInfoAt stx m!"type of instantiated expr: {indentD typeOfInstantiated}"

structure Foo where a : Nat
instance : LE Foo where le x y := x.a ≤ y.a

-- Now counts as a `dsimp` theorem
@[simp] theorem Foo.mk_le_mk {a₁ a₂} : { a := a₁ : Foo } ≤ { a := a₂ } ↔ a₁ ≤ a₂ := Iff.rfl

theorem Foo.le_iff_zero (l r) : { a := l + r : Foo} ≤ { a := l } ↔ r = 0 := sorry

example := by
  elab_type by simpa using Foo.le_iff_zero
  exact 0
/-
Currently, without `Foo.mk_le_mk` as a `dsimp` theorem:
type:
  ∀ (l r : Nat), l + r ≤ l ↔ r = 0
type of instantiated expr:
  ∀ (a a_1 : Nat), a + a_1 ≤ a ↔ a_1 = 0

Now, with `Foo.mk_le_mk` as a `dsimp` theorem:
type:
  ∀ (l r : Nat), l + r ≤ l ↔ r = 0
type of instantiated expr:
  ∀ (l r : Nat), { a := l + r } ≤ { a := l } ↔ r = 0
-- ^ note that this is just `Foo.le_iff_zero`, since `simpa` doesn't use `Foo.mk_le_mk` to construct the term
-/

Note that this is not because of an outright defeq failure in Foo.mk_le_mk—if the two sides weren't defeq, we couldn't have used Iff.rfl. However, these are not reducibly defeq, which might contribute.

Note also that this is not specific to any details of how this PR handles Iff theorems—it only comes from the fact that more theorems are now able to behave this way. This behavior already happens with =—and, in fact, replacing ↔ with = in the above example causes current Lean to behave in the same way the PR behaves.

[Thomas Murrills]

So, here are the questions that this leaves me with:

• Is the failure of reducible defeq really why simp can't use the new result of by simpa using ...?
• Would simply inferring the type before instantiating mvars "fix" the situation? Or might it break many other things? (There's an easy way to find out, I guess...)
• Should this simply be ignored for now/for this functionality? After all, it's extremely easy to patch over: simp [show <intended type> from by simpa using foo].

[Thomas Murrills]

(I've just realized I never linked the draft PR here directly. Here it is: lean4#2679)

[Mario Carneiro]

@Thomas Murrills said:

The simp in simpa here (and in general) doesn't include dsimp lemmas in its construction of the term. This PR makes more simp lemmas into dsimp lemmas, so when we elaborate by simpa using foo, we get a term that potentially has fewer lemmas in it. This means that when we now infer the type of that term, we might get one which is not as (d)simplified.

This seems counterintuitive to me. Why would simp not use a theorem because it is a dsimp lemma?

[Mario Carneiro]

I would expect simp to use @[simp] lemmas whether or not they are dsimp lemmas

[Thomas Murrills]

(Admittedly, I am still looking for where in the code that decision is actually made, but the only difference affecting a lemma's in- or exclusion seems to be its status as a dsimp lemma. It's possible the actual criterion is different.)

[Mario Carneiro]

Do you have a simpa-free example?

[Thomas Murrills]

Oh, I think the crucial thing might be here, in ..Simp.Rewrite:

private def tryTheoremCore ... (thm : SimpTheorem) ... : SimpM (Option Result) := do
  ...
      let proof? ← if thm.rfl then
        pure none

[Thomas Murrills]

Mario Carneiro said:

Do you have a simpa-free example?

I'll try to make one.

[Mario Carneiro]

that just says that if the lemma is a dsimp lemma then no proof is required

[Mario Carneiro]

it is still simplifying the expression itself

[Thomas Murrills]

Isn't saying no proof is required what we're talking about here, though? Like, simp(a) therefore doesn't insert the proof into the term it's constructing.

[Thomas Murrills]

Or is it used differently?

[Thomas Murrills]

Here's a simpa-free #mwe that doesn't require you to change your toolchain to observe the change in behavior.

import Lean

open Lean Meta Elab Tactic

elab "elab_term" stx:term : tactic => withMainContext <| withReducible do
  let e ← Term.elabTerm stx none
  Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
  let type ← instantiateMVars <|← inferType e
  logInfoAt stx m!"term: {indentD e}"
  logInfoAt stx m!"type: {indentD type}"
  let typeOfInstantiated ← inferType <|← instantiateMVars e
  logInfoAt stx m!"type of instantiated expr: {indentD typeOfInstantiated}"

structure Foo where a : Nat
instance : LE Foo where le x y := x.a ≤ y.a

theorem Foo.le_iff_zero (l r) : { a := l + r : Foo } ≤ { a := l } ↔ r = 0 := sorry

-- NOT a dsimp lemma currently:
@[simp] theorem Foo.mk_le_mk {a₁ a₂} : ({ a := a₁ : Foo } ≤ { a := a₂ }) ↔ (a₁ ≤ a₂) := Iff.rfl

example (l r : Nat): l + r ≤ l := by
  simp only [by
    have h := Foo.le_iff_zero
    simp at h
    exact h]
  -- unsolved goal: ⊢ r = 0

-- display term and type used by `simp only`
example := by
  elab_term by
    have h := Foo.le_iff_zero
    simp at h
    exact h
  exact 0

attribute [-simp] Foo.mk_le_mk
-- A dsimp lemma:
@[simp] theorem Foo.mk_le_mk_eq {a₁ a₂} : ({ a := a₁ : Foo } ≤ { a := a₂ }) = (a₁ ≤ a₂) := rfl

example (l r : Nat): l + r ≤ l := by
  simp only [by
    have h := Foo.le_iff_zero
    simp at h
    exact h]
  -- simp made no progress

-- display term and type used by `simp only`
example := by
  elab_term by
    have h := Foo.le_iff_zero
    simp at h
    exact h
  exact 0

[Thomas Murrills]

Mario Carneiro said:

it is still simplifying the expression itself

I'm guessing the thing here is that when simp [bar] is called, it has to infer the type of the term bar. When bar is e.g. by simpa using foo, simp only sees the proof term created by by simpa using foo, and infers the type from there. But you wind up inferring different types depending on whether you instantiate the mvar that by simpa using foo was working on. If you do instantiate that mvar before inferring the type, the exclusion of dsimp lemmas from the proof term means the inferred type isn't dsimp'd. If you don't, you get to use the mvar context, I'm guessing—which is what remembers that simplified expression.

[Thomas Murrills]

Hmm, it looks like making some things rfl theorems which weren't before just...causes things to act differently. There are a few odd breakages over at the lean-pr-testing-2679 branch (#7686), including a whnf timeout (maybe it's working on a different expression now?) and an aesop_cat failure. If anyone would like to investigate these and add to the branch, feel free; otherwise I'll get to them soon. :)

[Thomas Murrills]

One of them might be indicative of something a little more serious...a simp invocation now fails. The following used to work (Mathlib.Order.Atoms):

theorem covby_iff_atom_Ici (h : a ≤ b) : a ⋖ b ↔ IsAtom (⟨b, h⟩ : Set.Ici a) := by simp

It now (technically) makes progress but doesn't close the goal. Squeezing, we see that now it uses Set.mem_Ici, whereas the goal-closing invocation used to be equivalent to simp only [Set.Ici.isAtom_iff].

I suspect a crucial fact is that dsimp now makes progress on the type of Set.Ici.isAtom_iff (via Set.mem_Ici)—it rewrites something in an instance argument, so pp.explicit is required to see it. But there are still details to work out; I'm not totally sure where in simp things go wrong.

[Thomas Murrills]

It seems that the reason this changes is that simp calls dsimp specifically at certain points, e.g. mkCongrFun r (← dsimp arg) (which is the specific difference in this case). I'm not sure what the best way to proceed here is—just fix the broken cases?

It'd be nice to have an actual "solution" (maybe something else needs to be dsimpd as well), but I'd guess it's not worth holding up the dsimp Iff feature.

[Notification Bot]

24 messages were moved here from #mathlib4 > Tactic state explosion by Thomas Murrills.

[Thomas Murrills]

@Jannis Limperg , I was just wondering—do you happen to have any opinion on Iff.rfl lemmas being used by dsimp? I ask because in the testing this change (#7686), an aesop invocation breaks. I'm not sure how aesop depends on simp, so I thought I'd just ask. :) (aesop may also possibly involved in a separate whnf category theory timeout.)

(There are two major effects of such a change (as you might be aware): (1) the proofs of these lemmas are now not inserted into the constructed proof term (2) invocations specifically of dsimp during certain parts of simp can change how simp behaves.)

[Jannis Limperg]

Aesop runs simp_all on every goal before it does anything else (more or less). It treats simp_all as a black box, so changing simp's behaviour shouldn't affect Aesop itself. As such, I don't mind Iff.rfl lemmas being included. Any breakage would most likely be due to interactions with the current CategoryTheory rule set, which can hopefully be fixed.

[Thomas Murrills]

Ok, sounds good!

[Thomas Murrills]

General update for those interested: this causes >30 breakages in mathlib so far, which I've been fixing in a back-and-forth with CI.

Some of them are because simp is now more powerful (and thus there are no goals to be solved), which is nice, but most are resolved only by turning off dsimp via the config. I'm not sure I love the notion of "try it again with dsimp := false" being a more common strategy (albeit still quite uncommon) for making simp work.

The most common issue seems to be rewriting under a fun in the argument of a Subtype, which occurs because simp specifically runs dsimp before mkCongrFun. This can prevent other simp lemmas from applying. It can also change the lemmas that simps (or at least simps!) generates.

I wonder if we should either

1. just accept the dsimp := false strategy, at least for now
2. try out removing dsimp before mkCongrFun in simp (might break things)
3. consider dsimping something else inside simp (or when we register the simp lemma) so that these simp lemmas still apply (might not actually solve the issue)
4. something else?

[Thomas Murrills]

(I think I might try (2) just out of curiosity, and see what breaks.)

[Eric Wieser]

Can you give an example of the type of thing that causes trouble?