From cd4014e02ced3241dab15414e79e88a209c8a09b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 12:52:56 +0100 Subject: [PATCH 01/33] Switch to partial fixpoint pr-release --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 62ccd71..12fc5b0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.16.0-rc1 +leanprover/lean4-pr-releases:pr-release-6355 From 212d52d2eb3c6c7d9bd0b76c29fc21fd0ce20361 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 13:48:03 +0100 Subject: [PATCH 02/33] Reapply "Local setup" This reverts commit 7a0ee068c8ca593835ddfca42d3b1f363d80a500. --- .envrc | 1 + flake.lock | 27 +++++++++++++++++++++++++++ flake.nix | 15 +++++++++++++++ 3 files changed, 43 insertions(+) create mode 100644 .envrc create mode 100644 flake.lock create mode 100644 flake.nix diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..3550a30 --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +use flake diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..6f885a8 --- /dev/null +++ b/flake.lock @@ -0,0 +1,27 @@ +{ + "nodes": { + "nixpkgs": { + "locked": { + "lastModified": 1736243181, + "narHash": "sha256-yaAZO4ttZ3q9/U0zFVtzpVGO6B8+DMpshnF1+0E5Kkg=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "8bcd7d056d69e2e6c47ddf40c2c401cb173c0d67", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "master", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..d9fb84b --- /dev/null +++ b/flake.nix @@ -0,0 +1,15 @@ +{ + inputs.nixpkgs.url = "github:NixOS/nixpkgs/master"; + outputs = { self, nixpkgs }: + let + system = "x86_64-linux"; + pkgs = import nixpkgs { inherit system; }; + in + { devShell.${system} = pkgs.stdenv.mkDerivation rec { + name = "env"; + buildInputs = with pkgs; [ + elan + python3 + ]; + };}; +} From 168a53b01387eaaad042d03e3e3908ab6cd21f45 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 18:18:39 +0100 Subject: [PATCH 03/33] A bit more --- Manual/Language/RecursiveDefs.lean | 14 +- .../RecursiveDefs/PartialFixpoint.lean | 270 ++++++++++++++++++ 2 files changed, 283 insertions(+), 1 deletion(-) create mode 100644 Manual/Language/RecursiveDefs/PartialFixpoint.lean diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean index 777ea56..f8e8fa5 100644 --- a/Manual/Language/RecursiveDefs.lean +++ b/Manual/Language/RecursiveDefs.lean @@ -9,6 +9,7 @@ import VersoManual import Manual.Meta import Manual.Language.RecursiveDefs.Structural +import Manual.Language.RecursiveDefs.PartialFixpoint open Verso.Genre Manual open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode @@ -29,7 +30,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 @@ -47,6 +48,15 @@ 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 fixpoints + + Taking the function definition as an equation that specifies the behavior of the function, in + certain cases the existence of a function satisfying this specification can be proven. This stategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_. + + In particular monadic functions in certain monads (e.g. {name}`Option`) are amenable for this strategy, and additional theorems are generated by lean (partial correctness). + + As with well-founded recursion, applications of functions defined via partial fixpoint are not definitially equal to their return values. + : Partial functions with nonempty ranges For many applications, it's not important to reason about the implementation of certain functions. @@ -162,6 +172,8 @@ tag := "well-founded-recursion" This section will describe the translation of {deftech}[well-founded recursion]. ::: +{include 0 Manual.Language.RecursiveDefs.PartialFixpoint} + # Partial and Unsafe Recursive Definitions %%% tag := "partial-unsafe" diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean new file mode 100644 index 0000000..16e9ba6 --- /dev/null +++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean @@ -0,0 +1,270 @@ +/- +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 VersoManual + +import Manual.Meta + +open Manual +open Verso.Genre +open Verso.Genre.Manual +open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode + +#doc (Manual) "Partial Fixpoint Recursion" => +%%% +tag := "partial-fixpoint" +%%% + +A function definition can be understood as a request to Lean to construct a function of the given type that satisfies the given equation. +One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {tech}[well-founded recursion] is to guarantee the existence and uniqueness the constructued functions. + +In some cases, the equation may not uniquely determine the function's (extensional) behavior, because it +does not terminate for all arguments in the above sense, but there still exist functions for which the defining equation holds. +In these cases, a definition by {deftech}_partial fixpoint_ may be possible. + +Even in cases where the defining equation fully describes the function's behavior and a termination proof using {tech}[well-founded recursion] would be possible it may simply be more convenient to define the function using partial fixpoint, to avoid a possible tedious termination proof. + +Definition by partial fixpoint is only used when explicitly requested by the user, by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. + +There are two classes of functions for which a definition by partial fixpoint work: + +* tail-recursive functions of inhabited type, and +* monadic functions in a suitable monad, such as the {name}`Option` monad. + +Both classes are backed by the same theory and construction: least fixpoints of monotone equations in chain-complete partial orders. + +Lean supports {tech}[mutually recursive] functions to be defined by partial fixpoint. +For this, every function definition in a mutual block has to be annotated with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. + +:::example "Definition by Partial Fixpoint" + +The following function find the least natural number for which the predicate `p` holds. +If `p` never holds then this equation does not specify the behavior: the function `find` could return 42 in that case, and still satisfy the equation. + +```lean (keep := false) +def find (p : Nat → Bool) (i : Nat := 0) : Nat := + if p i then + i + else + find p (i + 1) +partial_fixpoint +``` + +The elaborator can prove that functions satisfying the equation exist, and defined `find` to be an arbitrary such function. +::: + +# Tail-recursive functions +%%% +tag := "partial-fixpoint-tailrec" +%%% + +Definition by partial fixpoint will succeed if the following two conditoins hold: + +1. The function's type is inhabited (as with {ref "partial-unsafe"}[functions marked {keywordOf Lean.Parser.Command.declaration}`partial`]). +2. All recursive calls are in {tech}[tail position] of the function. + +A {deftech}_tail position_ of the function body is + +* the funcion body itself, +* the branches of a {keywordOf Lean.Parser.Term.match}`match` expression in tail position, +* the branches of an {keywordOf termIfThenElse}`if` expression in tail position, and +* the body of a {keywordOf Lean.Parser.Term.let}`let` expression in tail position. + +In particular, the {tech key:="match discriminant"}[discriminant] of a {keywordOf Lean.Parser.Term.match}`match` expression, the condition of an {keywordOf termIfThenElse}`if` expression and the arguments of functions are not tail-positions. + +:::example "Tail recursive functions" + +Because the function body itself is a tail-position, clearly looping definitions are accepted: + +```lean (keep := false) +def loop (x : Nat) : Nat := loop (x + 1) +partial_fixpoint +``` + +More useful function definitions tend to have some branching. +The following example can also be constructed using well-founded recursion with a termination proof, but may be more convenient to define using {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. + +```lean (keep := false) +def Array.find (xs : Array α) (p : α → Bool) (i : Nat := 0) : Option α := + if h : i < xs.size then + if p xs[i] then + some xs[i] + else + Array.find xs p (i + 1) + else + none +partial_fixpoint +``` + +If the result of the recursive call is not just returned, but passed to another function, it is not in tail position and this definition fails. + +```lean (keep := false) (error := true) (name := nonTailPos) +def List.findIndex (xs : List α) (p : α → Bool) : Int := match xs with + | [] => -1 + | x::ys => + if p x then + 0 + else + let r := List.findIndex ys p + if r = -1 then -1 else r + 1 +partial_fixpoint +``` +```leanOutput nonTailPos +Could not prove 'List.findIndex' to be monotone in its recursive calls: + Cannot eliminate recursive call `List.findIndex ys p` enclosed in + let r := ys✝.findIndex p; + if r = -1 then -1 else r + 1 +``` + +::: + +# Monadic functions +%%% +tag := "partial-fixpoint-monadic" +%%% + + +Definition by partial fixpoint is more powerful if the function's type is monadic, the monad is an instance of {name}`Lean.Order.MonoBind` (such as {name}`Option`). +In this case, recursive call are not restricted to tail-positions, but can also be inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`. + +The set of higher-order functions for which this works is extensible (see TODO below), so no exhaustive list is given here. +The aspiration is that a monadic recursive function definition that is built using abstract monadic operations like {name}`bind`, but not open the abstraction of the monad (e.g. by matching on the {name}`Option` value), is accepted. +In particular, using {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation] should work. + +:::example "Monadic functions" + +The following function implements the Ackermann function in the {name}`Option` monad, and is accepted without a (explicit or implicit) termination proof: + +```lean (keep := false) +def ack : (n m : Nat) → Option Nat + | 0, y => some (y+1) + | x+1, 0 => ack x 1 + | x+1, y+1 => do ack x (← ack (x+1) y) +partial_fixpoint +``` + +Recursion can also happen within higher-order library functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]: + +```lean (keep := false) +structure Tree where cs : List Tree + +def Tree.rev (t : Tree) : Option Tree := do + Tree.mk (← t.cs.reverse.mapM (Tree.rev ·)) +partial_fixpoint + +def Tree.rev' (t : Tree) : Option Tree := do + let mut cs := [] + for c in t.cs do + cs := (← c.rev') :: cs + return Tree.mk cs +partial_fixpoint +``` + +Pattern matching on the result of the recursive call will prevent the definition by partial fixpoint to go through: + +```lean (keep := false) (error := true) (name := monoMatch) +def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with + | [] => none + | x::ys => + if p x then + some 0 + else + match List.findIndex ys p with + | none => none + | some r => some (r + 1) +partial_fixpoint +``` +```leanOutput monoMatch +Could not prove 'List.findIndex' to be monotone in its recursive calls: + Cannot eliminate recursive call `List.findIndex ys p` enclosed in + match ys✝.findIndex p with + | none => none + | some r => some (r + 1) +``` + +In this particular case, using the {name}`Functor.map` function instead of explicit pattern matching helps: + +```lean +def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with + | [] => none + | x::ys => + if p x then + some 0 + else + (· + 1) <$> List.findIndex ys p +partial_fixpoint +``` +::: + +# Partial Correctnes Theorem +%%% +tag := "partial-correctness-theorem" +%%% + +In general, for funcitons defined by partial fixpoint we know obtain the equational theorems that prove that the function indeed satisfies the given equation, and enables proofs by rewriting. +But these do not allow reasoning about the behavior of the function on the underspecified arguments. + +If the monad happens to be the {name}`Option` monad, then by construction the function equals {name}`Option.none` on all function inputs for which the defining equation is not terminating. +From this fact, Lean proves a {deftech}_partial correctness theorem_ for the function which allows concluding facts from the function's result being {name}`Option.some`. + + +:::example "Partial correctness theorem" + +Recall this function from an earlier example: + +```lean +def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with + | [] => none + | x::ys => + if p x then + some 0 + else + (· + 1) <$> List.findIndex ys p +partial_fixpoint +``` + +For this function definition, Lean proves the following partial correctness theorem: + +```signature +List.findIndex.partial_correctness {α : Type _} (motive : List α → (α → Bool) → Nat → Prop) + (h : + ∀ (findIndex : List α → (α → Bool) → Option Nat), + (∀ (xs : List α) (p : α → Bool) (r : Nat), findIndex xs p = some r → motive xs p r) → + ∀ (xs : List α) (p : α → Bool) (r : Nat), + (match xs with + | [] => none + | x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys p) = + some r → + motive xs p r) + (xs : List α) (p : α → Bool) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs p r✝ +``` + +We can use this theorem to prove that the resulting number is a valid index in the list and that the predicate holds for that index: + +```lean +theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : + xs.findIndex p = some i → xs[i]?.any p := by + apply List.findIndex.partial_correctness (motive := fun xs p i => xs[i]?.any p) + intro findIndex ih xs p r hsome + split at hsome + next => contradiction + next x ys => + split at hsome + next => + have : r = 0 := by simp_all + simp_all + next => + simp only [Option.map_eq_map, Option.map_eq_some'] at hsome + obtain ⟨r', hr, rfl⟩ := hsome + specialize ih _ _ _ hr + simpa +``` + +::: + +# Theory and Construction + +TODO From 3fd2703c8a973dc01101010a6dd53833ad7faaf8 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 18:19:51 +0100 Subject: [PATCH 04/33] 5 --- Manual/Language/RecursiveDefs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean index f8e8fa5..3ef8d78 100644 --- a/Manual/Language/RecursiveDefs.lean +++ b/Manual/Language/RecursiveDefs.lean @@ -87,7 +87,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 %%% From 59287ee88c70d4e4e2bd58aa8cf468dbab7b72d0 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 18:48:14 +0100 Subject: [PATCH 05/33] fixes --- Manual/Language/RecursiveDefs/PartialFixpoint.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean index 16e9ba6..689b73b 100644 --- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean @@ -108,14 +108,14 @@ def List.findIndex (xs : List α) (p : α → Bool) : Int := match xs with if p x then 0 else - let r := List.findIndex ys p + have r := List.findIndex ys p if r = -1 then -1 else r + 1 partial_fixpoint ``` ```leanOutput nonTailPos Could not prove 'List.findIndex' to be monotone in its recursive calls: Cannot eliminate recursive call `List.findIndex ys p` enclosed in - let r := ys✝.findIndex p; + let_fun r := ys✝.findIndex p; if r = -1 then -1 else r + 1 ``` @@ -228,7 +228,9 @@ partial_fixpoint For this function definition, Lean proves the following partial correctness theorem: -```signature +{TODO}[using `signature` causes max recursion error] + +``` List.findIndex.partial_correctness {α : Type _} (motive : List α → (α → Bool) → Nat → Prop) (h : ∀ (findIndex : List α → (α → Bool) → Option Nat), @@ -239,7 +241,7 @@ List.findIndex.partial_correctness {α : Type _} (motive : List α → (α → B | x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys p) = some r → motive xs p r) - (xs : List α) (p : α → Bool) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs p r✝ + (xs : List α) (p : α → Bool) (r : Nat) : xs.findIndex p = some r → motive xs p r ``` We can use this theorem to prove that the resulting number is a valid index in the list and that the predicate holds for that index: From 3c61ae90650febadb06acb4f088eb3d1ed295448 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 18:51:25 +0100 Subject: [PATCH 06/33] Shorter lines --- Manual/Language/RecursiveDefs/PartialFixpoint.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean index 689b73b..c9d37d8 100644 --- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean @@ -102,7 +102,8 @@ partial_fixpoint If the result of the recursive call is not just returned, but passed to another function, it is not in tail position and this definition fails. ```lean (keep := false) (error := true) (name := nonTailPos) -def List.findIndex (xs : List α) (p : α → Bool) : Int := match xs with +def List.findIndex (xs : List α) (p : α → Bool) : Int := + match xs with | [] => -1 | x::ys => if p x then @@ -166,7 +167,8 @@ partial_fixpoint Pattern matching on the result of the recursive call will prevent the definition by partial fixpoint to go through: ```lean (keep := false) (error := true) (name := monoMatch) -def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with +def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := + match xs with | [] => none | x::ys => if p x then @@ -188,7 +190,8 @@ Could not prove 'List.findIndex' to be monotone in its recursive calls: In this particular case, using the {name}`Functor.map` function instead of explicit pattern matching helps: ```lean -def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with +def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := + match xs with | [] => none | x::ys => if p x then @@ -216,7 +219,8 @@ From this fact, Lean proves a {deftech}_partial correctness theorem_ for the fun Recall this function from an earlier example: ```lean -def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with +def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := + match xs with | [] => none | x::ys => if p x then From cce70f53485396dcf9fd959df66ab78f1b7cbdd3 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 18:58:23 +0100 Subject: [PATCH 07/33] Copy editing --- Manual/Language/RecursiveDefs/PartialFixpoint.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean index c9d37d8..b2ddb4a 100644 --- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean @@ -128,7 +128,7 @@ tag := "partial-fixpoint-monadic" %%% -Definition by partial fixpoint is more powerful if the function's type is monadic, the monad is an instance of {name}`Lean.Order.MonoBind` (such as {name}`Option`). +Definition by partial fixpoint is more powerful if the function's type is monadic and the monad is an instance of {name}`Lean.Order.MonoBind`, such as {name}`Option`. In this case, recursive call are not restricted to tail-positions, but can also be inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`. The set of higher-order functions for which this works is extensible (see TODO below), so no exhaustive list is given here. @@ -207,7 +207,7 @@ partial_fixpoint tag := "partial-correctness-theorem" %%% -In general, for funcitons defined by partial fixpoint we know obtain the equational theorems that prove that the function indeed satisfies the given equation, and enables proofs by rewriting. +In general, for functions defined by partial fixpoint we only obtain the equational theorems that prove that the function indeed satisfies the given equation, and enables proofs by rewriting. But these do not allow reasoning about the behavior of the function on the underspecified arguments. If the monad happens to be the {name}`Option` monad, then by construction the function equals {name}`Option.none` on all function inputs for which the defining equation is not terminating. @@ -230,7 +230,7 @@ def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := partial_fixpoint ``` -For this function definition, Lean proves the following partial correctness theorem: +With this function definition, Lean proves the following partial correctness theorem: {TODO}[using `signature` causes max recursion error] From 3c3d32ef225dafc98dcc86fb9fbecf01df93b057 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 19:08:13 +0100 Subject: [PATCH 08/33] Typos --- .vale/styles/config/ignore/terms.txt | 2 ++ Manual/Language/RecursiveDefs.lean | 6 +++--- Manual/Language/RecursiveDefs/PartialFixpoint.lean | 8 ++++---- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt index fdc93e8..e259355 100644 --- a/.vale/styles/config/ignore/terms.txt +++ b/.vale/styles/config/ignore/terms.txt @@ -1,5 +1,6 @@ APIs Abelian +Ackermann Kleisli Packrat antiquotation @@ -49,6 +50,7 @@ enum equational extensional extensionality +fixpoint functor functor's functors diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean index 3ef8d78..2ffe914 100644 --- a/Manual/Language/RecursiveDefs.lean +++ b/Manual/Language/RecursiveDefs.lean @@ -50,12 +50,12 @@ There are five main kinds of recursive functions that can be defined: : Recursive functions as fixpoints - Taking the function definition as an equation that specifies the behavior of the function, in - certain cases the existence of a function satisfying this specification can be proven. This stategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_. + Taking the function definition as an equation that specifies the behavior of the function, in certain cases the existence of a function satisfying this specification can be proven. + This stategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_. In particular monadic functions in certain monads (e.g. {name}`Option`) are amenable for this strategy, and additional theorems are generated by lean (partial correctness). - As with well-founded recursion, applications of functions defined via partial fixpoint are not definitially equal to their return values. + As with well-founded recursion, applications of functions defined via partial fixpoint are not definitionally equal to their return values. : Partial functions with nonempty ranges diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean index b2ddb4a..3888270 100644 --- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean @@ -19,7 +19,7 @@ tag := "partial-fixpoint" %%% A function definition can be understood as a request to Lean to construct a function of the given type that satisfies the given equation. -One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {tech}[well-founded recursion] is to guarantee the existence and uniqueness the constructued functions. +One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {tech}[well-founded recursion] is to guarantee the existence and uniqueness the constructed functions. In some cases, the equation may not uniquely determine the function's (extensional) behavior, because it does not terminate for all arguments in the above sense, but there still exist functions for which the defining equation holds. @@ -61,7 +61,7 @@ The elaborator can prove that functions satisfying the equation exist, and defin tag := "partial-fixpoint-tailrec" %%% -Definition by partial fixpoint will succeed if the following two conditoins hold: +Definition by partial fixpoint will succeed if the following two conditions hold: 1. The function's type is inhabited (as with {ref "partial-unsafe"}[functions marked {keywordOf Lean.Parser.Command.declaration}`partial`]). 2. All recursive calls are in {tech}[tail position] of the function. @@ -202,13 +202,13 @@ partial_fixpoint ``` ::: -# Partial Correctnes Theorem +# Partial Correctness Theorem %%% tag := "partial-correctness-theorem" %%% In general, for functions defined by partial fixpoint we only obtain the equational theorems that prove that the function indeed satisfies the given equation, and enables proofs by rewriting. -But these do not allow reasoning about the behavior of the function on the underspecified arguments. +But these do not allow reasoning about the behavior of the function on arguments for which the function specification does not terminate. If the monad happens to be the {name}`Option` monad, then by construction the function equals {name}`Option.none` on all function inputs for which the defining equation is not terminating. From this fact, Lean proves a {deftech}_partial correctness theorem_ for the function which allows concluding facts from the function's result being {name}`Option.some`. From fe2a45b8a3541b48278807fbf2129511e2b1fd10 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 19:21:19 +0100 Subject: [PATCH 09/33] More typos --- .vale/styles/config/ignore/terms.txt | 1 + Manual/Language/RecursiveDefs.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt index e259355..7bcb040 100644 --- a/.vale/styles/config/ignore/terms.txt +++ b/.vale/styles/config/ignore/terms.txt @@ -51,6 +51,7 @@ equational extensional extensionality fixpoint +fixpoints functor functor's functors diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean index 2ffe914..b1e9ddd 100644 --- a/Manual/Language/RecursiveDefs.lean +++ b/Manual/Language/RecursiveDefs.lean @@ -51,7 +51,7 @@ There are five main kinds of recursive functions that can be defined: : Recursive functions as fixpoints Taking the function definition as an equation that specifies the behavior of the function, in certain cases the existence of a function satisfying this specification can be proven. - This stategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_. + This strategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_. In particular monadic functions in certain monads (e.g. {name}`Option`) are amenable for this strategy, and additional theorems are generated by lean (partial correctness). From 1b8706874479762d240877b091cf2bc04f78133e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Jan 2025 21:28:49 +0100 Subject: [PATCH 10/33] Even more typos --- Manual/Language/RecursiveDefs/PartialFixpoint.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean index 3888270..fe54433 100644 --- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean @@ -68,7 +68,7 @@ Definition by partial fixpoint will succeed if the following two conditions hold A {deftech}_tail position_ of the function body is -* the funcion body itself, +* the function body itself, * the branches of a {keywordOf Lean.Parser.Term.match}`match` expression in tail position, * the branches of an {keywordOf termIfThenElse}`if` expression in tail position, and * the body of a {keywordOf Lean.Parser.Term.let}`let` expression in tail position. From ccdb638e34e69f6c7b91a16e8bc70057b624dceb Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 17 Jan 2025 16:41:50 +0100 Subject: [PATCH 11/33] More on theory --- .../RecursiveDefs/PartialFixpoint.lean | 78 ++++++++++++++++++- Manual/Meta/Monotonicity.lean | 75 ++++++++++++++++++ 2 files changed, 151 insertions(+), 2 deletions(-) create mode 100644 Manual/Meta/Monotonicity.lean diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean index fe54433..69507c4 100644 --- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean @@ -7,12 +7,15 @@ Author: Joachim Breitner import VersoManual import Manual.Meta +import Manual.Meta.Monotonicity open Manual open Verso.Genre open Verso.Genre.Manual open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode +open Lean.Order + #doc (Manual) "Partial Fixpoint Recursion" => %%% tag := "partial-fixpoint" @@ -29,7 +32,7 @@ Even in cases where the defining equation fully describes the function's behavio Definition by partial fixpoint is only used when explicitly requested by the user, by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. -There are two classes of functions for which a definition by partial fixpoint work: +There are two classes of functions for which a definition by partial fixpoint works: * tail-recursive functions of inhabited type, and * monadic functions in a suitable monad, such as the {name}`Option` monad. @@ -272,5 +275,76 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : ::: # Theory and Construction +%%% +tag := "partial-fixpoint-theory" +%%% + +The construction builds on a variant of the Knaster–Tarski theorem: In a chain-complete partial order, every monotone function has a least fixed point. + +The necessary theory is found in the `Lean.Order` namespace. +This is not meant to be a general purpose library of order theoretic results. +Instead, the definitions and theorems therein are only intended to back the +{keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` feature. + +The notion of a partial order, and that of a chain-complete partial order, are represented as type classes: + +{docstring Lean.Order.PartialOrder} + +{docstring Lean.Order.CCPO} + +The fixpoint of a monotone function can be taken using {name}`fix`, which indeed constructs a fixpoint, as shown by {name}`fix_eq`, + +{docstring Lean.Order.fix} + +{docstring Lean.Order.fix_eq} + +So to construct the function, Lean first infers a suitable {name}`CCPO` instance. + +```lean (show := false) +section +universe u v +variable (α : Type u) +variable (β : α → Sort v) [∀ x, CCPO (β x)] +variable (w : α) +``` + +* If the function's result type has a dedicated instance, like {name}`Option` has with {inst}`CCPO (Option α)`, this is used together with the instance for the function type, {inst}`CCPO (∀ x, β x)`, to construct an instance for the whole function's type. + +* Else, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {inst}`CCPO (FlatOrder w)` is used, `w` is a least element and all other elements are incomparable. -TODO +```lean (show := false) +end +``` + +Next, the recursive calls in the right-hand side of the function definitions are abstracted; this turns into the argument `f` of {name}`fix`. The monotonicity requirement is solved by the {tactic}`monotonicity` tactic, which applies compositional monotonicity lemmas in a syntax-driven way + +The tactic solves goals of the form `monotone (fun x => …)` using the following steps: + +* Applying {name}`monotone_const` when there is no dependency on `x` left. +* Splitting on {keywordOf Lean.Parser.Term.match}`match` expressions. +* Splitting on {keywordOf termIfThenElse}`if` expressions. +* Moving {keywordOf Lean.Parser.Term.let}`let` expression to the context, if the value and type do not depend on `x`. +* Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on `x`. +* Applying lemmas annotated with {attr}`partial_fixpoint_monotone` + +:::example "List of Monotonicity Lemmas" + +::::TODO +Not really an example, but probably better to have this collapsible? +:::: + +The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function: + +::::TODO + +What I’d like to see here is + +* {name}`Lean.Order.monotone_array_allM`: applies to `List.mapM ⬝ _` + +where I use `·` and `_` to distinguish the monotone arguments from others. + +:::: + +{monotonicityLemmas} + +::: diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean new file mode 100644 index 0000000..e62d00e --- /dev/null +++ b/Manual/Meta/Monotonicity.lean @@ -0,0 +1,75 @@ +/- +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 Lean.Elab.Command +import Lean.Elab.InfoTree + +import Verso +import Verso.Doc.ArgParse +import Verso.Doc.Elab.Monad +import VersoManual +import Verso.Code + +import SubVerso.Highlighting +import SubVerso.Examples + +import Manual.Meta.Attribute +import Manual.Meta.Basic +import Manual.Meta.Bibliography +import Manual.Meta.CustomStyle +import Manual.Meta.Example +import Manual.Meta.Figure +import Manual.Meta.Lean +import Manual.Meta.Lean.IO +import Manual.Meta.Marginalia +import Manual.Meta.ParserAlias +import Manual.Meta.Syntax +import Manual.Meta.Table +import Manual.Meta.Tactics +import Manual.Meta.SpliceContents + +open Lean Meta Elab +open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets +open SubVerso.Highlighting Highlighted + +open Lean.Elab.Tactic.GuardMsgs + +namespace Manual + +@[block_role_expander monotonicityLemmas] +def monotonicityLemmas : BlockRoleExpander + | #[], #[] => do + let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values + let names := names.qsort (toString · < toString ·) + + let itemStx : TSyntaxArray `term ← names.mapM fun name => do + -- Extract the target pattern + let ci ← getConstInfo name + let targetStx : TSyntax `term ← + forallTelescope ci.type fun _ concl => do + unless concl.isAppOfArity ``Lean.Order.monotone 5 do + throwError "Unexpecte conclusion of {name}" + let f := concl.appArg! + unless f.isLambda do + throwError "Unexpecte conclusion of {name}" + lambdaBoundedTelescope f 1 fun _ _call => do + -- Could not get this to work: + -- let _stx ← Lean.PrettyPrinter.delab call + -- `(Inline.code $(quote stx)) + `(Inline.text "TODO") + -- pure (some stx) + + let hl : Highlighted ← constTok name name.toString + let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)]) + `(Verso.Doc.Block.para #[$nameStx, Inline.text ": applies to ", $targetStx]) + + let theList ← `(Verso.Doc.Block.ul #[$[⟨#[$itemStx]⟩],*]) + return #[theList] + | _, _ => throwError "Unexpected arguments" + +-- #eval do +-- let (ss, _) ← (monotonicityLemmas #[] #[]).run {} (.init .missing) +-- logInfo (ss[0]!.raw.prettyPrint) From 898660a89b358b3541f1b1e051d6071d18079cb7 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 17 Jan 2025 16:50:33 +0100 Subject: [PATCH 12/33] Render as plain text --- .../Language/RecursiveDefs/PartialFixpoint.lean | 15 +++++++-------- Manual/Meta/Monotonicity.lean | 11 +++++------ 2 files changed, 12 insertions(+), 14 deletions(-) diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean index 69507c4..6f030a2 100644 --- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean @@ -327,14 +327,6 @@ The tactic solves goals of the form `monotone (fun x => …)` using the followin * Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on `x`. * Applying lemmas annotated with {attr}`partial_fixpoint_monotone` -:::example "List of Monotonicity Lemmas" - -::::TODO -Not really an example, but probably better to have this collapsible? -:::: - -The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function: - ::::TODO What I’d like to see here is @@ -345,6 +337,13 @@ where I use `·` and `_` to distinguish the monotone arguments from others. :::: +:::example "List of Monotonicity Lemmas" + +{TODO}[Not really an example, but probably better to have this collapsible?] + +The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function: + + {monotonicityLemmas} ::: diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index e62d00e..c547850 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -55,12 +55,11 @@ def monotonicityLemmas : BlockRoleExpander let f := concl.appArg! unless f.isLambda do throwError "Unexpecte conclusion of {name}" - lambdaBoundedTelescope f 1 fun _ _call => do - -- Could not get this to work: - -- let _stx ← Lean.PrettyPrinter.delab call - -- `(Inline.code $(quote stx)) - `(Inline.text "TODO") - -- pure (some stx) + lambdaBoundedTelescope f 1 fun _ call => do + let stx ← Lean.PrettyPrinter.delab call + let format := Syntax.prettyPrint stx + let str := format.pretty' + `(Inline.code $(quote str)) let hl : Highlighted ← constTok name name.toString let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)]) From e18cb0cea5e2adcee7ac7fceced7efe4c494e18f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 17 Jan 2025 16:52:34 +0100 Subject: [PATCH 13/33] Less imports --- Manual/Meta/Monotonicity.lean | 23 +---------------------- 1 file changed, 1 insertion(+), 22 deletions(-) diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index c547850..0b75c28 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -4,38 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Joachim Breitner -/ -import Lean.Elab.Command -import Lean.Elab.InfoTree - import Verso -import Verso.Doc.ArgParse -import Verso.Doc.Elab.Monad -import VersoManual -import Verso.Code - -import SubVerso.Highlighting -import SubVerso.Examples import Manual.Meta.Attribute import Manual.Meta.Basic -import Manual.Meta.Bibliography -import Manual.Meta.CustomStyle -import Manual.Meta.Example -import Manual.Meta.Figure import Manual.Meta.Lean -import Manual.Meta.Lean.IO -import Manual.Meta.Marginalia -import Manual.Meta.ParserAlias -import Manual.Meta.Syntax import Manual.Meta.Table -import Manual.Meta.Tactics -import Manual.Meta.SpliceContents open Lean Meta Elab -open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets +open Verso Doc Elab open SubVerso.Highlighting Highlighted -open Lean.Elab.Tactic.GuardMsgs namespace Manual From 56b0219896008de8a350b4ff6d86681e3ddb3e9a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 17 Jan 2025 17:03:22 +0100 Subject: [PATCH 14/33] Try to use a table (need help with the error) --- Manual/Meta/Monotonicity.lean | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index 0b75c28..cb933e7 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -12,19 +12,32 @@ import Manual.Meta.Lean import Manual.Meta.Table open Lean Meta Elab -open Verso Doc Elab +open Verso Doc Elab Manual open SubVerso.Highlighting Highlighted namespace Manual +def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : 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 (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.mk) + ``(Block.other (Block.table $(quote columns) $(quote header) $(quote name)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]]) + @[block_role_expander monotonicityLemmas] def monotonicityLemmas : BlockRoleExpander | #[], #[] => do let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values let names := names.qsort (toString · < toString ·) - let itemStx : TSyntaxArray `term ← names.mapM fun name => do + let rows : Array (Array Syntax) ← names.mapM fun name => do -- Extract the target pattern let ci ← getConstInfo name let targetStx : TSyntax `term ← @@ -42,10 +55,10 @@ def monotonicityLemmas : BlockRoleExpander let hl : Highlighted ← constTok name name.toString let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)]) - `(Verso.Doc.Block.para #[$nameStx, Inline.text ": applies to ", $targetStx]) + pure #[nameStx, targetStx] - let theList ← `(Verso.Doc.Block.ul #[$[⟨#[$itemStx]⟩],*]) - return #[theList] + let tableStx ← mkTable rows "foo" "bar" + return #[tableStx] | _, _ => throwError "Unexpected arguments" -- #eval do From 007582034f9fe2e1d97bce818584c9d7c92be577 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 17 Jan 2025 17:03:24 +0100 Subject: [PATCH 15/33] Revert "Try to use a table (need help with the error)" This reverts commit 56b0219896008de8a350b4ff6d86681e3ddb3e9a. --- Manual/Meta/Monotonicity.lean | 23 +++++------------------ 1 file changed, 5 insertions(+), 18 deletions(-) diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index cb933e7..0b75c28 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -12,32 +12,19 @@ import Manual.Meta.Lean import Manual.Meta.Table open Lean Meta Elab -open Verso Doc Elab Manual +open Verso Doc Elab open SubVerso.Highlighting Highlighted namespace Manual -def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : 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 (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.mk) - ``(Block.other (Block.table $(quote columns) $(quote header) $(quote name)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]]) - @[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 Syntax) ← names.mapM fun name => do + let itemStx : TSyntaxArray `term ← names.mapM fun name => do -- Extract the target pattern let ci ← getConstInfo name let targetStx : TSyntax `term ← @@ -55,10 +42,10 @@ def monotonicityLemmas : BlockRoleExpander let hl : Highlighted ← constTok name name.toString let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)]) - pure #[nameStx, targetStx] + `(Verso.Doc.Block.para #[$nameStx, Inline.text ": applies to ", $targetStx]) - let tableStx ← mkTable rows "foo" "bar" - return #[tableStx] + let theList ← `(Verso.Doc.Block.ul #[$[⟨#[$itemStx]⟩],*]) + return #[theList] | _, _ => throwError "Unexpected arguments" -- #eval do From ea47ac54efd767336f10af184129c49e3749df33 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 09:20:42 +0100 Subject: [PATCH 16/33] Reapply "Try to use a table (need help with the error)" This reverts commit 007582034f9fe2e1d97bce818584c9d7c92be577. --- Manual/Meta/Monotonicity.lean | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index 0b75c28..cb933e7 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -12,19 +12,32 @@ import Manual.Meta.Lean import Manual.Meta.Table open Lean Meta Elab -open Verso Doc Elab +open Verso Doc Elab Manual open SubVerso.Highlighting Highlighted namespace Manual +def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : 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 (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.mk) + ``(Block.other (Block.table $(quote columns) $(quote header) $(quote name)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]]) + @[block_role_expander monotonicityLemmas] def monotonicityLemmas : BlockRoleExpander | #[], #[] => do let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values let names := names.qsort (toString · < toString ·) - let itemStx : TSyntaxArray `term ← names.mapM fun name => do + let rows : Array (Array Syntax) ← names.mapM fun name => do -- Extract the target pattern let ci ← getConstInfo name let targetStx : TSyntax `term ← @@ -42,10 +55,10 @@ def monotonicityLemmas : BlockRoleExpander let hl : Highlighted ← constTok name name.toString let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)]) - `(Verso.Doc.Block.para #[$nameStx, Inline.text ": applies to ", $targetStx]) + pure #[nameStx, targetStx] - let theList ← `(Verso.Doc.Block.ul #[$[⟨#[$itemStx]⟩],*]) - return #[theList] + let tableStx ← mkTable rows "foo" "bar" + return #[tableStx] | _, _ => throwError "Unexpected arguments" -- #eval do From f7f8c4260c57e4d3f0fa8f34e019ab80544bd0b5 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 09:50:55 +0100 Subject: [PATCH 17/33] Get table to work --- Manual/Meta/Monotonicity.lean | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index cb933e7..366731f 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -18,7 +18,7 @@ open SubVerso.Highlighting Highlighted namespace Manual -def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : TermElabM Term := do +def mkInlineTabe (rows : Array (Array Term)) : TermElabM Term := do if h : rows.size = 0 then throwError "Expected at least one row" else @@ -28,8 +28,10 @@ def mkTable (rows : Array (Array Syntax)) (header : String) (name : String) : Te 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 (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.mk) - ``(Block.other (Block.table $(quote columns) $(quote header) $(quote name)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]]) + -- let blocks : Array (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.ofElems) + let blocks : Array Term := rows.flatten + ``(Block.other (Block.table $(quote columns) False Option.none) + #[Block.ul #[$[Verso.Doc.ListItem.mk #[Block.para #[$blocks]]],*]]) @[block_role_expander monotonicityLemmas] def monotonicityLemmas : BlockRoleExpander @@ -37,7 +39,7 @@ def monotonicityLemmas : BlockRoleExpander let names := (Meta.Monotonicity.monotoneExt.getState (← getEnv)).values let names := names.qsort (toString · < toString ·) - let rows : Array (Array Syntax) ← names.mapM fun name => do + let rows : Array (Array Term) ← names.mapM fun name => do -- Extract the target pattern let ci ← getConstInfo name let targetStx : TSyntax `term ← @@ -54,10 +56,11 @@ def monotonicityLemmas : BlockRoleExpander `(Inline.code $(quote str)) let hl : Highlighted ← constTok name name.toString - let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)]) + let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} + #[Inline.code $(quote name.getString!)]) pure #[nameStx, targetStx] - let tableStx ← mkTable rows "foo" "bar" + let tableStx ← mkInlineTabe rows return #[tableStx] | _, _ => throwError "Unexpected arguments" From e16ca45a99bdd29ef103234ba4bebb40ea26ff1f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 10:57:45 +0100 Subject: [PATCH 18/33] More on the table --- .../RecursiveDefs/PartialFixpoint.lean | 19 +---- Manual/Meta/Monotonicity.lean | 73 +++++++++++++++---- 2 files changed, 62 insertions(+), 30 deletions(-) diff --git a/Manual/Language/RecursiveDefs/PartialFixpoint.lean b/Manual/Language/RecursiveDefs/PartialFixpoint.lean index 6f030a2..ad69aad 100644 --- a/Manual/Language/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/Language/RecursiveDefs/PartialFixpoint.lean @@ -327,23 +327,12 @@ The tactic solves goals of the form `monotone (fun x => …)` using the followin * Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on `x`. * Applying lemmas annotated with {attr}`partial_fixpoint_monotone` -::::TODO +{TODO}[I wonder if this needs to be collapsible. I at some point I had it in an example, but it's not really an example. Should be this collapsible? Is there a better way than to use example?] -What I’d like to see here is +{TODO}[This table probably needs some styling?] -* {name}`Lean.Order.monotone_array_allM`: applies to `List.mapM ⬝ _` - -where I use `·` and `_` to distinguish the monotone arguments from others. - -:::: - -:::example "List of Monotonicity Lemmas" - -{TODO}[Not really an example, but probably better to have this collapsible?] - -The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function: +{TODO}[How can we I pretty-print these pattern expressions so that hovers work?] +The following monotonicity lemmas are registered, and should allow recursive calls under the given higher-order functions in the arguments indicated by `.` (but not the other arguments, shown as `_`). {monotonicityLemmas} - -::: diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index 366731f..f114b07 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -18,7 +18,11 @@ open SubVerso.Highlighting Highlighted namespace Manual -def mkInlineTabe (rows : Array (Array Term)) : TermElabM Term := do +/-- +A table for monotonicity lemmas. Likely some of this logic can be extracted to a helper +in `Manual/Meta/Table.lean`. +-/ +private def mkInlineTabe (rows : Array (Array Term)) : TermElabM Term := do if h : rows.size = 0 then throwError "Expected at least one row" else @@ -28,11 +32,34 @@ def mkInlineTabe (rows : Array (Array Term)) : TermElabM Term := do 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 (Syntax.TSepArray `term ",") := rows.map (Syntax.TSepArray.ofElems) - let blocks : Array Term := rows.flatten - ``(Block.other (Block.table $(quote columns) False Option.none) + let blocks : Array Term := + #[ ← ``(Inline.text "Theorem"), ← ``(Inline.text "Pattern") ] ++ + rows.flatten + ``(Block.other (Block.table $(quote columns) (header := true) 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 @@ -42,23 +69,39 @@ def monotonicityLemmas : BlockRoleExpander let rows : Array (Array Term) ← names.mapM fun name => do -- Extract the target pattern let ci ← getConstInfo name - let targetStx : TSyntax `term ← + + -- 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 "Unexpecte conclusion of {name}" + throwError "Unexpected conclusion of {name}" let f := concl.appArg! unless f.isLambda do - throwError "Unexpecte conclusion of {name}" - lambdaBoundedTelescope f 1 fun _ call => do - let stx ← Lean.PrettyPrinter.delab call - let format := Syntax.prettyPrint stx - let str := format.pretty' + 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 stx ← Lean.PrettyPrinter.delab call' + let fmt ← Lean.PrettyPrinter.formatTerm stx + let str : String := fmt.pretty `(Inline.code $(quote str)) - let hl : Highlighted ← constTok name name.toString - let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} - #[Inline.code $(quote name.getString!)]) - pure #[nameStx, targetStx] + pure #[nameStx, patternStx] let tableStx ← mkInlineTabe rows return #[tableStx] From 7c36218e90e2f95876c1bc09a820fe2f534056ee Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 11:43:32 +0100 Subject: [PATCH 19/33] Use {name} not {inst} --- Manual/RecursiveDefs/PartialFixpoint.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index b529dfe..6a31363 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -22,13 +22,13 @@ tag := "partial-fixpoint" %%% A function definition can be understood as a request to Lean to construct a function of the given type that satisfies the given equation. -One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {tech}[well-founded recursion] is to guarantee the existence and uniqueness the constructed functions. +One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {ref "well-founded-recursion"}[well-founded recursion] is to guarantee the existence and uniqueness the constructed functions. In some cases, the equation may not uniquely determine the function's (extensional) behavior, because it does not terminate for all arguments in the above sense, but there still exist functions for which the defining equation holds. In these cases, a definition by {deftech}_partial fixpoint_ may be possible. -Even in cases where the defining equation fully describes the function's behavior and a termination proof using {tech}[well-founded recursion] would be possible it may simply be more convenient to define the function using partial fixpoint, to avoid a possible tedious termination proof. +Even in cases where the defining equation fully describes the function's behavior and a termination proof using {ref "well-founded-recursion"}[well-founded recursion] would be possible it may simply be more convenient to define the function using partial fixpoint, to avoid a possible tedious termination proof. Definition by partial fixpoint is only used when explicitly requested by the user, by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. @@ -88,7 +88,7 @@ partial_fixpoint ``` More useful function definitions tend to have some branching. -The following example can also be constructed using well-founded recursion with a termination proof, but may be more convenient to define using {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. +The following example could also be constructed using well-founded recursion with a termination proof, but may be more convenient to define using {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`, where no termination proof is needed. ```lean (keep := false) def Array.find (xs : Array α) (p : α → Bool) (i : Nat := 0) : Option α := @@ -308,7 +308,7 @@ variable (β : α → Sort v) [∀ x, CCPO (β x)] variable (w : α) ``` -* If the function's result type has a dedicated instance, like {name}`Option` has with {inst}`CCPO (Option α)`, this is used together with the instance for the function type, {inst}`CCPO (∀ x, β x)`, to construct an instance for the whole function's type. +* If the function's result type has a dedicated instance, like {name}`Option` has with {name}`instCCPOOption`, this is used together with the instance for the function type, {name}`instCCPOPi`, to construct an instance for the whole function's type. * Else, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {inst}`CCPO (FlatOrder w)` is used, `w` is a least element and all other elements are incomparable. From 370914260168cb68f51429981446709bc3d88cd4 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 12:06:39 +0100 Subject: [PATCH 20/33] cargo-cult local syntax tricks --- Manual/RecursiveDefs/PartialFixpoint.lean | 25 +++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index 6a31363..c33210c 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -310,7 +310,7 @@ variable (w : α) * If the function's result type has a dedicated instance, like {name}`Option` has with {name}`instCCPOOption`, this is used together with the instance for the function type, {name}`instCCPOPi`, to construct an instance for the whole function's type. -* Else, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {inst}`CCPO (FlatOrder w)` is used, `w` is a least element and all other elements are incomparable. +* Else, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {name}`FlatOrder.instCCPO` for the wrapper type {lean}`FlatOrder w` is used. In this order, {lean}`w` is a least element and all other elements are incomparable. ```lean (show := false) end @@ -318,18 +318,31 @@ end Next, the recursive calls in the right-hand side of the function definitions are abstracted; this turns into the argument `f` of {name}`fix`. The monotonicity requirement is solved by the {tactic}`monotonicity` tactic, which applies compositional monotonicity lemmas in a syntax-driven way -The tactic solves goals of the form `monotone (fun x => …)` using the following steps: +```lean (show := false) +section +set_option linter.unusedVariables false +variable {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] (more : (x : α) → β) (x : α) + +local macro "…" x:term:arg "…" : term => `(more $x) +``` + +The tactic solves goals of the form {lean}`monotone (fun x => … x …)` using the following steps: -* Applying {name}`monotone_const` when there is no dependency on `x` left. +* Applying {name}`monotone_const` when there is no dependency on {lean}`x` left. * Splitting on {keywordOf Lean.Parser.Term.match}`match` expressions. * Splitting on {keywordOf termIfThenElse}`if` expressions. -* Moving {keywordOf Lean.Parser.Term.let}`let` expression to the context, if the value and type do not depend on `x`. -* Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on `x`. +* Moving {keywordOf Lean.Parser.Term.let}`let` expression to the context, if the value and type do not depend on {lean}`x`. +* Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on {lean}`x`. * Applying lemmas annotated with {attr}`partial_fixpoint_monotone` +```lean (show := false) +end +``` + + {TODO}[I wonder if this needs to be collapsible. I at some point I had it in an example, but it's not really an example. Should be this collapsible? Is there a better way than to use example?] -{TODO}[This table probably needs some styling?] +{TODO}[This table probably needs some styling? Less vertical space maybe?] {TODO}[How can we I pretty-print these pattern expressions so that hovers work?] From 37020b8fa50cbb4625bcca08621a4755ee3e3806 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 12:15:51 +0100 Subject: [PATCH 21/33] Copy editing --- Manual/RecursiveDefs/PartialFixpoint.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index c33210c..929633c 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -140,7 +140,7 @@ In particular, using {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation] should :::example "Monadic functions" -The following function implements the Ackermann function in the {name}`Option` monad, and is accepted without a (explicit or implicit) termination proof: +The following function implements the Ackermann function in the {name}`Option` monad, and is accepted without an (explicit or implicit) termination proof: ```lean (keep := false) def ack : (n m : Nat) → Option Nat @@ -150,7 +150,7 @@ def ack : (n m : Nat) → Option Nat partial_fixpoint ``` -Recursion can also happen within higher-order library functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]: +Recursive calls may also occur Escurisve within higher-order functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]: ```lean (keep := false) structure Tree where cs : List Tree @@ -256,7 +256,8 @@ We can use this theorem to prove that the resulting number is a valid index in t ```lean theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : xs.findIndex p = some i → xs[i]?.any p := by - apply List.findIndex.partial_correctness (motive := fun xs p i => xs[i]?.any p) + apply List.findIndex.partial_correctness + (motive := fun xs p i => xs[i]?.any p) intro findIndex ih xs p r hsome split at hsome next => contradiction From 7c0d7ad1e63e1a336428e158075c521df6c2abde Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 12:22:21 +0100 Subject: [PATCH 22/33] A (not very interesting) mutual recursion section --- Manual/RecursiveDefs/PartialFixpoint.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index 929633c..8e45a0f 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -275,6 +275,17 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : ::: +# Mutual Well-Founded Recursion +%%% +tag := "mutual-well-founded-recursion" +%%% + +Lean supports the definition of {tech}[mutually recursive] functions using {tech}[partial fixpoint]. +Mutual recursion may be introduced using a {tech}[mutual block], but it also results from {keywordOf Lean.Parser.Term.letrec}`let rec` expressions and {keywordOf Lean.Parser.Command.declaration}`where` blocks. +The rules for mutual well-founded recursion are applied to a group of actually mutually recursive, lifted definitions, that results from the {ref "mutual-syntax"}[elaboration steps] for mutual groups. + +If all functions in the mutual group have the {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` clause, then this strategy is used. + # Theory and Construction %%% tag := "partial-fixpoint-theory" From 95a0625dc667661dd5eebcd10fb4adfa48552c16 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 12:23:29 +0100 Subject: [PATCH 23/33] Typo --- Manual/RecursiveDefs/PartialFixpoint.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index 8e45a0f..a3a3a49 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -150,7 +150,7 @@ def ack : (n m : Nat) → Option Nat partial_fixpoint ``` -Recursive calls may also occur Escurisve within higher-order functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]: +Recursive calls may also occur within higher-order functions such as {name}`List.mapM`, if they are set up appropriately, and {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation]: ```lean (keep := false) structure Tree where cs : List Tree From 39f81f1a6e36e68ea6d58102fdefc36eef38e097 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 14:28:16 +0100 Subject: [PATCH 24/33] Avoid duplicate anchor --- Manual/RecursiveDefs/PartialFixpoint.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index a3a3a49..59d9169 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -277,7 +277,7 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : # Mutual Well-Founded Recursion %%% -tag := "mutual-well-founded-recursion" +tag := "mutual-partial-fixpoint" %%% Lean supports the definition of {tech}[mutually recursive] functions using {tech}[partial fixpoint]. From 8478f381f2b164ffade718861a56b3c2bcfbca83 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Jan 2025 22:22:34 +0100 Subject: [PATCH 25/33] Use ppExpr --- Manual/Meta/Monotonicity.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index f114b07..547e01f 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -96,10 +96,8 @@ def monotonicityLemmas : BlockRoleExpander else pure .continue) - let stx ← Lean.PrettyPrinter.delab call' - let fmt ← Lean.PrettyPrinter.formatTerm stx - let str : String := fmt.pretty - `(Inline.code $(quote str)) + let fmt ← ppExpr call' + `(Inline.code $(quote fmt.pretty)) pure #[nameStx, patternStx] From 5b8409aa105974d3bd2b8d834ab50f6617ec1e98 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 22 Jan 2025 14:19:52 +0100 Subject: [PATCH 26/33] Bump to nightly --- lake-manifest.json | 2 +- lean-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 34a71e2..2ff79ee 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "844b9a53cf7acd71e0e81a3a56608bb28215646d", + "rev": "73ee3629d01f3255b23645f56d8e587e1337a01f", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 12fc5b0..2a88805 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-6355 +leanprover/lean4-nightly:nightly-2025-01-22 From 13f0ba9fde5fbe8675483c94404a76b6eb487502 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 22 Jan 2025 14:40:18 +0100 Subject: [PATCH 27/33] Make build work with nightly --- Manual/BasicTypes/String/FFI.lean | 2 +- Manual/RecursiveDefs/WF.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Manual/BasicTypes/String/FFI.lean b/Manual/BasicTypes/String/FFI.lean index 171c1d4..7e9165b 100644 --- a/Manual/BasicTypes/String/FFI.lean +++ b/Manual/BasicTypes/String/FFI.lean @@ -20,7 +20,7 @@ tag := "string-ffi" %%% -{docstring String.csize} +{docstring Char.utf8Size} :::ffi "lean_string_object" kind := type ``` diff --git a/Manual/RecursiveDefs/WF.lean b/Manual/RecursiveDefs/WF.lean index e05127c..f81c5bb 100644 --- a/Manual/RecursiveDefs/WF.lean +++ b/Manual/RecursiveDefs/WF.lean @@ -412,7 +412,7 @@ In particular, it tries the following tactics and theorems: * {tactic}`simp_arith` * {tactic}`assumption` -* theorems {name}`Nat.sub_succ_lt_self`, {name}`Nat.pred_lt'`, {name}`Nat.pred_lt`, which handle common arithmetic goals +* theorems {name}`Nat.sub_succ_lt_self`, {name}`Nat.pred_lt_of_lt`, {name}`Nat.pred_lt`, which handle common arithmetic goals * {tactic}`omega` * {tactic}`array_get_dec` and {tactic}`array_mem_dec`, which prove that the size of array elements is less than the size of the array * {tactic}`sizeOf_list_dec` that the size of list elements is less than the size of the list From 5bb05ce2f20c462e8e6c33ecf87d7318de4033ec Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 24 Jan 2025 22:47:06 +0100 Subject: [PATCH 28/33] Proofreading and minor style --- Manual/RecursiveDefs.lean | 19 ++- Manual/RecursiveDefs/PartialFixpoint.lean | 197 +++++++++++++++------- 2 files changed, 150 insertions(+), 66 deletions(-) diff --git a/Manual/RecursiveDefs.lean b/Manual/RecursiveDefs.lean index d43b30d..8d48980 100644 --- a/Manual/RecursiveDefs.lean +++ b/Manual/RecursiveDefs.lean @@ -49,14 +49,16 @@ There are five 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 fixpoints +: Recursive functions as partial fixpoints - Taking the function definition as an equation that specifies the behavior of the function, in certain cases the existence of a function satisfying this specification can be proven. - This strategy can apply even when the function definition is not necessarily terminating on all inputs; hence the term {tech}_partial fixpoint_. + 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 monadic functions in certain monads (e.g. {name}`Option`) are amenable for this strategy, and additional theorems are generated by lean (partial correctness). - - As with well-founded recursion, applications of functions defined via partial fixpoint are not definitionally equal to their return values. + 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 @@ -76,6 +78,11 @@ There are five 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. diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index 59d9169..f69816f 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -16,38 +16,54 @@ open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode open Lean.Order +set_option maxRecDepth 600 + #doc (Manual) "Partial Fixpoint Recursion" => %%% tag := "partial-fixpoint" %%% -A function definition can be understood as a request to Lean to construct a function of the given type that satisfies the given equation. -One purpose of the termination proof in {ref "structural-recursion"}[structural recursion] or {ref "well-founded-recursion"}[well-founded recursion] is to guarantee the existence and uniqueness the constructed functions. +All definitions are fundamentally equations: the new constant being defined is equal to the right-hand side of the definition. +For functions defined by {ref "structural-recursion"}[structural recursion], this equation holds {tech key:="definitional equality"}[definitionally], and there is a unique value returned by application of the function. +For functions defined by {ref "well-founded-recursion"}[well-founded recursion], the equation may hold only {tech key:="proposition"}[propositionally], but all type-correct applications of the function to arguments are equal to the respective values prescribed by the definition. +In both cases, the fact that the function terminates for all inputs means that the value computed by applying the function is always uniquely determined. + -In some cases, the equation may not uniquely determine the function's (extensional) behavior, because it -does not terminate for all arguments in the above sense, but there still exist functions for which the defining equation holds. -In these cases, a definition by {deftech}_partial fixpoint_ may be possible. +In some cases where a function does not terminate for all arguments, the equation may not uniquely determine the function's return value for each input, but there are nonetheless functions for which the defining equation holds. +In these cases, a definition as a {deftech}_partial fixpoint_ may still be possible. +Any function that satisfies the defining equation can be used to demonstrate that the equation does not create a logical contradiction, and the equation can then be proven as a theorem about this function. +As with the other strategies for defining recursive functions, compiled code uses the function as it was originally written; like definitions in terms of eliminators or recursion over accessibility proofs, the function used to define the partial fixpoint is used only to justify the function's equations in Lean's logic for purposes of mathematical reasoning. -Even in cases where the defining equation fully describes the function's behavior and a termination proof using {ref "well-founded-recursion"}[well-founded recursion] would be possible it may simply be more convenient to define the function using partial fixpoint, to avoid a possible tedious termination proof. +While partial fixpoints do allow more funtions to be defined in Lean, the are also useful for functions that can be defined without them. +Even in cases where the defining equation fully describes the function's behavior and a termination proof using {ref "well-founded-recursion"}[well-founded recursion] would be possible, it may simply be more convenient to define the function as a partial fixpoint to avoid a having to write a termination proof. -Definition by partial fixpoint is only used when explicitly requested by the user, by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. +Defining recursive functions as partial fixpoints only occurs when explicitly requested by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. -There are two classes of functions for which a definition by partial fixpoint works: +:::paragraph +There are two classes of functions that can be defined as partial fixpoints: -* tail-recursive functions of inhabited type, and -* monadic functions in a suitable monad, such as the {name}`Option` monad. + * Tail-recursive functions whose return type is inhabited type + + * Functions that return values in a suitable monad, such as the {name}`Option` monad Both classes are backed by the same theory and construction: least fixpoints of monotone equations in chain-complete partial orders. -Lean supports {tech}[mutually recursive] functions to be defined by partial fixpoint. -For this, every function definition in a mutual block has to be annotated with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. +::: + +Just as with structural and well-founded recursion, Lean allows {tech}[mutually recursive] functions to be defined as partial fixpoints. +To use this feature, every function definition in a {tech}[mutual block] must be annotated with the {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` modifier. + +```lean (show := false) +section +variable (p : Nat → Bool) +``` :::example "Definition by Partial Fixpoint" -The following function find the least natural number for which the predicate `p` holds. -If `p` never holds then this equation does not specify the behavior: the function `find` could return 42 in that case, and still satisfy the equation. +The following function finds the least natural number for which the predicate {lean}`p` holds. +If `p` never holds, then this equation does not specify the behavior: the function {lean}`find` could return {lean type:="Nat"}`42` or any other {lean}`Nat` in that case and still satisfy the equation. -```lean (keep := false) +```lean def find (p : Nat → Bool) (i : Nat := 0) : Nat := if p i then i @@ -56,42 +72,72 @@ def find (p : Nat → Bool) (i : Nat := 0) : Nat := partial_fixpoint ``` -The elaborator can prove that functions satisfying the equation exist, and defined `find` to be an arbitrary such function. +The elaborator can prove that functions satisfying the equation exist. +Within Lean's logic, {lean}`find` is defined to be an arbitrary such function. ::: -# Tail-recursive functions +```lean (show := false) +end +``` + +# Tail-Recursive Functions %%% tag := "partial-fixpoint-tailrec" %%% -Definition by partial fixpoint will succeed if the following two conditions hold: +:::paragraph -1. The function's type is inhabited (as with {ref "partial-unsafe"}[functions marked {keywordOf Lean.Parser.Command.declaration}`partial`]). -2. All recursive calls are in {tech}[tail position] of the function. +A recursive function can be defined as a partial fixpoint if the following two conditions hold: -A {deftech}_tail position_ of the function body is + 1. The function's return type is inhabited (as with {ref "partial-unsafe"}[functions marked {keywordOf Lean.Parser.Command.declaration}`partial`]) - either a {name}`Nonempty` or {name}`Inhabited` instance works. + 2. All recursive calls are in {tech}[tail position] of the function. -* the function body itself, -* the branches of a {keywordOf Lean.Parser.Term.match}`match` expression in tail position, -* the branches of an {keywordOf termIfThenElse}`if` expression in tail position, and -* the body of a {keywordOf Lean.Parser.Term.let}`let` expression in tail position. +An expression is in {deftech}_tail position_ in the function body if it is: -In particular, the {tech key:="match discriminant"}[discriminant] of a {keywordOf Lean.Parser.Term.match}`match` expression, the condition of an {keywordOf termIfThenElse}`if` expression and the arguments of functions are not tail-positions. + * the function body itself, + * the branches of a {keywordOf Lean.Parser.Term.match}`match` expression that is in tail position, + * the branches of an {keywordOf termIfThenElse}`if` expression that is in tail position, and + * the body of a {keywordOf Lean.Parser.Term.let}`let` expression that is in tail position. -:::example "Tail recursive functions" +In particular, the {tech key:="match discriminant"}[discriminant] of a {keywordOf Lean.Parser.Term.match}`match` expression, the condition of an {keywordOf termIfThenElse}`if` expression and the arguments of functions are not tail positions. -Because the function body itself is a tail-position, clearly looping definitions are accepted: +::: -```lean (keep := false) +```lean (show := false) +-- Test that nonempty is enough +inductive A : Type where + | mkA + | mkA' + +instance : Nonempty A := ⟨.mkA⟩ + +def getA (n : Nat) : A := + getA (n + 1) +partial_fixpoint + +example (n : Nat) : getA n = getA (n + 3) := by + conv => lhs; rw [getA, getA, getA] +``` + +:::example "Loops are Tail Recursive Functions" + +Because the function body itself is a {tech}[tail position], the infinitely looping function {lean}`loop` is tail recursive. +It can be defined as a partial fixpoint. + +```lean def loop (x : Nat) : Nat := loop (x + 1) partial_fixpoint ``` -More useful function definitions tend to have some branching. -The following example could also be constructed using well-founded recursion with a termination proof, but may be more convenient to define using {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`, where no termination proof is needed. +::: + +:::example "Tail Recursion with Branching" -```lean (keep := false) -def Array.find (xs : Array α) (p : α → Bool) (i : Nat := 0) : Option α := +{lean}`Array.find` could also be constructed using well-founded recursion with a termination proof, but may be more convenient to define using {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`, where no termination proof is needed. + +```lean +def Array.find (xs : Array α) (p : α → Bool) + (i : Nat := 0) : Option α := if h : i < xs.size then if p xs[i] then some xs[i] @@ -116,6 +162,7 @@ def List.findIndex (xs : List α) (p : α → Bool) : Int := if r = -1 then -1 else r + 1 partial_fixpoint ``` +The error message on the recursive call is: ```leanOutput nonTailPos Could not prove 'List.findIndex' to be monotone in its recursive calls: Cannot eliminate recursive call `List.findIndex ys p` enclosed in @@ -131,11 +178,11 @@ tag := "partial-fixpoint-monadic" %%% -Definition by partial fixpoint is more powerful if the function's type is monadic and the monad is an instance of {name}`Lean.Order.MonoBind`, such as {name}`Option`. -In this case, recursive call are not restricted to tail-positions, but can also be inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`. +Defining a function as a partial fixpoint is more powerful if the function's return type is a monad that is an instance of {name}`Lean.Order.MonoBind`, such as {name}`Option`. +In this case, recursive call are not restricted to tail-positions, but may also occur inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`. The set of higher-order functions for which this works is extensible (see TODO below), so no exhaustive list is given here. -The aspiration is that a monadic recursive function definition that is built using abstract monadic operations like {name}`bind`, but not open the abstraction of the monad (e.g. by matching on the {name}`Option` value), is accepted. +The aspiration is that a monadic recursive function definition that is built using abstract monadic operations like {name}`bind`, but that does not open the abstraction of the monad (e.g. by matching on the {name}`Option` value), is accepted. In particular, using {tech}[{keywordOf Lean.Parser.Term.do}`do`-notation] should work. :::example "Monadic functions" @@ -167,7 +214,7 @@ def Tree.rev' (t : Tree) : Option Tree := do partial_fixpoint ``` -Pattern matching on the result of the recursive call will prevent the definition by partial fixpoint to go through: +Pattern matching on the result of the recursive call will prevent the definition by partial fixpoint from going through: ```lean (keep := false) (error := true) (name := monoMatch) def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := @@ -190,7 +237,7 @@ Could not prove 'List.findIndex' to be monotone in its recursive calls: | some r => some (r + 1) ``` -In this particular case, using the {name}`Functor.map` function instead of explicit pattern matching helps: +In this particular case, using {name}`Functor.map` instead of explicit pattern matching helps: ```lean def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := @@ -205,21 +252,25 @@ partial_fixpoint ``` ::: -# Partial Correctness Theorem +# Partial Correctness Theorems %%% tag := "partial-correctness-theorem" %%% -In general, for functions defined by partial fixpoint we only obtain the equational theorems that prove that the function indeed satisfies the given equation, and enables proofs by rewriting. -But these do not allow reasoning about the behavior of the function on arguments for which the function specification does not terminate. -If the monad happens to be the {name}`Option` monad, then by construction the function equals {name}`Option.none` on all function inputs for which the defining equation is not terminating. -From this fact, Lean proves a {deftech}_partial correctness theorem_ for the function which allows concluding facts from the function's result being {name}`Option.some`. +For every function defined as a partial fixpoint, Lean proves that that the defining equation is satisfied. +This enables proofs by rewriting. +However, these equational theorems are not sufficient for reasoning about the behavior of the function on arguments for which the function specification does not terminate. +Code paths that lead to infinite recursion at runtime would end up as infinite chains of rewrites in a potential proof. + +Partial fixpoints in suitable monads, on the other hand, provide additional theorems that map the undefined values from non-termination to suitable values in the monad. +In the {name}`Option` monad, then partial fixpoint equals {name}`Option.none` on all function inputs for which the defining equation specifies non-termination. +From this fact, Lean proves a {deftech}_partial correctness theorem_ for the function which allows facts to be concluded when the function's result is {name}`Option.some`. -:::example "Partial correctness theorem" +::::example "Partial Correctness Theorem" -Recall this function from an earlier example: +Recall {lean}`List.findIndex` from an earlier example: ```lean def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := @@ -233,11 +284,9 @@ def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := partial_fixpoint ``` -With this function definition, Lean proves the following partial correctness theorem: +With this function definition, Lean automatically proves the following partial correctness theorem: -{TODO}[using `signature` causes max recursion error] - -``` +```signature List.findIndex.partial_correctness {α : Type _} (motive : List α → (α → Bool) → Nat → Prop) (h : ∀ (findIndex : List α → (α → Bool) → Option Nat), @@ -251,13 +300,26 @@ List.findIndex.partial_correctness {α : Type _} (motive : List α → (α → B (xs : List α) (p : α → Bool) (r : Nat) : xs.findIndex p = some r → motive xs p r ``` -We can use this theorem to prove that the resulting number is a valid index in the list and that the predicate holds for that index: +:::paragraph +Here, the motive is a relation between the parameter and return types of {lean}`List.findIndex`, with the {name}`Option` removed from the return type. +If, when given an arbitrary partial function with a signature that's compatible with {lean}`List.findIndex`, the following hold: + + * the motive is satisfied for all inputs for which the arbitrary function returns a value (rather than {name}`none`), + + * taking one rewriting step with the defining equation, in which the recursive calls are replaced by the arbitrary function, also implies the satisfaction of the motive + +then the motive is satsified for all inputs for which the {lean}`List.findIndex` returns {name}`some`. + +::: + +The partial correctness theorem is a reasoning principle. +It can be used to prove that the resulting number is a valid index in the list and that the predicate holds for that index: ```lean theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : - xs.findIndex p = some i → xs[i]?.any p := by + xs.findIndex p = some i → ∃x, xs[i]? = some x ∧ p x := by apply List.findIndex.partial_correctness - (motive := fun xs p i => xs[i]?.any p) + (motive := fun xs p i => ∃ x, xs[i]? = some x ∧ p x) intro findIndex ih xs p r hsome split at hsome next => contradiction @@ -273,9 +335,9 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : simpa ``` -::: +:::: -# Mutual Well-Founded Recursion +# Mutual Recursion with Partial Fixpoints %%% tag := "mutual-partial-fixpoint" %%% @@ -295,22 +357,35 @@ The construction builds on a variant of the Knaster–Tarski theorem: In a chain The necessary theory is found in the `Lean.Order` namespace. This is not meant to be a general purpose library of order theoretic results. -Instead, the definitions and theorems therein are only intended to back the -{keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` feature. +Instead, the definitions and theorems in `Lean.Order` are only intended as implementation details of the {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` feature, and they should be considered a private API that may change without notice. -The notion of a partial order, and that of a chain-complete partial order, are represented as type classes: +The notion of a partial order, and that of a chain-complete partial order, are represented by the type classes {name}`Lean.Order.PartialOrder` and {name}`Lean.Order.CCPO`, respectively. {docstring Lean.Order.PartialOrder} {docstring Lean.Order.CCPO} +```lean (show := false) +section +open Lean.Order +variable {α : Type u} {β : Type v} [PartialOrder α] [PartialOrder β] (f : α → β) (x y : α) +``` + +A function is monotone if it preserves partial orders. +That is, if {lean}`x ⊑ y` then {lean}`f x ⊑ f y`. +The operator `⊑` represent {name}`Lean.Order.PartialOrder.rel`. + +{docstring Lean.Order.monotone} + The fixpoint of a monotone function can be taken using {name}`fix`, which indeed constructs a fixpoint, as shown by {name}`fix_eq`, {docstring Lean.Order.fix} {docstring Lean.Order.fix_eq} -So to construct the function, Lean first infers a suitable {name}`CCPO` instance. +:::paragraph + +To construct the partial fixpoint, Lean first synthesizes a suitable {name}`CCPO` instance. ```lean (show := false) section @@ -322,13 +397,15 @@ variable (w : α) * If the function's result type has a dedicated instance, like {name}`Option` has with {name}`instCCPOOption`, this is used together with the instance for the function type, {name}`instCCPOPi`, to construct an instance for the whole function's type. -* Else, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {name}`FlatOrder.instCCPO` for the wrapper type {lean}`FlatOrder w` is used. In this order, {lean}`w` is a least element and all other elements are incomparable. +* Otherwise, if the function's type can be shown to be inhabited by a witness {lean}`w`, then the instance {name}`FlatOrder.instCCPO` for the wrapper type {lean}`FlatOrder w` is used. In this order, {lean}`w` is a least element and all other elements are incomparable. ```lean (show := false) end ``` -Next, the recursive calls in the right-hand side of the function definitions are abstracted; this turns into the argument `f` of {name}`fix`. The monotonicity requirement is solved by the {tactic}`monotonicity` tactic, which applies compositional monotonicity lemmas in a syntax-driven way +::: + +Next, the recursive calls in the right-hand side of the function definitions are abstracted; this turns into the argument `f` of {name}`fix`. The monotonicity requirement is solved by the {tactic}`monotonicity` tactic, which applies compositional monotonicity lemmas in a syntax-driven way. ```lean (show := false) section From e35470c82d2bcbfceb0a478c394a5a286ce8faa2 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 24 Jan 2025 23:00:20 +0100 Subject: [PATCH 29/33] render monotonicity lemmas with highlighting --- Manual/Meta/Monotonicity.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index 547e01f..9177c74 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -22,7 +22,7 @@ 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 mkInlineTabe (rows : Array (Array Term)) : TermElabM Term := do +private def mkInlineTable (rows : Array (Array Term)) : TermElabM Term := do if h : rows.size = 0 then throwError "Expected at least one row" else @@ -96,12 +96,15 @@ def monotonicityLemmas : BlockRoleExpander 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.code $(quote fmt.pretty)) + ``(Inline.other (Inline.lean $(quote hlCall)) #[(Inline.code $(quote fmt.pretty))]) pure #[nameStx, patternStx] - let tableStx ← mkInlineTabe rows + let tableStx ← mkInlineTable rows return #[tableStx] | _, _ => throwError "Unexpected arguments" From 497bd7ff2eaa0f38e114d9780ac39652d472dda1 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 24 Jan 2025 23:01:04 +0100 Subject: [PATCH 30/33] remove obsolete TODO --- Manual/RecursiveDefs/PartialFixpoint.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index f69816f..04ef69b 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -433,8 +433,6 @@ end {TODO}[This table probably needs some styling? Less vertical space maybe?] -{TODO}[How can we I pretty-print these pattern expressions so that hovers work?] - The following monotonicity lemmas are registered, and should allow recursive calls under the given higher-order functions in the arguments indicated by `·` (but not the other arguments, shown as `_`). {monotonicityLemmas} From 184fe73e125aa2437b43778229a76a4375b427d9 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 31 Jan 2025 10:11:45 +0100 Subject: [PATCH 31/33] Fix typo and repeated word --- Manual/RecursiveDefs/PartialFixpoint.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index 04ef69b..8ac4ded 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -34,7 +34,7 @@ In these cases, a definition as a {deftech}_partial fixpoint_ may still be possi Any function that satisfies the defining equation can be used to demonstrate that the equation does not create a logical contradiction, and the equation can then be proven as a theorem about this function. As with the other strategies for defining recursive functions, compiled code uses the function as it was originally written; like definitions in terms of eliminators or recursion over accessibility proofs, the function used to define the partial fixpoint is used only to justify the function's equations in Lean's logic for purposes of mathematical reasoning. -While partial fixpoints do allow more funtions to be defined in Lean, the are also useful for functions that can be defined without them. +While partial fixpoints do allow more functions to be defined in Lean, the are also useful for functions that can be defined without them. Even in cases where the defining equation fully describes the function's behavior and a termination proof using {ref "well-founded-recursion"}[well-founded recursion] would be possible, it may simply be more convenient to define the function as a partial fixpoint to avoid a having to write a termination proof. Defining recursive functions as partial fixpoints only occurs when explicitly requested by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. @@ -258,7 +258,7 @@ tag := "partial-correctness-theorem" %%% -For every function defined as a partial fixpoint, Lean proves that that the defining equation is satisfied. +For every function defined as a partial fixpoint, Lean proves that the defining equation is satisfied. This enables proofs by rewriting. However, these equational theorems are not sufficient for reasoning about the behavior of the function on arguments for which the function specification does not terminate. Code paths that lead to infinite recursion at runtime would end up as infinite chains of rewrites in a potential proof. From 51ff541b643e5403df4384d460b64604c56f4bfd Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 3 Feb 2025 08:27:32 +0100 Subject: [PATCH 32/33] Clarify status of partial fixpoint terminology --- Manual/RecursiveDefs/PartialFixpoint.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index 8ac4ded..b182abd 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -29,12 +29,19 @@ For functions defined by {ref "well-founded-recursion"}[well-founded recursion], In both cases, the fact that the function terminates for all inputs means that the value computed by applying the function is always uniquely determined. -In some cases where a function does not terminate for all arguments, the equation may not uniquely determine the function's return value for each input, but there are nonetheless functions for which the defining equation holds. +In some cases where a function does not terminate for all arguments, the equation may not _uniquely_ determine the function's return value for each input, but there are nonetheless functions for which the defining equation holds. In these cases, a definition as a {deftech}_partial fixpoint_ may still be possible. Any function that satisfies the defining equation can be used to demonstrate that the equation does not create a logical contradiction, and the equation can then be proven as a theorem about this function. As with the other strategies for defining recursive functions, compiled code uses the function as it was originally written; like definitions in terms of eliminators or recursion over accessibility proofs, the function used to define the partial fixpoint is used only to justify the function's equations in Lean's logic for purposes of mathematical reasoning. -While partial fixpoints do allow more functions to be defined in Lean, the are also useful for functions that can be defined without them. +The term {tech}_partial fixpoint_ is specific to Lean. +Functions declared {keywordOf Lean.Parser.Command.declaration}`partial` do not require termination proofs, so long as the type of their return values is inhabited, but they are completely opaque from the perspective of Lean's logic. +Partial fixpoints, on the other hand, can be rewritten using their defining equations while writing proofs. +They are _partial_ in the sense that they _can_ be used to define partial functions, but total functions may also be defined as partial fixpoints. +Logically speaking, partial fixpoints are total functions that don't reduce {tech key:="definitional equality"}[definitionally] when applied, but for which equational rewrite rule are provided. +They are _partial_ in the sense that the equational rewrite rules do not necessarily specify a value for all possible arguments. + +While partial fixpoints do allow functions to be defined that cannot be expressed using structural or well-founded recursion, the technique is also useful in other cases. Even in cases where the defining equation fully describes the function's behavior and a termination proof using {ref "well-founded-recursion"}[well-founded recursion] would be possible, it may simply be more convenient to define the function as a partial fixpoint to avoid a having to write a termination proof. Defining recursive functions as partial fixpoints only occurs when explicitly requested by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`. From 8b46c560ca8ec1295ba9ec721b6f1ce26e193db9 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 3 Feb 2025 12:47:34 +0100 Subject: [PATCH 33/33] Address table-related TODOs --- Manual/Meta/Monotonicity.lean | 30 ++++++++++++++++++++--- Manual/Meta/Table.lean | 6 ++--- Manual/RecursiveDefs/PartialFixpoint.lean | 9 ++----- 3 files changed, 31 insertions(+), 14 deletions(-) diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean index 4aebfc4..1604878 100644 --- a/Manual/Meta/Monotonicity.lean +++ b/Manual/Meta/Monotonicity.lean @@ -8,11 +8,13 @@ import Verso import Manual.Meta.Attribute import Manual.Meta.Basic +import Manual.Meta.CustomStyle import Manual.Meta.Lean import Manual.Meta.Table open Lean Meta Elab open Verso Doc Elab Manual +open Verso.Genre.Manual open SubVerso.Highlighting Highlighted @@ -22,7 +24,7 @@ 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 +private def mkInlineTable (rows : Array (Array Term)) (tag : Option String := none) : TermElabM Term := do if h : rows.size = 0 then throwError "Expected at least one row" else @@ -35,7 +37,8 @@ private def mkInlineTable (rows : Array (Array Term)) : TermElabM Term := do let blocks : Array Term := #[ ← ``(Inline.text "Theorem"), ← ``(Inline.text "Pattern") ] ++ rows.flatten - ``(Block.other (Block.table $(quote columns) (header := true) Option.none Option.none) + -- The tag down here is relying on the coercion from `String` to `Tag` + ``(Block.other (Block.table $(quote columns) (header := true) Option.none Option.none (tag := $(quote tag))) #[Block.ul #[$[Verso.Doc.ListItem.mk #[Block.para #[$blocks]]],*]]) @@ -104,9 +107,28 @@ def monotonicityLemmas : BlockRoleExpander pure #[nameStx, patternStx] - let tableStx ← mkInlineTable rows - return #[tableStx] + let tableStx ← mkInlineTable rows (tag := "--monotonicity-lemma-table") + let extraCss ← `(Block.other {Block.CSS with data := $(quote css)} #[]) + return #[extraCss, tableStx] | _, _ => throwError "Unexpected arguments" +where + css := r#" +table#--monotonicity-lemma-table { + border-collapse: collapse; +} +table#--monotonicity-lemma-table th { + text-align: center; +} +table#--monotonicity-lemma-table th, table#--monotonicity-lemma-table th p { + font-family: var(--verso-structure-font-family); +} +table#--monotonicity-lemma-table td:first-child { + padding-bottom: 0.25em; + padding-top: 0.25em; + padding-left: 0; + padding-right: 1.5em; +} + "# -- #eval do -- let (ss, _) ← (monotonicityLemmas #[] #[]).run {} (.init .missing) diff --git a/Manual/Meta/Table.lean b/Manual/Meta/Table.lean index 9e23c05..387c609 100644 --- a/Manual/Meta/Table.lean +++ b/Manual/Meta/Table.lean @@ -39,9 +39,9 @@ def Alignment.htmlClass : Alignment → String | .center => "center-align" end TableConfig -def Block.table (columns : Nat) (header : Bool) (name : Option String) (alignment : Option TableConfig.Alignment) (tag : Option Tag := none): Block where +def Block.table (columns : Nat) (header : Bool) (tag : Option String) (alignment : Option TableConfig.Alignment) (assignedTag : Option Tag := none) : Block where name := `Manual.table - data := ToJson.toJson (columns, header, name, tag, alignment) + data := ToJson.toJson (columns, header, tag, assignedTag, alignment) structure TableConfig where /-- Name for refs -/ @@ -111,7 +111,7 @@ def table.descr : BlockDescr where | .ok (c, hdr, some x, none, align) => let path ← (·.path) <$> read let tag ← Verso.Genre.Manual.externalTag id path x - pure <| some <| Block.other {Block.table c hdr (some x) (tag := some tag) align with id := some id} contents + pure <| some <| Block.other {Block.table c hdr (some x) (assignedTag := some tag) align with id := some id} contents | .ok (_, _, some _, some _, _) => pure none toTeX := none toHtml := diff --git a/Manual/RecursiveDefs/PartialFixpoint.lean b/Manual/RecursiveDefs/PartialFixpoint.lean index b182abd..1f906c9 100644 --- a/Manual/RecursiveDefs/PartialFixpoint.lean +++ b/Manual/RecursiveDefs/PartialFixpoint.lean @@ -37,9 +37,9 @@ As with the other strategies for defining recursive functions, compiled code use The term {tech}_partial fixpoint_ is specific to Lean. Functions declared {keywordOf Lean.Parser.Command.declaration}`partial` do not require termination proofs, so long as the type of their return values is inhabited, but they are completely opaque from the perspective of Lean's logic. Partial fixpoints, on the other hand, can be rewritten using their defining equations while writing proofs. -They are _partial_ in the sense that they _can_ be used to define partial functions, but total functions may also be defined as partial fixpoints. Logically speaking, partial fixpoints are total functions that don't reduce {tech key:="definitional equality"}[definitionally] when applied, but for which equational rewrite rule are provided. -They are _partial_ in the sense that the equational rewrite rules do not necessarily specify a value for all possible arguments. +They are _partial_ in the sense that the defining equation does not necessarily specify a value for all possible arguments. + While partial fixpoints do allow functions to be defined that cannot be expressed using structural or well-founded recursion, the technique is also useful in other cases. Even in cases where the defining equation fully describes the function's behavior and a termination proof using {ref "well-founded-recursion"}[well-founded recursion] would be possible, it may simply be more convenient to define the function as a partial fixpoint to avoid a having to write a termination proof. @@ -435,11 +435,6 @@ The tactic solves goals of the form {lean}`monotone (fun x => … x …)` using end ``` - -{TODO}[I wonder if this needs to be collapsible. I at some point I had it in an example, but it's not really an example. Should be this collapsible? Is there a better way than to use example?] - -{TODO}[This table probably needs some styling? Less vertical space maybe?] - The following monotonicity lemmas are registered, and should allow recursive calls under the given higher-order functions in the arguments indicated by `·` (but not the other arguments, shown as `_`). {monotonicityLemmas}