0 < 1 + 1

Stream: new members

[Nicolás Ojeda Bär]

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]

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

[Mario Carneiro]

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

[Patrick Massot]

Ha! I was faster than Mario! :tada:

[Nicolás Ojeda Bär]

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

[Bryan Gin-ge Chen]

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]

there is a tactic norm_num for solving problems like this

[Patrick Massot]

That was my next message.

[Patrick Massot]

and the next one.

[Mario Carneiro]

dec_trivial will also work here

[Patrick Massot]

I spent too much time celebrating my first successful race.

[Mario Carneiro]

lol

[Mario Carneiro]

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]

Thanks!

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Nicolás Ojeda Bär]

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]

not without it getting a lot uglier

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Nicolás Ojeda Bär]

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

[Patrick Massot]

Could you give a specific example lemma?

[Nicolás Ojeda Bär]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

but it's probably also dec_trivial

[Kevin Buzzard]

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]

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

[Rob Lewis]

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

But it sounds much less like a dance move.

[Reid Barton]

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

[Patrick Massot]

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]

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

Is that the Choreo-Howard interpretation?