supply implicit argument?

Stream: new members

[abaaba]

nat.one_div_pos_of_nat {n : ℕ} : 0 < 1 / (n + 1 : ℝ), the only argument is implicit. How should I use it?

[abaaba]

have triv : 0 < 1 / (N + 1) := by nat.one_div_pos_of_nat N, doesn't work, neither does have triv : 0 < 1 / (N + 1) := by nat.one_div_pos_of_nat,

[Kevin Buzzard]

Kill the by, you don't want to be in tactic mode if you're supplying the term. And in general we prefer #mwe s in questions because it reduces confusion overall

[abaaba]

i think it's still not working ... This is the 0074 from tutorial

-- 0074
example :
  (∀ u : ℕ → ℝ, seq_limit u x₀ → seq_limit (f ∘ u) (f x₀)) →
  continuous_at_pt f x₀ :=

begin
  -- if forall sequence approaching x0, f(u) approaches f(x0),
  -- then f is continuous at x0
  by_cases x₀ > 0, {
    intro h,
    unfold seq_limit at *,
    unfold continuous_at_pt at *,
    intros ε εg0,
    set u: ℕ -> ℝ := λ(n:ℕ), ((x₀ + 1 / (n + 1)):ℝ) with hu, -- STAR have forget definition, only declaration
    -- it remains to show seq_limit u x0
    have premise := limit_const_add_inv_succ x₀,
    specialize h u premise ε εg0,
    --  nat.one_div_pos_of_nat {n : ℕ} : 0 < 1 / (n + 1 : ℝ)
    -- inv_succ_le_all :  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1/(n + 1 : ℝ) ≤ ε
    cases h with N h,
    unfold seq_limit at premise,
    use u N, split,
      rw hu,
      have triv: 0 < 1 / (N + 1) := nat.one_div_pos_of_nat N,
  }
end

[Kevin Buzzard]

What's the error?

[abaaba]

function expected at
  nat.one_div_pos_of_nat
term has type
  linear_ordered_field.lt 0 (1 / (?m_3 + 1))
Additional information:
/tutorials/src/my_exercises/exercises/09_limits_final.lean:219:36: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments

[Kyle Miller]

If you want to explicitly give an implicit argument, put @ before the name of the function/theorem. For example, @nat.one_div_pos_of_nat N.

[Kyle Miller]

Lean can also infer implicit arguments, like

have triv: 0 < 1 / (N + 1) := nat.one_div_pos_of_nat

should work.

[abaaba]

Kyle Miller said:

If you want to explicitly give an implicit argument, put @ before the name of the function/theorem. For example, @nat.one_div_pos_of_nat N.

this fails with

type mismatch at application
  nat.one_div_pos_of_nat
term
  N
has type
  ℕ : Type
but is expected to have type
  Type ? : Type (?+1)

[abaaba]

Kyle Miller said:

Lean can also infer implicit arguments, like

have triv: 0 < 1 / (N + 1) := nat.one_div_pos_of_nat

should work.

this fails with

invalid type ascription, term has type
  0 < 1 / (?m_3 + 1)
but is expected to have type
  0 < 1 / (N + 1)

[Kyle Miller]

Could you give the output of the following?

#check @nat.one_div_pos_of_nat

[Kyle Miller]

(Put this on a line outside the theorem you're proving.)

[abaaba]

Kyle Miller said:

Could you give the output of the following?

#check @nat.one_div_pos_of_nat

nat.one_div_pos_of_nat : ∀ {α : Type u_1} [_inst_1 : linear_ordered_field α] {n : ℕ}, 0 < 1 / (n + 1)

[Kyle Miller]

Ok, so this is saying it has three implicit arguments, not just one, which is what caused the earlier type mismatch.

[Kyle Miller]

Let's ignore that for a moment, since I expect this should work:

have triv: 0 < 1 / (N + 1 : ℝ) := nat.one_div_pos_of_nat

(Sorry I haven't tried it.)

[Kyle Miller]

I think the problem was that N + 1 is a natural number by default, but we need to tell Lean we expect it to be a real number.

[abaaba]

it indeed worked :joy:

[abaaba]

and also the @nat.one_div_pos_of_nat _ _ N worked too once the :\R added to 1 + N

[Kyle Miller]

Yep, Lean is solving for that N automatically in the implicit version. You should also be able to put \R in for the first underscore if you wanted to be more explicit.

[Kyle Miller]

(or if you wanted to write have triv := @nat.one_div_pos_of_nat ℝ _ N))

[Patrick Massot]

@abaaba all those explanations are good to know, but the intended use in the tutorial is to write

have triv: 0 < 1 / (N + 1 : ℝ) := nat.one_div_pos_of_nat,

as in the indication.

[Patrick Massot]

That being said, nat.one_div_pos_of_nat should have n as an explicit argument. The library should be fixed.