d975e4302e
This is part of #3983. Fine-grained equational lemmas are useful even for non-recursive functions, so this adds them. The new option `eqns.nonrecursive` can be set to `false` to have the old behavior. ### Breaking channge This is a breaking change: Previously, `rw [Option.map]` would rewrite `Option.map f o` to `match o with … `. Now this rewrite will fail because the equational lemmas require constructors here (like they do for, say, `List.map`). Remedies: * Split on `o` before rewriting. * Use `rw [Option.map.eq_def]`, which rewrites any (saturated) application of `Option.map` * Use `set_option eqns.nonrecursive false` when *defining* the function in question. ### Interaction with simp The `simp` tactic so far had a special provision for non-recursive functions so that `simp [f]` will try to use the equational lemmas, but will also unfold `f` else, so less breakage here (but maybe performance improvements with functions with many cases when applied to a constructor, as the simplifier will no longer unfold to a large `match`-statement and then collapse it right away). For projection functions and functions marked `[reducible]`, `simp [f]` won’t use the equational theorems, and will only use its internal unfolding machinery. ### Implementation notes It uses the same `mkEqnTypes` function as for recursive functions, so we are close to a consistency here. There is still the wrinkle that for recursive functions we don't split matches without an interesting recursive call inside. Unifying that is future work.
27 lines
493 B
Text
27 lines
493 B
Text
open BitVec
|
|
|
|
def f (x : BitVec 32) : Nat :=
|
|
match x with
|
|
| 10#32 => 0
|
|
| 100#32 => 2
|
|
| 200#32 => 3
|
|
| 300#32 => 4
|
|
| 400#32 => 5
|
|
| 500#32 => 6
|
|
| 600#32 => 7
|
|
| 700#32 => 8
|
|
| 800#32 => 9
|
|
| 900#32 => 10
|
|
| 910#32 => 11
|
|
| 920#32 => 12
|
|
| _ => 1000
|
|
|
|
-- Generate the equational lemmas ahead of time, to avoid going
|
|
-- over the hearbeat limit below
|
|
#guard_msgs(drop all) in
|
|
#print equations f
|
|
|
|
set_option maxHeartbeats 300
|
|
example : f 500#32 = x := by
|
|
simp [f]
|
|
sorry
|