Stream: Coq users

Topic: Decidable types


view this post on Zulip Adrián García (May 08 2021 at 19:59):

Hi, I'im trying to prove the equality for an slist of inductive types, but I cannot prove it unless I know that X is decidable, but how can I tell to Coq that X is decidable in eq_dec_slist proposition?

Inductive slist (X: Type): Type :=
 | empty : slist X
 | snoc : slist X -> X -> slist X.

Arguments empty {X}.
Arguments snoc {X} _ _.

Proposition eq_dec_slist (X: Type) (G G': slist X): {G = G'} + {G <> G'}.
Proof.
intros.
decide equality.
Abort.

view this post on Zulip Kenji Maillard (May 08 2021 at 20:03):

you should add it as an hypothesis:

Proposition eq_dec_slist (X: Type) (deceqX : forall x x' : X, {x = x'} + {x <> x'}) (G G': slist X): {G = G'} + {G <> G'}.
Proof.
intros.
decide equality.
Defined.

Last updated: Oct 05 2023 at 02:01 UTC