The Coq mailing list

[François Thiré <franth2 AT gmail.com>]

I do not know the tactic generalize, but here is my proof, maybe you will find it easier to understand:

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.
  - easy.
  - intros ; simpl in H ; destruct (key =? fst a) eqn:eq.
    + inversion H ; subst ; now apply beq_nat_true in eq.
    + destruct (lookup pairs key) eqn:eq2.
      * destruct s0 ; inversion H ; subst.
        now apply IHpairs with (m:=m0).
      * inversion H.
Qed.

François

2017-05-19 11:47 GMT+02:00 Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>:

Hi Dominique,

thanks for your solution. That's quite instructive.

The puzzle piece I was missing is the "generalize (beq_nat_true keys n)"
part.

I'm still trying to understand why exactly it is necessary.

Klaus


Am 19/05/17 um 10:18 schrieb Dominique Larchey-Wendling:

> 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.