无需额外公理或UIP，用eq_rect证明Coq依赖等式

问题背景 #

需要在Coq中证明一个依赖等式，约束条件为：不使用额外公理（包括Streicher K/UIP公理）、不借助nat的可判定相等性，同时解决重写时同步处理eq_rect依赖部分以通过类型检查的问题。给出的示例定理如下：

Theorem toy_append (n i j : nat) (le_ji : j <= i) (w : toy n) :
    toy_plus n i w = eq_rect _ toy (toy_plus (j+n) (i-j) (toy_plus n j w)) _ (toy_regroup i j n le_ji).

尝试用le_dep_ind进行依赖归纳时，因未同步处理eq_rect的依赖部分导致类型检查失败，以下是具体疑问的解答：

疑问解答 #

1. 如何直接证明toy_append，不依赖额外公理或nat可判定相等性？ #

核心思路是对le_ji : j <= i进行依赖归纳，结合toy_plus的递归定义性质，在归纳过程中维护eq_rect与目标项的一致性：

• 基例（j=0）：此时i-j = i，j+n = n，toy_regroup对应eq_refl，目标简化为toy_plus n i w = eq_rect n toy (toy_plus n i (toy_plus n 0 w)) n eq_refl。结合toy_plus n 0 w = w的引理，直接利用eq_rect的计算规则（当证明项为eq_refl时，eq_rect A P x A eq_refl = x）即可得证。
• 归纳步骤：假设j = k且k <= i时定理成立，考虑j = S k且S k <= i的情况。将toy_plus n (S k) w展开为toy_S (toy_plus n k w)，同时对toy_regroup的归纳形式做对应展开，把归纳假设中的eq_rect结构同步替换，通过eq_trans组合多个小等式，确保类型匹配后完成重写。

2. 如何同时修改eq_rect中的证明项类型与目标其余部分，使其通过类型检查？ #

关键是利用依赖归纳的参数传递，让eq_rect的类型参数随归纳假设同步更新：

• 使用le_dep_ind时，不要仅归纳le_ji，而是将目标中涉及的依赖参数（如i-j、j+n）与le_ji绑定，确保归纳过程中eq_rect的类型参数（如j+n）能随j的变化自动调整。
• 不要单独重写eq_rect的某个参数，而是构造同时关联eq_rect参数与目标项的等式：先证明toy_plus n i w = toy_plus (j+n) (i-j) (toy_plus n j w)（基于j <= i的前提），再结合eq_rect的定义，证明这个等式与目标中的eq_rect表达式相等——本质是利用eq_rect的“运输”性质，当底层类型等式成立时，依赖类型元素的运输结果等于直接计算的结果。
• 可以用refine战术手动构建证明项，显式指定eq_rect的参数如何随归纳步骤变化，避免自动战术导致的类型不匹配。

3. 这类依赖等式有哪些推荐表示方式？ #

常见的依赖等式表示方式各有适用场景：

• 原生eq：即当前使用的形式，无需额外定义，直接依赖Coq核心等式，但需处理eq_rect的运输问题，适合熟悉类型系统细节的场景。
• JMeq（异质等式）：定义在Coq.Logic.JMeq中，形式为JMeq A B，表示A和B是同类型元素且类型相等，可避免手动编写eq_rect，直接表达“不同类型下的元素相等”；无公理前提下，JMeq x y蕴含eq (projT1 x) (projT1 y)且eq (projT2 x) (projT2 y)，但反向推导需要UIP。
• eq_dep：定义在Coq.Logic.Eqdep中，形式为eq_dep A x P y p，精准表达依赖类型下的元素运输等式，适合需要明确跟踪类型等式的场景，但写法相对繁琐。
• 自定义依赖等式：若上述方式不满足需求，可基于eq和eq_rect自定义贴合场景的等式谓词，比如针对toy类型定义toy_eq : toy n -> toy m -> Prop，当n = m时等价于原生eq，同时内置类型等式的处理逻辑。

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