feat: well-founded recursion (#250)

Closes #57

---------

Co-authored-by: David Thrane Christiansen <[email protected]>

Author: nomeata

.vale/styles/config/ignore/terms.txt

@@ -151,3 +151,4 @@ uninstantiated
 unparenthesized
 upvote
 walkthrough
+Ackermann

Manual.lean

@@ -9,6 +9,7 @@ import Manual.Intro
 import Manual.Elaboration
 import Manual.Types
 import Manual.Language
+import Manual.RecursiveDefs
 import Manual.Classes
 import Manual.Terms
 import Manual.Tactics
@@ -62,6 +63,8 @@ Additionally, we will be adding missing API reference documentation and revising
 
 {include 0 Manual.Language}
 
+{include 0 Manual.RecursiveDefs}
+
 {include 0 Manual.Terms}
 
 {include 0 Manual.Classes}
@@ -275,6 +278,7 @@ Quot
 Setoid
 Squash
 Subsingleton
+WellFoundedRelation
 ```
 
 ```exceptions

Manual/Language.lean

@@ -8,7 +8,6 @@ import VersoManual
 
 import Manual.Meta
 import Manual.Language.Files
-import Manual.Language.RecursiveDefs
 
 import Lean.Parser.Command
 
@@ -580,9 +579,6 @@ scoped
 Describe {deftech}_axioms_ in detail
 :::
 
-{include 0 Manual.Language.RecursiveDefs}
-
-
 # Attributes
 %%%
 tag := "attributes"

Manual/Meta/Bibliography.lean

@@ -146,7 +146,7 @@ def Citable.bibHtml (go : Doc.Inline Genre.Manual → HtmlT Manual (ReaderT Exte
   match c with
   |  .inProceedings p =>
     let authors ← andList <$> p.authors.mapM go
-    return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". In " <em>{{← go p.booktitle}}"."</em>{{(← p.series.mapM go).map ({{"(" {{·}} ")" }}) |>.getD .empty}} }}
+    return {{ {{authors}} s!", {p.year}. " {{ link {{"“" {{← go p.title}} "”"}} }} ". In " <em>{{← go p.booktitle}}"."</em>{{(← p.series.mapM go).map ({{" (" {{·}} ")" }}) |>.getD .empty}} }}
   | .thesis p =>
     return {{ {{← go p.author}} s!", {p.year}. " <em>{{link (← go p.title)}}</em> ". " {{← go p.degree}} ", " {{← go p.university}} }}
   | .arXiv p =>

Manual/Meta/Example.lean

@@ -113,7 +113,12 @@ r#".example {
   border-radius: 0.5em;
   margin-bottom: 0.75em;
   margin-top: 0.75em;
-  clear: both; /* Don't overlap margin notes with examples */
+}
+/* 1400 px is the cutoff for when the margin notes move out of the margin and into floated elements. */
+@media screen and (700px < width <= 1400px) {
+  .example {
+    clear: both; /* Don't overlap margin notes with examples */
+  }
 }
 .example p:last-child {margin-bottom:0;}
 .example .description::before {

Manual/Papers.lean

@@ -54,3 +54,19 @@ def launchbury94 : InProceedings where
   authors := #[.concat (inlines! "John Launchbury"), .concat (inlines!"Simon L Peyton Jones")]
   year := 1994
   booktitle := .concat (inlines!"Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation")
+
+def manolios2006 : InProceedings where
+  title := .concat (inlines!"Termination Analysis with Calling Context Graphs")
+  authors := #[.concat (inlines!"Panagiotis Manolios"), .concat (inlines!"Daron Vroon")]
+  year := 2006
+  booktitle := .concat (inlines!"Proceedings of the International Conference on Computer Aided Verification (CAV 2006)")
+  series := some <| .concat (inlines!"LNCS 4144")
+  url := "https://doi.org/10.1007/11817963_36"
+
+def bulwahn2007 : InProceedings where
+  title := .concat (inlines!"Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL")
+  authors := #[.concat (inlines!"Lukas Bulwahn"), .concat (inlines!"Alexander Krauss"), .concat (inlines!"Tobias Nipkow")]
+  year := 2007
+  booktitle := .concat (inlines!"Proceedings of the International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2007)")
+  series := some <| .concat (inlines!"LNTCS 4732")
+  url := "https://doi.org/10.1007/978-3-540-74591-4_5"

Manual/Language/RecursiveDefs.lean renamed to Manual/RecursiveDefs.lean

@@ -8,7 +8,8 @@ import VersoManual
 
 import Manual.Meta
 
-import Manual.Language.RecursiveDefs.Structural
+import Manual.RecursiveDefs.Structural
+import Manual.RecursiveDefs.WF
 
 open Verso.Genre Manual
 open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
@@ -151,16 +152,9 @@ Thus, helpers defined in a {keywordOf Lean.Parser.Command.declaration}`where` bl
 
 After the first step of elaboration, in which definitions are still recursive, and before translating recursion using the techniques above, Lean identifies the actually (mutually) recursive cliques{TODO}[define this term, it's useful]  among the definitions in the mutual block and processes them separately and in dependency order.
 
-{include 0 Manual.Language.RecursiveDefs.Structural}
+{include 0 Manual.RecursiveDefs.Structural}
 
-# Well-Founded Recursion
-%%%
-tag := "well-founded-recursion"
-%%%
-
-::: planned 57
-This section will describe the translation of {deftech}[well-founded recursion].
-:::
+{include 0 Manual.RecursiveDefs.WF}
 
 # Partial and Unsafe Recursive Definitions
 %%%

Manual/Language/RecursiveDefs/Structural.lean renamed to Manual/RecursiveDefs/Structural.lean

@@ -1,12 +1,12 @@
 /-
 Copyright (c) 2024 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: David Thrane Christiansen
+Author: David Thrane Christiansen, Joachim Breitner
 -/
 
 import VersoManual
-import Manual.Language.RecursiveDefs.Structural.RecursorExample
-import Manual.Language.RecursiveDefs.Structural.CourseOfValuesExample
+import Manual.RecursiveDefs.Structural.RecursorExample
+import Manual.RecursiveDefs.Structural.CourseOfValuesExample
 
 import Manual.Meta
 
@@ -481,6 +481,10 @@ Describe mutual structural recursion over {ref "nested-inductive-types"}[nested
 
 
 # Inferring Structural Recursion
+%%%
+tag := "inferring-structural-recursion"
+%%%
+
 
 If no {keyword}`termination_by` clauses are present in a recursive or mutually recursive function definition, then Lean attempts to infer a suitable structurally decreasing argument, effectively by trying all suitable parameters in sequence.
 If this search fails, Lean then attempts to infer {tech}[well-founded recursion].
@@ -511,13 +515,13 @@ Try this: termination_by structural x => x
 In this section, the construction used to elaborate structurally recursive functions is explained in more detail.
 This elaboration uses the {ref "recursor-elaboration-helpers"}[`below` and `brecOn` constructions] that are automatically generated from inductive types' recursors.
 
-{spliceContents Manual.Language.RecursiveDefs.Structural.RecursorExample}
+{spliceContents Manual.RecursiveDefs.Structural.RecursorExample}
 
 The structural recursion analysis attempts to translate the recursive pre-definition into a use of the appropriate structural recursion constructions.
 At this step, pattern matching has already been translated into the use of matcher functions; these are treated specially by the termination checker.
 Next, for each group of parameters, a translation using `brecOn` is attempted.
 
-{spliceContents Manual.Language.RecursiveDefs.Structural.CourseOfValuesExample}
+{spliceContents Manual.RecursiveDefs.Structural.CourseOfValuesExample}
 
 The `below` construction is a mapping from each value of a type to the results of some function call on _all_ smaller values; it can be understood as a memoization table that already contains the results for all smaller values.
 The notion of “smaller value” that is expressed in the `below` construction corresponds directly to the definition of {tech}[strict sub-terms].