9
$\begingroup$

I'm at the following exercise in 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 *)
[] *)

All of the answers I've seen on the Internet say that the answer is 2, and that the elements are x and y. If that's the case, then it's not clear to me what is meant by elements. There are certainly two constructors, but it's impossible to actually create a value of type baz.

It's impossible to create a value of type baz because x has type baz -> baz. y has type baz -> bool -> baz. In order to get a value of type baz we need to pass a value of type baz to either x or y. We can't get a value of type baz without already having a value of type baz.

So far I've been interpreting elements to mean values. So (cons nat 1 nil) and (cons nat 1 (cons nat 2 nil)) would both be elements of type list nat and there would be an infinite number of elements of type list nat. There would be two elements of type bool, which are true and false. Under this interpretation, I would argue that there are zero elements of type baz.

Am I correct, or can someone explain what I'm misunderstanding?

$\endgroup$
2
  • 1
    $\begingroup$ Sure. I've added a paragraph explaining why I think it's impossible to create a value of type baz. $\endgroup$ – Twernmilt Aug 24 '14 at 23:07
  • $\begingroup$ Nice. That's what I thought you were thinking. Thank you, Twernmilt. For what it's worth, I have the same reaction you do: I too would have expected the answer to be that there are zero elements of type baz. $\endgroup$ – D.W. Aug 24 '14 at 23:17
8
$\begingroup$

I agree with you. There's a bijection between baz and 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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.