96e7ab078d
This PR fixes a performance issue that occurs when generating equation lemmas for functions that use match-expressions containing several literals. This issue was exposed by #9322 and arises from a combination of factors: 1. Literal values are compiled into a chain of dependent if-then-else expressions. 2. Dependent if-then-else expressions are significantly more expensive to simplify than regular ones. 3. The `split` tactic selects a target, splits it, and then invokes `simp` on the resulting subgoals. Moreover, `simp` traverses the entire goal bottom-up and does not stop after reaching the target. This PR addresses the issue by introducing a custom simproc that avoids recursively simplifying nested if-then-else expressions. It does **not** alter the user-facing behavior of the `split` tactic because such a change would be highly disruptive. Instead, the PR adds a new flag, `backward.split` to control the behavior of the user-facing `split` tactic. It is currently set to `true`, i.e., the old behavior is still the default one. In a future PR, we should set this flag to `false` by default and begin repairing all affected proofs. closes #9322
64 lines
1.6 KiB
Text
64 lines
1.6 KiB
Text
example (b : Bool) : (if (if b then true else true) then 1 else 2) = 1 := by
|
|
split
|
|
next h =>
|
|
guard_target =ₛ (if true = true then 1 else 2) = 1
|
|
guard_hyp h : b = true
|
|
simp
|
|
next h =>
|
|
guard_target =ₛ (if true = true then 1 else 2) = 1
|
|
guard_hyp h : ¬b = true
|
|
simp
|
|
|
|
example (b : Bool) : (if h : (if b then true else true) then 1 else 2) = 1 := by
|
|
split
|
|
next h' =>
|
|
guard_target = (if h : true = true then 1 else 2) = 1
|
|
guard_hyp h' : b = true
|
|
simp
|
|
next h' =>
|
|
guard_target = (if h : true = true then 1 else 2) = 1
|
|
guard_hyp h' : ¬b = true
|
|
simp
|
|
|
|
opaque f (a : Nat) (h : a > 0) : Nat
|
|
axiom fax : f a h = a
|
|
|
|
example : (if h : (if true then a > 0 else False) then f a (by grind) else a) = a := by
|
|
split
|
|
next =>
|
|
split
|
|
next => simp [fax]
|
|
next => simp
|
|
next => simp
|
|
|
|
set_option backward.split false
|
|
|
|
example (b : Bool) : (if (if b then true else true) then 1 else 2) = 1 := by
|
|
split
|
|
next h =>
|
|
guard_target =ₛ (if true = true then 1 else 2) = 1
|
|
guard_hyp h : b = true
|
|
simp
|
|
next h =>
|
|
guard_target =ₛ (if true = true then 1 else 2) = 1
|
|
guard_hyp h : ¬b = true
|
|
simp
|
|
|
|
example (b : Bool) : (if h : (if b then true else true) then 1 else 2) = 1 := by
|
|
split
|
|
next h' =>
|
|
guard_target = (if h : true = true then 1 else 2) = 1
|
|
guard_hyp h' : b = true
|
|
simp
|
|
next h' =>
|
|
guard_target = (if h : true = true then 1 else 2) = 1
|
|
guard_hyp h' : ¬b = true
|
|
simp
|
|
|
|
example : (if h : (if true then a > 0 else False) then f a (by grind) else a) = a := by
|
|
split
|
|
next =>
|
|
split
|
|
next => simp [fax]
|
|
next => simp
|
|
next => simp
|