modifying exists prop

Stream: new members

[Matt Diamond]

Is there a simple way to rewrite (or map over) the prop within an existential without using conv?

Like if I have a hypothesis ∃ (c : ℕ), b = 2 * c and I want to rewrite it to ∃ (c : ℕ), 2 * c = b, is there a simple way to do that? I know it can be accomplished by going into conv mode (or just unpacking it with cases and operating on the contents directly), but I was wondering if there was an even easier way to do it.

I tried messing around with exists_congr and eq_comm but I couldn't get it to work that well.

[Matt Diamond]

it would be cool if I could do something like h.map eq.symm (where h is the name of an existential hypothesis)

Edit: that seems to be what exists_imp_exists is, so I just need to make it work with eq.symm

[Matt Diamond]

hmm, it looks like exists_congr and exists_imp_exists actually work as long as they're given explicit typing, though that can be kind of cumbersome

[Xavier Roblot]

It looks like simp_rw eq_comm works here.

[Matt Diamond]

ah nice!

[Matt Diamond]

I knew there had to be a trick somewhere

[Xavier Roblot]

simp_rw is really powerful and can work in many cases where rw does not.

[Matt Diamond]

@Xavier Roblot I'm running into an issue with this... here's a mwe:

import tactic.basic

def b : ℕ := 1

example (h : ∃ (c : ℕ), b = 2 * c) : ∃ (c : ℕ), 2 * c = b := begin
  simp_rw [eq_comm],
  exact h
end

example (h : ∃ (c : ℕ), 2 * c = b) : ∃ (c : ℕ), b = 2 * c := begin
  simp_rw [eq_comm],
  exact h
end

The first works but the second fails, and the only difference is the ordering of the left and right sides of the equation.

(Not a big deal as I can just rewrite from the other direction, of course.)

[Xavier Roblot]

Well, you reached (quite rapidly) the limits of my knowledge of Lean. Still, I think what happens is that Lean has some rules to decide if an expression is simpler than another one so that the simp process converges and does end up in an infinite loop. Thus, b = 2 * c is simpler than 2 * c = b and therefore the simplification part is failing in your second example. As you noticed, in this case, you can just do simp_rw [eq_comm] at h instead and the proof works then.
I guess somebody with a better knowledge of Lean can confirm or correct my explanation.

[Alex J. Best]

Another workaround is to give lean a bit more information

example (h : ∃ (c : ℕ), 2 * c = b) : ∃ (c : ℕ), b = 2 * c := begin
  simp_rw [(eq_comm : _ = _ * _ ↔ _)],
  exact h
end

I guess this breaks the symmetry so that it doesn't do the infinite loop thing Xavier mentions.

[Matt Diamond]

Thanks for the replies!

For the record, it didn't enter an infinite loop... it completed with the error message simplify tactic failed to simplify. Based on the fact that Alex's version works, I think it was just a case of being unable to match (unify?) eq_comm with the existing equation without further hints.

[Alex J. Best]

What Xavier mentioned is the mechanism for avoiding infinite loops, simp makes a somewhat arbitrary decision that one way round of your equality is the right one, and refuses to simplify the other way round as it thinks your expression is the best possible already. simp_rw is fairly close to calling simp only.

[Alex J. Best]

If you do set_option trace.simplify you can see a bunch of what is going on under the hood:

set_option trace.simplify true
example (h : ∃ (c : ℕ), 2 * c = b) : ∃ (c : ℕ), b = 2 * c := begin
  simp_rw [eq_comm],
  -- simp_rw [(eq_comm : _ = _ * _ ↔ _)],
  exact h
end

tells us a bunch of stuff including

[simplify.perm] perm rejected: 2 * c = b !< b = 2 * c

[Alex J. Best]

Rather amusingly instead simp_rw [(eq_comm : _ ↔ _)], does seem to enter an infinite loop...

[Damiano Testa]

On the topic of loops in simp/simp_rw, there was also this recent thread.

[Eric Wieser]

Does h.imp eq.symm work?

[Kevin Buzzard]

This works:

example (h : ∃ (c : ℕ), 2 * c = b) : ∃ (c : ℕ), b = 2 * c := begin
  simp_rw [@eq_comm _ b],
  exact h
end

[Patrick Johnson]

@eq_comm _ b doesn't work if both sides of the equality contain bound variables:

import tactic

example {α β : Type*} {f g : α → β}
  (h : ∃ (x : α), g x = f x) : ∃ (x : α), f x = g x :=
begin
  simp_rw [@eq_comm (f _) (g _)], -- fails
  simp_rw [(eq_comm : f _ = g _ ↔ _)], -- works
  exact h,
end

[Eric Rodriguez]

There's also docs#Exists.imp, which I think trivialises this a lpt