feat: partial_fixpoint

.envrc

@@ -0,0 +1 @@
+use flake

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

@@ -52,6 +52,8 @@ equational
 executable's
 extensional
 extensionality
+fixpoint
+fixpoints
 functor
 functor's
 functors

Manual/Meta/Monotonicity.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Joachim Breitner
+-/
+
+import Verso
+
+import Manual.Meta.Attribute
+import Manual.Meta.Basic
+import Manual.Meta.Lean
+import Manual.Meta.Table
+
+open Lean Meta Elab
+open Verso Doc Elab Manual
+open SubVerso.Highlighting Highlighted
+
+
+namespace Manual
+
+/--
+A table for monotonicity lemmas. Likely some of this logic can be extracted to a helper
+in `Manual/Meta/Table.lean`.
+-/
+private def mkInlineTable (rows : Array (Array Term)) : TermElabM Term := do
+  if h : rows.size = 0 then
+    throwError "Expected at least one row"
+  else
+    let columns := rows[0].size
+    if columns = 0 then
+      throwError "Expected at least one column"
+    if rows.any (·.size != columns) then
+      throwError s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}"
+
+    let blocks : Array Term :=
+      #[ ← ``(Inline.text "Theorem"), ← ``(Inline.text "Pattern") ] ++
+      rows.flatten
+    ``(Block.other (Block.table $(quote columns) (header := true) Option.none Option.none)
+        #[Block.ul #[$[Verso.Doc.ListItem.mk #[Block.para #[$blocks]]],*]])
+
+
+section delabhelpers
+
+/-!
+To format the monotonicy lemma patterns, I’d like to clearly mark the monotone arguments from
+the other arguments. So I define two gadgets with custom delaborators.
+-/
+
+def monoArg := @id
+def otherArg := @id
+
+open PrettyPrinter.Delaborator
+
+@[app_delab monoArg] def delabMonoArg : Delab :=
+  PrettyPrinter.Delaborator.withOverApp 2 `(·)
+@[app_delab otherArg] def delabOtherArg : Delab :=
+  PrettyPrinter.Delaborator.withOverApp 2 `(_)
+
+end delabhelpers
+
+
+
+@[block_role_expander monotonicityLemmas]
+def monotonicityLemmas : BlockRoleExpander
+  | #[], #[] => do
+    let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values
+    let names := names.qsort (toString · < toString ·)
+
+    let rows : Array (Array Term) ← names.mapM fun name => do
+      -- Extract the target pattern
+      let ci ← getConstInfo name
+
+      -- Omit the `Lean.Order` namespace, if present, to keep the table concise
+      let nameStr := (name.replacePrefix `Lean.Order .anonymous).getString!
+      let hl : Highlighted ← constTok name nameStr
+      let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)}
+        #[Inline.code $(quote nameStr)])
+
+      let patternStx : TSyntax `term ←
+        forallTelescope ci.type fun _ concl => do
+          unless concl.isAppOfArity ``Lean.Order.monotone 5 do
+            throwError "Unexpected conclusion of {name}"
+          let f := concl.appArg!
+          unless f.isLambda do
+            throwError "Unexpected conclusion of {name}"
+          lambdaBoundedTelescope f 1 fun x call => do
+            -- Monotone arguments are the free variables applied to `x`,
+            -- Other arguments the other
+            -- This is an ad-hoc transformation and may fail in cases more complex
+            -- than we need right now (e.g. binders in the goal).
+            let call' ← Meta.transform call (pre := fun e => do
+              if e.isApp && e.appFn!.isFVar && e.appArg! == x[0]! then
+                .done <$> mkAppM ``monoArg #[e]
+              else if e.isFVar then
+                .done <$> mkAppM ``otherArg #[e]
+              else
+                pure .continue)
+
+            let hlCall ← withOptions (·.setBool `pp.tagAppFns true) do
+              let fmt ← Lean.Widget.ppExprTagged call'
+              renderTagged none fmt ⟨{}, false⟩
+            let fmt ← ppExpr call'
+            ``(Inline.other (Inline.lean $(quote hlCall)) #[(Inline.code $(quote fmt.pretty))])
+
+      pure #[nameStx, patternStx]
+
+    let tableStx ← mkInlineTable rows
+    return #[tableStx]
+  | _, _ => throwError "Unexpected arguments"
+
+-- #eval do
+--   let (ss, _) ← (monotonicityLemmas #[] #[]).run {} (.init .missing)
+--   logInfo (ss[0]!.raw.prettyPrint)

Manual/RecursiveDefs.lean

@@ -10,6 +10,7 @@ import Manual.Meta
 
 import Manual.RecursiveDefs.Structural
 import Manual.RecursiveDefs.WF
+import Manual.RecursiveDefs.PartialFixpoint
 
 open Verso.Genre Manual
 open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
@@ -30,7 +31,7 @@ Furthermore, most useful recursive functions do not threaten soundness, and infi
 Instead of banning recursive functions, Lean requires that each recursive function is defined safely.
 While elaborating recursive definitions, the Lean elaborator also produces a justification that the function being defined is safe.{margin}[The section on {ref "elaboration-results"}[the elaborator's output] in the overview of elaboration contextualizes the elaboration of recursive definitions in the overall context of the elaborator.]
 
-There are four main kinds of recursive functions that can be defined:
+There are five main kinds of recursive functions that can be defined:
 
 : Structurally recursive functions
 
@@ -48,6 +49,17 @@ There are four main kinds of recursive functions that can be defined:
   Applications of functions defined via well-founded recursion are not necessarily definitionally equal to their return values, but this equality can be proved as a proposition.
   Even when definitional equalities exist, these functions are frequently slow to compute with because they require reducing proof terms that are often very large.
 
+: Recursive functions as partial fixpoints
+
+  The definition of a function can be understood as an equation that specifies its behavior.
+  In certain cases, the existence of a function that satisfies this specification can be proven even when the recursive function does not necessarily terminate for all inputs.
+  This strategy is even applicable in some cases where the function definition does not necessarily terminate for all inputs.
+  These partial functions emerge as fixed points of these equations are called {tech}_partial fixpoints_.
+
+  In particular, any function whose return type is in certain monads (e.g. {name}`Option`) can be defined using this strategy.
+  Lean generates additional partial correctness theorems for these monadic functions.
+  As with well-founded recursion, applications of functions defined as partial fixpoints are not definitionally equal to their return values, but Lean generates theorems that propositionally equate the function to its unfolding and to the reduction behavior specified in its definition.
+
 : Partial functions with nonempty ranges
 
   For many applications, it's not important to reason about the implementation of certain functions.
@@ -66,6 +78,11 @@ There are four main kinds of recursive functions that can be defined:
   The replaced function may be opaque, which results in the function name having a trivial equational theory in the logic, or it may be an ordinary function, in which case the function is used in the logic.
   Use this feature with care: logical soundness is not at risk, but the behavior of programs written in Lean may diverge from their verified logical models if the unsafe implementation is incorrect.
 
+:::TODO
+
+Table providing an overview of all strategies and their properties
+
+:::
 
 As described in the {ref "elaboration-results"}[overview of the elaborator's output], elaboration of recursive functions proceeds in two phases:
  1. The definition is elaborated as if Lean's core type theory had recursive definitions.
@@ -78,7 +95,7 @@ As described in the {ref "elaboration-results"}[overview of the elaborator's out
     If there is no such clause, then the elaborator performs a search, testing each parameter to the function as a candidate for structural recursion, and attempting to find a measure with a well-founded relation that decreases at each recursive call.
 
 This section describes the rules that govern recursive functions.
-After a description of mutual recursion, each of the four kinds of recursive definitions is specified, along with the tradeoffs between reasoning power and flexibility that go along with each.
+After a description of mutual recursion, each of the five kinds of recursive definitions is specified, along with the tradeoffs between reasoning power and flexibility that go along with each.
 
 # Mutual Recursion
 %%%
@@ -156,6 +173,8 @@ After the first step of elaboration, in which definitions are still recursive, a
 
 {include 0 Manual.RecursiveDefs.WF}
 
+{include 0 Manual.RecursiveDefs.PartialFixpoint}
+
 # Partial and Unsafe Recursive Definitions
 %%%
 tag := "partial-unsafe"