The Coq mailing list

["Sunil Kothari" <skothari AT uwyo.edu>]

Hello Coq Users,

   I am programming against the finite map interface based on my earlier posting to this list http://pauillac.inria.fr/pipermail/coq-club/2008/003945.html. I am trying to prove a very simple lemma but somehow I feel the interface (FMapInterface) is missing something. The lemma I am trying to prove is:

 

 forall s:M.t type, forall n:nat,
not (M.In n s) <->  M.find n s = None.

 

I was able to prove the lemma  from right to left (please see the below Coq script).

forall s:M.t type, forall n:nat,
 M.find n s = None -> not (M.In n s) 

 

But I am unable to prove  the other direction i.e.:

forall s:M.t type, forall n:nat,
not (M.In n s) -> M.find n s = None.

 

How can I prove it ?  Looking at the proof script you can see I couldn't make much progress. My incomplete  script (and all other needed code) is given below.

 

Is it because the axiom set (as given FMapInterface) is incomplete ?

 

Please help.

Sunil

--------------------------

Require Import FMapInterface.
Require Import OrderedTypeEx.

Inductive type:Set :=
    TyVar : nat -> type
  | Arrow : type -> type -> type .

Module Nat_as_MyOT <: UsualOrderedType := Nat_as_OT.

Module MyStuff (M:FMapInterface.S with Module E := Nat_as_MyOT).
(* the type of maps *)

Lemma none_and_find : forall s:M.t type, forall n:nat,
M.find n s = None -> not (M.In n s).
Proof.
intros.
unfold not.
intros.
unfold M.In in H0.
elim H0; intros.
apply M.find_1 in H1.
rewrite H in H1.
inversion H1.
Qed.

Lemma find_and_none: forall s:M.t type, forall n:nat,
not (M.In n s) ->  M.find n s = None.
Proof.
intros.
unfold M.In in H.