Implicit problem

Stream: new members

[Bjørn Kjos-Hanssen]

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]

#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]

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]

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

[Bjørn Kjos-Hanssen]

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]

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]

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]

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.