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