# Zulip Chat Archive

## Stream: new members

### Topic: rewriting with iff

#### Michael Beeson (Jun 15 2020 at 19:19):

I read somewhere that rewrite is supposed to work with iff as well as with =. At least in my example below that does not seem to work. Can someone please tell me how to alter this non-proof so it becomes a proof? It's the third line from

the bottom that doesn't work. Also, question 2, it's not clear to me why I have to import tactic.finish, as this file is included in a project that uses mathlib and tactic is part of mathlib.

```
import tactic.finish
constant M: Type
constant p: M->M->M
constant mem: M->M->Prop
axiom axiom_1: ∀ x a b, (mem x (p a b) ↔ (x = a ∨ x = b))
lemma pair_equality: ∀ x y a b:M, (p x y = p a b → (x=a ∧ y = b) ∨ (x=b ∧ y = a)) :=
assume x y a b,
assume h: p x y = p a b,
have q: ∀ u:M, (mem u ( p x y) = mem u (p a b)), from
begin
rewrite h,
ifinish
end,
let q :=q in
begin
repeat {rw axiom_1 at q},
ifinish
end
```

#### Jalex Stark (Jun 15 2020 at 19:20):

use #backticks to make the code more readable

#### Jalex Stark (Jun 15 2020 at 19:20):

you have to import that files you want from mathlib

#### Jalex Stark (Jun 15 2020 at 19:20):

the fact that mathlib is available is what makes the import statements work

#### Jalex Stark (Jun 15 2020 at 19:25):

here's how I would write your example

```
import tactic
variables {M : Type*} {op : M → M → M} {mem : M → M → Prop}
lemma pair_equality
(mem : M → M → Prop) (h : ∀ x a b, mem x (op a b) ↔ (x = a ∨ x = b)) :
∀ x y a b, (op x y = op a b → (x = a ∧ y = b) ∨ (x = b ∧ y = a)) :=
begin
intros x y a b h,
sorry
end
```

#### Kevin Buzzard (Jun 15 2020 at 19:30):

`pairing_axiom`

is not defined in your code

#### Jalex Stark (Jun 15 2020 at 19:31):

I think the problem you hit is that you can't rewrite under binders

#### Jalex Stark (Jun 15 2020 at 19:33):

I think this gets you where you wanted to go

```
import tactic
variables {M : Type*} {op : M → M → M} {mem : M → M → Prop}
lemma pair_equality (mem : M → M → Prop) (h : ∀ x a b, mem x (op a b) ↔ (x = a ∨ x = b)) :
∀ x y a b, (op x y = op a b → (x = a ∧ y = b) ∨ (x = b ∧ y = a)) :=
begin
intros x y a b h1,
have q : ∀ u, (mem u (op x y) = mem u (op a b)),
{ rw h1, simp },
specialize q x,
repeat {rw h at q},
squeeze_simp at q,
cases q,
{ sorry },
{ sorry }
end
```

#### Michael Beeson (Jun 15 2020 at 19:59):

Yes, Jalex has hit the nail on the head: you can't rewrite under binders. I did not know that. It is not obvious WHY you can't rewrite under binders, but that is clearly the problem with my code. Thank you.

#### Jalex Stark (Jun 15 2020 at 20:01):

i recommending avoiding constants and axioms in favor of variables or just arguments

#### Kevin Buzzard (Jun 15 2020 at 20:02):

The issue is not that it's illegal in some way to rewrite under binders, the issue is that the `rw`

tactic does not rewrite under binders. You can use `simp only [axiom_1]`

to rewrite under binders, or you can use `conv`

mode.

#### Bhavik Mehta (Jun 15 2020 at 20:23):

Or `simp_rw`

#### Bhavik Mehta (Jun 15 2020 at 20:23):

#### Michael Beeson (Jun 16 2020 at 00:56):

After using simp only or simp_rw there are two versions of the hypothesis that was simplified. The original, and the simplified, both named the same (!) and when I try to work on the simplified one, Lean works on the original instead and fails.

Eg.

```
q : ∀ (u : M), mem u (p x y) ↔ mem u (p a b),
q : ∀ (u : M), u = x ∨ u = y ↔ u = a ∨ u = b
```

I don't see how it makes sense to have q be of two different types.

So if I then try something like

```
have r: x = a ∨ x = b, from
(q x).1 (or.inl (refl eq))
```

intending the second "q", it tries the first "q" instead.

#### Kevin Buzzard (Jun 16 2020 at 01:00):

Is this related to the fact that in your original code block you created two q's with the line `let q :=q in...`

?

#### Kevin Buzzard (Jun 16 2020 at 01:00):

If not, then can you post some fully working code?

#### Michael Beeson (Jun 16 2020 at 01:01):

Maybe it is. That line bothered me too, but I imitated it from TPIL. If I tried let q2 := q it complains.

No, I can't post working code, that's why I'm posting non-working code.

#### Kevin Buzzard (Jun 16 2020 at 01:02):

Why not just delete the line? It's making two variables both called q and doing nothing else

#### Michael Beeson (Jun 16 2020 at 01:03):

If you don't put that line in then q isn't recognized. It seems to be like #include. Since hypotheses can be changed within a tactic block they don't live past the end of that tactic block unless you at least mention them, says TPIL.

#### Kevin Buzzard (Jun 16 2020 at 01:08):

I don't understand what you're saying. What I'm saying is that `let q := q in`

creates a second variable also called `q`

and that any complaints you have about having two variables called `q`

beyond that point are of your own making.

#### Michael Beeson (Jun 16 2020 at 01:11):

OK, I think you're right. I took that line out and it no longer produced the same complaint that caused me to

put it in in the first place. Thank you.

#### Eric Wieser (Jun 17 2020 at 08:20):

Continuing the topic of rewriting under binders - how can I apply cases under a binder?

I have `h: ∀ (m : ℕ → bool), eval m a = tt ∧ eval m b = tt`

, and would like to split on `∧`

into `h1`

and `h2`

#### Patrick Massot (Jun 17 2020 at 08:36):

Something like `cases forall_and_distrib.mp h with h1 h2`

#### Eric Wieser (Jun 17 2020 at 08:37):

`rw forall_and_distrib at h`

did the trick, thanks

#### Patrick Massot (Jun 17 2020 at 08:39):

What's the problem with my solution?

#### Patrick Massot (Jun 17 2020 at 08:39):

If you had posted a #mwe I could have helped you much better.

#### Eric Wieser (Jun 17 2020 at 08:39):

Nothing, just wanted to understand it piecewise :)

Last updated: May 08 2021 at 18:17 UTC