The Coq mailing list

[Leonard Siebeneicher <l-siebeneicher AT versanet.de>]

Hi Thomas,

thank you for your answer. I needed some time to answer, because I tried 
myself to get something working using OrderedTypeAlt.

You asked about the idea behind.

Instead of using a nat as key for a FMap of strings, numbers or tuples, 
I rather like to use own types for each FMap.
(FMap//stringKey  -> string ) instead of (FMap//nat -> string)
(FMap//tupleKey   -> nat,nat) instead of (FMap//nat -> nat,nat)
(FMap//integerKey -> integer) instead of (FMap//nat -> integer)

Using a functor I like to generate new types for such Keys automatically 
for a type.
> Module Type TypDesc.
> Parameter t.
> End TypDesc.
...
> Module GenerateKey (D : TypDesc) <: OrderedType.
...
(D: TypDesc) is only dummy. It is not used within GenerateKey. But, it 
makes Coq generating a new type automatically
> End GenerateKey.

But, (D:TypDesc) is used within this module.
> Module EncapsulatedMap (D : TypDesc).
> Module KeyTypes := GenerateKey (D).
> Module Map := FMapAVL.Make(KeyTypes).
>
> Definition itsMap := Map.t (D.t).
> End EncapsulatedMap.

Given some modules (itsANatTuple : TypDesc) (itsAString : TypDesc) we can do

> Module  TupleMap := EncapsulatedMap (itsANatTuple).
> Module StringMap := EncapsulatedMap (itsAString).
We cannot use a key from StringMap to access tuples from TupleMap. 
Because, they have different types. Thats the idea behind it.


Am still struggling with equations.
I thing I lack some fundamental knowledge about how to use Proof-Mode.
Below is a try, to define a Module out of OrderedTypeAlt.

Best Regards,
Leonard.

(* BEGIN COQ-FILE "StrugglingWithOTA.v" *)
Require Import Structures.OrderedTypeAlt.
Require Import Structures.OrderedTypeEx.



Module Type KeyTarget.
Parameter t : Type.
End KeyTarget.



Module MyKey (K : KeyTarget) <: OrderedTypeAlt.

Inductive a_key := key : nat -> a_key.

Definition t := a_key.
Definition compare (k1 k2 : a_key) : comparison :=
  match (k1,k2) with
  | (key n1, key n2) => NatOrderedType.Nat_as_OT.compare n1 n2

  end.

Infix "?=" := compare (at level 70, no associativity).


Definition compare_sym :
  forall x y, (y?=x) = CompOpp (x?=y).
Proof.
  intros x y.
  induction x; induction y.
  induction n; induction n0.
  unfold "?="; simpl; auto.
  unfold "?="; simpl; auto.
  unfold "?="; simpl; auto.

  (* how to get out of recursion ... still learning *)
Qed.


Definition compare_trans :
   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
Proof.
  intros c x y z.
  induction x; induction y; induction z.
  intros H1 H2.
  symmetry in H1.
  symmetry in H2.
  rewrite H1.

  (* struggling again. Need to understand how to deal with equalities 
in Coq? *)
Qed.

End MyKey.

(* END COQ-FILE "StrugglingWithOTA.v" *)