5cd90f5826
until around 7fe6881 the way to define well-founded recursions was to
specify a `WellFoundedRelation` on the argument explicitly. This was
rather low-level, for example one had to predict the packing of multiple
arguments into `PProd`s, the packing of mutual functions into `PSum`s,
and the cliques that were calculated.
Then the current `termination_by` syntax was introduced, where you
specify the termination argument at a higher level (one clause per
functions, unpacked arguments), and the `WellFoundedRelation` is found
using type class resolution.
The old syntax was kept around as `termination_by'`. This is not used
anywhere in the lean, std, mathlib or the theorem-proving-in-lean
repositories,
and three occurrences I found in the wild can do without
In particular, it should be possible to express anything that the old
syntax
supported also with the new one, possibly requiring a helper type with a
suitable instance, or the following generic wrapper that now lives in
std
```
def wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : {x : α // Acc r x}
```
Since the old syntax is unused, has an unhelpful name and relies on
internals, this removes the support. Now is a good time before the
refactoring that's planned in #2921.
The test suite was updated without particular surprises.
The parametric `terminationHint` parser is gone, which means we can
match on syntax more easily now, in `expandDecreasingBy?`.
29 lines
959 B
Text
29 lines
959 B
Text
def evenq (n: Nat) : Bool := Nat.mod n 2 = 0
|
|
|
|
private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
|
|
| 0 => by decide
|
|
| 1 => by decide
|
|
| n+2 => by
|
|
rw [Nat.div_eq]
|
|
split
|
|
· rw [Nat.add_sub_self_right]
|
|
have := pack_loop_terminates n
|
|
calc n/2 + 1 < Nat.succ n + 1 := Nat.add_le_add_right this 1
|
|
_ < Nat.succ (n + 2) := Nat.succ_lt_succ (Nat.succ_lt_succ (Nat.lt_succ_self _))
|
|
· apply Nat.zero_lt_succ
|
|
|
|
def pack (n: Nat) : List Nat :=
|
|
let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
|
|
let next (n: Nat) := n / 2;
|
|
match n with
|
|
| Nat.zero => List.cons acc accs
|
|
| n+1 => match evenq n with
|
|
| true => loop (next n) 0 (List.cons acc accs)
|
|
| false => loop (next n) (acc+1) accs
|
|
loop n 0 []
|
|
termination_by _ n _ _ => n
|
|
decreasing_by
|
|
simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
|
|
apply pack_loop_terminates
|
|
|
|
#eval pack 27
|