d1174e10e6
Previously, the tactic state shown at `decreasing_by` would leak lots of details about the translation, and mention `invImage`, `PSigma` etc. This is not nice. So this introduces `clean_wf`, which is like `simp_wf` but using `simp`'s `only` mode, and runs this unconditionally. This should clean up the goal to a reasonable extent. Previously `simp_wf` was an unrestricted `simp […]` call, but we probably don’t want arbitrary simplification to happen at this point, so this now became `simp only` call. For backwards compatibility, `decreasing_with` begins with `try simp`. The `simp_wf` tactic is still available to not break too much existing code; it’s docstring suggests to no longer use it. With `set_option cleanDecreasingByGoal false` one can disable the use of `clean_wf`. I hope this is only needed for debugging and understanding. Migration advise: If your `decreasing_by` proof begins with `simp_wf`, either remove that (if the proof still goes through), or replace with `simp`. I am a bit anxious about running even `simp only` unconditionally here, as it may do more than some user might want, e.g. because of options like `zetaDelta := true`. We'll see if we need to reign in this tactic some more. I wonder if in corner cases the `simp_wf` tactic might be able to close the goal, and if that is a problem. If so, we may have to promote simp’s internal `mayCloseGoal` parameter to a simp configuration option and use that here. fixes #4928
63 lines
2 KiB
Text
63 lines
2 KiB
Text
/-!
|
|
A “tricky” example from “Finding Lexicographic Orders for Termination Proofs in
|
|
Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow,
|
|
10.1007/978-3-540-74591-4_5
|
|
|
|
At the time of writing, Lean is able to find the lexicographic order
|
|
just fine, but only if the tactic is powerful enough. In partiuclar,
|
|
the default `decreasing_tactic` can only handle lexicographic descend when either
|
|
the left gets smaller, or the left stays equal and the right gets smaller.
|
|
But here we need to allow the general form, where the left is ≤ and the right
|
|
gets smaller. This needs a backtracking proof search, it seems, which we build here
|
|
(`search_lex`).
|
|
-/
|
|
|
|
set_option showInferredTerminationBy true
|
|
|
|
macro_rules | `(tactic| decreasing_trivial) =>
|
|
`(tactic| apply Nat.le_refl)
|
|
macro_rules | `(tactic| decreasing_trivial) =>
|
|
`(tactic| apply Nat.succ_lt_succ; decreasing_trivial)
|
|
macro_rules | `(tactic| decreasing_trivial) =>
|
|
`(tactic| apply Nat.sub_le)
|
|
macro_rules | `(tactic| decreasing_trivial) =>
|
|
`(tactic| apply Nat.div_le_self)
|
|
|
|
syntax "search_lex " tacticSeq : tactic
|
|
|
|
macro_rules | `(tactic|search_lex $ts:tacticSeq) => `(tactic| (
|
|
solve
|
|
| apply Prod.Lex.right'
|
|
· $ts
|
|
· search_lex $ts
|
|
| apply Prod.Lex.left
|
|
· $ts
|
|
| $ts
|
|
))
|
|
|
|
-- set_option trace.Elab.definition.wf true in
|
|
mutual
|
|
def prod (x y z : Nat) : Nat :=
|
|
if y % 2 = 0 then eprod x y z else oprod x y z
|
|
-- termination_by (y, 1, 0)
|
|
decreasing_by
|
|
all_goals
|
|
search_lex solve
|
|
| decreasing_trivial
|
|
| apply Nat.bitwise_rec_lemma; assumption
|
|
|
|
def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
|
|
-- termination_by (y, 0, 1)
|
|
decreasing_by
|
|
search_lex solve
|
|
| decreasing_trivial
|
|
| apply Nat.bitwise_rec_lemma; assumption
|
|
|
|
def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
|
|
-- termination_by (y, 0, 0)
|
|
decreasing_by
|
|
search_lex solve
|
|
| decreasing_trivial
|
|
| apply Nat.bitwise_rec_lemma; assumption
|
|
|
|
end
|