coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem proving "no number larger than n is in the subset of numbers up to n"

From: Volker Stolz <stolz+coq AT ifi.uio.no>
To: coq-club AT inria.fr
Subject: [Coq-Club] Problem proving "no number larger than n is in the subset of numbers up to n"
Date: Mon, 30 Nov 2015 12:38:29 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=stolz+coq AT ifi.uio.no; spf=None smtp.mailfrom=stolz+coq AT ifi.uio.no; spf=None smtp.helo=postmaster AT lambda.foldr.org
Ironport-phdr: 9a23:i+iNBRyVMRYVGJ/XCy+O+j09IxM/srCxBDY+r6Qd0ekQIJqq85mqBkHD//Il1AaPBtWGraIbwLGO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStOU35v8jLj60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWcwyL5XYGGl4KlR5aS1ze8Bb+TNT6tTLSt+R8njSbOovwSuZnCnyZ8653RUqw2288PDkj/TSPhw==

I had been trying to prove a property about a tree structure and its set
of subtrees and got stuck. So here is a reformulation on "Ensembles nat"
that illustrates the problem:

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?

-Volker

[Coq-Club] Problem proving "no number larger than n is in the subset of numbers up to n", Volker Stolz, 11/30/2015
- Re: [Coq-Club] Problem proving "no number larger than n is in the subset of numbers up to n", Laurent Thery, 11/30/2015
  - Re: [Coq-Club] Problem proving "no number larger than n is in the subset of numbers up to n", Amin Timany, 11/30/2015