The Coq mailing list

[geng chen <chengeng4001 AT gmail.com>]

Thanks ! But I think I have not describe my question clearly. I do some work on separation logic and I want to prove the following lemma.

w : v
p : positive
st : s
-----------------------------------------------------------------
match 
  store.lookup w
    match lookup w st with
    | 0 => store.union (singleton w p) st
    | Zpos => ......
    | Zneg => ......
    end
with 
| Some x => Zpos x
| None =>0
end = Zpos p

and I use the 'case lookup' tactic to do case analysis. Here is the first goal:

w : v
p : positive
st : s
----------------------------------------------------
match 
  store.lookup w (store.union (singleton w p) st)
with
| Some x => Zpos x
| None =>0
end = Zpos p

This case is when 'lookup w st = 0'. So why Coq do not put 'lookup w st = 0'
in hypotheses? If I want the 'lookup w st = 0' in the hypotheses, what tactics should I use?