The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi Dominique,

Thanks a lot for providing this shorter proof. I am going to study it with care so that I can apply similar techniques in other dependent type equalitity decidability proofs.

Sincerely,

Saulo

On Wed, Feb 24, 2016 at 7:49 AM, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Hi Saul,

May I suggest the following shorter proof for the decidability
of equality over List Digit n.

*****************************************************

Section List.

  Variable E : Type.

  Inductive List : nat -> Type :=
    | ListLeaf: E -> List 0
    | ListNode n: E -> List n -> List (S n).

  Definition List_leaf (l : List 0) := match l with | ListLeaf e => e end.

  Definition List_head n (l : List (S n)) := match l with | ListNode _ e
_ => e end.
  Definition List_tail n (l : List (S n)) := match l with | ListNode _ _
t => t end.

  Hypothesis eqE_dec : forall x y : E, { x = y } + { x <> y }.

  Definition List_inv_t n :=
    match n return List n -> Type with
      | 0   => fun a => { e | a = ListLeaf e }
      | S n => fun a => { e : _ & { b | a = ListNode _ e b } }
    end.

  Definition List_inv n l : List_inv_t n l.
  Proof.
    destruct l as [ e | n e l ]; simpl.
    exists e; reflexivity.
    exists e, l; reflexivity.
  Defined.

  Definition eq_List_dec n (a b : List n) : { a = b } + { a <> b }.
  Proof.
    revert b; induction a as [ e | n e a IHa ]; intros b.

    destruct (List_inv _ b) as (f & Hb).
    destruct (eqE_dec e f) as [ | C ].

    left; subst; reflexivity.

    right; subst; contradict C.
    apply f_equal with (f := List_leaf) in C.
    apply C.

    destruct (List_inv _ b) as (f & c & Hb).
    destruct (eqE_dec e f) as [ | C ].
    destruct (IHa c) as [ | D ].

    left; subst; reflexivity.

    right; subst; contradict D.
    apply f_equal with (f := List_tail _) in D.
    apply D.

    right; subst; contradict C.
    apply f_equal with (f := List_head _) in C.
    apply C.
  Defined.

End List.

Inductive Digit :=
| D0
| D1.

Definition eq_Digit_dec (x y : Digit) : { x = y } + { x <> y }.
Proof.
  decide equality.
Defined.

Theorem List_Digit_dec:
  forall n (cs ds: List Digit n), {cs = ds} + {cs <> ds}.
Proof.
  apply eq_List_dec, eq_Digit_dec.
Defined.

******************************************

Best regard,

Dominique

-------------------------------------

On 02/23/2016 12:49 PM, Saulo Araujo wrote:
> Hi Emilio,
>
> Thanks a lot for expanding your previous answer. As I´m studying
> dependent type programming in Coq in my spare time, it will take me some
> some days to try your suggestion. In any case, my dependent type is a
> very simple one:
>
> *Inductive List E: nat -> Type :=*
> *| ListLeaf: E -> List E 0*
> *| ListNode n: E -> List E n -> List E (S n).*
> *
> *
> *Inductive Digit :=*
> *| D0*
> *| D1.*
>
> Below is my proof of the decidability of List Digit n:
>
> *Theorem list_digit_dec:*
> *  forall n (cs ds: List Digit n), {cs = ds} + {cs <> ds}.*
> *Proof.*
> *  intros.*
> *  induction n. *
> *  {*
> *    assert ({c | cs = ListLeaf c}).*
> *    {*
> *      refine match cs with*
> *             | ListLeaf c => _*
> *             end.*
> *      exists c.*
> *      reflexivity.*
> *    }*
> *    destruct H as [c H].*
> *    rewrite H.*
> *
> *
> *    assert ({d | ds = ListLeaf d}).*
> *    {*
> *      refine match ds with*
> *             | ListLeaf d => _*
> *             end.*
> *      exists d.*
> *      reflexivity.*
> *    }*
> *    destruct H0 as [d H0].*
> *    rewrite H0.*
> *
> *
> *    destruct c.*
> *    {*
> *      destruct d.*
> *      {*
> *        apply left.*
> *        reflexivity.*
> *      }*
> *      {*
> *        apply right.*
> *        unfold not.*
> *        intros.*
> *        inversion H1.*
> *      }*
> *    }*
> *    {*
> *      destruct d.*
> *      {*
> *        apply right.*
> *        unfold not.*
> *        intros.*
> *        inversion H1.*
> *      }*
> *      {*
> *        apply left.*
> *        reflexivity.*
> *      }*
> *    }*
> *  }*
> *  {*
> *    assert ({c: _ & {cs' | cs = ListNode c cs'}}).*
> *    {*
> *      refine match cs with*
> *             | ListNode _ c cs' => _*
> *             end.*
> *      exists c.*
> *      exists cs'.*
> *      reflexivity.*
> *    }*
> *    destruct H as [c H].*
> *    destruct H as [cs' H].*
> *    rewrite H.*
> *
> *
> *    assert ({d: _ & {ds' | ds = ListNode d ds'}}).*
> *    {*
> *      refine match ds with*
> *             | ListNode _ d ds' => _*
> *             end.*
> *      exists d.*
> *      exists ds'.*
> *      reflexivity.*
> *    }*
> *    destruct H0 as [d H0].*
> *    destruct H0 as [ds' H0].*
> *    rewrite H0.*
> *
> *
> *    destruct c.*
> *    {*
> *      destruct d.*
> *      {*
> *        specialize IHn with cs' ds'.*
> *        destruct IHn.*
> *        {*
> *          left.*
> *          congruence.*
> *        }*
> *        {*
> *          right.*
> *          contradict n0.*
> *          inversion n0.*
> *          apply inj_pair2_eq_dec.*
> *          apply eq_nat_dec.*
> *          apply H2.*
> *        }*
> *      }*
> *      {*
> *        right.*
> *        contradict H.*
> *        inversion H.*
> *      }*
> *    }*
> *    {*
> *      destruct d.*
> *      {*
> *        right.*
> *        contradict H.*
> *        inversion H.*
> *      }*
> *      {*
> *        specialize IHn with cs' ds'.*
> *        destruct IHn.*
> *        {*
> *          left.*
> *          congruence.*
> *        }*
> *        {*
> *          right.*
> *          contradict n0.*
> *          inversion n0.*
> *          apply inj_pair2_eq_dec.*
> *          apply eq_nat_dec.*
> *          apply H2.*
> *        }*
> *      }*
> *    }*
> *  }*
> *Qed.*
> *
> *
> Sincerely,
> Saulo
> *
> *
>
>
> On Mon, Feb 22, 2016 at 7:51 PM, Emilio Jesús Gallego Arias
> <e+coq-club AT x80.org <mailto:e+coq-club AT x80.org>> wrote:
>
>     Hi Saulo,
>

>     Saulo Araujo <saulo2 AT gmail.com <mailto: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.
>
>