如何访问Coq内部依赖类型合一算法并获取apply的替换解

TLDR: 我希望能够比较两个项——一个带洞、一个不带洞——并提取可补全该项的实际lambda term，无论通过Coq、OCaml、Coq插件还是其他任意方式实现均可。

举一个简单示例，假设定理如下：

Theorem add_easy_0'':
forall n:nat,
  0 + n = n.
Proof.

该定理的(lambda term)证明为：

fun n : nat => eq_refl : 0 + n = n

如果编写如下部分证明脚本：

Theorem add_easy_0'':
forall n:nat,
  0 + n = n.
Proof.
    Show Proof.
    intros.
    Show Proof.

查看证明状态会得到如下部分lambda证明：

(fun n : nat => ?Goal)

实际上我们可以通过apply调用ddt unification算法隐式补全项、完成证明：

Theorem add_easy_0'':
forall n:nat,
  0 + n = n.
Proof.
    Show Proof.
    intros.
    Show Proof.
    apply (fun n : nat => eq_refl : 0 + n = n).
    Show Proof.
Qed.

上述流程可以关闭证明，但不会返回?Goal对应的解——显然Coq已经在内部隐式求解了CIC/ddt/Coq unification问题并关闭目标，我希望获取apply执行过程中生成的substitution solution。

如何从Coq内部实现这一需求？理想情况下可直接在Coq层面实现，但若提供OCaml内部接口调用、Coq插件开发方案或任意可行解决方案均可。

我确认apply会执行unification，是因为apply tactic的官方描述明确提到其匹配逻辑：

该tactic可适用于任意目标。输入参数为局部上下文下良构的项。apply tactic会尝试将当前目标与输入项类型的结论进行匹配，匹配成功后，返回的子目标数量与该项类型中非依赖前提的数量一致。

这与我曾在Isabelle合一相关课程中看到的逻辑高度相似：

相关逻辑说明如下：

- 已有/已知规则 [[A1; … ;An]] => A (*)
    - 含义：给定事实A1; …; An即可推出结论A
    - 对应反向推理逻辑：若要证明结论A，必须给出A1; …;An的证明（或已知Ai成立）
- 需要关闭证明 [[B1; …; Bm]] => C (**)（即当前子目标）
    - 即当前已有假设B1; …; Bm，需要证明结论C
- 若要使用规则(*)变换子目标(**)，执行逻辑如下：
    - 首先判断子目标(**)是否为规则(*)的特例，首先检查二者的结论（目标）是否“等价”。若结论匹配，则原本需要证明的C可转换为证明A。但要得到A，需要使用令C和A匹配的替换来证明A1; … ;An。之所以需要证明A1;...;An，是因为根据规则(*)，证明这些前提即可自动得到A，而通过“匹配”（unification）得到的A即可证明原目标。核心要求是必须使用令A和C匹配的替换完成证明，流程为：
    - 首先尝试“匹配”A和C，二者的结论必须匹配，该匹配过程即为unification，返回可令两个项相等的替换sig
        - sig = Unify(A,C) 满足 sig(A) = sig(C)
    - 由于使用规则(*)变换了子目标(**)，接下来需要证明规则(*)中与子目标(**)结论匹配的对应前提，证明过程可使用原子目标(**)的原有假设（假设依然成立），同时应用令规则匹配的替换sig
- 若当前子目标(*)与规则(**)匹配成功，生成的新子目标为：
    - [[sig(B1); … ; sig(Bm) ]] => sigm(A1)
    - ...
    - [[sig(B1); … ; sig(Bm) ]] => sigm(An)
- 完成/关闭上述证明（即证明所有子目标）即可得到：
    - [[sig(B1); …;sig(Bm) ]] => sig(C)
- 对应命令：apply (rule <(*)>), 其中(*)为规则名

最初我以为exact是我需要拦截的Coq tactic，但后续判断并非如此，我对exact的理解如下：

- exact p.（假设p的类型为U）
    - 当目标项T（即一个Type）与给定项p的类型匹配时，可关闭证明
        - 成功当且仅当T和U是convertible（直观上可理解为二者可unify，即T与U convertible）

conversion本质是相等性检查，并非真正的unification，即它不会尝试求解符号方程组。

简要说明：

- unification
    - 一种求解符号表达式/项之间方程组的算法
        - 即求解目标类似：
            - cons2( cons1( x, y, ...,) ..., cons3(a, b, c), ... ) = cons1(x, nil) 
            - x = y
            - 本质是给定多组左右项对，判断是否存在对其中变量/项的赋值，令所有等式成立
                - 可能包含term1 = term2, term3 = term4这类等式及若干变量
            - 解为满足所有等式的变量替换

我真诚希望了解如何拦截apply tactic或直接调用其使用的unification算法。

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