don't know how to synthesize placeholder

Stream: new members

[Michael Beeson]

Here is a short code sample that generates the error message in the post's title. Why does it
generate this message, and how do I get rid of it?

class  ExampleClass (M:Type) :=
(Rel: M →  Prop)
(p44:M)

variables (M:Type) [ExampleClass M] (a b x y z: M)
open ExampleClass

lemma test: (Rel  p44) :=
  begin
    sorry,
  end

[Patrick Massot]

It means Lean has no way to infer M.

[Patrick Massot]

One way to fix it is to write lemma test: Rel (p44 : M).

[Michael Beeson]

Yes, that worked, and also, if I add p44 to the list of variables of type M that works too.
"Lean has no way to infer that M is the type of p44" or
"Lean has no way to infer the type of p44"
There's really no other possibility in sight... but I see now what Lean needs, thank you.

[Michael Beeson]

What is the meaning of "placeholder" here? Why doesn't it say "don't know how to infer the type of a variable" ?

[Patrick Massot]

It's not about Lean. That lemma that you wrote never mention M anywhere!

[Patrick Massot]

And if you add p44 to your list of variable it simply shadows what you have from ExampleClass.

[Patrick Massot]

It doesn't say "don't know how to infer the type of a variable" because that's not the issue.

[Patrick Massot]

Maybe we could help you more if you could tell more about what you actually want to do. Maybe you minimized so much that it became meaningless.

[Kevin Buzzard]

Rel p44 is just a Prop. It can't see M any more

[Michael Beeson]

OK, then, I haven't understood what IS the issue. I still don't know what "placeholder means" . I thought that
"open ExampleClass" would mean that I could mention p44 and Lean would understand it as the p44 declared in ExampleClass to be of type M. So the lemma doesn't contain "M" literally but it does contain p44, which is declared in ExampleClass to be of type M. Something is wrong, that is fixed by explicitly saying (p44:M) instead of just p44, but I'm told inferring the type of a variable is not the issue. Well, I would like to understand exactly what is going on here....

[Alex J. Best]

If there is some information (a type or a term) that you don't want to provide explicitly, you can often write an "_" to signify that you want lean to try and work out what should go in place of "_" by its own. This is useful as sometimes what should go in the space is long or boring to work out, but clear from context, for example I can do this

example : 1 + 2 = 2 + 1 :=
begin
  exact add_comm _ _,
end

I could have written add_comm 1 2 but then I'd have to remember which way around the 1 and 2 should go in add_comm. This underscore is an explicit placeholder, by using a placeholder instead lean can work out what should go in the underscore for this to work.

Now in your example you haven't written any underscore explicitly, but there is information which is left implicit, and to lean there are terms which are left as placeholders, so lean has too try and work it out, but cannot, hence it complains that it can't fill in the blank (which is implicitly there).

[Alex J. Best]

You could think of it as if you wrote

lemma test: ((Rel : _ → Prop) (p44 : _)) :=
  begin
    sorry,
  end

those types are the placeholders lean can't fill. In most situations its okay not to write explicitly the type of everything all the time, just not in this situation!

[Marc Huisinga]

if i am understanding correctly:
variables are not passed to every function/lemma, only those that reference something of that name.
so in your definition of test, lean will look at Rel and p44, the type of which reference some type M'. because you're never referencing M anywhere in your lemma, M is not a parameter to test, and lean will not know that you want M for M', and hence it will yield an error.

[Marc Huisinga]

note that even adding M to the parameter list will still yield an error, because lean isn't sure whether M is the M' that you want

[Marc Huisinga]

when adding the type annotation, you tell lean that M' = M

[Marc Huisinga]

i think it says placeholder instead of missing type because placeholder is a more general concept that might also apply to other things like terms.

patrick's comment about it not being about lean refers to the first step with variables i mentioned: lean can't even take a stab at figuring out that the type is M because M does not appear in the parameter list when it is not mentioned. once you explicitly add it to the parameter list, lean still complains, but this time because it doesn't just nilly-willy want to assume that M' = M :)

[Michael Beeson]

So, the parameter M:Type that is mentioned in the class definition doesn't get passed automatically with the members of the class, in this case Rel and p44. I need to mention M in defining test. When I've successfully defined test, and I want to use it, I have to pass M as the first argument, e.g. test M. Then it's the passed M that will be used as the type of p44. That explains why you have to pass M as an argument to test. Are these statements correct?

[Alex J. Best]

Well the parameter M is exactly that a parameter, it could vary if you had

variables (M:Type) [ExampleClass M] (a b x y z: M)
variables (N:Type) [ExampleClass N]
open ExampleClass

lemma test: Rel p44 :=
  begin
    sorry,
  end

lean can't tell if you want the Rel and p44 from ExampleClass M or from ExampleClass N.

[Alex J. Best]

If test was enough to specify M it wouldn't be necessary to tell it: e.g. if you had

lemma test: p44 =x:=
  begin
    sorry,
  end

it works fine as x is of type M so lean knows what p44's type should be

[Violeta Hernández]

I've run into a very odd problem... I've got no idea what's causing this

import Mathlib.Order.TypeTags
import Mathlib.Data.List.Chain

variable {α : Type*} [DecidableEq α]

namespace List

