Zulip Chat Archive

Stream: new members

Topic: rewriting with iff


view this post on Zulip 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

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:20):

use #backticks to make the code more readable

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:20):

you have to import that files you want from mathlib

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:20):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 15 2020 at 19:30):

pairing_axiom is not defined in your code

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:31):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Jun 15 2020 at 20:01):

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

view this post on Zulip 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.

view this post on Zulip Bhavik Mehta (Jun 15 2020 at 20:23):

Or simp_rw

view this post on Zulip Bhavik Mehta (Jun 15 2020 at 20:23):

tactic#simp_rw

view this post on Zulip 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.

view this post on Zulip 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...?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 01:00):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 17 2020 at 08:36):

Something like cases forall_and_distrib.mp h with h1 h2

view this post on Zulip Eric Wieser (Jun 17 2020 at 08:37):

rw forall_and_distrib at h did the trick, thanks

view this post on Zulip Patrick Massot (Jun 17 2020 at 08:39):

What's the problem with my solution?

view this post on Zulip Patrick Massot (Jun 17 2020 at 08:39):

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

view this post on Zulip Eric Wieser (Jun 17 2020 at 08:39):

Nothing, just wanted to understand it piecewise :)


Last updated: May 08 2021 at 18:17 UTC