coq - Coq中的析取消除规则？

Question

我很惊讶在 Coq 中没有找到用于析取消除的内置命题：

P \/ ~ P -> (P -> C) -> (~ P -> C) -> C

没有战术怎么证明？仅使用 Curry/Howard 同构。

标签： coq

Answer 1

它确实存在。它被称为or_ind。

Check or_ind.
(*   : forall A B P : Prop,
       (A -> P) -> (B -> P) -> A \/ B -> P *)
(* shuffling arguments to get your signature *)
Check (fun (P C : Prop) (p : P \/ ~P) (l : P -> C) (r : ~P -> C) => or_ind l r p).

更深层次的是，此功能实际上是其or自身定义的一部分。or是一个归纳类型，每个归纳类型都带有在原始match构造中使用它的规则。or_ind只是一个包装器，让您match以函数形式使用它。您的函数/定理将根据 来match实现

fun (P C : Prop) (p : P \/ ~P) (l : P -> C) (r : ~P -> C) =>
  match p with
  | or_introl p => l p
  | or_intror p => r p
  end