我有一个函数Z -> Z -> whatever我把它看作是从(Z, Z)到whatever的映射，让我们把它键入为FF。
whatever是可从nix或inj_whatever构造的简单和。
这张地图我用一些数据初始化，方式是：
Definition i (x y : Z) (f : FF) : FF :=
fun x' y' =>
if andb (x =? x') (y =? y')
then inj_whatever
else f x y.
=?表示Z上的布尔可判定相等，来自Coq的ZArith。
现在我想在其中两个这样的FF上平等，我不介意调用functional_extensionality.我现在想做的是让Coq通过计算确定两个FF的相等性。
例如，假设我们做一些类似的事情：
Definition empty : FF := fun x y => nix.
现在我们添加一些任意值来做foo和foo'，这些值在函数外延下是等价的：
Definition foo := i 0 0 (i 0 (-42) (i 56 1 empty)).Definition foo' := i 0 (-42) (i 56 1 (i 0 0 empty)).
什么是自动让辅酶q确定foo = foo'的好方法。Ltac级的东西？实际终止计算？我是否需要将域限制为有限域？
域限制有点复杂。我以一种f : FF -> FF的方式操纵映射，其中f可以扩展定义计算的Z x Z子集。因此，想想看，它不能是f : FF -> FF的，而更像是f : FF -> FF_1，其中FF_1是由一个小常数扩展的Z x Z子集。因此，当一个人申请fn次时，最终得到FF_n相当于域限制FF加域n * constant。因此，函数f缓慢地(通过常数因子)扩展了定义 FF 的域。
正如我在评论中所说，为了详细阐述一个令人满意的答案，需要更多细节。请参阅以下示例---，以获取有关如何使用 mathcomp 在受限函数范围内玩相等的分步描述---：
From mathcomp Require Import all_ssreflect all_algebra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* We need this in order for the computation to work. *)
Section AllU.
Variable n : nat.
(* Bounded and unbounded fun *)
Definition FFb := {ffun 'I_n -> nat}.
Implicit Type (f : FFb).
Lemma FFP1 f1 f2 : reflect (f1 = f2) [forall x : 'I_n, f1 x == f2 x].
Proof. exact/(equivP eqfunP)/ffunP. Qed.
Lemma FFP2 f1 f2 :
[forall x : 'I_n, f1 x == f2 x] = all [fun x => f1 x == f2 x] (enum 'I_n).
Proof.
by apply/eqfunP/allP=> [eqf x he|eqf x]; apply/eqP/eqf; rewrite ?enumT.
Qed.
Definition f_inj (f : nat -> nat) : FFb := [ffun x => f (val x)].
Lemma FFP3 (f1 f2 : nat -> nat) :
all [fun x => f1 x == f2 x] (iota 0 n) -> f_inj f1 = f_inj f2.
Proof.
move/allP=> /= hb; apply/FFP1; rewrite FFP2; apply/allP=> x hx /=.
by rewrite !ffunE; apply/hb; rewrite mem_iota ?ltn_ord.
Qed.
(* Exercise, derive bounded eq from f_inj f1 = f_inj f2 *)
End AllU.
最终引理确实应该允许你将函数的相等性简化为一个计算的、完全可运行的 Gallina 函数。
上述内容的更简单版本，可能对您更有用：
Lemma FFP n (f1 f2 : nat -> nat) :
[forall x : 'I_n, f1 x == f2 x] = all [pred x | f1 x == f2 x] (iota 0 n).
Proof.
apply/eqfunP/allP=> eqf x; last by apply/eqP/eqf; rewrite mem_iota /=.
by rewrite mem_iota; case/andP=> ? hx; have /= -> := eqf (Ordinal hx).
Qed.
但这取决于您(不存在)范围限制条件的指定方式。
在您编辑之后，我想我应该添加一个关于地图相等性更一般主题的注释，事实上，您可以定义除A -> B之外更具体的地图类型，然后构建决策程序。
大多数典型的映射类型[包括 stdlib 中的映射类型]都可以工作，只要它们支持"绑定检索"的操作，因此您可以将相等性简化为有限多个绑定值的检查。
事实上，Coq标准库中的地图已经为你提供了这样的计算相等函数。
好的，这是一个相当残酷的解决方案，它不会试图避免多次进行相同的大小写区分，但它是完全自动化的。
我们从一种策略开始，该策略检查两个整数是否相等(使用Z.eqb)，并将结果转换为omega可以处理的命题。
Ltac inspect_eq y x :=
let p := fresh "p" in
let q := fresh "q" in
let H := fresh "H" in
assert (p := proj1 (Z.eqb_eq x y));
assert (q := proj1 (Z.eqb_neq x y));
destruct (Z.eqb x y) eqn: H;
[apply (fun p => p eq_refl) in p; clear q|
apply (fun p => p eq_refl) in q; clear p].
然后，我们可以编写一个函数，该函数触发它能找到的i的第一个匹配项。这可能会在上下文中引入相互矛盾的假设，例如，如果之前的匹配揭示了x = 0，但我们现在称之为inspect x 0，则第二个分支将在上下文中同时具有x = 0和x <> 0。它将被omega自动关闭。
Ltac fire_i x y := match goal with
| [ |- context[i ?x' ?y' _ _] ] =>
unfold i at 1; inspect_eq x x'; inspect_eq y y'; (omega || simpl)
end.
然后我们可以把所有东西放在一起：调用函数外延性两次，重复fire_i直到没有其他东西可以检查并通过reflexivity得出结论(事实上，所有有矛盾的分支都被自动忽略了！
Ltac eqFF :=
let x := fresh "x" in
let y := fresh "y" in
intros;
apply functional_extensionality; intro x;
apply functional_extensionality; intro y;
repeat fire_i x y; reflexivity.
我们可以看到它毫无问题地释放了您的引理：
Lemma foo_eq : foo = foo'.
Proof.
unfold foo, foo'; eqFF.
Qed.
这是一个包含所有导入和定义的独立要点。