Coq中使用decide equality时如何保留谓词P信息以证明相等性

在你的场景中，问题出在decide equality策略会自动解构归纳类型A的元素，但不会保留元素与构造子的等式关联，导致你无法将P a转化为P (A0 c)。解决的核心是手动解构a和b并保留它们与构造子的等式，而不是依赖decide equality的自动解构。

具体证明步骤 #

Variable C: Type.
Inductive A: Type:=
    | A0: C -> A.
Variable P: A -> Prop.
Variable P_dec: forall a: A, {P a} + {~ P a}.
(* 假设C的相等性可判定，若你的环境中已有此前提可省略 *)
Variable C_dec: forall c c0: C, {c = c0} + {c <> c0}.

Definition A_dec: forall a b, {a = b} + {a <>  b} + {~ P a}.
Proof.
intros a b.
(* 先分情况讨论a是否满足P *)
destruct (P_dec a) as [p | np].
- (* 当P a成立时，需要判定a和b的相等性 *)
  (* 手动解构a和b，同时保留等式 *)
  destruct a as [c] eqn:eq_a; destruct b as [c0] eqn:eq_b.
  (* 将P a转化为P (A0 c) *)
  rewrite eq_a in p.
  (* 此时p: P (A0 c)，你可以正常使用这个事实 *)
  (* 判定C类型元素的相等性 *)
  destruct (C_dec c c0) as [eq_c | neq_c].
  + left; rewrite eq_c; reflexivity. (* 返回a = b的情况 *)
  + right; intro eq_ab; injection eq_ab as eq_c'; contradiction neq_c. (* 返回a ≠ b的情况 *)
- (* 当~P a成立时，直接返回第三个选项 *)
  right; right; exact np.
Defined.

关键说明 #

• 使用destruct a as [c] eqn:eq_a解构a时，会生成等式eq_a: a = A0 c，通过rewrite eq_a in p就能将P a转化为P (A0 c)，从而获取你需要的谓词信息。
• 如果你没有显式定义C_dec，decide equality生成的{c = c0} + {c <> c0}目标，也可以在手动解构后继续证明，此时你已经拥有P (A0 c)的信息，不会再丢失。

内容的提问来源于stack exchange，提问作者user251130