The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Tue, Feb 24, 2009 at 01:21:24AM +0000, Ashish Darbari wrote:
> 
> 
> Am trying to prove a lemma on maps 
> 
> Require Import FMapAVL.
> Module FMap := FMapAVL.Make(Z_as_OT).
> 
> forall (tbl:FMap.t (list Z)), 
> (FMap.is_empty tbl = true) ->
> forall (key:Z), (FMap.find key tbl = None). 
> 
> 
> but not sure where to start. I tried adding the property not_find_iff
> by invoking 
> 
> generalize FMap.not_find_iff.
> 
> but Coq (8.2) complains that it can't find this lemma, it can find
> some of the others in the FMapAVL library though.
> 
> Ashish
> 
> 


Hi

The lemmas in an implementation file such as FMapAVL are not meant to
be used directly for proving properties later. They are only here to
prove that avl trees are indeed a correct implementation of
FMapInterface. Instead, many additional properties are proved 
in a functor of properties, see FMapFacts.v, that is based on
FMapInterface, and hence can be used independently of the specific
implementation you're using.

Here comes a proof of your property:

Require Import ZArith FMaps FMapAVL.
Module FMap := FMapAVL.Make(Z_as_OT).
Module FMapP := FMapFacts.Properties FMap.
Import FMapP.
Import F. (* a sub-module of FMapP, 
             containing more elementary properties *)

Lemma test : 
 forall (tbl:FMap.t (list Z)),
  (FMap.is_empty tbl = true) ->
  forall (key:Z), (FMap.find key tbl = None).
Proof.
intros tbl EMPTY key.
rewrite <- not_find_in_iff.
rewrite <- is_empty_iff in EMPTY.
intro IN.
destruct IN as (e,MAPSTO). 
 (* FMap.In ... means (exists ...,FMap.Mapsto ...) *)
apply EMPTY with key e; eauto. 
 (* Empty tbl means (forall k e, ~Mapsto k e tbl *)
Qed.



Best,

Pierre Letouzey