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