破坏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') |}

使用注入策略，我可以推断出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'在语法上不相同。我也不能将它们重写为相同的，因为重写 withfp_head fp' = fp_head fp会使右手边的类型错误。

我怎样才能从这里开始？是否有一些更聪明的版本以inj_pair2_eq_dec某种方式使用（非语法）基本相等而不是要求 sigma 类型的基本相等？

编辑：稍微考虑一下，我意识到要求尾巴相等是没有意义的（因为它们是不同的类型）。但是是否有可能基于 来证明它们之间的某种形式的莱布尼茨等式eq_rect？

Answer 1

诸如此类的问题就是为什么许多人更喜欢在 Coq 中避免依赖类型的原因。我将在 Coq sigma type 的情况下回答您的问题{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 ato 进行转换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不是变量，而是具有特定形状，这可能会阻止直接泛化。