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.
105 lines
3.1 KiB
Text
105 lines
3.1 KiB
Text
example : (λ x => x)
|
|
=
|
|
(λ x : Nat =>
|
|
have foo := λ y => id (id y)
|
|
foo (0 + x)) := by
|
|
simp -zeta only [id]
|
|
guard_target =ₛ
|
|
(λ x => x)
|
|
=
|
|
(λ x : Nat =>
|
|
have foo := λ y => y
|
|
foo (0 + x))
|
|
simp
|
|
|
|
example (a : Nat) (h : a = b) : (have x := 1*a; 0 + x) = 0 + b := by
|
|
simp -zeta only [Nat.zero_add]
|
|
guard_target =ₛ
|
|
(have x := 1 * a; x) = b
|
|
simp -zeta only [Nat.one_mul]
|
|
guard_target =ₛ
|
|
(have x := a; x) = b
|
|
simp [h]
|
|
|
|
example (a : Nat) (h : a = b) : (have x := 1*a; 0 + x) = 0 + b := by
|
|
simp -zeta only [Nat.zero_add, Nat.one_mul]
|
|
guard_target =ₛ
|
|
(have x := a; x) = b
|
|
simp [h]
|
|
|
|
example (a : Nat) (h : a = b) : (have _y := 0; have x := 1*a; 0 + x) = 0 + b := by
|
|
simp -zeta only [Nat.zero_add, Nat.one_mul]
|
|
guard_target =ₛ
|
|
(have x := a; x) = b
|
|
simp [h]
|
|
|
|
example (a : Nat) (h : a = b) : (have y := 0; have x := y*0 + 1*a; 0 + x) = 0 + b := by
|
|
simp -zeta only [Nat.zero_add, Nat.one_mul, Nat.mul_zero]
|
|
guard_target =ₛ
|
|
(have x := a; x) = b
|
|
simp [h]
|
|
|
|
example (a : Nat) (h : a = b) : (have y := 0; have x := y*0 + 1*a; 0 + x) = 0 + b := by
|
|
simp -zeta only [Nat.zero_add, Nat.one_mul]
|
|
guard_target =ₛ
|
|
(have y := 0; have x := y*0 + a; x) = b
|
|
fail_if_success simp -zeta only [Nat.zero_add, Nat.one_mul] -- Should not make progress
|
|
simp -zeta only [Nat.mul_zero]
|
|
guard_target =ₛ
|
|
(have x := 0 + a; x) = b
|
|
simp -zeta only [Nat.zero_add]
|
|
guard_target =ₛ
|
|
(have x := a; x) = b
|
|
simp [h]
|
|
|
|
def f (n : Nat) (e : Nat) :=
|
|
match n with
|
|
| 0 => e
|
|
| n+1 => have _y := true; have x := 1*e; f n x
|
|
|
|
example (a b : Nat) (h : a = b) : f 2 (0 + a) = b := by
|
|
simp -zeta only [f]
|
|
guard_target =ₛ
|
|
(have x := 1 * (0 + a); have x := 1 * x; x) = b
|
|
fail_if_success simp -zeta only [f]
|
|
simp -zeta only [Nat.one_mul]
|
|
guard_target =ₛ
|
|
(have x := 0 + a; have x := x; x) = b
|
|
simp [h]
|
|
|
|
example (a b : Nat) (h : a = b) : f 20 (0 + a) = b := by
|
|
simp -zeta only [f]
|
|
fail_if_success simp -zeta only [f]
|
|
simp -zeta only [Nat.one_mul]
|
|
simp [h]
|
|
|
|
example (a b : Nat) (h : a = b) : f 50 (0 + a) = b := by
|
|
simp -zeta only [f]
|
|
fail_if_success simp -zeta only [f]
|
|
simp -zeta only [Nat.one_mul]
|
|
simp [h]
|
|
|
|
def g (n : Nat) (b : Bool) (e : Nat) :=
|
|
match n with
|
|
| 0 => if b then e else 0
|
|
| n+1 => have b' := !b; have x := 1*e; g n b' x
|
|
|
|
example (a b : Nat) (h : a = b) : g 2 true (0 + a) = b := by
|
|
simp -zeta only [g]
|
|
guard_target =ₛ
|
|
(have b' := !true; have x := 1 * (0 + a); have b' := !b';
|
|
have x := 1 * x; if b' = true then x else 0) = b
|
|
simp -zeta only [Bool.not_true, Nat.one_mul]
|
|
guard_target =ₛ
|
|
(have b' := false; have x := 0 + a; have b' := !b';
|
|
let_fun x := x; if b' = true then x else 0) = b
|
|
simp [h]
|
|
|
|
example (a : Nat) : g 33 true (0 + a) = 0 := by
|
|
simp -zeta only [g]
|
|
fail_if_success simp -zeta only [g]
|
|
simp -zeta only [Bool.not_true, Nat.one_mul]
|
|
fail_if_success simp -zeta only [Bool.not_true, Nat.one_mul]
|
|
simp -zeta only [Nat.zero_add]
|
|
fail_if_success simp -zeta only [Nat.zero_add]
|
|
simp
|