## Stream: new members

### Topic: 0 < 1 + 1

#### Nicolás Ojeda Bär (Oct 12 2019 at 15:11):

I try to prove 0 < 1 + 1 with

example : 0 < 1 + 1 :=
begin
end


I get:

invalid apply tactic, failed to unify
0 < 1 + 1
with
0 < 1 + 1
state:
⊢ 0 < 1 + 1


?? Thanks!

#### Patrick Massot (Oct 12 2019 at 15:12):

By default, Lean thinks numerals are natural numbers, not integers

#### Mario Carneiro (Oct 12 2019 at 15:12):

the theorem statement is about nat, but the theorems you are applying are about ints

#### Patrick Massot (Oct 12 2019 at 15:12):

Ha! I was faster than Mario! :tada:

#### Nicolás Ojeda Bär (Oct 12 2019 at 15:12):

OK, got it ... I guess I have to look in the nat namespace then, right?

#### Bryan Gin-ge Chen (Oct 12 2019 at 15:13):

You can also coerce the numerals to ints:

example : (0 : ℤ) < 1 + 1 :=
begin
end


#### Mario Carneiro (Oct 12 2019 at 15:13):

there is a tactic norm_num for solving problems like this

#### Patrick Massot (Oct 12 2019 at 15:13):

That was my next message.

#### Patrick Massot (Oct 12 2019 at 15:13):

and the next one.

#### Mario Carneiro (Oct 12 2019 at 15:13):

dec_trivial will also work here

#### Patrick Massot (Oct 12 2019 at 15:13):

I spent too much time celebrating my first successful race.

lol

#### Mario Carneiro (Oct 12 2019 at 15:15):

import tactic.norm_num

example : 0 < 1 + 1 :=
nat.lt_succ_of_lt nat.zero_lt_one

example : 0 < 1 + 1 := dec_trivial

example : 0 < 1 + 1 := by norm_num


Thanks!

#### Mario Carneiro (Oct 12 2019 at 15:19):

Note that some theorems about nat are generic and don't have a prefix, like le_of_lt (there is no nat.le_of_lt)

#### Mario Carneiro (Oct 12 2019 at 15:20):

only theorems that are "uniquely about nat" have a nat prefix

#### Mario Carneiro (Oct 12 2019 at 15:21):

int.le_of_lt is an exception because it is used for bootstrapping before le_of_lt is available

#### Nicolás Ojeda Bär (Oct 12 2019 at 15:25):

Is there a way I can tell Lean to print some type annotations so that I can see the difference between nat and int ?

#### Mario Carneiro (Oct 12 2019 at 15:25):

not without it getting a lot uglier

#### Mario Carneiro (Oct 12 2019 at 15:26):

set_option pp.notation false
set_option pp.implicit true
#check 0 < 1 + 1


#### Patrick Massot (Oct 12 2019 at 15:26):

In that specific case, you could use set_option pp.numerals false, but only because we are talking about numerals.

#### Mario Carneiro (Oct 12 2019 at 15:27):

set_option pp.numerals false
#check 0 < 1 + 1
-- has_zero.zero ℕ < has_one.one ℕ + has_one.one ℕ : Prop


#### Nicolás Ojeda Bär (Oct 12 2019 at 15:29):

OK, got it. Another question : what is the simplest way of lifting properties (eg inequalities) about N to with_bot N ?

#### Patrick Massot (Oct 12 2019 at 15:30):

Could you give a specific example lemma?

#### Nicolás Ojeda Bär (Oct 12 2019 at 15:33):

For example, given the proof of 0 < 1 + 1 (for nat), I need it to apply to elements of with_bot nat.

#### Kenny Lau (Oct 12 2019 at 15:33):

example : 0 < 1 + 1 := by right; left


#### Mario Carneiro (Oct 12 2019 at 15:40):

that depends on how you have 0 and 1+1 expressed in with_bot nat

#### Mario Carneiro (Oct 12 2019 at 15:41):

but it's probably also dec_trivial

#### Kevin Buzzard (Oct 12 2019 at 15:41):

I just did an hour of marking so was in a grumpy mood, and then I popped back here just before going out and 20 seconds later was laughing out loud.

#### Reid Barton (Oct 12 2019 at 15:47):

by repeat { constructor } is a vast generalization of Kenny's proof

#### Rob Lewis (Oct 12 2019 at 15:49):

by repeat { constructor } is a vast generalization of Kenny's proof

But it sounds much less like a dance move.

#### Reid Barton (Oct 12 2019 at 15:51):

True, I hadn't thought about the choreographic interpretation of constructive type theory

#### Patrick Massot (Oct 12 2019 at 16:13):

Returning to the with_bot. There is a principled way to deal with those kind of things, using norm_cast but it seems the relevant tagging has not been done for with_bot. You can write:

import tactic
import algebra.ordered_group

variables {α : Type*}
@[elim_cast] lemma with_bot.coe_one' [has_one α] : (1 : with_bot α) = ((1 : α) : with_bot α) := rfl

@[elim_cast] lemma with_bot.coe_zero' [add_monoid α] : (0 : with_bot α) = ((0 : α) : with_bot α) := rfl

@[move_cast] lemma with_bot.add_coe' {α : Type*} [add_semigroup α] (a b : α) :
((a + b : α) : with_bot α) = (a : with_bot α) + b := rfl
attribute [elim_cast] with_bot.coe_lt_coe

example : (0 : with_bot ℕ) < 1 + 1 :=
begin
norm_cast,
norm_num,
end


But everything before the example should be in mathlib (feel free to open a PR!)

#### Floris van Doorn (Oct 12 2019 at 19:51):

True, I hadn't thought about the choreographic interpretation of constructive type theory

Is that the Choreo-Howard interpretation?

Last updated: Dec 20 2023 at 11:08 UTC