simp vs rw again

Stream: mathlib4

[Patrick Massot]

Still porting the sphere eversion project, I have a new example where simp is not working a very innocent looking goal, but rw works. The following is a SE-free example but it is not Mathlib-free.

import Mathlib.Analysis.NormedSpace.Basic
import Mathlib.Analysis.Calculus.FDeriv.Basic

noncomputable section

variable (E : Type _) [NormedAddCommGroup E] [NormedSpace ℝ E]
variable (F : Type _) [NormedAddCommGroup F] [NormedSpace ℝ F]
variable (P : Type _) [NormedAddCommGroup P] [NormedSpace ℝ P]

def OneJet :=
  E × F × (E →L[ℝ] F)

def RelLoc :=
  Set (OneJet E F)

instance : Membership (E × F × (E →L[ℝ] F)) (RelLoc E F) := by delta RelLoc; infer_instance

variable {E P F}

def oneJetSnd : OneJet (P × E) F → OneJet E F := fun p =>
  (p.1.2, p.2.1, p.2.2 ∘L fderiv ℝ (fun y => (p.1.1, y)) p.1.2)

variable (P)

def RelLoc.relativize (R : RelLoc E F) : RelLoc (P × E) F :=
  oneJetSnd ⁻¹' R

variable (R : RelLoc E F)

theorem RelLoc.mem_relativize  (w : OneJet (P × E) F) :
    w ∈ R.relativize P ↔ (w.1.2, w.2.1, w.2.2 ∘L ContinuousLinearMap.inr ℝ P E) ∈ R := by
  simp_rw [RelLoc.relativize]
  simp only [Set.mem_preimage]
  simp only [oneJetSnd_eq]

[Patrick Massot]

The goal is

w ∈ oneJetSnd ⁻¹' R ↔ (w.fst.snd, w.snd.fst, ContinuousLinearMap.comp w.snd.snd (ContinuousLinearMap.inr ℝ P E)) ∈ R

but simp only [Set.mem_preimage] fails.

[Patrick Massot]

Note there is no coercion to function involved. oneJetSnd is a honest (non-dependent) function.

[Kevin Buzzard]

Here's a start:

import Mathlib.Data.Set.Image

variable (E : Type)
variable (F : Type)
variable (P : Type)

def OneJet :=
  E × F × (E → F)

def RelLoc :=
  Set (OneJet E F)

instance short_name : Membership (E × F × (E → F)) (RelLoc E F) := by delta RelLoc; infer_instance

variable {E P F}

def oneJetSnd : OneJet (P × E) F → OneJet E F := fun p =>
  (p.1.2, p.2.1, (fun _ => p.2.1))

variable (P)

def RelLoc.relativize (R : RelLoc E F) : RelLoc (P × E) F :=
  oneJetSnd ⁻¹' R

variable (R : RelLoc E F)

theorem RelLoc.mem_relativize  (w : OneJet (P × E) F) :
    w ∈ R.relativize P ↔ (w.1.2, w.2.1, fun x => w.2.1) ∈ R := by
  simp_rw [RelLoc.relativize]
  simp only [Set.mem_preimage] -- fails
  rw [Set.mem_preimage] -- works
  sorry

[Matthew Ballard]

I am still confused about the last two :(

[Kevin Buzzard]

Heh :-)

OK, mathlib-free:

def Set (α : Type) := α → Prop

def setOf {α : Type} (p : α → Prop) : Set α :=
  p

namespace Set

variable {α : Type}

protected def Mem (a : α) (s : Set α) : Prop :=
  s a

instance : Membership α (Set α) :=
  ⟨Set.Mem⟩

def preimage {α : Type} {β : Type} (f : α → β) (s : Set β) : Set α := setOf (fun x => f x ∈ s)

infixl:80 " ⁻¹' " => preimage

theorem mem_preimage {α β : Type} {f : α → β} {s : Set β} {a : α} : a ∈ f ⁻¹' s ↔ f a ∈ s :=
  Iff.rfl

end Set

variable (E F P : Type)

