Zulip Chat Archive

Stream: new members

Topic: neg_le_neg


view this post on Zulip Thomas Browning (Jun 06 2020 at 22:47):

This code

lemma total (n : ) : 0  n  0  -n :=
(λ n, (le_total 0 n).elim (or.inl) (λ h, or.inr (neg_le_neg h)))

lemma my_neg_le_neg {a b : } : a  b  -b  -a :=
begin
exact neg_le_neg,
end

lemma my_total (n : ) : 0  n  0  -n :=
(λ n, (le_total 0 n).elim (or.inl) (λ h, or.inr (my_neg_le_neg h)))

gives this error on line 2:

type mismatch at application
  neg_le_neg h
term
  h
has type
  n  0
but is expected to have type
  ?m_3  ?m_4

but if I use my own version of neg_le_neg then there is no error. Why is this?

The error seems strange because n ≤ 0 seems like it actually does have type ?m_3 ≤ ?m_4.

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 23:09):

I get unknown identifier neg_le_neg. Can you post fully working code?

view this post on Zulip Thomas Browning (Jun 06 2020 at 23:21):

Ok, so it looks like I found a way to resolve the error. The problem was the lambda. This code:

lemma my_total (n : ) : 0  n  0  -n :=
(le_total 0 n).elim (or.inl) (λ h, or.inr (neg_le_neg h))

works with no errors (in an empty lean file). However, I'm still confused as to why this code (in an empty lean file):

lemma my_total (n : ) : 0  n  0  -n :=
(λ n, (le_total 0 n).elim (or.inl) (λ h, or.inr (neg_le_neg h)))

produces the error

type mismatch at application
  neg_le_neg h
term
  h
has type
  n  0
but is expected to have type
  ?m_3  ?m_4

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 23:24):

Which version of Lean are you using? I am still getting unknown identifier 'neg_le_neg'

view this post on Zulip Thomas Browning (Jun 06 2020 at 23:26):

I'm not exactly sure (maybe 3.11.0?). The "neg_le_neg" is coming from .elan/toolchains/leanprover-community-lean-3.11.0/lib/lean/library/init/algebra/ordered_group.lean (but it doesn't seem to require an import for me).

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 23:27):

Oh there have been a lot of changes to core since 3.11

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 23:28):

But anyway, is the problem with your my_total thing the fact that you have a random lambda n in the term, but you have put the n before the colon when defining the type?

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 23:29):

def test1 (n : ) :  := 37

def test2 :  n : ,  := λ n, 37

example : test1 = test2 := rfl

Or is the issue something else?

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 23:30):

init/algebra got ripped out of core around 3.13 by the way

view this post on Zulip Thomas Browning (Jun 06 2020 at 23:31):

That looks like the issue. Thanks! Is there a reference for getting the most recent version of lean/mathlib?

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 23:32):

leanproject up

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 23:32):

in the root directory of your project

view this post on Zulip Kevin Buzzard (Jun 06 2020 at 23:33):

I think it became int.neg_le_neg by the way

view this post on Zulip Thomas Browning (Jun 06 2020 at 23:51):

Great! Thanks for the help!


Last updated: May 16 2021 at 05:21 UTC