ćwiczenie baz_num_elts z Software Foundations

Jestem na następującym ćwiczeniu w zakresie podstaw oprogramowania :

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

Wszystkie odpowiedzi, które widziałem w Internecie, mówią, że odpowiedź to 2, a elementy to xiy. Jeśli tak jest, to nie jest dla mnie jasne, co oznaczają elementy . Z pewnością istnieją dwa konstruktory, ale nie można w rzeczywistości utworzyć wartości typu baz .

Nie można utworzyć wartości typu, bazponieważ xma ona typ baz -> baz. yma typ baz -> bool -> baz. W celu uzyskania wartości typu bazmusimy przekazać wartość typu bazalbo xalbo y. Nie możemy uzyskać wartości typu, bazjeśli nie mamy już wartości typu baz.

Do tej pory interpretowałem elementy jako wartości średnie . Tak więc (cons nat 1 nil)i (cons nat 1 (cons nat 2 nil))oba byłyby elementami typu list nati byłaby nieskończona liczba elementów typu list nat. Byłyby dwa elementy typu bool, które są truei false. Zgodnie z tą interpretacją twierdziłbym, że nie ma elementów typu zero baz.

Czy mam rację, czy ktoś może wyjaśnić to, co źle zrozumiałem?

coq

— Twernmilt
źródło

Pewnie. Dodałem akapit wyjaśniający, dlaczego uważam, że niemożliwe jest utworzenie wartości typu baz.

— Twernmilt,

Miły. Tak myślałem, że myślisz. Dziękuję Twernmilt. Jeśli chodzi o to, co warto, mam taką samą reakcję, jak ty: ja też spodziewałbym się, że odpowiedź będzie taka, że nie ma elementów typu zero baz.

— DW

Zgadzam się z Tobą. Istnieje bijection między bazi 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
źródło