CODEWITHSUNDEEP
coq
user251130
user251130

Reputation: 33

Decide equality with some predicate

I would like to prove that equality is decidable for those a that satisfy some predicate P:

Variable C: Type.
Inductive A: Type:=
    | A0: C -> A.
Variable P: A -> Prop.
Variable P_dec: forall a: A, {P a} + {~ P a}.

Definition A_dec: forall a b, {a = b} + {a <>  b} + {~ P a}.

But using decide equality, I lose the information that a satisfies P:

intros. destruct (P_dec a). left. decide equality.

I get

a, b: A
p: P a
c, c0: C
----------
{c = c0} + {c <> c0}

and I cannot use the fact that we have P (A0 c). It seems to me that somehow I am legitimate to assume that a = P c - how can I proceed to get this information?

Upvotes: 0

Views: 218

Answers (1)

Pierre Cast&#233;ran
Pierre Cast&#233;ran

Reputation: 916

Do you have any hypothesis on C? For instance :

Variable Ceqdec : forall c c':C, {c = c'}+{c <> c'}.

Some types don't have this possibility (e.g; C = nat->nat)

About your other question : You may start your proof with intros [c] [c0] in order to decompose aand b.

Upvotes: 1

Related Questions