Underscore _x vs. x

Stream: new members

[Bjørn Kjos-Hanssen]

I never called anything _x so what is the meaning of the underscore in this error?

has type
  (λ (l : ℕ), l < k.succ) x.length
but is expected to have type
  (λ (l : ℕ), l < k.succ) _x.length

[Alex J. Best]

#mwe I would guess _x is something generated by a match and you also happen to have a variable called x or something, but it's hard to say with an example

[Bjørn Kjos-Hanssen]

Alex J. Best said:

#mwe I would guess _x is something generated by a match and you also happen to have a variable called x or something, but it's hard to say with an example

OK thanks, you're right _x is not generated by adding _ to x, as demonstrated by renaming x to xx.
Here is a MWE, it doesn't try to do anything interesting but why does it give an error?

theorem mwe (k:ℕ) (xx:list α)
(g: xx.length < k.succ):
  let σ  := {l : ℕ // l < k.succ} in
  let qx :σ := ⟨xx.length,g⟩ in
  xx = xx := sorry

[Reid Barton]

Works fine for me (once I add a declaration of \a)

[Bjørn Kjos-Hanssen]

Reid Barton said:

Works fine for me (once I add a declaration of \a)

Oops, I actually meant:

theorem mwe (k:ℕ) (xx:list α)
(g: xx.length < k.succ):
  let σ  := {l : ℕ // l < k.succ} in
  let qx :σ := ⟨xx.length,g⟩ in
  xx = xx
  :=
list.rec_on xx sorry sorry

[Reid Barton]

Well that's bizarre

[Reid Barton]

Actually it's just the location of the reported error that's wrong I think

[Reid Barton]

You can't apply list.rec_on without first reverting g

[Reid Barton]

(because g appears in the conclusion, and the type of g depends on xx)

[Bjørn Kjos-Hanssen]

What's meant by "reverting"?

[Reid Barton]

Move g after the colon, or

theorem mwe {α : Type} (k:ℕ) (xx:list α)
(g: xx.length < k.succ):
  let σ  := {l : ℕ // l < k.succ} in
  let qx :σ := ⟨xx.length,g⟩ in
  xx = xx
  :=
begin
  revert g,
  /-
  α : Type,
  k : ℕ,
  xx : list.{0} α
  ⊢ ∀ (g : xx.length < k.succ), let σ : Type := {l // l < k.succ}, qx : σ := ⟨xx.length, g⟩ in xx = xx
  -/
end

[Bjørn Kjos-Hanssen]

@Reid Barton I guess more broadly the problem is: can we not refer to an object in a theorem statement, if the type of that object relies on hypotheses of that theorem? OK so this works:

theorem really_mwe (k l:ℕ) (h: l < k):
(⟨l,h⟩: {m:ℕ//m<k}) = (⟨l,h⟩: {m:ℕ//m<k}) := sorry

[Reid Barton]

This cannot be the correct error

[Reid Barton]

Anyways, there was no problem with the theorem statement itself. The start of the proof was wrong

[Bjørn Kjos-Hanssen]

Right, sorry...

[Bjørn Kjos-Hanssen]

Well, I guess a solution is to rewrite the whole thing so that instead of referring to qx one has an existential statement: ∃ q, q.1 = xx.length ∧ ...