`lean.projNonPropFromProp`

Tried to project data from a proof.

Severity: ErrorSince: 4.23.0

This error occurs when attempting to project a piece of data from a proof of a proposition using an index projection. For example, if h is a proof of an existential proposition, attempting to extract the witness h.1 is an example of this error. Such projections are disallowed because they may violate Lean's prohibition of large elimination from Prop (refer to the Propositions manual section for further details).

Instead of an index projection, consider using a pattern-matching let, match expression, or a destructuring tactic like cases to eliminate from one propositional type to another. Note that such elimination is only valid if the resulting value is also in Prop; if it is not, the error lean.propRecLargeElim will be raised.

Examples

Attempting to use index projection on existential proof

example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > 0 :=
  ⟨Invalid projection: Cannot project a value of non-propositional type
  Nat
from the expression
  h
which has propositional type
  ∃ x, x > a + 1h.1, Nat.lt_of_succ_lt h.2⟩

Invalid projection: Cannot project a value of non-propositional type
  Nat
from the expression
  h
which has propositional type
  ∃ x, x > a + 1

example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a :=
  let ⟨w, hw⟩ := h
  ⟨w, Nat.lt_of_succ_lt hw⟩

example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a := bya:Nath:∃ x, x > a + 1⊢ ∃ x, x > a
  cases h with
  | intro w hw =>introa:Natw:Nathw:w > a + 1⊢ ∃ x, x > a
    exists wintroa:Natw:Nathw:w > a + 1⊢ w > a
    omegaAll goals completed! 🐙

The witness associated with a proof of an existential proposition cannot be extracted using an index projection. Instead, it is necessary to use a pattern match: either a term like a let binding or a tactic like cases.