Rewriting inside quantifiers

Stream: new members

[Daniel Roca González]

I would like this to work, but it doesn't

import topology.metric_space.basic

variables {α : Type*} [metric_space α] {P : α → α → Prop}

lemma test : ∃ x y : α, P x y ∧ dist x y ≤ 2 →  ∃ x y : α, P x y ∧ dist y x ≤ 2 :=
begin
  rw dist_comm, -- rewrite tactic failed, did not find instance of the pattern in the target expression dist ?m_3 ?m_4
  tauto
end

Using dist_comm would make the lemma trivial, but Lean doesn't seem to be able to rewrite "inside quantifiers". Is there a nice way to get it to do this? The obvious solution would be to rcases to get xand y, use them and rewrite, but that would be disappointing.

[Mario Carneiro]

you can either use conv to enter the binder, or use simp or simp_rw, which can rewrite under binders

[Daniel Roca González]

I see thank you, I will look into conv

[Daniel Roca González]

A version using conv (closer to what I actually need), it's still longer than using intro and cases though...

import topology.metric_space.basic

variables {α : Type*} [metric_space α] {P : α → α → Prop}

lemma test : (∃ r, ∀ x y : α, P x y ∧ dist x y ≤ r) →  ∃ r, ∀ x y : α, P y x ∧ dist x y ≤ r :=
begin
  conv in (∃ r, ∀ x y : α, P y x ∧ dist x y ≤ r)
  begin
    congr, funext,
    rw forall_swap,
    find (dist _ _) {rw dist_comm},
  end,
  tauto,
end

[Stuart Presnell]

Does simp_rw dist_comm work for this?

[Patrick Johnson]

rw cannot rewrite under binders, but simp_rw can:

example {α : Type*} [metric_space α] {P : α → α → Prop} :
  (∃ (x y : α), P x y ∧ dist x y ≤ 2) →
  (∃ (x y : α), P x y ∧ dist y x ≤ 2) :=
by simp_rw dist_comm; exact id

Also, note that your original example is incorrect. Parentheses around the first existential quantifier are not optional. The statement

∃ x y : α, P x y ∧ dist x y ≤ 2 → ∃ x y : α, P x y ∧ dist y x ≤ 2

is interpreted as

∃ x y : α, (P x y ∧ dist x y ≤ 2 → ∃ x y : α, P x y ∧ dist y x ≤ 2)

which is not true, because a metric space can be empty:

example : ¬Π {α : Type*} [h₁ : metric_space α] {P : α → α → Prop}
  (dist : α → α → ℝ)
  (h₂ : dist = h₁.to_pseudo_metric_space.to_has_dist.dist),
  ∃ (x y : α), P x y ∧ dist x y ≤ 2 →
  (∃ (x y : α), P x y ∧ dist y x ≤ 2) :=
begin
  rw not_forall, use empty, push_neg,
  refine ⟨by split; intro x; cases x, _⟩,
  refine ⟨by intro x; cases x, _⟩,
  refine ⟨by intro x; cases x, _⟩,
  refine ⟨by ext x; cases x, _⟩,
  intro x, cases x,
end

[Kyle Miller]

I've been unsure about precisely what it means when we say "rw cannot rewrite under binders," because it definitely can sometimes.

example (p q : Prop) (h : p ↔ q) : (∀ x : ℕ, p) ↔ (∀ x : ℕ, q) := by rw h -- OK

example (p q : ℕ → Prop) (h : p = q) : (∀ x : ℕ, p x) ↔ (∀ x : ℕ, q x) := by rw h -- OK

example (p q : ℕ → Prop) (h : ∀ x, p x = q x) : (∀ x : ℕ, p x) ↔ (∀ x : ℕ, q x) := by rw h -- fails

Is the rule actually "rw cannot rewrite subexpressions containing bound variables"?

[Ruben Van de Velde]

That sounds like an accurate summary, yeah

[Daniel Roca González]

@Stuart Presnell gives me "simplify tactic failed to simplify"

[Daniel Roca González]

Patrick Johnson said:

rw cannot rewrite under binders, but simp_rw can:

example {α : Type*} [metric_space α] {P : α → α → Prop} :
  (∃ (x y : α), P x y ∧ dist x y ≤ 2) →
  (∃ (x y : α), P x y ∧ dist y x ≤ 2) :=
by simp_rw dist_comm; exact id

That's nice, but it doesn't work in my (second, correct) example, and I have no idea what the diference is. That is how I would expect it to work.

[Patrick Johnson]

-- Without using dist_comm
lemma test :
  (∃ r, ∀ x y : α, P x y ∧ dist x y ≤ r) →
  ∃ r, ∀ x y : α, P y x ∧ dist x y ≤ r :=
λ ⟨r, h⟩, ⟨r, λx y, ⟨(h y x).1, (h x y).2⟩⟩

[Patrick Johnson]

or if you insist to use dist_comm:

lemma test :
  (∃ r, ∀ x y : α, P x y ∧ dist x y ≤ r) →
  ∃ r, ∀ x y : α, P y x ∧ dist x y ≤ r :=
begin
  rintro ⟨r, h⟩,
  rw forall_swap at h,
  simp_rw dist_comm at h, -- works
  exact ⟨r, h⟩,
end

[Patrick Johnson]

Daniel Roca González said:

it doesn't work in my (second, correct) example, and I have no idea what the diference is.

I'm not sure what your question exactly is. The two examples you showed are different statements. I don't think you can simplify the proof of the second one too much further.

[Kyle Miller]

Another proof, using the contextual configuration for simp (this causes it to use p in p -> q when simplifying q).

example {α : Type*} [metric_space α] {P : α → α → Prop} :
  (∃ (x y : α), P x y ∧ dist x y ≤ 2) →
  (∃ (x y : α), P x y ∧ dist y x ≤ 2) :=
by simp [dist_comm] { contextual := tt }

[Stuart Presnell]

Ah, I think this is the crucial missing piece of the puzzle!