theorem ne_nil_of_mem_groupBy (r : α → α → Bool) {l m : List α} (h : m ∈ l.groupBy r) : m ≠ [] := sorry

theorem groupBy_append {r : α → α → Bool} {l m : List α} (hn : l ≠ [])
    (h : l.Chain' fun x y ↦ r x y) (ha : ∀ h : m ≠ [], r (l.getLast hn) (m.head h) = false) :
    (l ++ m).groupBy r = l :: m.groupBy r := sorry

theorem chain'_replicate (n : ℕ) (a : α) : Chain' (· = ·) (replicate n a) := sorry

/-- Run-length encoding of a list. Returns a list of pairs `(n, a)` representing consecutive groups
of `a` of length `n`. -/
def RunLength (l : List α) : List (ℕ+ × α) :=
  ((l.groupBy (· == ·)).attachWith _ (fun _ ↦ ne_nil_of_mem_groupBy _)).map
    fun m ↦ (⟨m.1.length, length_pos_of_ne_nil m.2⟩, m.1.head m.2)

theorem runLength_append {n : ℕ} (hn : 0 < n) {a : α} {l : List α} (ha : a ∉ l.head?) :
    (replicate n a ++ l).RunLength = (⟨n, hn⟩, a) :: l.RunLength := by
  suffices groupBy (· == ·) (replicate n a ++ l) = replicate n a :: l.groupBy (· == ·) by
    simp [this, RunLength, attachWith]
  apply groupBy_append
  · simp_rw [beq_iff_eq]
    exact chain'_replicate n a
  · cases l with
    | nil => simp
    | cons b l =>
      rw [Option.mem_def, eq_comm] at ha
      simpa using ha

end List

[Violeta Hernández]

Do excuse the long code snippet, I don't really know how to minimize this.

[Violeta Hernández]

I've usually seen this placeholder error when some theorem accidentally has an unused variable. I don't really see how that's the case here, though.

[Mauricio Collares]

Probably something to do with the use of == and lean4#2038 (i.e. DecidableEq does not give you a good BEq instance by default)

[Mauricio Collares]

Hmm, apparently not

[Edward van de Meent]

actually, i think it might be because there somehow is a metavariable in the proof?
replace the suffices with

let this: (groupBy (fun x y => x == y) (replicate n a ++ l : List α): List (List α)) = (replicate n a :: l.groupBy (fun x y => x == y) : List (List α)):=  by

    apply groupBy_append
    · simp_rw [beq_iff_eq]
      exact chain'_replicate n a
    · cases l with
      | nil => simp
      | cons b l =>
        rw [Option.mem_def, eq_comm] at ha
        simpa using ha
  ```

[Edward van de Meent]

to see that there is a metavariable ?refine_2

[Edward van de Meent]

actually it looks like multiple metavariables?

[Edward van de Meent]

adding a line case hn => sorry after the apply groupBy_append seems to fix things?

[Edward van de Meent]

somehow the second proof clause seems to be unhygenic?

[Mauricio Collares]

(deleted)

[Violeta Hernández]

Edward van de Meent said:

adding a line case hn => sorry after the apply groupBy_append seems to fix things?

That's odd... why wouldn't it just add that to my goals?

[Edward van de Meent]

it did, but the second case seems to remove it...

[Edward van de Meent]

i'm guessing that somehow · cases is unhygienic

[Violeta Hernández]

cases' has the same problem.

[Violeta Hernández]

As does match

[Edward van de Meent]

fwiw, here's a proof for that case:

 case hn =>
    simp only [ne_eq, replicate_eq_nil]
    exact hn.ne.symm

[Mauricio Collares]

I don't understand the ordering of the goals produced by apply. The parameter order for groupBy_append is hn, h, ha. Why are the goals ordered as h, ha, hn?

[Edward van de Meent]

they are added in order, and the list of goals is stack-like?

[Mauricio Collares]

I had a typo originally, sorry. The order produced by apply is a cyclic permutation of the original ordering, not just the reverse order.

[Mauricio Collares]

ha depends on both h and hn, so I don't fully get why it appears as the middle one

[Edward van de Meent]

anyhow, i expect this is worth making an issue, as well as maybe asking around in #lean4 ?

[Edward van de Meent]

i think the issue is that somehow simpa and simp both fill in the proof of hn, however the · makes it so the term eventually isn't filled in?

[Edward van de Meent]

nope, removing the · doesn't fix it...

[Edward van de Meent]

after some experimenting, i'm starting to think that maybe the apply is at fault here...

[Edward van de Meent]

but i still don't know exactly what's going on here.

[Damiano Testa]

It seems that someone is not recovering goals gracefully:

theorem runLength_append {n : ℕ} (hn : 0 < n) {a : α} {l : List α} (ha : a ∉ l.head?) :
    (replicate n a ++ l).RunLength = (⟨n, hn⟩, a) :: l.RunLength := by
  suffices groupBy (· == ·) (replicate n a ++ l) = replicate n a :: l.groupBy (· == ·) by
    simp [this, RunLength, attachWith]
  apply groupBy_append
  · simp_rw [beq_iff_eq]
    exact chain'_replicate n a
  recover
    cases l with
      | nil =>
        simp
      | cons b l =>
        rw [Option.mem_def, eq_comm] at ha
        simpa using ha
  -- recovered goal
  intros
  simpa using Nat.not_eq_zero_of_lt hn