## Stream: new members

### Topic: Implicit problem

#### Bjørn Kjos-Hanssen (Oct 21 2020 at 22:55):

I don't know why this doesn't work? The check test x is fine, so why does Lean not accept test x in the Theorem?
I could change it to test a x etc. but I want to avoid dragging around the a all the time.

variables x : ℕ

def test {a:ℕ}: ℕ → ℕ :=
λ x, a+x

#check test x

theorem triviality {x : ℕ} : test x = test x :=
sorry


#### Reid Barton (Oct 21 2020 at 22:58):

#check accepts expressions which still have metavariables--parts of the expression that Lean can't determine (yet), like the variable a here. However, they can't appear in the statements of theorems/lemmas.

#### Reid Barton (Oct 21 2020 at 22:58):

I guess this is a minimized example, since in this example it doesn't make a lot of sense to leave a implicit.

#### Bjørn Kjos-Hanssen (Oct 21 2020 at 22:59):

Right, it's a Minimal (not) Working Example

#### Bjørn Kjos-Hanssen (Oct 21 2020 at 23:00):

It's more like, imagine we have test a x, test a y, test a (x+y), ... and we get tired of writing a all the time

#### Reid Barton (Oct 21 2020 at 23:07):

When you make an argument implicit you normally expect that Lean will infer the value at the call site, so generally an implicit argument should appear again in the rest of the type somewhere.

#### Reid Barton (Oct 21 2020 at 23:08):

It sounds like you might be looking for something more like parameters, but it's hard to make a suggestion without more information about what you want to do.

#### Bjørn Kjos-Hanssen (Oct 21 2020 at 23:15):

OK thanks for the suggestion, here's a more realistic version.

def δ : ℕ → ℕ → finset ℕ → (finset ℕ → ℕ) :=
λ m, λ M,
λ A, λ B,
M * max (|A\B|) (|B\A|) + m * min (|A\B|) (|B\A|)

theorem delta_comm {m M: ℕ} {A B : finset ℕ}: δ m M A B = δ m M B A :=
have h1: max (|A\B|) (|B\A|) = max (|B\A|) (|A\B|), from max_comm (|A\B|) (|B\A|),
have h2: min (|A\B|) (|B\A|) = min (|B\A|) (|A\B|), from min_comm (|A\B|) (|B\A|),
calc δ m M A B =
M * max (|A\B|) (|B\A|) + m * min (|A\B|) (|B\A|): by tidy
... = M * max (|B\A|) (|A\B|) + m * min (|B\A|) (|A\B|): by begin rw[h1,h2] end
... = δ m M B A: by tidy


I want to prove theorems like delta_comm by just writing theorem delta_comm {m M: ℕ} {A B : finset ℕ}: δ A B = δ B A :=
or theorem delta_comm {A B : finset ℕ}: δ A B = δ B A :=
and have m and M be inferred from context.

Last updated: May 18 2021 at 17:44 UTC