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?
Asked By : Twernmilt
Answered By : Rui Baptista
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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/29365
0 comments:
Post a Comment
Let us know your responses and feedback