proving (0,0) ≠ (2,1)

Stream: new members

[rzeta0]

What is a good way to resolve (0,0) ≠ (2,1) ?

There are two differences between vanilla lean+mathlib and MoP:

• in MoP the custom tactic numbers works, but norm_num doesn't, even though numbers is supposed to be a weakened version of norm_num
• the by_contra method I tried below works in live.lean but not MoP. (I find it strange it doesn't need further code.)

import Mathlib.Tactic

example : (0,0) ≠ (2,1) := by
  -- numbers tactic from MoP works
  -- norm_num doesn't
  by_contra g
  obtain ⟨ha , hb⟩ := g -- this works in live.lean but not MoP !
  -- no additional code needed, eg to find ¬P and P hypotheses then `contradiction`

So given things have changed since MoP, what is the recommended way to resolve that goal?

[Aaron Liu]

I would go with simp or decide

[Julian Berman]

decide definitely works, intro h; cases h seems to as well

[Eric Wieser]

Does nofun work?

[rzeta0]

Thanks for the replies, I'll wait for more and see which are "beginner" enough for me.

Believe it or not, I actually have not learned simp despite using dsimp to unfold definitions.

I haven't learned decide nor nofun.

I have used intro and cases so that is worth me playing with.

[Chris Wong]

I think the reason why norm_num doesn't work here is because it's about numbers, and technically the goal is about pairs.

If you break it down to the individual components using extensionality then it does work.

import Mathlib

example : (0, 0) ≠ (2, 1) := by
  rw [Ne, Prod.ext_iff]
  norm_num

[Chris Wong]

Though if this weren't an exercise, I would indeed go with nofun or decide, as simple statements deserve simple proofs.

[suhr]

example : (0,0) ≠ (2,1) := (by decide) ∘ (congrArg Prod.fst)

[suhr]

example : (0,0) ≠ (2,1) := by decide also works.

[suhr]

Here's how to prove it without decide:

example : (0,0) ≠ (2,1) := Nat.noConfusion ∘ (congrArg Prod.fst)

Hopefully your tutorial allows you to use congrArg and Nat.noConfusion, otherwise I don't quite see a point in such a tutorial.

[Andrew Yang]

About the obtain:
It does not in general give you a = b and c = d from (a, c) = (b, d) (which I imagine is what you are looking for). For example this fails:

import Mathlib.Tactic

axiom a : Nat
axiom b : Nat
axiom c : Nat
axiom d : Nat

example : (a, b) ≠ (c, d) := by
  by_contra g
  obtain ⟨ha, hb⟩ := g -- fails

I'm guessing that MoP thinks this is confusing for beginners so they weakened obtain and made it always fail.

[Edward van de Meent]

Andrew Yang said:

It does not in general give you a = b and c = d from (a, c) = (b, d)

indeed, if you think about it, it does not make sense to match on an equality with a constructor with two variables, as Eq.refl only has one argument, even if it states an equality of 2-tuples. Indeed, the error message suggests that what obtain does when you try anyway, is cases on the equality

[Edward van de Meent]

which then in the (0,0) ≠ (2,1) case will try unifying 0 with 2 (and 0 with 1 too), and note that there is no such case possible (rather than not knowing if it is true or not, as in the (a,b) case), leaving you with all goals solved.

[Chris Wong]

Is the obtain thing another example of rcases syntax being overly permissive? I remember a recent thread on this.

[rzeta0]

Hi @Andrew Yang - thanks for exploring obtain. The following is a quite from the MoP course which seems to suggest I do use obtain...

To write these proofs in Lean, notice the use of the tactic obtain in the injectivity problem to convert the hypothesis of a equality in a product type,
hm : (m1 + 1, 2 - m1) = (m2 + 1, 2 - m2)
to two hypotheses of equality in the two components of the product:

hm' : m1 + 1 = m2 + 1
hm'' : 2 - m1 = 2 - m2

This is consistent with how you should think about equality in a product type: two ordered pairs are equal if the two left parts are equal and the two right parts are equal. So we use the same tactic, with the same syntax, as for the logical operator “and”.
..
..
The tactic obtain is used similarly in the non-surjectivity problem to break down the hypothesis of equality in a product type
hm : (m + 1, 2 - m) = (0, 1)

Perhaps I'm reading this wrong - but I interpret it to mean that (a,b)=(c,d) should be seen as a conjunction a=c ∧ b=d and obtain can split these into two.

[Edward van de Meent]

Well, it appears that obtain does not work like this on live lean. It is true that equality of tuples behaves this way, as evidenced by docs#Prod.ext_iff, but it seems obtain is not able to get there.

[rzeta0]

Thanks Edward.

In my mind I still haven't arrived at a "beginner" yet canonical way to do this. I'll keep watching the replies.

It feels like one of those "easy things should be easy" that some languages/frameworks excel at.

[Dan Velleman]

Here's a very elementary approach. Not the quickest, but elementary:

import Mathlib.Tactic

example : (0,0) ≠ (2,1) := by
  by_contra g
  have h : 0 = 2 :=
    calc 0
      _ = (0,0).1 := by rfl
      _ = (2,1).1 := by rw[g]
      _ = 2 := by rfl
  norm_num

[Ruben Van de Velde]

An easy was is to note that if you apply a function to two values, and they give different results, the original values must also be different:

import Mathlib.Tactic

example : (0,0) ≠ (2,1) := by
  apply ne_of_apply_ne Prod.fst
  simp

[Derek Rhodes]

here's another way that just uses cases and mysteriously proves it without any actual case handling!
*edit: oops! Julian found this one first^^*

import Mathlib.Tactic

example : (0,0) ≠ (2,1) := by
  intro h
  cases h

[Edward van de Meent]

(the reason why cases and obtain solve this on live is precisely what i explained above)

[rzeta0]

do we think Lean should be enhanced to allow:

• norm_num to resolve numerically instantiated expressions like (0,1) = (0,1) and (0,1) ≠ (0,2)
• obtain to treat algebraic expressions (a,b)=(c,d) as a = c ∧ b = d

[Julian Berman]

To me neither seem immediately attractive, because in my brain this doesn't look enough like numerals to think norm_num is appropriate, and because obtain is for splitting apart structures, and equality isn't a structure. I think your definition of beginner is again too strict personally, and that the right approach here is to add decide to your toolkit, to me at least it seems very beginner friendly, it corresponds to something like "this proof is a concrete calculation, so do it and then you'll be convinced Lean".

[suhr]

I believe that beginners should be taught basics rather than fluff. From this perspective, a beginner should know how to use terms and also know some essential functions on commonly used types.

For equality such functions are rfl, Eq.subst, Eq.symm, Eq.trans, Eq.subst and congrArg. For pairs, it's Pair.fst and Pair.snd. For natural numbers, it's Nat.zero, Nat.succ, Nat.recOn and Nat.noConfusion.

It seems to be a rather unpopular opinion though, since most tutorials do not even mention congrArg.

[rzeta0]

ok - I'll take some time to learn about decide

[Chris Wong]

I don't 100% agree with @suhr, but I do think that "congruence" and "extensionality" are fundamental concepts – if you want to relate equality of a whole to equality on parts, then you should be looking for those keywords.