упражнение baz_num_elts из фондов программного обеспечения

Я занимаюсь следующими упражнениями в Фонде программного обеспечения :

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

Все ответы, которые я видел в Интернете, говорят, что ответ - 2, а элементы - x и y. Если это так, то мне не ясно, что подразумевается под элементами . Конечно, есть два конструктора, но на самом деле невозможно создать значение типа baz .

Невозможно создать значение типа, bazпотому что xимеет тип baz -> baz. yимеет тип baz -> bool -> baz. Чтобы получить значение типа, bazнам нужно передать значение типа bazлибо в, xлибо y. Мы не можем получить значение типа, bazне имея значения типа baz.

До сих пор я интерпретировал элементы как средние значения . Таким образом, (cons nat 1 nil)и (cons nat 1 (cons nat 2 nil))оба будут элементами типа, list natи будет бесконечное число элементов типа list nat. Там будет два элемента типа bool, которые trueи false. При таком толковании я бы сказал, что элементов типа ноль baz.

Я прав, или кто-то может объяснить, что я неправильно понимаю?

Я с тобой согласен. Есть биекция между bazи 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.