# Decidable equality with Prop-carrying type

Hello!

In a development I’m working on, I have a type that represents the combination of a string and a proof that the string is “valid” according to some rules. Validity is decidable, and I’m trying to show that equality of names is decidable, but I’m running up against something I don’t know how to solve:

``````Require Import Coq.Lists.List.
Require Import Coq.Unicode.Utf8_core.
Require Import Coq.Strings.String.

Open Scope string_scope.
Open Scope char_scope.

Import ListNotations.

Set Mangle Names.

Definition acceptable_characters : list Ascii.ascii :=
list_ascii_of_string "abcdefghijklmnopqrstuvwxyz0123456789_.".

Definition valid_name (s : string) : Prop :=
Forall (λ c, In c acceptable_characters) (list_ascii_of_string s)
∧ length s >= 1
∧ length s <= 256.

(* Whether all characters in a string are valid is decidable. *)
Lemma valid_name_acceptable_dec : ∀ s,
{Forall (λ c, In c acceptable_characters) (list_ascii_of_string s)}
+
{¬ Forall (λ c, In c acceptable_characters) (list_ascii_of_string s)}.
Proof.
intros s.
apply Forall_dec.
intro x.
apply in_dec.
apply Ascii.ascii_dec.
Qed.

(* Whether a string is non-empty is decidable. *)
Lemma valid_name_length1_dec : ∀ s,
{length s >= 1}+{¬ length s >= 1}.
Proof. intros s. apply Compare_dec.ge_dec. Qed.

(* Whether a string is short enough is decidable. *)
Lemma valid_name_length256_dec : ∀ s,
{length s <= 256}+{¬ length s <= 256}.
Proof. intros s. apply Compare_dec.le_dec. Qed.

(* Whether a string is valid is decidable. *)
Lemma valid_name_dec : ∀ s,
{valid_name s}+{¬ valid_name s}.
Proof.
intros s.
unfold valid_name.
destruct (valid_name_acceptable_dec s); firstorder.
destruct (valid_name_length1_dec s); firstorder.
destruct (valid_name_length256_dec s); firstorder.
Qed.

(* A name, and a proof that the name is valid. *)
Inductive action_name_t :=
ActionName : ∀ s, valid_name s → action_name_t.

(* Whether two names are equal is decidable. *)
Lemma action_name_eq_dec : ∀ (s0 s1 : action_name_t),
{s0 = s1}+{s0 <> s1}.
Proof.
intros s0 s1.
destruct s0 as [s0s s0p].
destruct s1 as [s1s s1p].
destruct (string_dec s0s s1s) as [Hseq|Hsneq]. {
left.
rewrite Hseq.
}
``````

The `rewrite Hseq` tactic fails:

``````Abstracting over the term "s0s" leads to a term λ _0 : string, ((ActionName _0 s0p) = (ActionName s1s s1p))
which is ill-typed.
Reason is: Illegal application:
The term "ActionName" of type "∀ _0 : string, ((valid_name _0) → action_name_t)"
cannot be applied to the terms
"_0" : "string"
"s0p" : "valid_name s0s"
The 2nd term has type "valid_name s0s" which should be coercible to "valid_name _0".
``````

This is reasonable, but I’m not sure how to proceed. The equality of the two proof terms is irrelevant to the equality of the values as a whole. Is this a case where I need to include the proof irrelevance axiom? If so, what would be the correct way to apply it here? I’ve avoided all axioms up to now, and I’m a little concerned about soundness.

While I wouldn’t worry too much about adding a proof-irrelevance axiom in this case, it’s nice to know that there is a straightforward workaround.

Specifically, you write that your validity criterion is decidable. This being the case, you can replace `valid_name s` by `valid_name_checker s = true`, where `valid_name_checker` is a function returning a Boolean. The benefit of doing this is that you have UIP (uniqueness of identity proofs) for types with decidable equality, like `bool`:

``````Axiom valid_name_checker: string -> bool.
Axiom valid_name_checker_ok: forall s,
valid_name_checker s = true <-> valid_name s.

(* A name, and a proof that the name is valid. *)
Inductive action_name_t :=
ActionName : ∀ s, valid_name_checker s = true → action_name_t.

(* Whether two names are equal is decidable. *)
Lemma action_name_eq_dec : ∀ (s0 s1 : action_name_t),
{s0 = s1}+{s0 <> s1}.
Proof.
intros s0 s1.
destruct s0 as [s0s s0p].
destruct s1 as [s1s s1p].
destruct (string_dec s0s s1s) as [Hseq|Hsneq]. {
left.
destruct Hseq. (* Rewrite everywhere *)
pose proof (Eqdep_dec.UIP_dec Bool.bool_dec s0p s1p) as Heqpr.
destruct Heqpr. (* Rewrite everywhere *)
reflexivity.
(* … etc: continue the proof here *)
``````

Thank you! That makes sense.