Zulip Chat Archive
Stream: new members
Topic: don't know how to synthesize placeholder
Michael Beeson (Jun 29 2020 at 22:35):
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 (Jun 29 2020 at 22:39):
It means Lean has no way to infer M
.
Patrick Massot (Jun 29 2020 at 22:40):
One way to fix it is to write lemma test: Rel (p44 : M)
.
Michael Beeson (Jun 29 2020 at 22:43):
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 (Jun 29 2020 at 22:44):
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 (Jun 29 2020 at 22:48):
It's not about Lean. That lemma that you wrote never mention M
anywhere!
Patrick Massot (Jun 29 2020 at 22:49):
And if you add p44
to your list of variable it simply shadows what you have from ExampleClass
.
Patrick Massot (Jun 29 2020 at 22:51):
It doesn't say "don't know how to infer the type of a variable" because that's not the issue.
Patrick Massot (Jun 29 2020 at 22:51):
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 (Jun 29 2020 at 22:55):
Rel p44 is just a Prop. It can't see M any more
Michael Beeson (Jun 29 2020 at 23:59):
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 (Jun 30 2020 at 00:13):
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 (Jun 30 2020 at 00:16):
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 (Jun 30 2020 at 00:17):
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 (Jun 30 2020 at 00:20):
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 (Jun 30 2020 at 00:20):
when adding the type annotation, you tell lean that M' = M
Marc Huisinga (Jun 30 2020 at 00:30):
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 (Jun 30 2020 at 00:31):
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 (Jun 30 2020 at 00:39):
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 (Jun 30 2020 at 00:41):
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 (Sep 24 2024 at 11:20):
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 (Sep 24 2024 at 11:21):
Do excuse the long code snippet, I don't really know how to minimize this.
Violeta Hernández (Sep 24 2024 at 11:22):
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 (Sep 24 2024 at 11:29):
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 (Sep 24 2024 at 11:33):
Hmm, apparently not
Edward van de Meent (Sep 24 2024 at 11:34):
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 (Sep 24 2024 at 11:34):
to see that there is a metavariable ?refine_2
Edward van de Meent (Sep 24 2024 at 11:35):
actually it looks like multiple metavariables?
Edward van de Meent (Sep 24 2024 at 11:40):
adding a line case hn => sorry
after the apply groupBy_append
seems to fix things?
Edward van de Meent (Sep 24 2024 at 11:41):
somehow the second proof clause seems to be unhygenic?
Mauricio Collares (Sep 24 2024 at 11:42):
(deleted)
Violeta Hernández (Sep 24 2024 at 11:45):
Edward van de Meent said:
adding a line
case hn => sorry
after theapply groupBy_append
seems to fix things?
That's odd... why wouldn't it just add that to my goals?
Edward van de Meent (Sep 24 2024 at 11:45):
it did, but the second case seems to remove it...
Edward van de Meent (Sep 24 2024 at 11:45):
i'm guessing that somehow · cases
is unhygienic
Violeta Hernández (Sep 24 2024 at 11:47):
cases'
has the same problem.
Violeta Hernández (Sep 24 2024 at 11:48):
As does match
Edward van de Meent (Sep 24 2024 at 11:49):
fwiw, here's a proof for that case:
case hn =>
simp only [ne_eq, replicate_eq_nil]
exact hn.ne.symm
Mauricio Collares (Sep 24 2024 at 11:50):
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 (Sep 24 2024 at 11:51):
they are added in order, and the list of goals is stack-like?
Mauricio Collares (Sep 24 2024 at 11:52):
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 (Sep 24 2024 at 11:52):
ha
depends on both h
and hn
, so I don't fully get why it appears as the middle one
Edward van de Meent (Sep 24 2024 at 11:54):
anyhow, i expect this is worth making an issue, as well as maybe asking around in #lean4 ?
Edward van de Meent (Sep 24 2024 at 12:03):
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 (Sep 24 2024 at 12:06):
nope, removing the ·
doesn't fix it...
Edward van de Meent (Sep 24 2024 at 12:15):
after some experimenting, i'm starting to think that maybe the apply
is at fault here...
Edward van de Meent (Sep 24 2024 at 12:17):
but i still don't know exactly what's going on here.
Damiano Testa (Sep 24 2024 at 12:37):
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
Last updated: May 02 2025 at 03:31 UTC