The Coq mailing list

[(e29315a54f%hidden_head%e29315a54f)l-siebeneicher(e29315a54f%hidden_at%e29315a54f)versanet.de(e29315a54f%hidden_end%e29315a54f)]

Dear Reader, 

I am a Coq-Beginner.

Till now I did not find a replacement for FMaps, so I try to use them.
The module 'Reference' tries to encapsulate a key of type nat onto another
type.  The Idea behind ... I try to make 'keys' of a FMap only working for a
speciffic map, Encapsulating it into another Module. Like That.


(* BEGIN COQ *)
Module MyEncapsulatedMap.
Module MyMap := FMapAVL.Make (Reference).
End MyEncapsulatedMap.
(* END COQ *)


(* BEGIN COQ *)
Module Reference <: UsualOrderedType.
Module O := Nat_as_OT.
Record reference : Type := 
  mkRef { 
    ref  : nat
  }.

Definition t := reference.

(* ((1)) --- Uncomment this or below *
Definition eq      (r1 r2 : reference)  := 
  O.eq (ref r1) (ref r2).
Definition eq_refl (r : reference) :=  
  eq r r.
Definition eq_sym := 
  forall (r1 r2 : reference), eq r1 r2 -> eq r2 r1.
Definition eq_trans (r1 r2 : reference) := 
  forall (r1 r2 r3 : reference),
    eq r1 r2 -> eq r2 r3 -> eq r1 r3.
*)

(* ((2)) --- Uncomment this or above *
Definition eq       := @eq reference.

Definition eq_refl  := @eq_refl reference.
Definition eq_sym   := @eq_sym reference.
Definition eq_trans := @eq_trans reference.
*)

Definition lt (r1 r2: reference) := O.lt (ref r1) (ref r2).

Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
Proof. 
  unfold lt.
  intros (r1) (r2) (r3).
  simpl.
  apply O.lt_trans.
Qed.

Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof.
  unfold lt.
  intros (r1) (r2); simpl.
  unfold eq. simpl.
  apply O.lt_not_eq.
Qed.

Definition compare (r1 r2 : reference) := O.compare (ref r1) (ref r2).
Definition eq_dec (r1 r2 : reference) := O.eq_dec (ref r1) (ref r2).
End Reference.
(* END COQ *)





Firstly I tried to code with ((1)) uncommented. Every proof works well. 
But continuing to 'End Referende' I get this error:

>> "Error: Signature components for label eq do not match."




That Way, I dont get further. If I try to code with ((2)) uncommented. I do 
not
really understand what the terms (@eq, @eq_refl, etc) mean. Do those
@<ident>-Terms generate Coq-Code (like Template Haskell)? 

Well, I also need to change the proof for 'lt_not_eq'.

(* BEGIN COQ *)
Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof.
Proof.
  unfold lt.
  intros (r1) (r2); simpl.
  intro.
  red.

 (*etcetera*)
Qed.
(* END COQ *)

Stopping at 'red'.
This Goal is shown then:

eq {| ref := r1 |} {| ref := r2 |} -> False     

(r1 r2 have type nat) 

Currently I do not know how to solve this, as I do not know how to tell coq to
use r1 and r2 to compute equality. 
Defining Equality 'by hand' leads to the Error-Message ( "Error: Signature
components for label eq do not match.")

Thank you for reading.

Leonard Siebeneicher