Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How to represent tabular data in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] How to represent tabular data in Coq
  • Date: Mon, 8 May 2017 17:14:52 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.mailfrom=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.helo=postmaster AT mx04.uni-tuebingen.de
  • Ironport-phdr: 9a23:5eVDDh0p8uR6YbPgsmDT+DRfVm0co7zxezQtwd8Zse0RLPad9pjvdHbS+e9qxAeQG96Kt7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXbAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmlicJOSM6/m/ZhMN/g75Urh26qhxj2o7Zep2ZOOZwc67fe94RWGpPXtxWVyxEGo6yao8PAPAcPeZDsoLzvkAOrQegCgm2AePg0DlIhnnr1qA90OQhFRvJ3BE7H94Ut3TUt8n1O7kIUeCw1qbIyzPDYuhL2Tf76YjEawwhoeySUr1rcMrRz0YvGB3DjlmKtIPqISqY2+IQuGaY9+ptTf+jhmAopg1rvDSj3MchhpPXio4IxV3I7Th1zYg6KNGiVkJ3e8OoHIVKuy2HN4Z6XsUvSHxytikg0L0Jo5u7cTAKyJs5wx7fbOSKc42H4x7/W+udOyp4hHRkeL6mmxay7Favxfb9Vsmy31ZFsCxFnsPRuX8TzxDT686HReVh/kq5xDqC2Q/e5vtaLUwulafXMYAtzqM/m5YLtETMBC72mEH4jK+McUUk//Cl6+fjYrr8u5+cLJV4igblMqQyhMO/G+E4PRIIX2id4um8ybvj/UzgTLVWk/05jLLWsJHcJcQUuKG5BRVZ3Zs95BqnFTepzMwYnWUbLFJCYB+Ik4/pO0jXLP/kCfe/nk+jnSxwx/HGO73hGo/CImLCkLfnZ7Z96lRTxBA9zdBFtNpoDeQKJ+u2UUvsvvTZCAU4Okq62bXJEtJ4g6AaUH+USoiCLK7ItFaO4Kp7IO2FeZRTvy3hJuIg7vjopWI/mBoBYKSj3J0YZXb+EvkwcBbRWmblntpUSTRChQE5VuG/0FA=

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





Archive powered by MHonArc 2.6.18.

Top of Page