The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

Hi,

You could also use a more straightforward definition of ss as follows:

Definition ss n : Ensemble nat := fun x => x <= n.

This way, your lemma would easily simplify to:

forall n x, x > n -> ~ x <= n

— Amin

> On 30 Nov 2015, at 12:51, Laurent Thery 
> <Laurent.Thery AT inria.fr>
>  wrote:
> 
> 
> 
> On 11/30/2015 12:38 PM, Volker Stolz wrote:
>> Require Import Ensembles.
>> Require Import Lt.
>> 
>> Fixpoint ss n : Ensemble nat :=
>>   match n with
>>   | 0 => Singleton _ 0
>>   | S m => Add _ (ss m) (S m)
>>   end.
>> 
>> Lemma succNotInSS: forall n x, x > n -> ~ In _ (ss n) x.
>> Proof.
>> Admitted.
>> 
>> E.g., ss 1 := {0,1}, and show that no x>1 in (ss 1). It seems a proof by
>> induction is going nowhere, since I always end up having to prove that
>> an even larger value is also not in there.
>> 
>> Could anyone please hint me at what I am missing?
> 
> If you rewrite your goal as
> 
> forall n x, ~ In _ (ss n) (S (n + x)).
> 
> an induction on n makes you use the induction principle for (S x)
> 
> --
> Laurent