# Zulip Chat Archive

## 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 `insert`

and 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