coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Adding strong induction to the standard library
Date: Mon, 5 Dec 2016 10:48:38 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f179.google.com
Ironport-phdr: 9a23:mVxRMxcLhp3ZtJGXxm5MpEwclGMj4u6mDksu8pMizoh2WeGdxcu+YR7h7PlgxGXEQZ/co6odzbGH6Oa8CSdav96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCzbL52Ihi6twrcu8oZjYd8K6s61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9ZwgbpVrhyhuRJxwIzbYI+IOvVxYqzQZskVSXZbU8tLSyBNHoGxYo0SBOQBJ+ZYqIz9qkMQoxSgBwmnGf3iyj9SiX/0w6I1zvkqHAba3AM8H9IBqnbUo8voO6oJVOC1zbXIwS/dYPxLxDfw8Y7FeQ0vr/GLWLJ/a8vRyU83GgPKj1WQtYzlPy6O2egXr2eb6O9gWOSygGAkswF8uiajytsoh4XThY8YykrI+TtnzIopP9G0VUx2bNq8HJdNqS2XNJF6T80/T21ytis3yqcKtJy5cSUM1Z8p3QTQa+adfIiN+h/jVPieITN/hH99fbKwnRey8Uy5xu3lVcm4zE9GriRYntTOsn0BzRPT6s+ASvty+keuxyyD2BzU6uFBOUw0lKzbJIA9wrMoiJYfrUDOEjX1lUj2lqOaaFso9vSy5+j6YLjrooeQN4puhQH/NqQulNa/AeM9MgUWQ2iU5eS826fh/ULnXbpHlfI2kqzDv5DbIcQXvLK2AwhQ0oo78RawEy+m0MgEnXkANF9KZBWHj5HwN17SJPD4EOywjk+3kDZrwvDGJqfuDo/MLnjFirfhfKxy51RSyAopnphj4MdfDahEK/buUGfwssbZB1k3KV+a2eHiXelw1Ms1WWuND6PRZL/ZsVaK6+4HJuiQIoIZpWCueLAe+/fygCphyhcmdq6z0M5PZQ==

I stand corrected, I didn’t realize strong induction was well-founded induction on lt (this is actually the first I’ve seen a reference to [well_founded induction lt_wf]).

In that case, it would be good to find a place in the documentation to mention this, such that searching for “strong induction coq” pulls this up.

On Dec 5, 2016, 10:40 AM -0500, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>, wrote:

Le 05/12/2016 à 16:30, Tej Chajed a écrit :

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

It is already included ...

Require Import Arith Wf.

Proof.
...
induction n as [ n IHn ] using (well_founded_induction lt_wf).
...
Qed.

Dominique

[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