The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

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.