Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Volker Stolz <stolz AT ifi.uio.no>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Problem proving "no number larger than n is in the subset of numbers up to n"
  • Date: Wed, 2 Dec 2015 11:46:06 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stolz AT ifi.uio.no; spf=None smtp.mailfrom=stolz AT ifi.uio.no; spf=None smtp.helo=postmaster AT lambda.foldr.org
  • Ironport-phdr: 9a23:yANKHRdVwu1jfhNO28JL90pHlGMj4u6mDksu8pMizoh2WeGdxc65Zh7h7PlgxGXEQZ/co6odzbGG7ea4AydZsd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDsvcWJKFwYzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB1sRlhlFGUD+8Bb+TN+lqTf9svhV2Sebe9D3SvYyXmLxvO9QVBb0hXJfZHYC+2bNh5kogQ==
On 01/12/15 23:48, Dominique Larchey-Wendling wrote:
> A way to do this is to strengthen the property so that it can be proved
> easily inductively.

Dear Dominique, thank you for your detailed comment -- that helped! I
had been experimenting with depth of the formula already yesterday, but
I had forgotten to formulate that all elements in sf are less or equal
in depth, which is of course essential.

All the individual proofs turn indeed out to be very simple, as expected.


-Volker

Archive powered by MHonArc 2.6.18.

Top of Page