Decidable equality with Prop-carrying type

Using Coq
1

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.

2

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 *)
3

Thank you! That makes sense.