The Coq mailing list

[Morgan Sinclaire <morgansinclaire AT boisestate.edu>]

I'm having an issue with a certain construction. The details/background shouldn't be important, but I have types "formula", "ord", and "nf : ord -> Prop" defined (the latter two taken from a paper). I'm trying to build a new type "ptree" and assign members of type "e_0" to it in a certain way. Here's the relevant (grossly abridged) part of my code:

Definition e_0 : Set := {a : ord & nf a}.

Theorem Zero_nf : nf Zero.

Proof. apply zero_nf. Qed.

Inductive ptree : Type :=

| node_p : formula -> e_0 -> ptree.

Fixpoint finite_valid_p (t : ptree) : Prop :=

  match t with

  | node_p f alpha => alpha = exist nf Zero Zero_nf

  end.

When I run that, the Fixpoint fails with the error:

"The term "exist nf Zero Zero_nf" has type "{x : ord | nf x}"

while it is expected to have type "e_0"."

Which I don't understand, since that's exactly how I defined e_0. On the other hand, when I changed the definition of "ptree" to:

Inductive ptree : Type :=

| node_p : formula -> {x : ord | nf x} -> ptree.

Then everything works. What am I doing wrong here?

Thanks,

Morgan