From 08dd6d19ef0bd995f97a660a42fe77622c043699 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 14 Feb 2025 08:32:25 +0100 Subject: [PATCH] feat: well-founded function definition preprocessing (#296) This documents the changes from https://github.com/leanprover/lean4/pull/6744. --------- Co-authored-by: David Thrane Christiansen --- .vale/styles/config/ignore/terms.txt | 1 + Manual/BasicTypes.lean | 3 + Manual/Meta/Lean.lean | 11 +- Manual/Meta/Tactics.lean | 10 +- Manual/RecursiveDefs/WF.lean | 320 +++++++++++------- .../RecursiveDefs/WF/PreprocessExample.lean | 188 ++++++++++ Manual/Simp.lean | 2 +- Manual/Tactics.lean | 15 + lake-manifest.json | 2 +- static/theme.css | 7 + 10 files changed, 423 insertions(+), 136 deletions(-) create mode 100644 Manual/RecursiveDefs/WF/PreprocessExample.lean diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt index eb208ed..74baeda 100644 --- a/.vale/styles/config/ignore/terms.txt +++ b/.vale/styles/config/ignore/terms.txt @@ -170,3 +170,4 @@ unparenthesized uploader upvote walkthrough +preprocesses \ No newline at end of file diff --git a/Manual/BasicTypes.lean b/Manual/BasicTypes.lean index 9748814..4dc7475 100644 --- a/Manual/BasicTypes.lean +++ b/Manual/BasicTypes.lean @@ -357,6 +357,9 @@ end ShortCircuit {include 0 Manual.BasicTypes.Array} # Subtypes +%%% +tag := "Subtype" +%%% :::planned 173 * When to use them? diff --git a/Manual/Meta/Lean.lean b/Manual/Meta/Lean.lean index be6da12..5847069 100644 --- a/Manual/Meta/Lean.lean +++ b/Manual/Meta/Lean.lean @@ -579,6 +579,8 @@ def signature : CodeBlockExpander | args, str => do let {«show»} ← SignatureConfig.parse.run args let altStr ← parserInputString str + let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character) + match Parser.runParserCategory (← getEnv) `signature_spec altStr (← getFileName) with | .error e => throwError e @@ -602,14 +604,19 @@ def signature : CodeBlockExpander try let ((hls, _, _, _), st') ← ((SubVerso.Examples.checkSignature name sig).run cmdCtx).run cmdState setInfoState st'.infoState - pure hls + pure (Highlighted.seq hls) catch e => let fmt ← PrettyPrinter.ppSignature (TSyntax.mk name.raw[0]).getId Suggestion.saveSuggestion str (fmt.fmt.pretty 60) (fmt.fmt.pretty 30 ++ "\n") throw e + let hls := + if let some col := col? then + hls.deIndent col + else hls + if «show» then - pure #[← `(Block.other {Block.signature with data := ToJson.toJson $(quote (Highlighted.seq hls))} #[Block.code $(quote str.getString)])] + pure #[← `(Block.other {Block.signature with data := ToJson.toJson $(quote hls)} #[Block.code $(quote str.getString)])] else pure #[] diff --git a/Manual/Meta/Tactics.lean b/Manual/Meta/Tactics.lean index 49518ea..6754150 100644 --- a/Manual/Meta/Tactics.lean +++ b/Manual/Meta/Tactics.lean @@ -563,11 +563,19 @@ def proofStateStyle := r#" padding: 0; border: none; } - .hl.lean.tactic-view .tactic-state .goal { + margin-top: 1em; + margin-bottom: 1em; + display: block; +} +.hl.lean.tactic-view .tactic-state .goal:first-child { margin-top: 0.25em; +} +.hl.lean.tactic-view .tactic-state .goal:last-child { margin-bottom: 0.25em; } + + "# diff --git a/Manual/RecursiveDefs/WF.lean b/Manual/RecursiveDefs/WF.lean index 8d5821b..f91636b 100644 --- a/Manual/RecursiveDefs/WF.lean +++ b/Manual/RecursiveDefs/WF.lean @@ -9,6 +9,7 @@ import VersoManual import Manual.Meta import Manual.Papers import Manual.RecursiveDefs.WF.GuessLexExample +import Manual.RecursiveDefs.WF.PreprocessExample open Manual open Verso.Genre @@ -270,12 +271,26 @@ n : Nat ::: -Additionally, in the branches of {ref "if-then-else"}[if-then-else] expressions, a hypothesis asserting the current branch's condition is brought into scope, much as if the dependent if-then-else syntax had been used. +:::paragraph +Additionally, the context is enriched with additional assumptions that can make it easier to prove termination. +Some examples include: + * In the branches of an {ref "if-then-else"}[if-then-else] expression, a hypothesis that asserts the current branch's condition is added, much as if the dependent if-then-else syntax had been used. + * In the function argument to certain higher-order functions, the context of the function's body is enriched with assumptions about the argument. -:::example "Local Assumptions and Conditionals" +This list is not exhaustive, and the mechanism is extensible. +It is described in detail in {ref "well-founded-preprocessing"}[the section on preprocessing]. +::: + +```lean (show := false) +section +variable {x : Nat} {xs : List Nat} {n : Nat} +``` + +:::example "Enriched Proof Obligation Contexts" + +Here, the {keywordOf termIfThenElse}`if` does not add a local assumption about the condition (that is, whether {lean}`n ≤ 1`) to the local contexts in the branches. -Here, the {keywordOf termIfThenElse}`if` does not bring a local assumption about the condition into scope. Nevertheless, it is available in the context of the termination proof. ```lean (error := true) (keep := false) (name := fibGoals3) def fib (n : Nat) := @@ -299,6 +314,8 @@ unsolved goals ⊢ n - 2 < n ``` +Nevertheless, the assumptions are available in the context of the termination proof: + ```proofState ∀ (n : Nat), («h✝» : ¬ n ≤ 1) → n - 1 < n ∧ n - 2 < n := by intro n «h✝» @@ -315,150 +332,89 @@ h✝ : ¬n ≤ 1 ``` +Termination proof obligations in body of a {keywordOf Lean.Parser.Term.doFor}`for`​`…`​{keywordOf Lean.Parser.Term.doFor}`in` loop are also enriched, in this case with a {name}`Std.Range` membership hypothesis: - -::: - -```lean (show := false) -section -``` - -:::example "Nested Recursion in Higher-order Functions" - -When recursive calls are nested in higher-order functions, sometimes the function definition has to be adjusted so that the termination proof obligations can be discharged. -This often happens when defining functions recursively over {ref "nested-inductive-types"}[nested inductive types], such as the following tree structure: - -```lean -structure Tree where - children : List Tree +```lean (error := true) (keep := false) (name := nestGoal3) +def f (xs : Array Nat) : Nat := Id.run do + let mut s := xs.sum + for i in [:xs.size] do + s := s + f (xs.take i) + pure s +termination_by xs +decreasing_by + skip ``` - -The depth of a tree can be calculated by a recursive function: -```lean (keep := false) (name := nestedOk) -def Tree.depth : Tree → Nat - | {children} => - let depths := children.map fun c => Tree.depth c - match depths.max? with - | some d => d+1 - | none => 0 -termination_by t => t +```leanOutput nestGoal3 (whitespace := lax) (show := false) +unsolved goals +xs : Array Nat +i : Nat +h✝ : i ∈ { start := 0, stop := xs.size, step := 1, step_pos := Nat.zero_lt_one } +⊢ sizeOf (xs.take i) < sizeOf xs ``` -Rewriting the function by replacing pattern matching with a structure field lookup results in an error. -The relationship between the recursive call and the original structure is still present, but the proof is no longer automatic. - -```lean (keep := false) (name := nestedBad) (error := true) -def Tree.depth (t : Tree) : Nat := - let depths := t.children.map fun c => Tree.depth c - match depths.max? with - | some d => d+1 - | none => 0 -termination_by t -``` -```leanOutput nestedBad -failed to prove termination, possible solutions: - - Use `have`-expressions to prove the remaining goals - - Use `termination_by` to specify a different well-founded relation - - Use `decreasing_by` to specify your own tactic for discharging this kind of goal -t c : Tree -h✝ : c ∈ t.children -⊢ sizeOf c < sizeOf t +```proofState +∀ (xs : Array Nat) + (i : Nat) + («h✝» : i ∈ { start := 0, stop := xs.size, step := 1, step_pos := Nat.zero_lt_one : Std.Range}), + sizeOf (xs.take i) < sizeOf xs := by + set_option tactic.hygienic false in + intros ``` -Introducing a {keywordOf Lean.Parser.Term.let}`let`-binding for the children removes even this relationship: +Similarly, in the following (contrived) example, the termination proof contains an additional assumption showing that {lean}`x ∈ xs`. -```lean (keep := false) (name := nestedBad2) (error := true) -def Tree.depth (t : Tree) : Nat := - let children := t.children - let depths := children.map fun c => Tree.depth c - match depths.max? with - | some d => d+1 - | none => 0 -termination_by t +```lean (error := true) (keep := false) (name := nestGoal1) +def f (n : Nat) (xs : List Nat) : Nat := + List.sum (xs.map (fun x => f x [])) +termination_by xs +decreasing_by + skip ``` -```leanOutput nestedBad2 -failed to prove termination, possible solutions: - - Use `have`-expressions to prove the remaining goals - - Use `termination_by` to specify a different well-founded relation - - Use `decreasing_by` to specify your own tactic for discharging this kind of goal -t c : Tree -⊢ sizeOf c < sizeOf t +```leanOutput nestGoal1 (whitespace := lax) (show := false) +unsolved goals +n : Nat +xs : List Nat +x : Nat +h✝ : x ∈ xs +⊢ sizeOf [] < sizeOf xs ``` - -```lean (show := false) -variable (t : Tree) (c : Tree) (children : List Tree) +```proofState +∀ (n : Nat) (xs : List Nat) (x : Nat) («h✝» : x ∈ xs), sizeOf ([] : List Nat) < sizeOf xs := by + set_option tactic.hygienic false in + intros +/-- +n : Nat +xs : List Nat +x : Nat +h✝ : x ∈ xs +⊢ sizeOf [] < sizeOf xs +-/ ``` -The termination proof obligation is not provable, because there is no connection between the local variable {lean}`c` and the parameter {lean}`t`. -However, {name}`List.map` applies its function argument only to elements of the given list; thus, {lean}`c` is always an element of {lean}`t.children`. +This feature requires special setup for the higher-order function under which the recursive call is nested, as described in {ref "well-founded-preprocessing"}[the section on preprocessing]. +In the following definition, identical to the one above except using a custom, equivalent function instead of {name}`List.map`, the proof obligation context is not enriched: -Because the termination proof goal provides access to the local context of the recursive call, it helps to bring facts into scope in the function definition that indicate that {lean}`c` is indeed an element of the list {lean}`children`. -This can be achieved by “attaching” a proof of membership in {lean}`children` to each of its elements using the function {name}`List.attach` and then bringing this proof into scope in the function passed to {name}`List.map`: - -```lean (keep := false) (name := nestedBad3) (error := true) -def Tree.depth (t : Tree) : Nat := - let children := t.children - let depths := children.attach.map fun ⟨c, hc⟩ => - Tree.depth c - match depths.max? with - | some d => d+1 - | none => 0 -termination_by t -``` -```leanOutput nestedBad3 -failed to prove termination, possible solutions: - - Use `have`-expressions to prove the remaining goals - - Use `termination_by` to specify a different well-founded relation - - Use `decreasing_by` to specify your own tactic for discharging this kind of goal -t : Tree -children : List Tree := t.children -c : Tree -hc : c ∈ children -⊢ sizeOf c < sizeOf t -``` - -The context now contains everything needed to write the proof: -```lean (keep := false) -def Tree.depth (t : Tree) : Nat := - let children := t.children - let depths := children.attach.map fun ⟨c, hc⟩ => - Tree.depth c - match depths.max? with - | some d => d+1 - | none => 0 -termination_by t +```lean (error := true) (keep := false) (name := nestGoal4) +def List.myMap := @List.map +def f (n : Nat) (xs : List Nat) : Nat := + List.sum (xs.myMap (fun x => f x [])) +termination_by xs decreasing_by - cases t - decreasing_trivial + skip +``` +```leanOutput nestGoal4 (whitespace := lax) (show := false) +unsolved goals +n : Nat +xs : List Nat +x : Nat +⊢ sizeOf [] < sizeOf xs ``` -In particular, the proof goal after {keywordOf Lean.Parser.Command.declaration}`decreasing_by` now includes the assumption {lean}`c ∈ children`. -The initial goal, that {lean}`sizeOf c < sizeOf t`, can be simplified with the {tactic}`cases` tactic into one for which {tactic}`decreasing_tactic` succeeds. - -Behind the scenes, Lean automatically inserts calls to {name}`List.attach` and related functions for other collection types.{TODO}[xref] -This is why the second version of {name}`Tree.depth` had a local assumption relating {lean}`c` and {lean}`t.children`. -Inserting the {keywordOf Lean.Parser.Term.let}`let`-binding defeated this automatic insertion. - -```lean (keep := true) (show := false) -/-- -error: failed to prove termination, possible solutions: - - Use `have`-expressions to prove the remaining goals - - Use `termination_by` to specify a different well-founded relation - - Use `decreasing_by` to specify your own tactic for discharging this kind of goal -t c : Tree -hc : c ∈ t.children -⊢ sizeOf c < sizeOf t --/ -#guard_msgs in -def Tree.depth (t : Tree) : Nat := - let depths := t.children.attach.map (fun ⟨c, hc⟩ => Tree.depth c) - match depths.max? with - | some d => d+1 - | none => 0 -termination_by t -decreasing_by - decreasing_tactic +```proofState +∀ (n : Nat) (xs : List Nat) (x : Nat), sizeOf ([] : List Nat) < sizeOf xs := by + set_option tactic.hygienic false in + intros ``` ::: @@ -468,6 +424,10 @@ end ``` +```lean (show := false) +section +``` + ::::TODO :::example "Nested recursive calls and subtypes" @@ -751,6 +711,104 @@ Try this: termination_by (n, 1) ::: +# Preprocessing Function Definitions +%%% +tag := "well-founded-preprocessing" +%%% + +Lean _preprocesses_ the function's body before determining the proof obligations at each call site, transforming it into an equivalent definition that may include additional information. +This preprocessing step is primarily used to enrich the local context with additional assumptions that may be necessary in order to solve the termination proof obligations, freeing users from the need to perform equivalent transformations by hand. +Preprocessing uses the {ref "the-simplifier"}[simplifier] and is extensible by the user. + +:::paragraph + +The preprocessing happens in three steps: + +1. Lean annotates occurrences of a function's parameter, or a subterm of a parameter, with the {name}`wfParam` {tech}[gadget]. + + ```signature + wfParam {α} (a : α) : α + ``` + + More precisely, every occurrence of the function's parameters is wrapped in {name}`wfParam`. + Whenever a {keywordOf Lean.Parser.Term.match}`match` expression has _any_ discriminant wrapped in {name}`wfParam`, the gadget is removed and every occurrence of a pattern match variable (regardless of whether it comes from the discriminant with the {name}`wfParam` gadget) is wrapped in {name}`wfParam`. + The {name}`wfParam` gadget is additionally floated out of {tech}[projection function] applications. + +2. The annotated function body is simplified using {ref "the-simplifier"}[the simplifier], using only simplification rules from the {attr}`wf_preprocess` {tech}[custom simp set]. + +3. Finally, any left-over {name}`wfParam` markers are removed. + +Annotating function parameters that are used for well-founded recursion allows the preprocessing simplification rules to distinguish between parameters and other terms. +::: + +:::syntax attr (title := "Preprocessing Simp Set for Well-Founded Recursion") +```grammar +wf_preprocess +``` + +{includeDocstring Lean.Parser.Attr.wf_preprocess} + +::: + +{docstring wfParam} + +Some rewrite rules in the {attr}`wf_preprocess` simp set apply generally, without heeding the {lean}`wfParam` marker. +In particular, the theorem {name}`ite_eq_dite` is used to extend the context of an {ref "if-then-else"}[if-then-else] expression branch with an assumption about the condition:{margin}[This assumption's name should be an inaccessible name based on `h`, as is indicated by using {name}`binderNameHint` with the term {lean}`()`. Binder name hints are described in the {ref "bound-variable-name-hints"}[tactic language reference].] + +```signature +ite_eq_dite {P : Prop} {α : Sort u} {a b : α} [Decidable P] : + (if P then a else b) = + if h : P then + binderNameHint h () a + else + binderNameHint h () b +``` + + +```lean (show := false) +section +variable (xs : List α) (p : α → Bool) (f : α → β) (x : α) +``` + +:::paragraph + +Other rewrite rules use the {name}`wfParam` marker to restrict their applicability; they are used only when a function (like {name}`List.map`) is applied to a parameter or subterm of a parameter, but not otherwise. +This is typically done in two steps: + +1. A theorem such as {name}`List.map_wfParam` recognizes a call of {name}`List.map` on a function parameter (or subterm), and uses {name}`List.attach` to enrich the type of the list elements with the assertion that they are indeed elements of that list: + + ```signature + List.map_wfParam (xs : List α) (f : α → β) : + (wfParam xs).map f = xs.attach.unattach.map f + ``` +2. A theorem such as {name}`List.map_unattach` makes that assertion available to the function parameter of {name}`List.map`. + + ```signature + List.map_unattach (P : α → Prop) + (xs : List { x : α // P x }) (f : α → β) : + xs.unattach.map f = xs.map fun ⟨x, h⟩ => + binderNameHint x f <| + binderNameHint h () <| + f (wfParam x) + ``` + + This theorem uses the {name}`binderNameHint` gadget to preserve a user-chosen binder name, should {lean}`f` be a lambda expression. + +By separating the introduction of {name}`List.attach` from the propagation of the introduced assumption, the desired the {lean}`x ∈ xs` assumption is made available to {lean}`f` even in chains such as `(xs.reverse.filter p).map f`. + +::: + +```lean (show := false) +end +``` + +This preprocessing can be disabled by setting the option {option}`wf.preprocess` to {lean}`false`. +To see the preprocessed function definition, before and after the removal of {name}`wfParam` markers, set the option {option}`trace.Elab.definition.wf` to {lean}`true`. + +{optionDocs trace.Elab.definition.wf} + +{spliceContents Manual.RecursiveDefs.WF.PreprocessExample} + # Theory and Construction ```lean (show := false) diff --git a/Manual/RecursiveDefs/WF/PreprocessExample.lean b/Manual/RecursiveDefs/WF/PreprocessExample.lean new file mode 100644 index 0000000..b252c68 --- /dev/null +++ b/Manual/RecursiveDefs/WF/PreprocessExample.lean @@ -0,0 +1,188 @@ +/- +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 + +/-! +This is extracted into its own file because line numbers show up in the error message, and we don't +want to update it over and over again as we edit the large file. +-/ + +open Verso.Genre Manual +open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode + +set_option linter.constructorNameAsVariable false + +#doc (Manual) "Well-founded recursion preprocessing example (for inclusion elsewhere)" => + +::::example "Preprocessing for a custom data type" + +This example demonstrates what is necessary to enable automatic well-founded recursion for a custom container type. +The structure type {name}`Pair` is a homogeneous pair: it contains precisely two elements, both of which have the same type. +It can be thought of as being similar to a list or array that always contains precisely two elements. + +As a container, {name}`Pair` can support a {name Pair.map}`map` operation. +To support well-founded recursion in which recursive calls occur in the body of a function being mapped over a {name}`Pair`, some additional definitions are required, including a membership predicate, a theorem that relates the size of a member to the size of the containing pair, helpers to introduce and eliminate assumptions about membership, {attr}`wf_preprocess` rules to insert these helpers, and an extension to the {tactic}`decreasing_trivial` tactic. +Each of these steps makes it easier to work with {name}`Pair`, but none are strictly necessary; there's no need to immediately implement all steps for every type. + +```lean +/-- A homogeneous pair -/ +structure Pair (α : Type u) where + fst : α + snd : α + +/-- Mapping a function over the elements of a pair -/ +def Pair.map (f : α → β) (p : Pair α) : Pair β where + fst := f p.fst + snd := f p.snd +``` + +Defining a nested inductive data type of binary trees that uses {name}`Pair` and attempting to define its {name Tree.map}`map` function demonstrates the need for preprocessing rules. + +```lean +/-- A binary tree defined using `Pair` -/ +inductive Tree (α : Type u) where + | leaf : α → Tree α + | node : Pair (Tree α) → Tree α +``` + +A straightforward definition of the {name Tree.map}`map` function fails: + +```lean (error := true) (keep := false) (name := badwf) +def Tree.map (f : α → β) : Tree α → Tree β + | leaf x => leaf (f x) + | node p => node (p.map (fun t' => t'.map f)) +termination_by t => t +``` + +```leanOutput badwf (whitespace := lax) +failed to prove termination, possible solutions: + - Use `have`-expressions to prove the remaining goals + - Use `termination_by` to specify a different well-founded relation + - Use `decreasing_by` to specify your own tactic for discharging this kind of goal +α : Type u_1 +p : Pair (Tree α) +t' : Tree α +⊢ sizeOf t' < 1 + sizeOf p +``` + +:::paragraph +```lean (show := false) +section +variable (t' : Tree α) (p : Pair (Tree α)) +``` +Clearly the proof obligation is not solvable, because nothing connects {lean}`t'` to {lean}`p`. +```lean (show := false) +end +``` +::: + +The standard idiom to enable this kind of function definition is to have a function that enriches each element of a collection with a proof that they are, in fact, elements of the collection. +Stating this property requires a membership predicate. + +```lean +inductive Pair.Mem (p : Pair α) : α → Prop where + | fst : Mem p p.fst + | snd : Mem p p.snd + +instance : Membership α (Pair α) where + mem := Pair.Mem +``` + +Every inductive type automatically has a {name}`SizeOf` instance. +An element of a collection should be smaller than the collection, but this fact must be proved before it can be used to construct a termination proof: + +```lean +theorem Pair.sizeOf_lt_of_mem {α} [SizeOf α] + {p : Pair α} {x : α} (h : x ∈ p) : + sizeOf x < sizeOf p := by + cases h <;> cases p <;> (simp; omega) +``` + +The next step is to define {name Pair.attach}`attach` and {name Pair.unattach}`unattach` functions that enrich the elements of the pair with a proof that they are elements of the pair, or remove said proof. +Here, the type of {name}`Pair.unattach` is more general and can be used with any {ref "Subtype"}[subtype]; this is a typical pattern. + +```lean +def Pair.attach (p : Pair α) : Pair {x : α // x ∈ p} where + fst := ⟨p.fst, .fst⟩ + snd := ⟨p.snd, .snd⟩ + +def Pair.unattach {P : α → Prop} : + Pair {x : α // P x} → Pair α := + Pair.map Subtype.val +``` + +{name Tree.map}`Tree.map` can now be defined by using {name}`Pair.attach` and {name}`Pair.sizeOf_lt_of_mem` explicitly: + +```lean (keep := false) +def Tree.map (f : α → β) : Tree α → Tree β + | leaf x => leaf (f x) + | node p => node (p.attach.map (fun ⟨t', _⟩ => t'.map f)) +termination_by t => t +decreasing_by + have := Pair.sizeOf_lt_of_mem ‹_› + simp_all +arith + omega +``` + +This transformation can be made fully automatic. +The preprocessing feature of well-founded recursion can be used to automate the introduction of the {lean}`Pair.attach` function. +This is done in two stages. +First, when {name}`Pair.map` is applied to one of the function's parameters, it is rewritten to an {name Pair.attach}`attach`/{name Pair.unattach}`unattach` composition. +Then, when a function is mapped over the result of {name}`Pair.unattach`, the function is rewritten to accept the proof of membership and bring it into scope. +```lean +@[wf_preprocess] +theorem Pair.map_wfParam (f : α → β) (p : Pair α) : + (wfParam p).map f = p.attach.unattach.map f := by + cases p + simp [wfParam, Pair.attach, Pair.unattach, Pair.map] + +@[wf_preprocess] +theorem Pair.map_unattach {P : α → Prop} + (p : Pair (Subtype P)) (f : α → β) : + p.unattach.map f = + p.map fun ⟨x, h⟩ => + binderNameHint x f <| + f (wfParam x) := by + cases p; simp [wfParam, Pair.unattach, Pair.map] +``` + +Now the function body can be written without extra considerations, and the membership assumption is still available to the termination proof. + +```lean (keep := false) +def Tree.map (f : α → β) : Tree α → Tree β + | leaf x => leaf (f x) + | node p => node (p.map (fun t' => t'.map f)) +termination_by t => t +decreasing_by + have := Pair.sizeOf_lt_of_mem ‹_› + simp_all + omega +``` + +The proof can be made fully automatic by adding {name Pair.sizeOf_lt_of_mem}`sizeOf_lt_of_mem` to the {tactic}`decreasing_trivial` tactic, as is done for similar built-in theorems. + +```lean +macro "sizeOf_pair_dec" : tactic => + `(tactic| with_reducible + have := Pair.sizeOf_lt_of_mem ‹_› + omega + done) + +macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_pair_dec) + +def Tree.map (f : α → β) : Tree α → Tree β + | leaf x => leaf (f x) + | node p => node (p.map (fun t' => t'.map f)) +termination_by t => t +``` + +To keep the example short, the {tactic}`sizeOf_pair_dec` tactic is tailored to this particular recursion pattern and isn't really general enough for a general-purpose container library. +It does, however, demonstrate that libraries can be just as convenient in practice as the container types in the standard library. + +:::: diff --git a/Manual/Simp.lean b/Manual/Simp.lean index c93549c..3fa75c8 100644 --- a/Manual/Simp.lean +++ b/Manual/Simp.lean @@ -363,7 +363,7 @@ simp $p:prio ``` ::: -Custom simp sets are created with {name Lean.Meta.registerSimpAttr}`registerSimpAttr`, which must be run during {tech}[initialization] by placing it in an {keywordOf Lean.Parser.Command.initialize}`initialize` block. +{deftech}_Custom simp sets_ are created with {name Lean.Meta.registerSimpAttr}`registerSimpAttr`, which must be run during {tech}[initialization] by placing it in an {keywordOf Lean.Parser.Command.initialize}`initialize` block. As a side effect, it creates a new attribute with the same interface as {attr}`simp` that adds rules to the custom simp set. The returned value is a {name Lean.Meta.SimpExtension}`SimpExtension`, which can be used to programmatically access the contents of the custom simp set. The {tactic}`simp` tactics can be instructed to use the new simp set by including its attribute name in the rule list. diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean index 23809e1..0a252ab 100644 --- a/Manual/Tactics.lean +++ b/Manual/Tactics.lean @@ -973,4 +973,19 @@ These options affect the meaning of tactics. {include 0 Manual.Tactics.Conv} +# Naming Bound Variables +%%% +tag := "bound-variable-name-hints" +%%% + +When the {ref "the-simplifier"}[simplifier] or the {tactic}`rw` tactic introduce new binding forms such as function parameters, they select a name for the bound variable based on the one in the statement of the rewrite rule being applied. +This name is made unique if necessary. +In some situations, such as {ref "well-founded-preprocessing"}[preprocessing definitions for termination proofs that use well-founded recursion], the names that appear in termination proof obligations should be the corresponding names written in the original function definition. + +The {name}`binderNameHint` {tech}[gadget] can be used to indicate that a bound variable should be named according to the variables bound in some other term. +By convention, the term {lean}`()` is used to indicate that a name should _not_ be taken from the original definition. + +{docstring binderNameHint} + + {include 0 Manual.Tactics.Custom} diff --git a/lake-manifest.json b/lake-manifest.json index 6f8df1b..e2d2ff3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "74dc0be45e548e6ade778081aa8c308de287edd4", + "rev": "d15e407047fcfd248694d69b6236ade1198449db", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/static/theme.css b/static/theme.css index 24b162d..35d8034 100644 --- a/static/theme.css +++ b/static/theme.css @@ -31,6 +31,13 @@ div.paragraph > dl:not(:last-child) { margin-bottom: 0.5rem; } +/* +Don't shrink code blocks when there's marginalia +*/ +.hl.lean.block { +clear: right; +} + /* Don't impose margins on lists or list items from their contents. */