The Coq mailing list

[Sunil Kothari <skothari AT uwyo.edu>]

Title: FW: [Coq-Club] Proving a proper sublist is smaller

-----Original Message-----
From: Sunil Kothari
Sent: Mon 3/2/2009 11:50 AM
To: Nadeem Abdul Hamid
Subject: RE: [Coq-Club] Proving a proper sublist is smaller

If you are looking at list with no duplicates, then I think you should look at Laurent Thery's formulation of Sudoku in Coq (available at http://coq.inria.fr/contribs/Sudoku.html). In particular, you should look at Ulist.v which contains lemmas very similar to what you need.

Sunil


-----Original Message-----
From: Nadeem Abdul Hamid [mailto:nadeem AT acm.org]
Sent: Mon 3/2/2009 11:47 AM
To: Luke Palmer
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Proving a proper sublist is smaller

Yeah, that's problematic. :) OK, so perhaps I am missing some 
additional assumptions in the statement of the lemma like (NoDup A), 
(NoDup B)...


On Mar 2, 2009, at 1:44 PM, Luke Palmer wrote:

> On Mon, Mar 2, 2009 at 11:35 AM, Nadeem Abdul Hamid <nadeem AT acm.org> 
> wrote:
> I'm having trouble figuring out how to prove the statement below. 
> What it's saying is that if every element in list A is also in list 
> B, and then you know that there is an additional element in list B 
> that's not in list A, then the size of list B must
> be larger than A.
>
> You will always have trouble proving false theorems. :-)
>
> A = [1,1,1,2,3] ; B = [1,2,3,4]
>
> Luke
>
> Whether I try induction on A or B (with either rearranged to be 
> first), I run into problems at the very end. Can someone help me 
> figure out this puzzle, a different way to prove it than direct 
> induction on A/B, or if there is a reason why it's not true?
>
> Lemma properSubset_smaller
>  : forall (A B : list nat) (m:nat),
>    (forall n, In n A -> In n B) ->
>    In m B ->
>    ~In m A ->
>    length B > length A.
>
> Thanks very much,
>
> nadeem
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>