## Stream: new members

### Topic: Underscore _x vs. x

#### Bjørn Kjos-Hanssen (Jul 20 2022 at 19:25):

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 (Jul 20 2022 at 19:33):

#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 (Jul 20 2022 at 19:49):

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 (Jul 20 2022 at 19:51):

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

#### Bjørn Kjos-Hanssen (Jul 20 2022 at 19:52):

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 (Jul 20 2022 at 19:55):

Well that's bizarre

#### Reid Barton (Jul 20 2022 at 19:58):

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

#### Reid Barton (Jul 20 2022 at 19:59):

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

#### Reid Barton (Jul 20 2022 at 20:00):

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

#### Bjørn Kjos-Hanssen (Jul 20 2022 at 20:10):

What's meant by "reverting"?

#### Reid Barton (Jul 20 2022 at 20:15):

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 (Jul 20 2022 at 20:25):

@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 (Jul 20 2022 at 20:26):

This cannot be the correct error

#### Reid Barton (Jul 20 2022 at 20:27):

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

Right, sorry...

#### Bjørn Kjos-Hanssen (Jul 20 2022 at 20:42):

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 ∧ ...

Last updated: Dec 20 2023 at 11:08 UTC