# Zulip Chat Archive

## 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 apply (int.lt_add_one_of_le (int.le_of_lt int.zero_lt_one)) 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 apply (int.lt_add_one_of_le (int.le_of_lt int.zero_lt_one)) 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.

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

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

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

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 -- @has_lt.lt nat nat.has_lt 0 (@has_add.add nat nat.has_add 1 1) : Prop

#### 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