The Coq mailing list

[Leonard Siebeneicher <(e29315a54f%hidden_head%e29315a54f)l-siebeneicher(e29315a54f%hidden_at%e29315a54f)versanet.de(e29315a54f%hidden_end%e29315a54f)>]

(Title should be: struggling creating a Module of type UsualOrderedType )


Dear Reader,

I am sorry for the missing title. After I send the message from 
"sympa-roc.inria.fr/wws/" I got an error that there were illegal chars 
within the title. The posting appeared within the mailing list --- but 
it dropped the title completely. And there is no way to correct it but 
to delete it.



Without Coq, I would simply solve the equation on paper
> eq {| ref := r1 |} {| ref := r2 |}
Using the fact that
))) ref {| ref :=r |} === r     (* r is a nat *)
I would apply ref on both sides of equation. Then I would get

))) r1 === r2 (* r1 and r2 are nat's *)

After this we have a term

)))  r1 < r2 -> not (r1 === r2)    (* r1 and r2 are nat's *)

(r1 === r2) shold be (Nat_as_OT.eq r1 r2) and (r1 < r2) should be 
(Nat_as_OT.lt r1 r2)

We have

(Nat_as_OT.lt r1 r2) -> ~(Nat_as_OT.eq r1 r2)

We could ...

apply Nat_as_OT.lt_not_eq

and we are done.

My problem ... I do not know how this could be done in coq.


Please help me, I am new to COQ.


Best Regards,
Leonard Siebeneicher



(*
BEGIN COQ (( Executable code. ))
*)

Require Import FSets.FSets.

Require Import FSets.FMaps.
Require Import FSets.FMapAVL.




Module Type RChanDesc.
Parameter r : Type.
End RChanDesc.




(* We use references to access entities of a FMap *)

Module Reference (R : RChanDesc) <: UsualOrderedType.
Module O := Nat_as_OT.

Record reference : Type :=
  mkRef {
    ref  : nat
  }.

Definition t := reference.


Definition eq      (r1 r2 : reference) : Prop :=
  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.
(* ((1)) Uncomment this
*)

(* ((2)) Uncomment this
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 eq_sub : forall (ref1 ref2: reference),
  eq ref1 ref2 -> (ref ref1) = (ref ref2).
Proof.
  intros (r1) (r2).
  simpl.
  auto.
Qed.

Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
Proof.
  intros (r1) (r2).
  unfold lt. 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.





(* Encapsulating a FMap into a RChannel *)

Module RChannel (R : RChanDesc).
Module RefM := Reference(R).
Module RMap := FMapAVL.Make(RefM).
(* etcetera *)
End RChannel.


(*
END COQ
*)