Coinduction sur Coq, type mismatch

Question

J'ai essayé des types coinductifs et j'ai décidé de définir des versions coinductives des nombres naturels et des vecteurs (listes avec leur taille dans le type). Je les ai définis et le nombre infini comme si:

CoInductive conat : Set := 
| cozero : conat 
| cosuc : conat -> conat. 

CoInductive covec (A : Set) : conat -> Set := 
| conil : covec A cozero 
| cocons : forall (n : conat), A -> covec A n -> covec A (cosuc n).   

CoFixpoint infnum : conat := cosuc infnum. 

Tout a l'exception de la définition que j'ai donné une covecteur infinie

CoFixpoint ones : covec nat infnum := cocons 1 ones. 

qui a donné le décalage de type suivant

Error: 
In environment 
ones : covec nat infnum 
The term "cocons 1 ones" has type "covec nat (cosuc infnum)" while it is expected to have type 
"covec nat infnum". 

Je pensais que le compilateur accepterait cette définition puisque, par définition, infnum = cosuc infnum. Comment puis-je faire comprendre au compilateur que ces expressions sont identiques?

Answer 1

La méthode standard pour résoudre ce problème est décrite dans le CPDT d'Adam Chlipala (voir le chapitre sur Coinduction).

Definition frob (c : conat) := 
    match c with 
    | cozero => cozero 
    | cosuc c' => cosuc c' 
    end. 

Lemma frob_eq (c : conat) : c = frob c. 
Proof. now destruct c. Qed. 

Vous pouvez utiliser les définitions ci-dessus comme ceci:

CoFixpoint ones : covec nat infnum. 
Proof. rewrite frob_eq; exact (cocons 1 ones). Defined. 

ou, peut-être, un peu de manière plus lisible:

Require Import Coq.Program.Tactics. 

Program CoFixpoint ones : covec nat infnum := cocons 1 ones. 
Next Obligation. now rewrite frob_eq. Qed.