Coq fixpoint defintion nummeriert durch natürliche Zahlen (Typ von (n + 1) 's Typ hängt von (n) Typ)

Question

Ich möchte Typ urt induktiv definieren. Ich möchte etwas über (urt n) wissen, während ich definiere (urt n. + 1). (Ich werde die Projektion auf das zweite Element pr1 innerhalb der Definition von urt verwenden.) Identitifier sigT erzeugt den Typ der abhängigen Paare; pr1, pr2 sind Projektionen von einem solchen Paar.

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*) 

Der Fehler ist The term "q" has type "urt (S (S (S (S O))))" while it is expected to have type "Type". Wie soll ich die Definition ändern?

Answer 1

Ihre urt Definition hat einen Fixpunkt auf oberster Ebene, daher müssen Sie y für den Fixpunkt löschen, um auf ein sigT _ _ Formular zu reduzieren. (Tipp: Versuchen Sie (S y) in Ihrer Check Anweisung zu verwenden).

Es ist schwer zu erraten, was Sie tun möchten, aber eine mögliche Lösung wäre, den Fixpunkt nach dem sigT Konstruktor zu verzögern.

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.