The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

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