The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

Dear Ben,

thanks these are very useful pointers.

A few question, though: Why don't you use the "In" predicate from
the standard library instead of "member"?

Haven't you only given me the interface for tables but not their
representation?
How would I construct an actual table?

The difference between "member" and "members" is also interesting.
How do I "see" that "member" requires UIP?

Another mailing list member pointed me to another solution based on
hlists like
described in Chlipala's book
(http://adam.chlipala.net/cpdt/html/DataStruct.html).

With hlist, a table could be represented as:

Definition table (A R C : Type) (r : list R) (c : list C) : Type :=
  hlist (fun _ => hlist (fun _ => A) c) r.

Definition lookup A R C (r : list R) (c : list C) (t : table A r c) x y
           (mx : member x r) (my : member y c) : A :=
  hget my (hget mx t).

I found out that in my particular application it is useful if the type
of cells can
depend on the row and column labels. With hlist, this can be encoded as:

Definition table' (R C : Type) (r : list R) (c : list C)(celltype: R ->
C -> Type) : Type :=
  hlist (fun r => hlist (fun c => celltype r c) c) r.

Definition lookup' R C (r : list R) (c : list C) ct (t : table' r c ct) x y
           (mx : member x r) (my : member y c) : ct x y :=
  hget my (hget mx t).

I've constructed a small library around these definitions. If anyone
wants to take a look:
https://gist.github.com/klauso/ffcff8c37fe62f3af5dc1cde878d941c

Thanks and best regards,
Klaus