inequality proof

Stream: general

[Kevin Sullivan]

What is the simplest exact proof term that proves ~0=1 (not zero equals one)?

[Kevin Sullivan]

I.e., without tactics complete this: theorem zneqo: not 0 = 1 := _

[Rob Lewis]

zero_ne_one

[Rob Lewis]

Oh, wait, there's a better one, although it may not count depending on what you call an "exact proof term."

theorem zneqo : ¬ (0 = 1).
#check zneqo

[Kenny Lau]

dec_trivial

[Rob Lewis]

dec_trivial is notation for a tactic though.

[Kenny Lau]

dec_trivial isn't a tactic

[Rob Lewis]

It's notation for of_as_true (by tactic.triv)

[Kenny Lau]

heh...

[Kevin Sullivan]

Right. I'm really looking for the proof term that I'd write to fill in the _. It'd presumably say something about injectivity of constructors.

[Rob Lewis]

That's what the . proof is doing under the hood. Look at the proof term it generates.

theorem zneqo : ¬ (0 = 1).
#print zneqo

[Kevin Sullivan]

Oh, wait, there's a better one, although it may not count depending on what you call an "exact proof term."

theorem zneqo : ¬ (0 = 1).
#check zneqo

Right, I'm really looking for the proof term that I'd use to fill in the _. Presumably something about injectivity of constructors. Also, where is it documented that and how Lean accepts your version?

[Reid Barton]

This is the no_confusion stuff right?

[Reid Barton]

The strategy is: you can define a function t : nat \to Prop which sends nat.zero to false and nat.succ _ to true (using nat.cases). Then if you had an equality nat.zero = nat.succ x, you could use it to transport trivial : true to a proof of false

[Rob Lewis]

It's an empty pattern match. I guess it's documented somewhere in TPiL, but I couldn't tell you where. The only proof that 0 = 1 is by rfl, but this is structurally impossible, and the equation compiler fills in the no_confusion proof automatically.

[Reid Barton]

I think if you look for no_confusion in TPiL you might be able to find it

[Kenny Lau]

prelude

inductive nat : Type
| zero : nat
| succ : nat → nat

inductive eq {α : Sort*} (x : α) : α → Sort 0
| refl : eq x

inductive false : Sort 0.

def strange_prop (n : nat) : Sort 0 :=
nat.rec_on n (eq nat.zero nat.zero) (λ n _, false)

example : (eq nat.zero (nat.succ nat.zero)) → false :=
λ H, show strange_prop (nat.succ nat.zero),
from eq.rec_on H (eq.refl nat.zero)

[Kenny Lau]

also see this blogpost by kevin

[Kenny Lau]

(I followed Reid Barton's idea)

[Kevin Sullivan]

That's what the . proof is doing under the hood. Look at the proof term it generates.

theorem zneqo : ¬ (0 = 1).
#print zneqo

Sorry, here's a better response.

First, the proof term is: λ (a : 0 = 1), eq.dcases_on a (λ (a_1 : 1 = 0), nat.no_confusion a_1) (eq.refl 1) (heq.refl a)

However, when I copy and paste it in place of the underscore, after the :=, I get the following error. Still not sure exactly what I need to type after the := as an exact proof term.

[Lean]
"eliminator" elaborator type mismatch, term
λ (a_1 : 1 = 0), nat.no_confusion a_1
has type
1 = 0 → nat.no_confusion_type (_ == _ → false) 1 0
but is expected to have type
0 = 0 → _ == _ → false
Additional information:
/Users/sullivan/teaching/2102f18/cs-dm.sullivan/06_Negation/00_intro.lean:60:40: context: the inferred motive for the eliminator-like application is
λ (_x : ℕ) (_x_1 : 0 = _x), _x = _x → _x_1 == _x_1 → false
eq.dcases_on : ∀ {α : Type} {a : α} {C : Π (a_1 : α), a = a_1 → Prop} {a_1 : α} (n : a = a_1), C a _ → C a_1 n

[Andrew Ashworth]

example : 0 ≠ 1 := λ h, nat.no_confusion h

[Kevin Sullivan]

example : 0 ≠ 1 := λ h, nat.no_confusion h

Thank you. That got me where I needed to go.