[Coq-Club] Problem with Definition Matching

[Morgan Sinclaire]

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

[Gaëtan Gilbert]

{ x : foo & bar } and { x : foo | bar } are different types (sigT and
sig respectively)
exist produces sig, you need existT for sigT

(sig accepts only Prop for the second component, the difference is
useful for extraction)

Gaëtan Gilbert

Post by Morgan Sinclaire
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
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.
"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
Inductive ptree : Type :=
| node_p : formula -> {x : ord | nf x} -> ptree.
Then everything works. What am I doing wrong here?
Thanks,
Morgan