Définir une 'tête' pour un flux de type coinductif dans Coq (sans appariement de formes)

Question

1) Je crois qu'il est possible d'utiliser des types inductifs sans appariement de formes. (en utilisant _rec, _rect, _ind seulement). C'est opaque, compliqué, mais possible. 2) Est-il possible d'utiliser des types coinductifs sans correspondance de motif?

Il existe une fonction du type coinductif à l'union des domaines de constructeurs de type coinductif. Est-ce que Coq le génère explicitement? Si oui, comment réécrire 'hd'?

Section stream. 
    Variable A : Type. 

    CoInductive stream : Type := 
    | Cons : A -> stream -> stream. 
End stream. 

Definition hd A (s : stream A) : A := 
    match s with 
    | Cons x _ => x 
    end. 

Answer 1

Bien qu'il soit possible d'utiliser des types inductifs directement sans avoir recours à l'appariement de motif, ceci est seulement superficiellement vrai: les _rec, _rect et _ind combinateurs générés par Coq sont tous définis en termes de match. Par exemple:

Print nat_rect. 

nat_rect = 
fun (P : nat -> Type) (f : P 0) (f0 : forall n : nat, P n -> P (S n)) => 
fix F (n : nat) : P n := 
    match n as n0 return (P n0) with 
    | 0 => f 
    | S n0 => f0 n0 (F n0) 
    end 
    : forall P : nat -> Type, 
     P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n 

En outre, il existe de nombreux cas où le remplacement de correspondance de motif par un éliminateur entraînerait un terme avec un comportement différent de calcul. Considérons la fonction suivante, qui divise une nat par deux:

Fixpoint div2 (n : nat) := 
    match n with 
    | 0 | 1 => 0 
    | S (S n') => S (div2 n') 
    end. 

Il est possible de réécrire cette fonction à l'aide nat_rec, mais l'appel récursif sur n - 2 fait un peu compliqué (essayez!).

Maintenant, revenons à votre question principale, Coq ne pas générer automatiquement des principes d'élimination similaires pour les types coinductive. La bibliothèque Paco permet de déduire des principes plus utiles pour en raisonnant sur les données coinductives. Mais autant que je sache, il n'y a rien de semblable pour écrire des fonctions simples. Il est intéressant de souligner que l'approche que vous proposez est différente de ce que Coq fait pour les types de données inductifs, en ce sens que nat_rect et les amis permettent d'écrire des fonctions récursives et des preuves par induction. Une des raisons de fournir ces combinateurs est qu'ils sont utilisés par la tactique induction. Quelque chose de type nat -> unit + nat, qui correspond plus ou moins à ce que vous avez proposé, ne suffirait pas.