coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Adding strong induction to the standard library

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Adding strong induction to the standard library
Date: Mon, 5 Dec 2016 16:36:49 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp2.science.ru.nl
Ironport-phdr: 9a23:/3bcoxTXMPg6VW0j2Ln+J82o29psv+yvbD5Q0YIujvd0So/mwa6yYhaN2/xhgRfzUJnB7Loc0qyN4vumBTxLu8vJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanb75/KBu7oR/eu8QVjoduNKY8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMDE07G/ah85+ga5CvB6sqAF0z4rUbY2JMfZzeL7Wc9EHSmpbRstfSjJPAo28YYUMAeQOM+lXoIvhqFUBtha+GQuhCfnzxjNUiHL736s32PkhHwHc2wwgGsoDvmjTrNruL6gdT/q1zLXVxjvGdfNZxyzy55PWfRA7uvGHQLV9cc/LxkkuEwPFj1OQqYPhPzOUzeQNr3Ob4vF6VeKokGEosB9+oiKzxscvkInGmJkaxUva+iVj24Y5P9u4SEpibNOiDZBeuSaaN45sTcMjRWFloCk6yrwauZ67YSgF044ryALYa/yCdYWD/xHtVP6JLDtlin9pZaiziwuw/EWv0OHwS8i53ExXoidKktTArm0B2hPT58SdTvZw8V2t1DeR2wzJ9O1JLl44mKzGIJA72LEwjIAcsUHbEy/2hkr2iKiWe10/+uit9+TneqvqqoWHN4BoiwHxLKIuldChDugiKAgOQnKX+eK41LH7/E35RqtFjuEun6XEvp3WON4XqrO7DgJayIov9heyAy273NkXnXQLNFdFdwiGj4jtNVHOOvf4DfKnjlSpijhrxvTGPrznApXCKnjDkazhfapm60NH0gozystQ6IlKBbEbPPLzWVXxu8LDARAiLQO02f3nBM971oMaQW6PGLOWMLvOsV+U4eIiO/WDZIgMuDrkN/cl4+PugmQilF8Gfaip2IMXZ2qiEvRnJUWZe3vsjc0bHWcEpAptBNDt3VaFSHtYY2u4d6M6/DAyToy8XqnZQYX4uruL1iqhAtV1fG1MAF2WCj+8coyFX/YKZyaTOdN6uiYDX7KsUZMizxykvgLg0PxhKryHqWUjqZv/2Y0ttKXonhYo+GkpV8k=

If you import Wf_nat you can make use of well-foundedness of <, i.e.:

(* Performs strong induction on n, the IH is called IH *)
induction (lt_wf n) as [n _ IH].

On 12/05/2016 04:30 PM, Tej Chajed wrote:

The standard library does not include strong induction. Could it be
added? A proposed addition is
at
_https://github.com/tchajed/strong-induction/blob/master/StrongInduction.v_.
Comments welcome, including nitpicks on the comments and pull requests.

Thanks!
Tej

[Coq-Club] Adding strong induction to the standard library, Tej Chajed, 12/05/2016
- Re: [Coq-Club] Adding strong induction to the standard library, Robbert Krebbers, 12/05/2016
- Re: [Coq-Club] Adding strong induction to the standard library, Dominique Larchey-Wendling, 12/05/2016
  - Re: [Coq-Club] Adding strong induction to the standard library, Tej Chajed, 12/05/2016
    - Re: [Coq-Club] Adding strong induction to the standard library, Dominique Larchey-Wendling, 12/05/2016