## Stream: new members

### Topic: eq_and?

#### Jake Levinson (Apr 30 2022 at 18:18):

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 (Apr 30 2022 at 18:21):

Surely that first one is false?

#### Jake Levinson (Apr 30 2022 at 18:22):

Oh what am I saying.

#### Jake Levinson (Apr 30 2022 at 18:27):

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

#### Jake Levinson (Apr 30 2022 at 18:28):

I'll edit the post.

#### Patrick Johnson (Apr 30 2022 at 18:31):

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 (Apr 30 2022 at 18:32):

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

#### Kyle Miller (Apr 30 2022 at 18:33):

@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 (Apr 30 2022 at 18:35):

@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 (Apr 30 2022 at 18:37):

(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 (Apr 30 2022 at 18:38):

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

#### Jake Levinson (Apr 30 2022 at 18:38):

For example I might have

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


#### Kyle Miller (Apr 30 2022 at 18:39):

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 (Apr 30 2022 at 18:40):

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

#### Kyle Miller (Apr 30 2022 at 18:41):

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 (Apr 30 2022 at 18:42):

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

#### Kyle Miller (Apr 30 2022 at 18:43):

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

#### Kyle Miller (Apr 30 2022 at 18:44):

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 (Apr 30 2022 at 19:15):

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 (Apr 30 2022 at 19:20):

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 (Apr 30 2022 at 19:26):

Is rintro rfl somehow doing substitutions?

#### Jake Levinson (Apr 30 2022 at 19:32):

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 (Apr 30 2022 at 19:50):

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 (Apr 30 2022 at 19:51):

rintro rfl is doing subst for you after doing intro

Last updated: Dec 20 2023 at 11:08 UTC