Exercice baz_num_elts de Software Foundations

9

Je suis à l'exercice suivant dans Software Foundations :

(** **** Exercise: 2 stars (baz_num_elts) *)
(** Consider the following inductive definition: *)

Inductive baz : Type :=
   | x : baz -> baz
   | y : baz -> bool -> baz.

(** How _many_ elements does the type [baz] have? 
(* FILL IN HERE *)
[] *)

Toutes les réponses que j'ai vues sur Internet disent que la réponse est 2 et que les éléments sont x et y. Si tel est le cas, il n'est pas clair pour moi ce que l'on entend par éléments . Il y a certainement deux constructeurs, mais il est impossible de créer réellement une valeur de type baz .

Il est impossible de créer une valeur de type bazcar xhas type baz -> baz. ya un type baz -> bool -> baz. Afin d'obtenir une valeur de type, baznous devons transmettre une valeur de type bazà xou y. Nous ne pouvons pas obtenir une valeur de type bazsans avoir déjà une valeur de type baz.

Jusqu'à présent, j'ai interprété les éléments comme des valeurs moyennes . Ainsi (cons nat 1 nil)et (cons nat 1 (cons nat 2 nil))seraient tous les deux des éléments de type list natet il y aurait un nombre infini d'éléments de type list nat. Il y aurait deux éléments de type bool, qui sont trueet false. Selon cette interprétation, je dirais qu'il n'y a aucun élément de type baz.

Ai-je raison, ou quelqu'un peut-il expliquer ce que je comprends mal?

coq Twernmilt
la source
1
Sûr. J'ai ajouté un paragraphe expliquant pourquoi je pense qu'il est impossible de créer une valeur de type baz.
Twernmilt
Agréable. C'est ce que je pensais que tu pensais. Merci, Twernmilt. Pour ce que ça vaut, j'ai la même réaction que vous: moi aussi, je m'attendais à ce qu'il y ait zéro élément de type baz.
DW

Réponses:

8

Je suis d'accord avec toi. Il y a une bijection entre bazet False.

Definition injective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1 x2, f1 x1 = f1 x2 -> x1 = x2.

Definition surjective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1, exists x2, f1 x2 = x1.

Definition bijective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => injective f1 /\ surjective f1.

Inductive baz : Type :=
   | x : baz -> baz
   | y : baz -> bool -> baz.

Theorem baz_False : baz -> False. Proof. induction 1; firstorder. Qed.

Goal exists f1 : baz -> False, bijective f1.
Proof.
exists baz_False. unfold bijective, injective, surjective. firstorder.
assert (H2 := baz_False x1). firstorder.
assert (H2 := x1). firstorder.
Qed.
Rui Baptista
la source