def OneJet :=
  E × F × (E → F)

def RelLoc :=
  Set (OneJet E F)

instance short_name : Membership (E × F × (E → F)) (RelLoc E F) := by delta RelLoc; infer_instance

variable {E P F}

def oneJetSnd : OneJet (P × E) F → OneJet E F := fun p =>
  (p.1.2, p.2.1, (fun _ => p.2.1))

variable (P)

def RelLoc.relativize (R : RelLoc E F) : RelLoc (P × E) F :=
  oneJetSnd ⁻¹' R

variable (R : RelLoc E F)

theorem RelLoc.mem_relativize  (w : OneJet (P × E) F) :
    w ∈ R.relativize P ↔ (w.1.2, w.2.1, fun x => w.2.1) ∈ R := by
  simp only [RelLoc.relativize]
  simp only [Set.mem_preimage] -- fails
  rw [Set.mem_preimage] -- works
  sorry

[Patrick Massot]

Thanks Kevin!

[Matthew Ballard]

abbrev RelLoc

[Kevin Buzzard]

Yeah but that still doesn't explain what's going on :-/

[Matthew Ballard]

Ok, I think the care is less about why simp does what it does now but whether the following statement should be valid:

Whenever rw [h] applies so should simp only [h].

[Patrick Massot]

There is also the statement: "simp should be able to do whatever it could do in Lean 3".

[Patrick Massot]

Of course I'm currently porting Lean 3 code, so I get to see explicitly only regressions. But I would still be very much afraid of starting a new ambitious project with the current Lean 4 simp.

[Matthew Ballard]

I chose the most anodyne version :)

[Matthew Ballard]

Since this smells like an RFC, should I make a poll on #lean4 ?

[Eric Wieser]

Matthew Ballard said:

Whenever rw [h] applies so should simp only [h].

This is false in Lean3 and Lean4 if h has hypotheses that create side goals

[Matthew Ballard]

Yael pointed that out in the other thread and I don't think you want to change that

[Eric Wieser]

Hot take: I think this is working as intended

[Eric Wieser]

The problem is

def RelLoc :=
  Set (OneJet E F)

which says "let me make a new type, that's implemented with Set". But then you try and use Set.preimage on RelLoc, which is defeq-abusing nonsense that simp won't put up with.

If you change it to an abbrev then everything is fine.

[Kevin Buzzard]

If rw works then why shouldn't simp? This is a regression, regardless of this reasoning, right?

[Eric Wieser]

Here's a smaller mwe:

-- mathlib-like setup
def Set (α : Type) := α → Prop

def setOf {α : Type} (p : α → Prop) : Set α := p

namespace Set
variable {α : Type}

protected def Mem (a : α) (s : Set α) : Prop := s a
instance : Membership α (Set α) where mem := Set.Mem

def preimage {α : Type} {β : Type} (f : α → β) (s : Set β) : Set α := setOf (fun x => f x ∈ s)
infixl:80 " ⁻¹' " => preimage
theorem mem_preimage {α β : Type} {f : α → β} {s : Set β} {a : α} : a ∈ f ⁻¹' s ↔ f a ∈ s := Iff.rfl

end Set

variable (E : Type)
def SetWrapper := Set E
instance instMem : Membership (E) (SetWrapper E) := by delta SetWrapper; infer_instance

-- this def has defeq abuse in its implementation and should not be unfolded
def preimageWrapper (s : SetWrapper E) : SetWrapper E := id ⁻¹' s

theorem RelLoc.mem_relativize  (x : E) (s : SetWrapper E) :
    x ∈ preimageWrapper _ s ↔ x ∈ s := by
  simp only [preimageWrapper]
  simp only [Set.mem_preimage] -- fails
  rw [Set.mem_preimage] -- works
  sorry

[Eric Wieser]

The key piece here is that we're doing lots of messy casting between defeq-but-not-reducibly-equal types

[Kevin Buzzard]

I am still very unclear about why one of rw and simp should work, but not the other. What is one tactic doing that the other cannot and, more to the point, why?

