How do tactics "reach into" quantifiers.

Stream: new members

[Daniel James]

I am trying to understand a bit more about how tactics work under the hood.

I have this example code:

import Mathlib.Data.Nat.Basic

theorem foo : ∀ x, x - x = 0 := by
  -- rw [Nat.sub_self]
  simp

Now I think I get why the rw doesn't close the goal (since x is a bound variable it is not nameable from outside the forall expression and so cannot be an argument to sub_self), and I understand that simp is a much more powerful tactic, but what mechanism does simp use to be able to in essence reach into the quantifier? I know I can #print foo to see the proof term but I didn't find that super illuminating.

What is the general technique here that allows simp to search inside the quantifier but that doesn't work for rw? And also is there a way to make rw work here?

[Henrik Böving]

It's the forall_congr theorem that simp is applying. There is work on a version of rw that can just reach under quantifiers among other cool things but for now if you want to do that you probably want to use mathlib's home cooked simp_rw

[Robin Arnez]

Alternatively you can use conv to manually apply forall_congr:

theorem foo : ∀ x, x - x = 0 := by
  conv => intro x; rw [Nat.sub_self]

(intro x is the step here that applies forall_congr)

[Kenny Lau]

@Daniel James you can write simp? to see which lemmas simp used, in this case Nat.sub_self is the first one, then you can write simp only [Nat.sub_self] to isolate that part, and then when you finally #print foo, then you'll see that the key lemma used is forall_congr

[Kyle Miller]

conv is a good suggestion, since it uses generally the same mechanisms as simp to enter expressions.

I tend to reach for enter [x] instead of intro so that I don't have to remember all the tactics.

[Kyle Miller]

It's possible for rw to rewrite under binders in a sense, but it takes funext (which is what simp is implicitly using) and rearranging things to get a subexpression that can be lifted out.

Here's it done manually:

import Mathlib.Data.Nat.Basic

theorem foo : ∀ x, x - x = 0 := by
  change ∀ x, (fun y => y - y) x = 0
  generalize h : (fun y : ℕ => y - y) = f
  have h' := funext (Nat.sub_self)
  have h'' := h'.symm.trans h
  clear h h'
  subst f
  dsimp only
  -- ⊢ ∀ (x : ℕ), 0 = 0

(The generalize is replicating how rw does its rewriting.)

Here's it being done with rw itself

theorem foo : ∀ x, x - x = 0 := by
  change ∀ x, (fun y => y - y) x = 0
  have : (fun y : Nat => y - y) = (fun y : Nat => 0) :=
    funext Nat.sub_self
  rw [this]
  dsimp only
  -- ⊢ ∀ (x : ℕ), 0 = 0

That have isn't necessary — rw [funext Nat.sub_self] works.