The Coq mailing list

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

Hi Saulo,

Saulo Araujo 
<saulo2 AT gmail.com>
 writes:

> 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.

I hope you have fun!

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

That's indeed a reasonably simple type. In this case the injectivity
proof is very similar to the decidability proof.

> 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.*

I attach a short and somewhat more generic proof using the idea we
discussed, the key point to make your life easier here is to generalize
a bit the theorem:

> Lemma to_list_inj_gen n m (x : List n) (y : List m) (i_eq : n = m) :
>   to_list x = to_list y -> eq_dep nat List n x m y.

My proof is a bit cumbersome, likely due to my unfamiliarity with LTAC,
using other tactic languages is just a couple of lines.

A couple of comments:

- Note instead of defining your own type, you may be better served by
  using a "subtype" of list, see [1] for more details, but the basic
  idea is to have:

  List T n = { val : list T ; _ : length val == n.+1 }

  For all such structures, val is injective, thus equality on the base
  type implies equality in the subtype.

- Regarding your questions about "In", if you are verifying an
  algorithm, you will be almost surely better suited by assuming
  decidability of you base types and using a version of In that is
  computational, similar to the typical ocaml mem:

  mem :: T -> list T -> bool
  mem a []      = false
  mem a (x::xs) = (a == x) || mem a xs

I don't know these two patterns are supported in the regular Coq Stdlib.

There are libraries that natively support such concepts, ask me in
private for more details if you are interested.

E.

[1] 
http://stackoverflow.com/questions/35290012/inductive-subset-of-an-inductive-set-in-coq

Attachment: saulo.v
Description: Binary data