The Coq mailing list

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

Title: RE: [Coq-Club] Finite Map - Unable to prove a simple lemma

Thanks Stéphane. Your proof script proved the lemma. Greatly appreciate your help.
Sunil

-----Original Message-----
From: Stéphane Lescuyer [mailto:stephane.lescuyer AT polytechnique.org]
Sent: Tue 10/28/2008 6:22 PM
To: Sunil Kothari
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Finite Map - Unable to prove a simple lemma

Hello,

There's sufficient information in the interface here. Lemma M.find_2
in the interface tells you that if find n s does not return None but
some element a, s maps n to a (and therefore n is in s), which means
you have a contradiction with your hypothesis. On the other hand, if
find n s returns None, then your goal is trivial. Here is a
stand-alone proof script :

Require Import OrderedType FMapInterface.

Declare Module E : OrderedType.
Declare Module M : FMapInterface.S with Module E := E.

Parameter A : Type.

Goal forall (s : M.t A) (e : E.t), ~(M.In e s) -> M.find e s = None.
Proof.
  intros s e Hnotin.
  case_eq (M.find e s); intros; [|reflexivity].
  contradiction Hnotin; exists a; exact (M.find_2 H).
Qed.

HTH,

Stéphane L.

On Wed, Oct 29, 2008 at 12:29 AM, Sunil Kothari <skothari AT uwyo.edu> wrote:
> 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.



--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06