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

tactic#simp_rw

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