coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Adam Chlipala <adamc AT csail.mit.edu>
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 14:15:57 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:Z+GztxEUg+P+R/CkL7YSC51GYnF86YWxBRYc798ds5kLTJ78pcWwAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSMn/mHZisJ+j6xVrxyuqBN934HZe5uaOOZkc67HYd8XS2hMU8BMXCJBGIO8aI4PAvIdMOlFtYb9okYFoAW+BQmoBePv0iVHhnvs0qYn1OkuCxzJ0xYlH90Sq3nbsM71O70TUeCx1qXIyDTDb+9M1Tjj9YfIbwksrPeRVrxzacrc0VQjGx3Gg1mKp4HpIymZ2voXv2SF8uZsSfqjhmw6pw1rvDSiyMkhhpPUio8VyF3I7zt1zJs7KNC+VUV1e8SrEIFKuCGfL4Z2Qt0tQ2VvuCsizb0GpIK7fCcNyJQmwR7fZOWLc5OU4h35SOaeOy10i25+eL2lhhay9VKsyuj9VsmoylpFsDdKksTUunAM0Rzc9NSHR+Ng8ku/2juDzQ7e5v1eLUwqj6bXNYMtzqIompoWq0vDHyv2mEvsjK+Rc0Up4vKn5Pn9bbXjupCRLJN7ihrkPaQvnsyzG+E4MgkSX2SB5+uzyaDj8VXjQLpWlv02jrXZsJfCKMsHoa65GhZZ3Zon6xaiFDiry88YnHkCLFJdYh2LlYnpO1fUIPD5F/izmVqskC04j8zBa7bmG9DGKmXJuLbnZ7d0rUBGmyQpytUKzp5dD/kqIPbyQkb1vZSMBxMwNgecyP3uCdE704ICH2+DH/nKY+vprVaU67d3cKG3b4gPtWOlJg==

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