5f4d724c2d
This PR improves `match` generalization such that it abstracts metavariables in types of local variables and in the result type of the match over the match discriminants. Previously, a metavariable in the result type would silently default to the behavior of `generalizing := false`, and a metavariable in the type of a free variable would lead to an error (#8099). Example of a `match` that elaborates now but previously wouldn't: ```lean example (a : Nat) (ha : a = 37) := (match a with | 42 => by contradiction | n => n) = 37 ``` This is because the result type of the `match` is a metavariable that was not abstracted over `a` and hence generalization failed; the result is that `contradiction` cannot pick up the proof `ha : 42 = 37`. The old behavior can be recovered by passing `(generalizing := false)` to the `match`. Furthermore, programs such as the following can now be elaborated: ```lean example (n : Nat) : Id (Fin (n + 1)) := have jp : ?m := ?rhs match n with | 0 => ?jmp1 | n + 1 => ?jmp2 where finally case m => exact Fin (n + 1) → Id (Fin (n + 1)) case jmp1 => exact jp ⟨0, by decide⟩ case jmp2 => exact jp ⟨n, by omega⟩ case rhs => exact pure ``` This is useful for the `do` elaborator. Fixes #8099.
111 lines
3.2 KiB
Text
111 lines
3.2 KiB
Text
/-!
|
||
Checks that splitters have `Unit →` thunks and that nothing is confused because of that.
|
||
-/
|
||
|
||
set_option linter.unusedVariables false
|
||
|
||
|
||
-- set_option trace.Meta.Match.matchEqs true
|
||
|
||
def f (xs : List Nat) : Nat :=
|
||
match xs with
|
||
| [] => 1
|
||
| _ => 2
|
||
|
||
/--
|
||
info: def f.match_1.{u_1} : (motive : List Nat → Sort u_1) →
|
||
(xs : List Nat) → (Unit → motive []) → ((x : List Nat) → motive x) → motive xs
|
||
-/
|
||
#guard_msgs in
|
||
#print sig f.match_1
|
||
|
||
/--
|
||
info: private def f.match_1.splitter.{u_1} : (motive : List Nat → Sort u_1) →
|
||
(xs : List Nat) → (Unit → motive []) → ((x : List Nat) → (x = [] → False) → motive x) → motive xs
|
||
-/
|
||
#guard_msgs(pass trace, all) in
|
||
#print sig f.match_1.splitter
|
||
|
||
|
||
/--
|
||
info: private theorem f.match_1.congr_eq_1.{u_1} : ∀ (motive : List Nat → Sort u_1) (xs : List Nat) (h_1 : Unit → motive [])
|
||
(h_2 : (x : List Nat) → motive x),
|
||
xs = [] →
|
||
(match xs with
|
||
| [] => h_1 ()
|
||
| x => h_2 x) ≍
|
||
h_1 ()
|
||
-/
|
||
#guard_msgs(pass trace, all) in
|
||
#print sig f.match_1.congr_eq_1
|
||
|
||
-- set_option trace.split.debug true
|
||
|
||
theorem test1: f n ≤ 2 := by
|
||
unfold f
|
||
split <;> grind
|
||
|
||
|
||
theorem test2 : f n ≤ 2 := by
|
||
unfold f
|
||
grind
|
||
|
||
/--
|
||
info: theorem f.fun_cases : ∀ (motive : List Nat → Prop),
|
||
motive [] → (∀ (xs : List Nat), (xs = [] → False) → motive xs) → ∀ (xs : List Nat), motive xs
|
||
-/
|
||
#guard_msgs(pass trace, all) in
|
||
#print sig f.fun_cases
|
||
|
||
def Option_map (f : α → β) : Option α → Option β
|
||
| some x => some (f x)
|
||
| none => none
|
||
|
||
/--
|
||
info: def Option_map.match_1.{u_1, u_2} : {α : Type u_1} →
|
||
(motive : Option α → Sort u_2) → (x : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive x
|
||
-/
|
||
#guard_msgs in
|
||
#print sig Option_map.match_1
|
||
|
||
/--
|
||
info: private def Option_map.match_1.splitter.{u_1, u_2} : {α : Type u_1} →
|
||
(motive : Option α → Sort u_2) → (x : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive x :=
|
||
@Option_map.match_1
|
||
-/
|
||
#guard_msgs in
|
||
#print Option_map.match_1.splitter
|
||
|
||
/--
|
||
info: theorem Option_map.fun_cases.{u_1} : ∀ {α : Type u_1} (motive : Option α → Prop),
|
||
(∀ (x : α), motive (some x)) → motive none → ∀ (x : Option α), motive x
|
||
-/
|
||
#guard_msgs(pass trace, all) in
|
||
#print sig Option_map.fun_cases
|
||
|
||
def List_map (f : α → β) (l : List α) : List β := match _ : l with
|
||
| x::xs => f x :: List_map f xs
|
||
| [] => []
|
||
termination_by l
|
||
|
||
def foo₁ (a : Nat) (ha : a = 37) :=
|
||
(match (generalizing := false) h : a with | 42 => 23 | n => n) = 37
|
||
|
||
/--
|
||
info: private def foo₁.match_1.splitter.{u_1} : (motive : Nat → Sort u_1) →
|
||
(a : Nat) → (a = 42 → motive 42) → ((n : Nat) → (n = 42 → False) → a = n → motive n) → motive a
|
||
-/
|
||
#guard_msgs in
|
||
#print sig foo₁.match_1.splitter
|
||
|
||
def foo₂ (a : Nat) (ha : a = 37) :=
|
||
(match h : a with | 42 => 23 | n => n) = 37
|
||
|
||
/--
|
||
info: private def foo₂.match_1.splitter.{u_1} : (motive : (a : Nat) → a = 37 → Sort u_1) →
|
||
(a : Nat) →
|
||
(ha : a = 37) →
|
||
((ha : 42 = 37) → a = 42 → motive 42 ha) → ((n : Nat) → (ha : n = 37) → a = n → motive n ha) → motive a ha
|
||
-/
|
||
#guard_msgs in
|
||
#print sig foo₂.match_1.splitter
|