我们如何为依赖类型定义`eqType`？

Question

我想将从属类型定义为eqType。例如，假设我们定义了以下依赖类型Tn：

From mathcomp Require Import all_ssreflect.

Variable T: nat -> eqType.

Inductive Tn: Type := BuildT: forall n, T n -> Tn.

[为了使用eqType，我为Tn_eq定义了一个相等函数Tn：

Definition Tn_eq: rel Tn :=
  fun '(BuildT n1 t1) '(BuildT n2 t2) =>
    (if n1 == n2 as b return (n1==n2) = b -> bool
     then fun E => t1 == eq_rect_r T t2 (elimTF eqP E)
     else fun _ => false) (erefl (n1 == n2)).

然后我试图证明Tn_eq的相等公理，但失败了。

Lemma Tn_eqP: Equality.axiom Tn_eq.
Proof.
  case=>n1 t1; case=>n2 t2//=.
  case_eq(n1==n2).

我在这里出错：

Illegal application: 
The term "elimTF" of type
 "forall (P : Prop) (b c : bool), reflect P b -> b = c -> if c then P else ~ P"
cannot be applied to the terms
 "n1 = n2" : "Prop"
 "b" : "bool"
 "true" : "bool"
 "eqP" : "reflect (n1 = n2) (n1 == n2)"
 "E" : "b = true"
The 4th term has type "reflect (n1 = n2) (n1 == n2)" which should be coercible to
 "reflect (n1 = n2) b".

我应该如何证明这个引理？

Answer 1

我们去：

From Coq Require Import EqdepFacts.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

Variable T: nat -> eqType.

Inductive Tn: Type := BuildT: forall n, T n -> Tn.

Definition Tn_eq: rel Tn :=
  fun '(BuildT n1 t1) '(BuildT n2 t2) =>
    (if n1 == n2 as b return (n1==n2) = b -> bool
     then fun E => t1 == eq_rect_r T t2 (elimTF eqP E)
     else fun _ => false) (erefl (n1 == n2)).

Lemma Tn_eqP: Equality.axiom Tn_eq.
Proof.
case=> n1 t1; case=> n2 t2 /=.
case: eqP => [eq1 | neq1]; last by constructor; case.
case: eqP.
- move=> ->; constructor; move: t2; rewrite [elimTF _ _]eq_irrelevance.
  by case: _ / eq1.
move=> neq2; constructor.
case=> _ exT; move: (eq_sigT_snd exT) => Cast; apply: neq2.
rewrite -Cast.
rewrite [eq_sigT_fst _]eq_irrelevance [elimTF _ _]eq_irrelevance.
by case: _ / eq1.
Qed.