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
69 lines
1.4 KiB
Text
69 lines
1.4 KiB
Text
/--
|
|
error: tactic 'fail' failed
|
|
x y : Nat
|
|
⊢ x - 1 < x
|
|
-/
|
|
#guard_msgs in
|
|
def g (x : Nat) (y : Nat) : Nat := g (x - 1) y
|
|
termination_by x
|
|
decreasing_by fail
|
|
|
|
/--
|
|
error: tactic 'fail' failed
|
|
x : List Nat
|
|
y : Nat
|
|
⊢ sizeOf x.tail < sizeOf x
|
|
-/
|
|
#guard_msgs in
|
|
def h (x : List Nat) (y : Nat) : Nat := h x.tail y
|
|
termination_by x
|
|
decreasing_by fail
|
|
|
|
/--
|
|
error: tactic 'fail' failed
|
|
x : List Nat
|
|
y : Nat
|
|
⊢ x.tail.length < x.length
|
|
-/
|
|
#guard_msgs in
|
|
def f (x : List Nat) (y : Nat) : Nat := f x.tail y
|
|
termination_by x.length
|
|
decreasing_by fail
|
|
|
|
/--
|
|
error: tactic 'fail' failed
|
|
x : List Nat
|
|
y : Nat
|
|
⊢ x.tail.length < x.length
|
|
-/
|
|
#guard_msgs in
|
|
mutual
|
|
def f1 (x : List Nat) (y : Nat) : Nat := f2 x.tail y
|
|
termination_by x.length
|
|
decreasing_by fail
|
|
def f2 (x : List Nat) (y : Nat) : Nat := f1 x.tail y
|
|
termination_by x.length
|
|
decreasing_by fail
|
|
end
|
|
|
|
/--
|
|
error: tactic 'fail' failed
|
|
x : List Nat
|
|
y : Nat
|
|
⊢ (invImage
|
|
(fun x =>
|
|
PSum.casesOn x (fun _x => PSigma.casesOn _x fun x y => x.length) fun _x =>
|
|
PSigma.casesOn _x fun x y => x.length)
|
|
instWellFoundedRelationOfSizeOf).1
|
|
(PSum.inr ⟨x.tail, y⟩) (PSum.inl ⟨x, y⟩)
|
|
-/
|
|
#guard_msgs in
|
|
set_option cleanDecreasingByGoal false in
|
|
mutual
|
|
def g1 (x : List Nat) (y : Nat) : Nat := g2 x.tail y
|
|
termination_by x.length
|
|
decreasing_by fail
|
|
def g2 (x : List Nat) (y : Nat) : Nat := g1 x.tail y
|
|
termination_by x.length
|
|
decreasing_by fail
|
|
end
|