## Stream: new members

### Topic: supply implicit argument?

#### abaaba (Oct 22 2021 at 02:52):

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

#### abaaba (Oct 22 2021 at 02:52):

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 (Oct 22 2021 at 02:55):

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 (Oct 22 2021 at 02:57):

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
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 (Oct 22 2021 at 02:59):

What's the error?

#### abaaba (Oct 22 2021 at 03:01):

function expected at
nat.one_div_pos_of_nat
term has type
linear_ordered_field.lt 0 (1 / (?m_3 + 1))
/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 (Oct 22 2021 at 03:03):

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 (Oct 22 2021 at 03:04):

Lean can also infer implicit arguments, like

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


should work.

#### abaaba (Oct 22 2021 at 03:04):

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 (Oct 22 2021 at 03:04):

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 (Oct 22 2021 at 03:05):

Could you give the output of the following?

#check @nat.one_div_pos_of_nat


#### Kyle Miller (Oct 22 2021 at 03:05):

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

#### abaaba (Oct 22 2021 at 03:06):

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 (Oct 22 2021 at 03:07):

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

#### Kyle Miller (Oct 22 2021 at 03:08):

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 (Oct 22 2021 at 03:09):

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 (Oct 22 2021 at 03:10):

it indeed worked :joy:

#### abaaba (Oct 22 2021 at 03:12):

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

#### Kyle Miller (Oct 22 2021 at 03:13):

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 (Oct 22 2021 at 03:14):

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

#### Patrick Massot (Oct 22 2021 at 06:31):

@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 (Oct 22 2021 at 06:32):

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

Last updated: Dec 20 2023 at 11:08 UTC