The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Saulo,

Saulo Araujo 
<saulo2 AT gmail.com>
 writes:

> Have you got a small example of this technique that you could share?

I'm sorry I wasn't more concrete. I'll try to make an example without
requiring external libraries.

What I meant is a technique that actually happens two steps:

a) Find an injective representation of your dependent type T into a
   "simpler" one U. This way, you can reuse the proof of decidability of
   U as this holds:

8<--------------------------------------------------------------------8<
Section EqInj.

Variable (T U : Type).

Definition injective (f : T -> U) := forall (x y : T), f x = f y -> x = y.
Definition eq_dec T := forall (x y : T), {x = y} + {x <> y}.

Variable (f : T -> U).
Hypothesis (f_inj : injective f).
Hypothesis (U_dec : eq_dec U).

Lemma eq_inj : eq_dec T.
Proof.
intros x y; destruct (U_dec (f x) (f y)) as [u_eq|u_neq].
+ now apply f_inj in u_eq; rewrite u_eq; left.
+ now right; intros xy_eq; apply u_neq; rewrite xy_eq.
Qed.

End EqInj.
8<--------------------------------------------------------------------8<

Fair enough, now the key is, what should U be? Usually you want U to be
a type such that its decidability can be inferred automatically. This is
what happens in math-comp if you use a combination of the basic data
types, pairs, products, sigma types, etc...

b) Composing decidability proofs:

For instance, if two types are decidable, their sum is:

8<--------------------------------------------------------------------8<
Section EqSum.

Variable (T U : Type).

Definition eq_dec T := forall (x y : T), {x = y} + {x <> y}.

Hypothesis (T_dec : eq_dec T).
Hypothesis (U_dec : eq_dec U).

Lemma sum_dec : eq_dec (T + U).
Proof.
intros [x1|y1] [x2|y2]; try (right; congruence).
+ destruct (T_dec x1 x2) as [t_eq|t_neq]; try (right; congruence).
  - now rewrite t_eq; left.
+ destruct (U_dec y1 y2) as [u_eq|u_neq]; try (right; congruence).
  - now rewrite u_eq; left.
Qed.

End EqSum.
8<--------------------------------------------------------------------8<

I learn this technique from the math-comp library where it is used
extensively and may be the best source of examples. There you have the
advantage that b) happens mostly automatically, so providing a) works
quite well. A randomly picked example:

> Definition natsum_of_int (m : int) : nat + nat :=
>   match m with Posz p => inl _ p | Negz n => inr _ n end.
>
> Definition int_of_natsum (m : nat + nat) :=
>   match m with inl p => Posz p | inr n => Negz n end.
>
> Lemma natsum_of_intK : cancel natsum_of_int int_of_natsum.
> Proof. by case. Qed.
>
> Definition int_eqMixin := CanEqMixin natsum_of_intK.
> Definition int_countMixin := CanCountMixin natsum_of_intK.
> Definition int_choiceMixin := CountChoiceMixin int_countMixin.

Note that the same technique is used not only to derive decidability of
equality but to derive countable and choice instances. 

The concrete example I was thinking of is following:

imagine your original datatype T is a very complex dependent data type
with lots of well-formedness conditions. This type may be hard to
program and work with, however, there exists a forgetful injection into
a type with no well-formedness conditions, but which has a composable
decidability proof in virtue of its "simple" nature.

Maybe it would help if you could post a small example of your dependent
data type, so we could try to figure out whether there exists such an
embedding or not.

I hope it helps.
E.