mathematics in lean error

Stream: general

[Gihan Marasingha]

Section 3.1 of 'Mathematics in Lean' contains the code

variables {α : Type*} (r s t : set α)

example : s ⊆ s :=
by { intros x xs, exact xs }

example : s ⊆ s := λ x xs, xs

The last line causes an error in vscode and in the community web editor:

type mismatch, term
  λ (x : ?m_1) (xs : ?m_2[x]), xs
has type
  Π (x : ?m_1), ?m_2[x] → ?m_2[x]
but is expected to have type
  s ⊆ s

I don't understand why there's an error message.

@Jeremy Avigad

[Jalex Stark]

notice that the following works

import data.set.basic
variables {α : Type*} (s : set α)
example : s ⊆ s := by exact λ x xs, xs

(In case it's not clear, the difference here is that exact will use something like refl to unify the goal and the target)

[Jalex Stark]

this doesn't work

import data.set.basic
variables {α : Type*} (s : set α)
local attribute [reducible] set.subset
example : s ⊆ s := λ x xs, xs

[Jalex Stark]

and this does work

import data.set.basic
variables {α : Type*} (s : set α)

example : s ⊆ s := set.subset_def.mpr $ λ x xs, xs

[Kenny Lau]

variables {α : Type*} (s : set α)
example : s ⊆ s := λ x, id

[Jeremy Avigad]

This is a quirk of Lean's parser: example is parsed like def rather than theorem, which means that the elaborator doesn't use the statement of the theorem to elaborate the proof term. That's why exact works where the proof term doesn't. It will also work if you change example to theorem foo.

I don't remember why Leo implemented example that way, except maybe that he also wanted it to work for definitions, like example := 3. I also don't know why this example made it past the test suite, but we'll fix it. @Gihan Marasingha, thanks for the correction.

[Gihan Marasingha]

Thanks @Jeremy Avigad . This was really confusing me.

[Sebastian Ullrich]

Jeremy Avigad said:

I don't remember why Leo implemented example that way, except maybe that he also wanted it to work for definitions, like example := 3.

I would guess so as well. Fortunately it won't matter in Lean 4 because a def with a specified type will behave exactly like theorem does in Lean 3 (except for the parallelism, currently).

[Mario Carneiro]

This is a surprise to me. Not that example is parsed like def but that def ignores the expected type. Why would it do that? I would have expected that it behaves the same as def f := show s ⊆ s, from λ x xs, xs

[Sebastian Ullrich]

...good question. I hadn't looked very closely at the actual example. I don't think it completely ignores it, but there must be some subtle, probably unintended difference.

[ZHAO Jinxiang]

Section (3.3. Negation) of 'Mathematics in Lean' contains the code

import data.real.basic

-- BEGIN
example :
  ¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b :=
begin
  intro h,
  let f := λ x : ℝ, (0 : ℝ),
  have monof : monotone f,
  { intros x y h1, dsimp [f], reflexivity},
  have h' : f 1 ≤ f 0,
    dsimp [f],
    reflexivity,
  have h1: 1 ≤ 0, {
    -- exact h monof h',
    sorry,
  },
  linarith,
end
-- END

If I remove sorry and use exact h monof h',, it will told me

unnamed_1180.lean:15:10
invalid type ascription, term has type
  ?m_1 ≤ ?m_2
but is expected to have type
  1 ≤ 0
state:
h : ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b : ℝ}, f a ≤ f b → a ≤ b,
f : ℝ → ℝ := λ (x : ℝ), 0,
monof : monotone f,
h' : f 1 ≤ f 0
⊢ 1 ≤ 0

I don't understand why there's an error message.

@Jeremy Avigad

[Mario Carneiro]

The statement h1 says (1 : nat) <= 0, because there is nothing to suggest what the type should be so lean picks nat by default. Change that line to have h1: (1 : ℝ) ≤ 0,

[Bryan Gin-ge Chen]

That error message is incredibly unhelpful though.

[ZHAO Jinxiang]

@Mario Carneiro Thank you very much.

[ZHAO Jinxiang]

Is the 1 here a polymorphic 1, not nat and not real?

[Kevin Buzzard]

It's polymorphic until lean gives up on the idea that you're going to tell it which one, and then it uses nat

[ZHAO Jinxiang]

So the ?m_1 here is (1:nat)

[Mario Carneiro]

The 1 at the bottom is 1:nat, the ?m_1 at the top is ?m_1:real and that's why there is a type unification error

[Mario Carneiro]

and yes, the message is incredibly unhelpful, I only know the problem because I've seen it many times

[ZHAO Jinxiang]

I have another question about this:

import data.real.basic

-- BEGIN
example :
  ¬ ∀ {f : ℝ → ℝ}, monotone f → ∀ {a b}, f a ≤ f b → a ≤ b :=
