Regression with simps?

Stream: Analysis I

[Dan Abramov]

I've noticed https://github.com/teorth/analysis/pull/251 broke one of my proofs:

theorem SetTheory.Set.image_preimage_f_3_4_2' :
    image f_3_4_2 (preimage f_3_4_2 {1,2,3}) ≠ {1,2,3} := by
  intro h
  have : 1 ∉ image f_3_4_2 (preimage f_3_4_2 {1, 2, 3}) := by
    simp [mem_image] -- This simp no longer works
  simp_all

Before the change, it worked and unrolled into

    simp only [mem_image, Object.ofnat_eq, nat_coe_eq_iff, mul_eq_one, OfNat.ofNat_ne_one,
      false_and, and_false, exists_const, not_false_eq_true]

After the change, it doesn't work and unrolls to

    simp only [pair_comm, replacement_axiom, Object.ofnat_eq, specification_axiom'',
      Subtype.coe_eta, mem_triple, nat_coe_eq_iff, mul_eq_one, OfNat.ofNat_ne_one, false_and, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, mul_eq_left₀, false_or, exists_prop, Subtype.exists,
      not_exists, not_and, not_or]
  /-
  ⊢ ∀ (x : Object) (x_1 : x ∈ nat), 1 = ↑(2 * nat_equiv.symm ⟨x, ⋯⟩) → x ∈ nat → ¬2 * nat_equiv.symm ⟨x, ⋯⟩ = 3 ∧ ¬nat_equiv.symm ⟨x, ⋯⟩ = 1
  -/

I don't mind the change per se (easily fixable by changing my code to simp; aesop) but I was wondering whether this could indicate a legit regression? Like maybe some of the ones from https://github.com/teorth/analysis/pull/251 were unsafe to mark as simp for whatever reason. I don't have a mental model for which theorems are OK to mark with simp.

[Dan Abramov]

It seems to narrow down to having @[simp] on replacement_axiom.

If that simp is present, it seems like it gets unfolded first, and turns

⊢ 1 ∉ image f_3_4_2 (preimage f_3_4_2 {1, 2, 3})

into

⊢ ¬∃ x, 1 = ↑(f_3_4_2 x) ∧ ↑x ∈ preimage f_3_4_2 {1, 2, 3}

which for some reason leads into corner.

But if I exclude replacement_axiom and instead let mem_image simplify first with simp [mem_image], I get

⊢ ¬∃ x, ↑x ∈ preimage f_3_4_2 {1, 2, 3} ∧ ↑(f_3_4_2 x) = 1

And then it's able to continue.

I wonder if somehow 1 = ↑(f_3_4_2 x) is easier to unroll than ↑(f_3_4_2 x) = 1 later?

[Dan Abramov]

An alternative fix that seems to work is to change SetTheory.Set.image to say fun x y ↦ f x = y rather than fun x y ↦ y = f x in its definition. Which I guess matches mem_image.

[Kyle Miller]

SetTheory.Set.pair_comm looks like it shouldn't be a simp lemma

Lemmas like SetTheory.Set.subset_inter_iff and SetTheory.Set.union_subset_iff can be problematic since they're "nonlinear" (there are more occurrences of a variable after the rewrite)

[Kyle Miller]

Dan Abramov said:

I wonder if somehow 1 = ↑(f_3_4_2 x) is easier to unroll than ↑(f_3_4_2 x) = 1 later?

That seems worth looking into. Have you used simp? to see which lemmas are applying?

[Dan Abramov]

Yup, that's the simp only lists above in the first message

[Dan Abramov]

This is the list I get if I change y = f x to f x = y:

    simp only [pair_comm, replacement_axiom, Object.ofnat_eq, nat_coe_eq_iff, mul_eq_one,
      OfNat.ofNat_ne_one, false_and, specification_axiom'', Subtype.coe_eta, mem_triple, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, mul_eq_left₀, false_or, exists_prop, exists_const]

It works.

And this is the list that doesn't work (without that change):

    simp only [pair_comm, replacement_axiom, Object.ofnat_eq, specification_axiom'',
      Subtype.coe_eta, mem_triple, nat_coe_eq_iff, mul_eq_one, OfNat.ofNat_ne_one, false_and, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, mul_eq_left₀, false_or, exists_prop, Subtype.exists,
      not_exists, not_and, not_or]

[Dan Abramov]

Narrowing it down a bit.

On main, this:

simp only [replacement_axiom, Object.ofnat_eq, nat_coe_eq_iff, mul_eq_one, OfNat.ofNat_ne_one, false_and]

leads to ¬∃ x, 1 = ↑(2 * nat_equiv.symm x) ∧ ↑x ∈ preimage f_3_4_2 {1, 2, 3}.

But if I edit SetTheory.Set.image to f x = y, then the same list leads to

⊢ ¬∃ x, False

[Dan Abramov]

Ok I think this is because mul_eq_one doesn't simplify 1 = ↑(2 * nat_equiv.symm x) but it does simplify ↑(2 * nat_equiv.symm x) = 1. This is why unfolding it as f x = y works but y = f x doesn't. And before replacement_axiom was marked as a simp, it wouldn't get unfolded at all and was being unfolded by mem_image which does have f x = y.

I guess this is a case of me relying on fragile impl details?

[Dan Abramov]

Probably not a bad idea to align the order between y and f x between definitions to make it more consistent

[Dan Abramov]

And yea I agree pair_comm probably shouldn't be @[simp] although not the issue in this case

[Terence Tao]

Marking SetTheory.Set.pair_comm as @[simp] was definitely a mistake, I will revert that now, as well as swap the equality in SetTheory.Set.image (at first I thought this was due to the way it was written in the book, but actually the book doesn't state either form).

On the other hand, Mathlib marks docs#Set.subset_inter_iff and docs#Set.union_subset_iff as @[simp] so I assume these particular types of simp lemmas are "battle-tested"?

[Dan Abramov]

Thanks, confirmed it works after a rebase

[Kyle Miller]

Terence Tao said:

I assume these particular types of simp lemmas are "battle-tested"?

I'm not really sure. Distributivity lemmas sometimes are and sometimes aren't simp lemmas, and it's not clear why or why not.

Those subset lemmas are simp lemmas, docs#map_mul is a simp lemma, yet docs#mul_add is not a simp lemma.

(Sometimes I've thought it would be nice if we had an expand simp set that contained all the distribution lemmas.)

[Kyle Miller]

Dan Abramov said:

mul_eq_one

Interesting, mul_eq_one is a simp lemma, but there's no one_eq_mul... That seems like a little bit of an oversight in the simp set.

Possibly the answer is that there needs to be a 1 = x <-> x = 1 simp lemma, if _ = 1 is decided to be the simp normal form.