[Kevin Buzzard]

I understand the defeq abuse issue, what I don't understand is why this causes different behaviour in the two tactics.

[Kevin Buzzard]

My mental model of simp is that it's "repeat for h in list_of_all_lemmas_tagged_simp, try rw [h]" and I'm trying to work out what it should be.

[Eric Wieser]

I think probably there is a DiscrTree lookup for simp but not rw

[Kevin Buzzard]

Yeah but I have no real idea what a discrimination tree is. My vague mental model is that it's "a good way of deciding which order to try the simp lemmas" and in particular is shredding no light on the question of why some defeq abuse is allowed by rw but not simp.

Aah! Are you saying that the discrimination tree is deciding that it's not going to try rewriting the lemma at all because it doesn't match?

Is it possible to find out if the lemma is not being rewritten by simp "because of a failure at the discrimination tree stage" or does this make no sense?

(I'm also aware that another difference between simp and rw is how they might handle conditional lemmas but I'm assuming that this is not relevant in this example)

[Kyle Miller]

Kevin Buzzard said:

more to the point, why?

I think the idea is that rw is a tactic that must be able to apply the lemma it's been given, but simp is a tactic that is expected to efficiently figure out which lemma from the whole @[simp] set could apply. This "discrimination tree" business in other words is "simp has a database of simp lemmas keyed by expressions, where given an expression it can quickly give come up with a list of lemmas whose LHS matches." It looks things up mostly syntactically, though it can handle a little bit of defeq.

[Kyle Miller]

Kevin Buzzard said:

My mental model of simp is that it's "repeat for h in list_of_all_lemmas_tagged_simp, try rw [h]" and I'm trying to work out what it should be.

That's not an accurate mental model (two observable differences: (1) rw is less powerful under binders (2) you can use simp sometimes to avoid "motive is not type correct"). Both simp and rw have some overlap but they use completely different algorithms.

1. What rw does: it computes a "key" from the LHS of the lemma (like in a function application, the head constant) using docs#Lean.Expr.toHeadIndex, and then it looks for all subexpressions in the goal with that key which are defeq to the LHS using docs#Lean.Meta.kabstract. This function punches holes into goal whenever there were matches, creates a lambda function f from this (the "motive"), uses this to prove h : f LHS = f RHS, and then basically does apply cast h.symm.

2. What simp does: it basically uses conv to navigate into every part of an expression (using "congruence lemmas" like funext, congr, etc.), and then while it's at every given subexpression it looks for a relevant lemma h and tries doing apply h.

[Kyle Miller]

Here's a short version of the differences, to point out how rw and simp match up "one" and "many" with "lemma" and "subexpression" in both ways:

• rw tries using the "kabstract" algorithm to find all matching subexpressions in the goal given the LHS pattern of a single rw lemma.
• simp tries using this "congruence lemma" algorithm to find all matching simp lemmas given a single subexpression in the goal.

[Kyle Miller]

Matthew Ballard said:

Whenever rw [h] applies so should simp only [h].

Even if simp tried every simp lemma in the simp set, rather than only the ones it thinks might match (maybe by using the key system that rw uses to be a little more efficient), there would be examples where rw works but simp doesn't and vice versa. One reason is that rw rewrites all matches simultaneously but simp can only rewrite one at a time, which might not be possible since intermediate rewrites might not typecheck. Another is that there are places in an expression that simp might be too conservative due to its congruence lemma algorithm and it will only try rfl lemmas, where rw doesn't have that restriction and will try anyway (with "motive not type correct" if it didn't work out).

[Antoine Chambert-Loir]

One remark that you may confirm, just to check I understand the underlying dynamics : when given only one lemma ‘rw‘ will find the first applicable instance, deduce the arguments and then rewrite with those arguments at all possible places. But these places will necessarily be disjoint.
On the other hand, ‘simp‘ similarly applies at the first applicable instance, but then starts again and it may apply either at a one of the initial possible instances (those where ‘rw‘ would have applied), or to an earlier instance, and that one might have been created by the first application of ‘simp‘.