Missing something fundamental about Props

Stream: lean4

[Björn W]

I'm trying to understand Prop a little better. Let's say I'm trying to prove something about a Vector ℕ p where Nat.prime p. In my proof, I need to pop off the first element in the Vector. Something like this:

theorem test123 (p : ℕ) (hp: Nat.Prime p) :
  p ≥ 0 := by

  let X := {x : Vector ℕ p | p ≥ 0}

  have : ∀ x ∈ X, x.head ≥ 0 := by
    sorry

This gives the following error on x.head:

failed to synthesize
  NeZero p

So I tried the following:

theorem test123 (p : ℕ) (hp: Nat.Prime p) :
  p ≥ 0 := by

  let X := {x : Vector ℕ p | p ≥ 0}

  have : NeZero p := by
    apply Nat.Prime.ne_zero at hp -- gives hp : p ≠ 0
    --exact hp doesn't work here, for example (neither does simp, linarith)
    sorry

  have : ∀ x ∈ X, x.head ≥ 0 := by
    sorry

This makes the x.head error disappear, but I'm not able to prove NeZero p.

Looking at the definition of NeZero:

/-- A type-class version of `n ≠ 0`.  -/
class NeZero (n : R) : Prop where
  /-- The proposition that `n` is not zero. -/
  out : n ≠ 0

My assumption was that I could show that p ≠ 0 and that this would be enough to get NeZero p. My approach is what's typical in mathematics that one shows that the object of interest satisfies some property, but I have a feeling this is maybe not the correct course of action in Lean?

[Aaron Liu]

docs#neZero_iff

[Aaron Liu]

You can also use NeZero.mk

[Björn W]

Thanks, this solves the immediate issue, but I'm still confused about Props.

Ideally, I'd like to turn the goal NeZero p into p ≠ 0 and work from there, but maybe this is not possible? (I'm asking since I'm sure I will run into a similar situation again but with a different Prop)

[Damiano Testa]

Is using the tactic constructor an answer to your question?

[Björn W]

Yes, this works, thank you!

[Damiano Testa]

The NeZero class creates a (small) barrier between the structure itself and what it contains.

[Damiano Testa]

In this case, the proof that something is non-zero is inside the barrier and constructor "pulls it out".