The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

Hello everyone,

I'm stuck for hours with what I thought would be a very simple induction
proof.

The full code of the example and the proof is here:

https://gist.github.com/klauso/fd3787841a44e594715cdd2e758c53b1

I've defined a simple function to look up a key in a list of key value
pairs.

Fixpoint lookup_simple {A} (pairs: list (nat * A)) (key :nat) : option
(nat * A) := match pairs with
  | [] => None
  | a :: ss => if (beq_nat key (fst a))
               then Some a
               else match (lookup_simple ss key) with
                | None => None
                | Some b => Some b
               end
end.

It's a simple induction proof to prove that they returned pair has the
correct key.

Lemma lookup_simple_correct : forall A (pairs : list (nat * A)) key s ,
  lookup_simple pairs key = Some s ->  key = fst s.

However, my lookup function should also return a proof that the returned
pair is
in the original list. For this I use a subset type:

Inductive member (A : Type) (x : A) : list A -> Type :=
| here : forall l, member x (x :: l)
| there : forall y l, member x l -> member x (y :: l).


Fixpoint lookup {A} (pairs: list (nat * A)) (key :nat) : option { s:
(nat * A) & member s pairs} := match pairs with
  | [] => None
  | a :: ss => if (beq_nat key (fst a))
               then Some (existT _ a (here a ss))
               else match (lookup ss key) with
                | None => None
                | Some (existT s m) => Some (existT _ s (there a m))
               end
end.

The  new version of the correctness lemma is easy to state:

Lemma lookup_correct : forall A (pairs : list (nat * A)) key s (m :
member s pairs),
  lookup pairs key = Some (existT _ s m ) ->  key = fst s.

But I'm totally stuck on the proof. I don't know how to get the right
"member" for using the induction
hypothesis. My proof attempt is also in the gist linked above.

Any ideas?

Thanks,

Klaus