Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Stuck with an induction proof using subset types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Stuck with an induction proof using subset types


Chronological Thread 
  • From: François Thiré <franth2 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Stuck with an induction proof using subset types
  • Date: Fri, 19 May 2017 11:56:15 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=franth2 AT gmail.com; spf=Pass smtp.mailfrom=franth2 AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f178.google.com
  • Ironport-phdr: 9a23:rj9NghGgFS9j5E8+AX82ZZ1GYnF86YWxBRYc798ds5kLTJ78o86wAkXT6L1XgUPTWs2DsrQf2rSQ7v+oGTRZp83Q7zZaKN0EfiRGoPtVtjRjOvLNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMj4ZvLqc8xgHJr3ZKZu9awX9kKU+Jkxvy4sq9/oRv/zhMt/4k6sVNTbj0c6MkQLNXCzgrL3o76Mr3uxfdUACB/GEcUmIYkhpJBwjK8hT3VYrvvyX5q+RwxjCUMdX5Qr4oVzui6bxrSALzhyccKzE56mDXhddug69dvRmsugZww4/QYIGSKfp+YqbQds4USGZdQspcUTFKD4WhZIUNEuUBJ/5VoIvzp1UOoxWwBhSiCv3zxTJTnHD6wbc33v49HQ3a3gEtGc8FvnTOrNXyMacfSeC7zLPSwjXFd/RW3jb96JPVeR4/ofGMXKhwdtDMwkQoGQPFlE+fqYr5PzOVyOgAqGeb7+96WuKuj24rsR1+oj+qxso1jITCm4Ebykjc+Cln3Io4Ice0RU17bNK+DZdcqSKXO5FrTs4gQGxlvjsxxKcctp6hZicKzYwqxx7BZPyDdIiF+hfjW/yQITd8nX5kdqi/iwqr/Uiu1+HxVMq53ExFripCldnMuXQN2ALJ5sebTft9+1+t2TeJ1w/N9uFJOV44mbbfJpI7wbM9loAfvVndEiL1gkn6ka2be0Y89uit8evnY7HmppGGN49zjwHzKqoumtalDuQ+LggOX3aX9P+z1L3m50L5QbFKgucqnanetZDWPd4bqbKhAw9JzoYj7A6yACuh0NQBhHUIMFZFeA+cgIXyIFHPIPX4De+ljFi2kTdrwerGPrz7DZnXIHjDiuSpQbEo4ElFjQE30Np35pROC7hHLuigdFX2sYn2FBY/vAu12K7bCNRnV8tKV3iGBLOZaovdtFaJ4qQkJOzaN9xdgyr0N/Vwv62mtnQ+g1JIJaQ=

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.





Archive powered by MHonArc 2.6.18.

Top of Page