coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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çoisLemma 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.
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.
- [Coq-Club] Stuck with an induction proof using subset types, Klaus Ostermann, 05/19/2017
- Re: [Coq-Club] Stuck with an induction proof using subset types, Dominique Larchey-Wendling, 05/19/2017
- Re: [Coq-Club] Stuck with an induction proof using subset types, Klaus Ostermann, 05/19/2017
- Re: [Coq-Club] Stuck with an induction proof using subset types, François Thiré, 05/19/2017
- Re: [Coq-Club] Stuck with an induction proof using subset types, Dominique Larchey-Wendling, 05/19/2017
- Re: [Coq-Club] Stuck with an induction proof using subset types, Klaus Ostermann, 05/19/2017
- Re: [Coq-Club] Stuck with an induction proof using subset types, Dominique Larchey-Wendling, 05/19/2017
Archive powered by MHonArc 2.6.18.