The Coq mailing list

[Ben Sherman <sherman AT csail.mit.edu>]

If you're just looking to represent something like this (rather than implement it with some efficient data structure), you can basically do exactly what you wrote:

Inductive member {A} (x : A) : list A -> Type :=

  | here : forall xs, member x (x :: xs)

  | there : forall y xs, member x xs -> member x (y :: xs).

Infix "∈" := member (at level 30).

Record Table (R C : Type) (r : list R) (c : list C) A := MkTable

  { lookup : forall x y, x ∈ r -> y ∈ c -> A }.

(* Another version, which could be a bit easier in saving

   you from needing UIP unnecessarily *)

Inductive members {A} : list A -> Type :=

  | here' : forall x xs, members (x :: xs)

  | there' : forall x xs, members xs -> members (x :: xs).

Record Table' (R C : Type) (r : list R) (c : list C) A :=

  MkTable' { lookup' : members r -> members c -> A }.

The [member] inductive family is not in the Coq standard library, though it's a common thing to do. I can point you to various code defining such a family that could have lemmas you could use that you might find useful:

http://adam.chlipala.net/cpdt/html/DataStruct.html

https://github.com/coq-ext-lib/coq-ext-lib/blob/v8.5/theories/Data/Member.v

https://github.com/bmsherman/topology/blob/master/src/Types/List.v#L8-L10

(You might notice that [list unit] is isomorphic to [nat], and similarly [@members unit] is isomorphic to [Fin.t], and [Fin.t n -> A] is isomorphic to [Vector.t A n], which relates some of the definitions here to [Vector.t].) 

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>

Subject: [Coq-Club] How to represent tabular data in Coq

Date: May 8, 2017 at 11:14:52 AM EDT

To: coq-club AT inria.fr

Reply-To: coq-club AT inria.fr

I have data that one would write down on a piece of paper as a table
with row and column headers.

The type of the headers is not "nat", though (otherwise I could use
nested vectors).
Let's call them R and C for the type of row headers and column headers,
respectively.
The type of the table elements is A.

Let's say I have finite sets r and c of R's and C's, respectively. r and
c are the labels
of a particular table.

Such a table should feature a function to look up an entry in the table,
which should
have a type similar to this:

lookup: Table R C r c A -> x in r -> y in c -> A

where "x in r" means a label x that is in the label set r.

In particular, the lookup function should not return an "option A".

Is there something like this in a standard library? How would I go about
this?

As a starter, is there something that is to standard finite maps as
vectors are to lists?
That is, finite maps where the type system keeps track of the available
keys?

Klaus