Don't know how to synthesize placeholder (2)

Stream: new members

[Gareth Ma]

Hi, I am trying the follow code, but I am not sure why it says "don't know how to synthesize placeholder". Isn't the required condition in the global scope (or whatever it's called)? Also, when I click on the error, the hf : monotone f is in the context as well.

import tactic

open set
open_locale big_operators

namespace seq

variables (f : ℕ → ℕ) {hf : monotone f}
include hf

-- Property indicating a number which is the sum of subsequence of f
def summable (x : ℕ) : Prop := ∃ (S : finset ℕ), (∑ s in S, f s) = x

-- The set of subset sums is numbers which is the sum of subsequence of f
def subset_sums : set ℕ := { x : ℕ | summable f x }

[Gareth Ma]

Oh, and also writing it as @summable f hf x fixes the problem? Which makes it even more confusing, since hf is literally in the scope

[Reid Barton]

Lean doesn't try to fill placeholders with stuff from the environment, even when (as I'm assuming is the case here) it's a proposition so it could be a sensible thing to do.

[Reid Barton]

I recommend making hf explicit. Otherwise it will be annoying anyways when, eventually, you have to actually provide it somewhere.

[Gareth Ma]

Ah okay, so replace {} with () then write summable f hf x?

[Yaël Dillies]

Or simply remove it, as it's a useless assumption.

[Gareth Ma]

I need it for later lemmas

[Yaël Dillies]

Yes, but the definition doesn't need it.

[Gareth Ma]

Oh, I see what you mean now\

[Gareth Ma]

Another question, I think I am slightly confused. For the following definitions:

def complete  : Prop := ∃ (N : ℕ) (h : 0 < N), ∀ (n : ℕ) (N ≤ n), summable f n
def complete' : Prop := ∃ (N : ℕ) (h : 0 < N), ∀ (n : ℕ), N ≤ n → summable f n

Are these two definitions different? And is the second definition the correct style to write it, or is there some better syntax

[Kyle Miller]

The first one is inadvertently incorrect. If you did

def complete  : Prop := ∃ (N : ℕ) (h : 0 < N), ∀ (n : ℕ) (h : N ≤ n), summable f n

then it'd be equivalent to the second one.

Instead, it's the same as

def complete  : Prop := ∃ (N : ℕ) (h : 0 < N), ∀ (n : ℕ) (N : ℕ) (H : N ≤ n), summable f n

and that N in the for-all shadows the N from the there-exists. This is how the "cute binders" feature works when applied to (N ≤ n).

[Gareth Ma]

Oh, now I understand. No wonder my proof didn't work :P