d41f39fb10
This PR lets the match compilation procedure use sparse case analysis when the patterns only match on some but not all constructors of an inductive type. This way, less code is produce. Before, code handling each of the other cases was then optimized and commoned-up by later compilation pipeline, but that is wasteful to do. In some cases this will prevent Lean from noticing that a match statement is complete because it performs less case-splitting for the unreachable case. In this case, give explicit patterns to perform the deeper split with `by contradiction` as the right-hand side. At least temporarily, there is also the option to disable this behaviour with ``` set_option backwards.match.sparseCases false ```
39 lines
1.4 KiB
Text
39 lines
1.4 KiB
Text
import Lean
|
||
|
||
set_option warn.sorry false
|
||
|
||
/-!
|
||
#2564. `match` reduction currently has some special cases.
|
||
When combined with nonlinear functions like `List.insert` below,
|
||
it is crucial to preserve sharing during reduction. -/
|
||
|
||
section decidability_instances
|
||
|
||
variable {α : Type} {p : α → Prop} [DecidablePred p]
|
||
|
||
instance decidableBex : ∀ (l : List α), Decidable (∃ x, x ∈ l → p x)
|
||
| [] => isFalse sorry
|
||
| x::xs =>
|
||
match ‹DecidablePred p› x with
|
||
| isTrue h₁ => isTrue sorry
|
||
| isFalse h₁ => match decidableBex xs with
|
||
| isTrue h₂ => isTrue sorry
|
||
| isFalse h₂ => isFalse sorry
|
||
|
||
instance decidableBall (l : List α) : Decidable (∀ x, x ∈ l → p x) :=
|
||
match (inferInstance : Decidable <| ∃ x, x ∈ l → ¬ p x) with
|
||
| isFalse h => isTrue $ fun x hx => match ‹DecidablePred p› x with
|
||
| isTrue h' => h'
|
||
| isFalse h' => False.elim $ h sorry
|
||
| isTrue h => isFalse sorry
|
||
|
||
end decidability_instances
|
||
|
||
def parts : List (List Nat) := List.insert ([1, 1, 0, 0]) <| List.insert ([0, 0, 1, 1]) <|
|
||
List.insert ([1, 0, 0, 1]) <| List.insert ([1, 1, 1, 0]) <| List.insert ([1, 0, 0, 0]) <|
|
||
List.insert [1, 2, 3, 4] <| List.insert [5, 6, 7, 8] []
|
||
|
||
run_cmd
|
||
for _ in *...(10 : Nat) do
|
||
Lean.Elab.Command.elabCommand (←
|
||
`(example : ∀ (x) (_ : x ∈ parts) (y) (_ : y ∈ parts), x ++ y ∉ parts := by decide))
|