关于：`propRecLargeElim`🔗

Error code: lean.propRecLargeElim

Attempted to eliminate a proof into a higher type universe.

Severity: ErrorSince: 4.23.0

当尝试将命题证明消去到更高的类型宇宙时，会产生此错误。由于 Lean 的类型论不允许从 Prop 进行大消去，因此不能对这类值进行模式匹配，例如使用 Lean.Parser.Term.let : termlet 或 Lean.Parser.Term.match : termmatch 来在非命题宇宙（即 Type u）中生成数据。更准确地说，命题递归子的动机必须是命题。（此规则的例外情况请参阅手册中的单例消去一节。）

注意，任何将证明消去到非命题宇宙的表达式都会引发此错误，即使该表达式位于另一个命题类型的表达式中（例如证明中的 Lean.Parser.Term.let : termlet 绑定）。下方“在证明中定义中间数据值”的示例展示了这种情况。此类错误通常可以通过将递归子应用 “向外”移动来解决，使其动机成为正在证明的命题，而不是数据值项的类型。

示例🔗

在证明中定义中间数据值

example {α : Type} [inst : Nonempty α] (p : α → Prop) :
    ∃ x, p x ∨ ¬ p x :=
  let val :=
    Tactic `cases` failed with a nested error:
Tactic `induction` failed: recursor `Nonempty.casesOn` can only eliminate into `Prop`

α:Typemotive:Nonempty α → Sort ?u.14h_1:(x : α) → motive ⋯inst✝:Nonempty α⊢ motive inst✝ after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nilmatch inst with
    | .intro x => x
  ⟨val, Classical.em (p val)⟩

Tactic `cases` failed with a nested error:
Tactic `induction` failed: recursor `Nonempty.casesOn` can only eliminate into `Prop`

α:Typemotive:Nonempty α → Sort ?u.14h_1:(x : α) → motive ⋯inst✝:Nonempty α⊢ motive inst✝ after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

example {α : Type} [inst : Nonempty α] (p : α → Prop) :
    ∃ x, p x ∨ ¬ p x :=
  match inst with
  | .intro x => ⟨x, Classical.em (p x)⟩

尽管所定义的 Lean.Parser.Command.exampleexample 具有命题类型， val 的主体却不是；它的类型是 α : Type。因此，对 Nonempty α（一个命题）的证明进行模式匹配以生成 val，需要将该证明消去到非命题类型中，这是不允许的。相反，必须将 Lean.Parser.Term.match : termmatch 表达式移到 example 的顶层，此时结果是对示例标题中所述存在性断言的 Prop 值证明。也可以使用模式匹配的 Lean.Parser.Term.let : termlet 绑定来完成这种重构。

从存在性证明中提取见证

def getWitness {α : Type u} {p : α → Prop} (h : ∃ x, p x) : α :=
  Tactic `cases` failed with a nested error:
Tactic `induction` failed: recursor `Exists.casesOn` can only eliminate into `Prop`

α:Type up:α → Propmotive:(∃ x, p x) → Sort ?u.11h_1:(x : α) → (h : p x) → motive ⋯h✝:∃ x, p x⊢ motive h✝ after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nilmatch h with
  | .intro x _ => x

Tactic `cases` failed with a nested error:
Tactic `induction` failed: recursor `Exists.casesOn` can only eliminate into `Prop`

α:Type up:α → Propmotive:(∃ x, p x) → Sort ?u.11h_1:(x : α) → (h : p x) → motive ⋯h✝:∃ x, p x⊢ motive h✝ after processing
  _
the dependent pattern matcher can solve the following kinds of equations
- <var> = <term> and <term> = <var>
- <term> = <term> where the terms are definitionally equal
- <constructor> = <constructor>, examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil

-- 这是 `Exists.elim`
theorem useWitness {α : Type u} {p : α → Prop} {q : Prop}
    (h : ∃ x, p x) (hq : (x : α) → p x → q) : q :=
  match h with
  | .intro x hx => hq x hx

def getWitness {α : Type u} {p : α → Prop}
    (h : (x : α) ×' p x) : α :=
  match h with
  | .mk x _ => x

在此示例中，简单地移动模式匹配并不够；尝试定义的 getWitness 从根本上是不健全的。（考虑 p 为 fun (n : Nat) => n > 0 的情况：如果 h 和 h' 是 ∃ x, x > 0 的证明，其中 h 使用见证 1，而 h' 使用见证 2，那么根据证明无关性 h = h'，可推出 getWitness h = getWitness h'——即 1 = 2。）

因此，必须重写 getWitness：函数的结果类型必须是命题（上面的第一个修正示例），或者 h 不能是命题（第二个修正示例）。

在第一个修正示例中，useWitness 的结果类型现在是命题 q。这允许我们对 h 进行模式匹配（因为我们将其消去到命题类型中），并将解包后的值传递给 hq。从编程角度看，可以将 useWitness 视为以延续传递风格重写 getWitness，限制后续计算仅使用其结果来构造 Prop 中的值，正如禁止命题大消去所要求的那样。注意，useWitness 就是存在性消去原理 Exists.elim。

第二个修正示例将 h 的类型从存在性命题改为一个取 Type 值的依赖对（对应于 PSigma 类型构造器）。由于该类型不是命题，将其消去到 α : Type u 不再无效，之前尝试的模式匹配现在可以通过类型检查。

关于：propRecLargeElim🔗

示例🔗

关于：`propRecLargeElim`🔗