coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proving complex properties of Fixpoint's for all Ns greater than a value

From: Igor Jirkov <igorjirkov AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proving complex properties of Fixpoint's for all Ns greater than a value
Date: Mon, 27 Mar 2017 20:21:40 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=igorjirkov AT gmail.com; spf=Pass smtp.mailfrom=igorjirkov AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f170.google.com
Ironport-phdr: 9a23:s+xakRD9sq4t4lKyVCu4UyQJP3N1i/DPJgcQr6AfoPdwSPryo8bcNUDSrc9gkEXOFd2CrakV16yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMizexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoINTA5/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kbIUPAO0BPfxFpIf5plsOtxi+BQ6yBOjyzTJIh3D23aog0+QjEAHGxg8gH9UQsHnPo9X1Mb0dUeGxzKXS0TrDaPZW1C775YPVcR4huemBUaxsfcfV00UiFAPIgk+NpYD7PD6ZzPkBvmqH4+dmSOmhkXQoqxtrrTiq3sosipfGhoYSyl3c8CV22oc1JdmhRE91e96oDIJcty+HO4Z0Xs8uWW5ouCE9yr0JvZ60YjIGx4ggxx7ac/CHco6I7Qz/VOuJPzt0mHZodKi8ihuy60Ss1/PwW8qu3FpXrCdJjsHAtnUX2BzS7siHROF9/kCk2TuX1gDT5eZEIVo2laraMZ4hwbkwloQIvETMGy/5gkT2jKuMeko4/eio7vzrYq/6qZ+EK490lgb+P7wylcy4GOQ0KxQBX2yG+eunz7Dj5k34QLBSjvIsiKXZsZbaJd4apqGjGQNV3JwjuF6DCGKt181dln0aJnpEfgiGhs7nIQLgOvf9WNawhE7ksjZxxPfYdungDZLXLHnZk7D/Vbl44k9YjgE0yIYMtNpvFrgdLaerCQfKv9vCA0phPg==

And I indeed use `induction n` right away. I have also tried `lt_wf_ind` but it seems to lead to the same problem eventually.

Igor Zhirkov

2017-03-27 20:15 GMT+02:00 Adam Chlipala <adamc AT csail.mit.edu>:

On 03/27/2017 02:11 PM, Igor Jirkov wrote:

I have a problem trying to prove a property of form:

forall (n:nat) (m:T), n > s m -> f (g n m) = f n.
[...]
However, induction over n is giving me premises I can not satisfy:

(n > s m -> f (g n m) = f n) -> (S n > s m -> f (g n m) ).

To start with, it looks like you should run [induction n] _before_ running [intros]. Then [m] will remain quantified in the induction hypothesis.

[Coq-Club] Proving complex properties of Fixpoint's for all Ns greater than a value, Igor Jirkov, 03/27/2017
- Re: [Coq-Club] Proving complex properties of Fixpoint's for all Ns greater than a value, Adam Chlipala, 03/27/2017
  - Re: [Coq-Club] Proving complex properties of Fixpoint's for all Ns greater than a value, Igor Jirkov, 03/27/2017
  - Re: [Coq-Club] Proving complex properties of Fixpoint's for all Ns greater than a value, Igor Jirkov, 03/27/2017
- Re: [Coq-Club] Proving complex properties of Fixpoint's for all Ns greater than a value, Guillaume Melquiond, 03/28/2017