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:20:36 +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-f180.google.com
Ironport-phdr: 9a23:hXuc1R9viubgfv9uRHKM819IXTAuvvDOBiVQ1KB52u4cTK2v8tzYMVDF4r011RmSDNmds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2e2//5Lebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRx3miCkHOTA383zZhNJsg69Auh2tuwZyzpTIbI2JNvdzeL7Wc9MARWpGW8ZcTy9PAoy7b4sVEuEPOedYr5P+p1sJsxu1GA6hBOLgyj9PnH/236w60/4iEQHBwgwtBN0OsHHOo9X0MKceS/y6zK7NzTjaaf5dxDTz6JDQfxw/vf2BWah8fMnRxEU1Cg/JkFadpZb4Mz6WyugAtXWQ4fB6WuK1kWEnrhl8ojixyccojYnEnocVxUrF9SV92Yo0K8e4RFJibd6qDZddtD2WO5F5QsMlRGFotyI6xaMctZGneygKzYwrxx/Za/OZb4iF+gzvWPqVLDtih39oeKiziwus/UWj0OHwS8q53EpSoipAiNbMt3QN1xLJ6siAT/tw5kah2TmI1wDJ6OFEIFo0lancK54/2bMwmZ8Tvl7CHi/ygkn5kKiWdkA89uiy9+vneqnmpoObN4Jslg7+Nb0ultWjDuQ8LwgBRHOW+f+81b3m5U32Wq9GjvwwkqnDsZDVP94XpqCjA1wd7oF24BGmSjyizd4wnH8dLVsDdgjUoZLuPgTvL/fiRdW+mVerjn8/xv/BJL/gGJbKMFDMlb7gefB27EsKm1l79sxW+58BUuJJG/n0QEKk7NE=

Just to clarify, I did made distinction between `s` (a function) and `S` (as `successor`), sorry for the poor naming.

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