Kernel Invalid Projection

Stream: lean4

[Gareth Ma]

Can someone help with this error?

-- (kernel) invalid projection h.2
example (h : ∃ _ : ℕ, P) : P := h.2

-- works
example (h : ∃ _ : ℕ, P) : P := by
  let ⟨_, P⟩ := h
  exact P

[Timo Carlin-Burns]

I think I understand the reason behind this error. p.2 usually means applying some function to p to extract the second value (e.g. Prod.snd), but there can't in general be such a function for ∃ x : α, p x.

set_option autoImplicit false

def extractSecond {α : Type _} (p : Nat × α) : α := p.2
-- `.2` really means applying the function `Prod.snd`
#check Prod.snd -- α × β → β
#print extractSecond -- fun {α} p => p.snd

-- The only way of extracting the second value from an `Exists` is by
-- supplying a function which will take it as an input.
#check Exists.elim -- (∃ x, p x) → (∀ x, p x → b) → b

-- There couldn't be a general `Exists.snd` function, because we don't know what type it should return.
def Exists.snd {α : Type _} {p : α → Prop}: (∃ x, p x) → p x := -- error: unknown identifier `x`
  sorry

[Gareth Ma]

Ah I think that makes sense

[Gareth Ma]

(deleted)

[Gareth Ma]

So what I wrote (P "not dependent on x") is actually what you wrote, where P is, because x is in the local context? Will that be correct

[Timo Carlin-Burns]

I'm not sure I understand the question. Where is x is the local context?

[Timo Carlin-Burns]

If you're asking why it works with let, yeah, given h : ∃ x, p x, the let ⟨x, h'⟩ := h syntax puts x in the local context so h' : p x will be clearly well-typed

[Timo Carlin-Burns]

In your case you're right that P not does not depend on x. You could make an Exists.snd function which works for such non-dependent cases

-- Note: `p` is `Prop`, not `α → Prop`
def Exists.snd {α : Type _} {p : Prop} (h : (∃ x : α, p)) : p := Exists.elim h fun x h' => h'

[Alex J. Best]

Any error with "kernel" in is normally considered a bug in the elaborator letting it get that far. I'd suggest opening a Lean 4 issue for this example

[Gareth Ma]

Ah okay :)

[Alex Keizer]

You can define an Exists.snd perfectly fine, just have it use Exists.fst to refer to the witness (i.e., x), reflecting the dependent nature. In fact, https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Basic.html#Exists.snd does exist in Mathlib

[Timo Carlin-Burns]

Looks like Exists.snd is only defined for ∃ x : b, p b where b : Prop

[Anatole Dedecker]

That’s because its type mentions Exists.fst, which can’t exist if b is not a proposition (you’d have to use docs#Classical.choose). That’s probably also why the .2 notation fails.

[Alex Keizer]

Ah, apologies. I thought Exists.fst could be defined so long as it is marked noncomputable, but that turns out not to be true