coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] How to represent tabular data in Coq, Klaus Ostermann, 05/08/2017
- Re: [Coq-Club] How to represent tabular data in Coq, Wilayat Khan, 05/09/2017
- <Possible follow-up(s)>
- Re: [Coq-Club] How to represent tabular data in Coq, Ben Sherman, 05/10/2017
- Re: [Coq-Club] How to represent tabular data in Coq, Klaus Ostermann, 05/10/2017
- Re: [Coq-Club] How to represent tabular data in Coq, Ben Sherman, 05/17/2017
- Re: [Coq-Club] How to represent tabular data in Coq, Jason Gross, 05/17/2017
Archive powered by MHonArc 2.6.18.