coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marco Servetto <marco.servetto AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Finite Maps
- Date: Sat, 6 Aug 2011 09:37:19 +0200
Dear all,
Thanks for your adivces about finite maps but i'm totally lost.
I'm searching in internet an example of minimal usage for such maps
but I can't find it.
Moreover I have seen that setoid is (indirectly) required by such maps.
I have heard about setoid, most about the possibility of making rewrite with
<->
and i wonder if setoid adds axioms to do that and other stuff or if it
is only a smart use of other primitive tactique.
Moreover It is also quite clear that there is some "standard well
know" way to use abstract datastructures like this maps, but i have no
idea what it is, is there a guide about it? some sort of documentation
for "simple users".
I came from Java, I know basic of ocaml, that is my knoledge stops in
front of " locations for modifiable state" and "modules"
in the sense that I know nothing about the two.
W.r.t. coq I have have no problem in working with predefined lists,
nat, bool, and I fell/hope I have a decent understanding of type
classes, records with constraints, and basic of the tactique language.
From the point of view of mathematical charatterization of stuff, and
category (ring, morhism, vectorial space, axiom of choice) I know
really nothing.
What is your suggestion on how to proceed in the understanding of coq
/ setoid /finitemaps/finitesets ?
I should be able to insitantiate finitemaps/sets over keys of forms like
Inductive VarName : Set :=
| x : nat->VarName
| this.
Where function beq and blt are
Definition beq_VarName a b:= match a with
| this => match b with
|this =>true
| x i => false
end
| x ai => match b with
|this => false
|x bi => beq_nat ai bi end
end.
Definition blt_VarName a b := match b with
| this =>false
| x b1 => match a with
|this => true
|x a1=> blt_nat a1 b1
end
end.
------
That should be very straigthforward, I think.
- [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps,
Xavier Leroy
- Re: [Coq-Club] Finite Maps,
Marco Servetto
- Re: [Coq-Club] Finite Maps,
AUGER Cedric
- Re: [Coq-Club] Finite Maps,
Adam Chlipala
- Re: [Coq-Club] Finite Maps,
AUGER Cedric
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps, Adam Chlipala
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps, Adam Chlipala
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps, Adam Chlipala
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps, Adam Chlipala
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps,
AUGER Cedric
- Re: [Coq-Club] Finite Maps,
Adam Chlipala
- Re: [Coq-Club] Finite Maps,
AUGER Cedric
- Re: [Coq-Club] Finite Maps,
Marco Servetto
- Re: [Coq-Club] Finite Maps,
Xavier Leroy
Archive powered by MhonArc 2.6.16.