在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'是语法上不一样的。我也不能重写他们是相同的，因为与fp_head fp' = fp_head fp重写会留下右手边虐待类型。

我怎样才能从这里出发？有inj_pair2_eq_dec的一些聪明的版本，不知怎的，使用（非句法）基础的平等，而不是要求西格玛类型的基础是平等的吗？

编辑：关于这个思路有点难度，我知道这是没有意义的问那个尾巴是相等的（因为它们是不同类型的）。但是，它可以证明某种形式的它们之间莱布尼茨平等的基础上eq_rect？

Answer 1

像这些问题是为什么为什么很多勒柯克宁愿避免依赖类型。我会回答在勒柯克σ型{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，不是一个变量，但有一个特定的形状，这可能会导致一个直接的概括。