coq - 破坏 coq 中依赖记录的相等性

Question

给定依赖记录类型:

Record FinPath : Type := mkPath { fp_head : S i;
                                  fp_tail : FinPathTail fp_head
                                }.

并且两个 Path 类型的对象相等，我想推断它们的头和尾是相等的。问题是我很快就得到了这种形式的东西:

fpH : {| path_head := fp_head fp; path_tail := fpt_to_pt (fp_tail fp) |} =
      {| path_head := fp_head fp'; path_tail := fpt_to_pt (fp_tail fp') |}

使用注入(inject)策略，我可以推断出 fp_head fp = fp_head fp' 以及这个术语:

existT (fun path_head : S i => PathTail path_head) (fp_head fp)
       (fpt_to_pt (fp_tail fp)) =
existT (fun path_head : S i => PathTail path_head) (fp_head fp')
       (fpt_to_pt (fp_tail fp'))

假设S i的可判定性，我通常会想使用inj_pair2_eq_dec，但这在这种情况下不适用，因为fp_head fp 和 fp_head fp' 在语法上并不相同。我也无法将它们重写为相同的，因为使用 fp_head fp' = fp_head fp 重写会导致右侧类型错误。

我该如何继续？是否有一些更聪明的 inj_pair2_eq_dec 版本以某种方式使用(非语法)基数相等，而不是要求 sigma 类型的基数相等？

编辑:再仔细考虑一下，我意识到要求尾部相等是没有意义的(因为它们是不同类型的)。但是是否有可能基于 eq_rect 证明它们之间某种形式的莱布尼兹相等性？

Answer 1

像这样的问题是许多人宁愿避免 Coq 中的依赖类型的原因。我将在 Coq sigma 类型 {x : T & S x} 的情况下回答您的问题，可以推广到其他相关记录。

我们可以通过强制转换函数来表达该对的依赖组件应满足的相等性:

Definition cast {T} (S : T -> Type) {a b : T} (p : a = b) : S a -> S b :=
  match p with eq_refl => fun a => a end.

Definition eq_sig T (S : T -> Type) (a b : T) x y
  (p : existT S a x = existT S b y) :
  {q : a = b & cast S q x = y} :=
  match p in _ = z return {q : a = projT1 z & cast S q x = projT2 z} with
  | eq_refl => existT _ eq_refl eq_refl
  end.

cast函数允许我们使用等式 p : a = b从 S a 转换至S b 。 eq_sig我通过证明术语定义的引理说，给定一个等式 p两个依赖对之间existT S a x和existT S b y ，我可以生成另一个依赖对，其中包含:

1. 平等 q : a = b ，并且

2. 证明 x和y 类型转换后相等。

通过类似的定义，我们可以提供“归纳”依赖对之间的相等性证明的证明原理:

Definition eq_sig_elim T (S : T -> Type) (a b : T) x y
  (p : existT S a x = existT S b y) :
  forall (R : forall c, S c -> Prop), R a x -> R b y :=
  match p in _ = z return forall (R : forall c, S c -> Prop), R a x -> R _ (projT2 z) with
  | eq_refl => fun R H => H
  end.

引理的形状与 eq_sig 类似。 ，但这一次它说，在存在这样的等式的情况下，我们可以证明任意依赖谓词 R b y提供了R a x的证明.

使用这种依赖原则可能会很尴尬。挑战在于找到这样一个R这允许您表达您的目标:在上面的结果类型中， R 第二个参数的类型相对于第一个参数是参数化的。在许多有趣的情况下，第二项的第一个组成部分 y ，不是变量，而是具有特定的形状，这可能会妨碍直接泛化。