The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Klaus,

Well I do not really understand what got you stuck.
Here is a possible proof.

Best,

Dominique

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


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.
Proof.
  induction pairs as [ | (n,a) pairs IH ]; simpl; intros keys (i,b) m Hs.
  discriminate Hs.
  generalize (beq_nat_true keys n) (beq_nat_false keys n); intros H1 H2.
  destruct (beq_nat keys n).
  injection Hs; clear Hs; intros; subst i b.
  rewrite H1; auto.
  case_eq (lookup pairs keys).
  intros (p & m') Hp; rewrite Hp in Hs; apply IH in Hp.
  injection Hs; intros; subst; auto.
  intros H; rewrite H in Hs; discriminate.
Qed.


Le 19/05/2017 à 09:47, Klaus Ostermann a écrit :
> 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.