neg_le_neg

Stream: new members

[Thomas Browning]

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.

[Kevin Buzzard]

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

[Thomas Browning]

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

[Kevin Buzzard]

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

[Thomas Browning]

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).

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

def test1 (n : ℕ) : ℤ := 37

def test2 : ∀ n : ℕ, ℤ := λ n, 37

example : test1 = test2 := rfl

Or is the issue something else?

[Kevin Buzzard]

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

[Thomas Browning]

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

[Kevin Buzzard]

leanproject up

[Kevin Buzzard]

in the root directory of your project

[Kevin Buzzard]

I think it became int.neg_le_neg by the way

[Thomas Browning]

Great! Thanks for the help!