Coq 定点定义由自然数表示。（（n+1）的类型取决于（n）的类型）

Question

我想归纳定义类型 urt。我想在定义 (urt n.+1) 时了解 (urt n)。（我将使用 urt 定义中第二个元素 pr1 的投影。）标识符 sigT 创建依赖对的类型； pr1, pr2 是这一对的投影。

 Context (qsigT: forall (A : Type) (P : forall a : A, Type), Type).
 Context (qpr1: forall (A : Type) (P : forall a : A, Type), (@qsigT A P) -> A ).
 Inductive Unit : Type :=
  | tt : Unit.
 Inductive Bool : Type :=
  | true : Bool
  | false : Bool.
 Fixpoint urt (n:nat): Type.

 Proof.
  refine (@qsigT Bool _).

  destruct n.

  exact (fun _ => Unit).
  exact (fun q =>
          (@qsigT (urt n) (fun q => (*error below occurs because of using (urt n)*)
            Unit+Unit+Unit (*I also cannot use here something like (qpr1 q), because of the same reasons*)
          ))
  ).
  Show Proof.

 Defined.
 Check fun (q : urt 4) => qpr1 q. (*Error!*)

 Context (y:nat).
 Check fun (q : urt y) => qpr1 q. (*Error here, need to be solved*)

错误是 The term "q" has type "urt (S (S (S (S O))))" while it is expected to have type "Type". 我应该如何更改定义？

Answer 1

您的 urt 定义有一个顶级固定点，因此您需要解构 y 以使固定点缩减为 sigT _ _ 形式。（提示：尝试在 Check 语句中使用 (S y)）。

很难猜测您想做什么，但一个可能的解决方案是在 sigT 构造函数之后延迟定点。

 Definition urt (n : nat) : Type.
 Proof.
  refine (@qsigT Bool _).
  revert n.
  fix urt 1.
  intros [|n].
  exact (fun _ => Unit).
  exact (fun q =>
          (@qsigT (urt n q) (fun q => (*error below occurs because of using (urt n)*)
            (Unit+Unit+Unit)%type (*I also cannot use here something like (qpr1 q), because of the same reasons*)
          ))
  ).
  Show Proof.

 Defined.
 Check fun (q : urt 4) => qpr1 _ _ q.
 Context (y:nat).
 Check fun (q : urt y) => qpr1 _ _ q.

Coq 定点定义由自然数表示。（（n+1）的类型取决于（n）的类型）

Coq fixpoint defintion numerated by natural numbers.(type of (n+1)'s type depends on (n)'s type)

coq