The Coq mailing list

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

The generalize is just a trick to keep track
of the properties on the Boolean value
(beq_nat_true keys n) after the next destruct.
As case_eq would to the same but after that
you need to apply beq_nat_[true,false] anyway.

Dominique

---

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