7abc9106d7
This PR adds the following features to `simp`: - A routine for simplifying `have` telescopes in a way that avoids quadratic complexity arising from locally nameless expression representations, like what #6220 did for `letFun` telescopes. Furthermore, simp converts `letFun`s into `have`s (nondependent lets), and we remove the #6220 routine since we are moving away from `letFun` encodings of nondependent lets. - A `+letToHave` configuration option (enabled by default) that converts lets into haves when possible, when `-zeta` is set. Previously Lean would need to do a full typecheck of the bodies of `let`s, but the `letToHave` procedure can skip checking some subexpressions, and it modifies the `let`s in an entire expression at once rather than one at a time. - A `+zetaHave` configuration option, to turn off zeta reduction of `have`s specifically. The motivation is that dependent `let`s can only be dsimped by let, so zeta reducing just the dependent lets is a reasonable way to make progress. The `+zetaHave` option is also added to the meta configuration. - When `simp` is zeta reducing, it now uses an algorithm that avoids complexity quadratic in the depth of the let telescope. - Additionally, the zeta reduction routines in `simp`, `whnf`, and `isDefEq` now all are consistent with how they apply the `zeta`, `zetaHave`, and `zetaUnused` configurations. The `letToFun` option is addressing a TODO in `getSimpLetCase` ("handle a block of nested let decls in a single pass if this becomes a performance problem"). Performance should be compared to before #8804, which temporarily disabled the #6220 optimizations for `letFun` telescopes. Good kernel performance depends on carefully handling the `have` encoding. Due to the way the kernel instantiates bvars (it does *not* beta reduce when instantiating), we cannot use congruence theorems of the form `(have x := v; f x) = (have x ;= v'; f' x)`, since the bodies of the `have`s will not be syntactically equal, which triggers zeta reduction in the kernel in `is_def_eq`. Instead, we work with `f v = f' v'`, where `f` and `f'` are lambda expressions. There is still zeta reduction, but only when converting between these two forms at the outset of the generated proof.
35 lines
1.2 KiB
Text
35 lines
1.2 KiB
Text
opaque f : Nat → Nat
|
||
axiom f_eq (x : Nat) : f (f x) = x
|
||
|
||
theorem ex0 (x : Nat) (h : f (f x) = x) : (have y := 0 + x*x; if f (f x) = x then 1 else y + 1) = 1 := by
|
||
simp (config := { zeta := false }) only [h, Nat.zero_add]
|
||
trace_state
|
||
simp
|
||
|
||
#print ex0 -- uses have_congr
|
||
|
||
theorem ex1 (x : Nat) (h : f (f x) = x) : (have y := x*x; if f (f x) = x then 1 else y + 1) = 1 := by
|
||
simp (config := { zeta := false }) only [h]
|
||
trace_state
|
||
simp
|
||
|
||
#print ex1 -- uses have_body_congr
|
||
|
||
theorem ex2 (x z : Nat) (h : f (f x) = x) (h' : z = x) : (have y := f (f x); y) = z := by
|
||
simp (config := { zeta := false }) only [h]
|
||
trace_state
|
||
simp [h']
|
||
|
||
#print ex2 -- uses have_val_congr
|
||
|
||
theorem ex3 (x z : Nat) : (let α := Nat; (fun x : α => 0 + x)) = id := by
|
||
simp (config := { zeta := false, failIfUnchanged := false })
|
||
trace_state -- should not simplify let body since `fun α : Nat => fun x : α => 0 + x` is not type correct
|
||
simp (config := { unfoldPartialApp := true }) [id]
|
||
|
||
theorem ex4 (p : Prop) (h : p) : (have n := 10; fun x : { z : Nat // z < n } => x = x) = fun z => p := by
|
||
simp (config := { zeta := false })
|
||
trace_state
|
||
simp [h]
|
||
|
||
#print ex4 -- uses have_body_congr
|