rewriting with iff

Stream: new members

[Michael Beeson]

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]

use #backticks to make the code more readable

[Jalex Stark]

you have to import that files you want from mathlib

[Jalex Stark]

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

[Jalex Stark]

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]

pairing_axiom is not defined in your code

[Jalex Stark]

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

[Jalex Stark]

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]

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]

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

[Kevin Buzzard]

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]

Or simp_rw

[Bhavik Mehta]

tactic#simp_rw

[Michael Beeson]

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]

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]

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

[Michael Beeson]

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]

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

[Michael Beeson]

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]

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]

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]

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]

Something like cases forall_and_distrib.mp h with h1 h2

[Eric Wieser]

rw forall_and_distrib at h did the trick, thanks

[Patrick Massot]

What's the problem with my solution?

[Patrick Massot]

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

[Eric Wieser]

Nothing, just wanted to understand it piecewise :)