eq_and?

Stream: new members

[Jake Levinson]

Do we have the following?

lemma eq_and {X : Type} {x y : X} {p : X → Prop} : x = y ∧ p x ↔ x = y ∧ p y := sorry

(corrected from x = y ∧ p x ↔ p y)

I did library_search for all four arrangements (p x ∧ x = y and so on) and didn't find it. This would be very convenient for rewrites. There is already

exists_eq_left : ∀ {α : Sort ?} {p : α → Prop} {a' : α}, (∃ (a : α), a = a' ∧ p a) ↔ p a'

and several variants (exists_eq_right, exists_eq_left', exists_eq_right_right...), but I'm not sure how to use them exactly here.

[Eric Wieser]

Surely that first one is false?

[Jake Levinson]

Oh what am I saying.

[Jake Levinson]

I think I meant x = y ∧ p x ↔ x = y ∧ p y.

[Jake Levinson]

I'll edit the post.

[Patrick Johnson]

Your original lemma is false:

example : ¬Π {X : Type} {x y : X} {p : X → Prop}, x = y ∧ p x ↔ p y :=
begin
  intro h,
  specialize @h bool ff tt (λ a, a),
  simp at h,
  exact h,
end

Your updated lemma seems too specific to be in mathlib, but it can be proved easily:

example {X : Type} {x y : X} {p : X → Prop} : x = y ∧ p x ↔ x = y ∧ p y :=
begin
  simp,
  intro h,
  rw h,
end

Are you sure that's what you want? Maybe you want this instead:

example {X : Type} {x y : X} : x = y ↔ ∀ (p : X → Prop), p x ↔ p y :=
begin
  split; intro h,
  { intro P, rw h },
  { specialize h (eq x), simp at h, exact h },
end

[Jake Levinson]

There is and.congr_right_iff : ∀ {a b c : Prop}, a ∧ b ↔ a ∧ c ↔ a → (b ↔ c) which seems related.

[Kyle Miller]

@Patrick Johnson If you want a fun proof of the second example:

example {X : Type} {x y : X} {p : X → Prop} : x = y ∧ p x ↔ x = y ∧ p y :=
by split; simp { contextual := tt }

[Jake Levinson]

@Patrick Johnson the point isn't to prove the (corrected) lemma, which I agree is easy, it's to have it for rewrites.

I have some situations where, for example, I am showing that two sets are equal, both defined in terms of filter and insertand so on in two different ways. Then ext converts this to two logical statements that each contain x = y somewhere, but statement 1 has the other properties in terms of x and statement 2 in terms of y.

[Kyle Miller]

(I wish the contextual option were a flag that could join the likes of ! and ?. Perhaps simpᶜ or simp¢? Or simp@ since contextual is adding additional assumptions from implication hypotheses?)

[Kyle Miller]

@Jake Levinson Does adding { contextual := tt } to a relevant simp help in your cases?

[Jake Levinson]

For example I might have

q z ∧ x = y ∧ p x ↔ (x = y ∧ p y) ∧ q z

[Kyle Miller]

example {X : Type} {x y z : X} {p q : X → Prop} : q z ∧ x = y ∧ p x ↔ (x = y ∧ p y) ∧ q z :=
begin
  split; simp { contextual := tt }
end

[Jake Levinson]

Neato, I'll try that. What does it mean?

[Kyle Miller]

It adds additional simp lemmas contextually. There might be other effects, but the one I know about is that when simplifying a -> b it adds a as a simp lemma when simplifying b.

[Kyle Miller]

Key to this working in these cases is that simp is using docs#and_imp first

[Kyle Miller]

Also key is that x = y happened to be near the front on each side of the iff.

[Kyle Miller]

This fails:

example {X : Type} {x y z : X} {p q : X → Prop} : q z ∧ p x ∧ x = y ↔ (x = y ∧ p y) ∧ q z :=
begin
  split; simp { contextual := tt }
end

though there are other tactics that can solve it automatically, like by tidy or by split; cc.

[Jake Levinson]

Thanks @Patrick Johnson and @Kyle Miller.

A more complicated version of the example would be something like

example {X : Type} {x y z : X} {p : X → Prop} {r : X → X → Prop} :
  (x = y ∧ w = z ∧ p x ∧ r x w) ↔ (x = y ∧ w = z ∧ p y ∧ r y z) := by simp { contextual := tt }

This seems to work great. I'll try it out in my actual situation soon.

In general I'm imagining something like doing subst x locally within a statement that contains an equation x = y, by rewriting away x (or perhaps y) from the remainder of the statement.

[Kyle Miller]

Here's a quick tactic that simulates what contextual is doing here while also actually doing substitutions

example {X : Type} {x y z w : X} {p : X → Prop} {r : X → X → Prop} :
  (p x ∧ r x w ∧ x = y ∧ w = z) ↔ (p y ∧ r y z ∧ x = y ∧ w = z) :=
begin
  split; repeat { simp [*] <|> rintro rfl <|> intro },
end

(Notice the equalities are now at the end, so contextual alone doesn't work.)

[Jake Levinson]

Is rintro rfl somehow doing substitutions?

[Jake Levinson]

Also, a related question: I have vaguely heard that certain uses of ("nonterminal"?) simp are discouraged in mathlib because of either speed (simp being inefficient compared to simp only or an explicit proof) or fragility (updates to the library breaking a simp proof). Would the tactic you wrote be OK for code in mathlib, given that it repeatedly uses simp?

[Kyle Miller]

I think it's similar to using norm_num to finish a proof. norm_num also repeatedly calls simp, but it's a tactic with understood behavior. Still, I think it would probably be better to turn that into a simp only.

[Kyle Miller]

rintro rfl is doing subst for you after doing intro