ejercicio baz_num_elts de Fundamentos de software

9

Estoy en el siguiente ejercicio en Fundamentos de software :

(** **** 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 *)
[] *)

Todas las respuestas que he visto en Internet dicen que la respuesta es 2 y que los elementos son x e y. Si ese es el caso, entonces no me queda claro qué se entiende por elementos . Ciertamente hay dos constructores, pero es imposible crear un valor de tipo baz .

Es imposible crear un valor de tipo bazporque xtiene tipo baz -> baz. ytiene tipo baz -> bool -> baz. Para obtener un valor de tipo baz, necesitamos pasar un valor de tipo baza cualquiera xo y. No podemos obtener un valor de tipo bazsin tener ya un valor de tipo baz.

Hasta ahora he estado interpretando elementos como valores medios . Por lo tanto (cons nat 1 nil), y (cons nat 1 (cons nat 2 nil))ambos serían elementos de tipo list naty no habría un número infinito de elementos de tipo list nat. Habría dos elementos de tipo bool, que son truey false. Según esta interpretación, diría que hay cero elementos de tipo baz.

¿Estoy en lo cierto, o alguien puede explicar lo que estoy entendiendo mal?

coq Twernmilt
fuente
1
Por supuesto. He agregado un párrafo que explica por qué creo que es imposible crear un valor de tipo baz.
Twernmilt
Agradable. Eso es lo que pensé que estabas pensando. Gracias Twernmilt. Por lo que vale, tengo la misma reacción que ustedes: yo también hubiera esperado que la respuesta fuera que hay cero elementos de tipo baz.
DW

Respuestas:

8

Estoy de acuerdo contigo. Hay una biyección entre bazy 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
fuente