begin
  intro h,
  let f := λ x : ℝ, (0 : ℝ),
  have monof : monotone f,
  { intros x y h1, dsimp [f], reflexivity},
  have h' : f 1 ≤ f 0,
    dsimp [f],
    reflexivity,
  -- have h1: (1:ℝ) ≤ 0,
  --   exact h monof h',
  have h'':monotone f → ∀ {a b}, f a ≤ f b → a ≤ b,
    exact h,
  have h''':∀ {a b : ℝ}, f a ≤ f b → a ≤ b,
    exact h'' monof,
  -- linarith,
end
-- END

Error message:

invalid type ascription, term has type
  f ?m_1 ≤ f ?m_2 → ?m_1 ≤ ?m_2
but is expected to have type
  ∀ {a b : ℝ}, f a ≤ f b → a ≤ b

[Floris van Doorn]

replace the line where you declare h'' by

  have h'' : monotone f → ∀ a b, f a ≤ f b → a ≤ b,

[Floris van Doorn]

The curly braces mean these are implicit arguments, so h'' monof is interpreted as @h'' monof _ _.

[Floris van Doorn]

You can also use strict implicit arguments, using {{a b}} or \{a b\}.

[Kenny Lau]

we really need {{}} to be the default behaviour

[Johan Commelin]

Can we swap the meaning of {{ }} and { } in C++?

[Johan Commelin]

That would save us a huge refactor

[Kenny Lau]

yeah that's what I mean

[Mario Carneiro]

I don't know about this. I think there are a significant fraction of { } that should be { }, compared to a small fraction where {{ }} is noticeably better or more appropriate

[Johan Commelin]

@Mario Carneiro I'm slow today. Can you give an example where {{ }} is clearly the wrong choice?

[Mario Carneiro]

Something like \forall {{x y}}, f x y = 0

[Mario Carneiro]

really anything where there are no explicit arguments after the semi implicit args

[Mario Carneiro]

because then you can't apply the semi implicit args even if you want to

[Mario Carneiro]

you would have to write @foo _ _

[Johan Commelin]

Fair enough. Personally, I wouldn't mind having these explicit.

[Johan Commelin]

For quite some time, I've been thinking that we're marking too many things implicit.

[Mario Carneiro]

For a local hypothesis that makes sense, but it is not uncommon for type arguments to be implicit like this

[Mario Carneiro]

my ballpark estimate is that today with { } default we use { } 99% of the time and prefer {{ }} about 1% of the time, while if {{ }} was the default then we would use it 90% of the time and would find reasons to use { } 10% of the time

[Johan Commelin]

I'm also talking about things like

lemma submodule.neg_mem (hx : x ∈ p) : -x ∈ p := -- x is implicit

but I realise that this is somewhat off topic in this thread.

These statements are annoying when you don't have hx yet, and -x \in p is also not exactly the expected type.

[ZHAO Jinxiang]

import data.real.basic

def fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a
def fn_has_ub (f : ℝ → ℝ) := ∃ a, fn_ub f a

open_locale classical

variable (f : ℝ → ℝ)

-- BEGIN
example (h : ¬ ∀ a, ∃ x, f x > a) : fn_has_ub f :=
begin
  push_neg at h,
  exact h
end

example (h : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a :=
begin
  simp only [fn_has_ub, fn_ub] at h,
  push_neg at h,
  exact h
end
-- END

If I change simp only [fn_has_ub, fn_ub] at h to simp only [fn_has_ub] at h,simp only [fn_ub] at h, it will told me:

unnamed_1338.lean:19:29
simplify tactic failed to simplify
state:
f : ℝ → ℝ,
h : ¬Exists (fn_ub f)
⊢ ∀ (a : ℝ), ∃ (x : ℝ), f x > a

[Kevin Buzzard]

If this is not an error in the mathematics in Lean book, can I request that we move this to a new thread?

[Jeremy Avigad]

I am doing my late-morning Zulip catch-up, so I don't know if this moved to a new thread. BA long time ago I suggested exactly this change to Leo, and he tried it and said that lots of things broke with the change. IIRC he came to the conclusion that neither was clearly the more natural default. This is not an argument against trying it again and seeing what happens. It's just a (vaguely remembered) data point.

[Floris van Doorn]

I think normal implicit is a better default, but there are plenty of cases where strict implicit is desirable. If you like to write inv_inj.mpr or more generallyany_proof_of_an_iff_without_explicit_arguments.mp, then you have a hard time with strict implicit arguments.

[DBE]

Beginner questions, I'm following the guide on this link:
https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html
using Lean "4.2.0-rc4"
1 At the end of section 5.1 there is a mention to Nat.count_factors_mul_of_pos which I can't #check, and is not used at all in the following example:

example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} (prime_p : p.Prime) :
    k ∣ r.factorization p :=

2 In this example, the prime_p hypothesis is not used in the proof (as provided in the solutions)
3 I don't understand why I can't execute

#eval factorization 20 5

The InfoView says: "failed to compile definition, consider marking it as 'noncomputable' because it depends on 'factorization', and it does not have executable code". I suspect there is a good reason for this behavior (or is a bug?) but I think the guide could make some advice to clarify.

[Ruben Van de Velde]

3. In lean, there are definitions that you can compute in the sense of #eval because there is machine code generated for them, and other definitions that you can't. factorization is one of the latter

[Patrick Massot]

DBE, could you open an issue at https://github.com/avigad/mathematics_in_lean_source about the first two points?

[DBE]

Done: https://github.com/avigad/mathematics_in_lean_source/issues/151