Morgan Sinclaire

2018-11-08 19:50:47 UTC

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

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