The Coq mailing list

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

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

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

Date: May 10, 2017 at 4:19:57 AM EDT

To: coq-club AT inria.fr

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"?

Note that [In] is a prop, whereas [member] is a type. Since [In] is a prop, it can't be used to retrieve any information, like looking up an element in a list. For example, imagine the list [1; 1]. If I have [p : In 1 [1; 1]], I don't know whether the proof was made with the first or second member of the list (in particular, it is admissible to assume that all elements of [In 1 [1; 1] are equal), but if I have [p : member 1 [1; 1]], that data may be used computationally.

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

You would write a lambda that computes the value from the indices (i.e., [members] terms) that are input. So you'd be pattern matching on those [members] terms. Here's some example code that might give some idea:

Fixpoint get_members {A} {xs : list A} (m : members xs) : A

  := match m with

  | here' x _ => x

  | there' _ _ m' => get_members m'

  end.

Fixpoint to_nat {A} {xs : list A} (m : members xs) : nat 

  := match m with

  | here' _ _ => 0

  | there' _ _ m' => S (to_nat m')

  end.

Fixpoint eq_members {A B} {xs : list A} {ys : list B}

  (m : members xs) (m' : members ys) :=

  Nat.eqb (to_nat m) (to_nat m').

Definition ComputeTable {R C A} (r : list R) (c : list C)

  (f : R -> C -> A) : Table' R C r c A :=

  {| lookup' := fun mr mc => f (get_members mr) (get_members mc) |}.

Definition UpdateTable {R C A r c}

  (t : Table' R C r c A) (mr : members r) (mc : members c)

  (a : A)

  : Table' R C r c A

  := {| lookup' := fun mr' mc' =>

   if andb (eq_members mr mr') (eq_members mc mc')

     then a

     else lookup' _ _ _ _ _ t mr' mc' |}.

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

Sorry, I wasn't clear about this. Neither one requires UIP. But I believe the types [members xs] and [sigT (fun x => member x xs)] are isomorphic only if [A] satisfies UIP. The reason is that [member] could be equivalently defined

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

  | here : forall y xs, x = y -> member x (y :: xs)

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

So if there is more than one proof of [x = y], there will be more elements in [sigT (fun x => member x xs)] than [members xs]. Usually I've found that I prefer [members] to [member] for this reason.