Coq中定义依赖参数可合一性的函数问题求助

首先得说清楚你原来的定义为啥不行：你用ltac:(match x with z => ...)的时候，这里的x和z是函数定义阶段的绑定变量，它们是两个完全不同的标识符，所以这个match永远不会匹配成功——不管你调用时传入的实际值是不是一样的，结果自然每次都返回g fa b。要实现“返回值依赖x和z可合一”的需求，得利用Coq的依赖类型特性或者可判定相等性来处理，而不是静态的ltac匹配。

下面给你两种可行的解决方案：

方案一：使用Program Definition结合等式约束 #

这个方法通过显式的等式约束来区分x和z相等的情况，需要先导入Program模块：

Require Import Program.
Require Import Logic.Eqdep.

Inductive A := a | a0 | fa.
Inductive B := b | b0.
Parameter C: Type.
Parameter g: A -> B -> C.
Parameter CT:> C -> Type.
Parameter gab: g a b.
Parameter ga0b: g a0 b.

Program Definition f {x y z w}(n: g x y)(m: g z w) : C :=
  match eq_refl with
  | eq_refl when x = z => g z b
  | _ => g fa b
  end.
Next Obligation. destruct H; reflexivity. Qed.

测试一下：

Compute f gab ga0b. (*= g fa b: C *)
Compute f gab gab. (*= g a b: C *)

原理是Program Definition允许我们在定义中加入隐含的等式约束，Next Obligation用来证明这个约束的合理性，当x和z确实相等时，就能触发对应的分支。

方案二：使用可判定相等性做分支判断 #

如果你的类型支持可判定相等（比如枚举类型A），可以先为A添加可判定相等的实例，然后用eq_dec来做运行时的相等判断：

Require Import Decidable.

Inductive A := a | a0 | fa.
Inductive B := b | b0.
Parameter C: Type.
Parameter g: A -> B -> C.
Parameter CT:> C -> Type.
Parameter gab: g a b.
Parameter ga0b: g a0 b.

(* 为A添加可判定相等实例 *)
Instance A_eq_dec : EqDec A eq.
Proof. decide equality. Qed.

Definition f {x y z w}(n: g x y)(m: g z w) : C :=
  match eq_dec x z with
  | left e => eq_rect z (fun a => g a b) (g z b) x e
  | right _ => g fa b
  end.

测试结果同样符合预期：

Compute f gab ga0b. (*= g fa b: C *)
Compute f gab gab. (*= g a b: C *)

这里eq_dec x z会返回left e（当x和z相等时，e是x=z的证明）或者right _（不相等时）。eq_rect用来把g z b的类型转换成g x b（因为x=z，所以两者其实是同一个值），保证类型一致性。

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