proof 1 ≠ 2 the hard way

Stream: lean4

[James Sully]

How do I prove 1 ≠ 2? I can always use by simp, but what about without it?

I know this is the same as 1 = 2 → False, so presumably I want something along these lines?

example : 1 ≠ 2 :=
  fun h1eq2 : 1 = 2 =>
    show False from _

[Ruben Van de Velde]

What type are your numbers?

[James Sully]

Nat

[James Sully]

let's say

[Mario Carneiro]

fun.

[Mario Carneiro]

or fun h => nomatch h

[Mario Carneiro]

one more step lower in abstraction is

example : 1 ≠ 2 :=
  fun (h : 1 = 2) =>
    Nat.noConfusion h fun (h : 0 = 1) =>
      Nat.noConfusion h

[James Sully]

Thanks! ok, the nomatch one works (I'll have to look up nomatch)

theorem oneNeqTwo : (1 : Nat) ≠ 2 :=
  fun h => nomatch h

But i'm not sure where to put that fun. syntax. This is a syntax error:

theorem oneNeqTwo : (1 : Nat) ≠ 2 :=
  fun.

[Mario Carneiro]

import Std.Tactic.NoMatch

[Mario Carneiro]

it's just syntax over nomatch , to allow empty pattern matches in match and fun

[James Sully]

unknown package 'Std'

[Mario Carneiro]

put this in your lakefile:

require std from git "https://github.com/leanprover/std4" @ "main"

[Mario Carneiro]

the lean core distribution basically only contains the compiler and facilities needed to write the compiler

[James Sully]

Ah, I see. I'm just working through Theorem Proving, so I'm not in a project, I'm just using the vscode extension on a standalone file.

[Mario Carneiro]

You will hit on limitations of that mode pretty quickly

[Mario Carneiro]

not being able to import anything being the main one

[Mario Carneiro]

You can start a lake project depending on mathlib using lake new myproj math, you will want to do that to play with more advanced library stuff

[James Sully]

makes sense.
I'm also not seeing Nat.noConfusion when I search the docs?
https://leanprover-community.github.io/mathlib4_docs/search.html?sitesearch=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib4_docs&q=Nat.noConfusion

[Mario Carneiro]

It's an automatically generated definition created for every inductive type

[Mario Carneiro]

recommended reading: https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/

[Mario Carneiro]

you can use #print Nat.noConfusion and #print Nat.noConfusionType to see the definitions

[James Sully]

Ok, cheers! Doing a quick search, it looks like it comes up in chapter 8 of Theorem Proving as well

[Kyle Miller]

Here's another alternative:

example : 1 ≠ 2 :=
  fun h1eq2 : 1 = 2 => by cases h1eq2

cases on an equality means it tries to unify the LHS and RHS since rfl is the only constructor, and cases knows how to peel off constructors and that different constructors can't be equal, so it sees 1 = 2, turns it into 0 = 1, and then knows 0 can't equal Nat.succ so recognizes the contradiction.

[Kyle Miller]

match/nomatch can do the same kinds of calculations

[Kyle Miller]

A term proof is

example : 1 ≠ 2 :=
  fun h1eq2 : 1 = 2 =>
    Nat.zero_ne_one (Nat.succ_inj'.mp h1eq2)

though these are probably proved using match or Nat.noConfusion

[Mario Carneiro]

It is worth noting that the actual proof that simp comes up with is actually a bit closer to

example : 1 ≠ 2 := Nat.ne_of_beq_eq_false rfl

taking advantage of the fact that natural number equality has a primitive implementation in the kernel. This is especially important if the proof is not about 1 ≠ 2 but rather 1000000000 ≠ 2000000000, because the methods involving noConfusion involve peeling one constructor off at a time, which would mean a billion steps to prove this

[Kevin Buzzard]

It's all very well explaining these cute hacky methods/tricks but by norm_num is really the correct answer because this is the technique which generalises. norm_num is the tactic which proves equalities and inequalities between numerals.

[James Sully]

how do I look at the term proof a tactic produces?

[Henrik Böving]

#print mytheorem

[James Sully]

ah, of course lol

[Kevin Buzzard]

You don't want to look at the term proof that norm_num produces though :-)

[Mario Carneiro]

you know, saying that is just going to make people want to look at it

[James Sully]

I'm staying away from std for the duration of this book. The book hasn't told me to use it and I assume there are pedagogical reasons not to yet

[James Sully]

or mathlib rather

[Kevin Buzzard]

Now I've found that James is a "let me look at the proof term" kind of person (ie not a mathematician) I wish I'd not opened my mouth :-)

[James Sully]

hahaha

[James Sully]

my cover's blown

[Kevin Buzzard]

Re pedagogical reasons -- it depends what you're trying to teach. "Mathematics in Lean" uses mathlib from page 1

[James Sully]

I actually started on Functional Programming in lean and then switched halfway through out of curiosity

[Kevin Buzzard]

I teach maths undergraduates lean from scratch using mathlib, but I don't teach them anything about term mode at all, or proof terms etc

[Kevin Buzzard]

It all depends on the level of abstraction you're interested in

[Mario Carneiro]

lol, I tried it and got:

example : 1 ≠ 2 := show_term by norm_num
-- Try this: of_eq_true (eq_true_of_decide (Eq.refl true))

[James Sully]

yeah, I'm more interested in the FP side and potentially bringing insights back with me to other languages

[Mario Carneiro]

which is not a norm_num proof at all

[Mario Carneiro]

using norm_num1 produces the expected horror:

example : 1 ≠ 2 := show_term by norm_num1
-- Try this: of_eq_true
--   (eq_true
--     (Mathlib.Meta.NormNum.isNat_eq_false (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1))
--       (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl false)))

[Mario Carneiro]

(which BTW is just an obfuscated version of the same proof)

[Kevin Buzzard]

James can take that insight back with them to other languages