# Zulip Chat Archive

## Stream: general

### Topic: inequality proof

#### Kevin Sullivan (Sep 14 2018 at 14:24):

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

#### Kevin Sullivan (Sep 14 2018 at 14:26):

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

#### Rob Lewis (Sep 14 2018 at 14:29):

`zero_ne_one`

#### Rob Lewis (Sep 14 2018 at 14:36):

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 (Sep 14 2018 at 14:37):

dec_trivial

#### Rob Lewis (Sep 14 2018 at 14:47):

`dec_trivial`

is notation for a tactic though.

#### Kenny Lau (Sep 14 2018 at 14:48):

dec_trivial isn't a tactic

#### Rob Lewis (Sep 14 2018 at 14:49):

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

#### Kenny Lau (Sep 14 2018 at 15:01):

heh...

#### Kevin Sullivan (Sep 14 2018 at 15:04):

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 (Sep 14 2018 at 15:05):

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 (Sep 14 2018 at 15:05):

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 (Sep 14 2018 at 15:06):

This is the `no_confusion`

stuff right?

#### Reid Barton (Sep 14 2018 at 15:08):

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 (Sep 14 2018 at 15:08):

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 (Sep 14 2018 at 15:09):

I think if you look for `no_confusion`

in TPiL you might be able to find it

#### Kenny Lau (Sep 14 2018 at 15:13):

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 (Sep 14 2018 at 15:13):

also see this blogpost by kevin

#### Kenny Lau (Sep 14 2018 at 15:14):

(I followed Reid Barton's idea)

#### Kevin Sullivan (Sep 15 2018 at 03:03):

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 (Sep 15 2018 at 06:03):

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

#### Kevin Sullivan (Sep 15 2018 at 21:25):

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

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

Last updated: Dec 20 2023 at 11:08 UTC