| /-! | |
| Terms are often duplicated in lean. One example is default arguments | |
| referring to earlier ones; observed in the wild with `Array.foldl` and friends. | |
| Ideally, compiling a recursive definition will still only consider such a recursive call once. | |
| -/ | |
| def dup (a : Nat) (b : Nat := a) := a + b | |
| namespace TestingFix | |
| def rec : Nat → Nat | |
| | 0 => 1 | |
| | n+1 => dup (dup (dup (rec n))) | |
| decreasing_by trace "Tactic is run (ideally only once)"; decreasing_tactic | |
| end TestingFix | |
| namespace TestingGuessLex | |
| -- GuessLex should run the tactic an extra time, that is expected | |
| def rec : Nat → Nat → Nat | |
| | 0, _m => 1 | |
| | n+1, m => dup (dup (dup (rec n (m + 1)))) | |
| decreasing_by trace "Tactic is run (ideally only twice)"; decreasing_tactic | |
| end TestingGuessLex | |
| namespace Subcontext | |
| set_option linter.unusedVariables false | |
| -- Now with a duplication into another context | |
| -- We thread through `x` so that we can make the context mention something | |
| -- that appears in the goal, else `mvarId.cleanup` will remove it | |
| def dup2 (x : Nat) (a : Nat) (b : x ≠ x → Nat := fun h => a) := a | |
| namespace TestingFix | |
| def rec : Nat → Nat | |
| | 0 => 1 | |
| | n+1 => dup2 n (rec n) | |
| decreasing_by | |
| trace "Tactic is run (ideally only once, in most general context)" | |
| trace_state | |
| decreasing_tactic | |
| end TestingFix | |
| namespace TestingGuessLex | |
| -- GuessLex should run the tactic an extra time, that is expected | |
| def rec : Nat → Nat → Nat | |
| | 0, _m => 1 | |
| | n+1, m => dup2 n (rec n (m + 1)) | |
| decreasing_by | |
| trace "Tactic is run (ideally only twice, in most general context)" | |
| trace_state | |
| decreasing_tactic | |
| end TestingGuessLex |