max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: grind annotations for getElem?_pos and variants (#8590)

Browse source 
This PR adds `@[grind]` to `getElem?_pos` and variants.

I'd initially thought these would result in too much case splitting, but
it seems to be only minor, and in use cases the payoff is good.
This commit is contained in:
Kim Morrison 2025-06-03 16:17:05 +10:00 • committed by GitHub
parent 106411420b
commit 9fc8713946
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/GetElem.lean
View file

@ -164,25 +164,25 @@ export LawfulGetElem (getElem?_def getElem!_def)
instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
LawfulGetElem coll idx elem valid where
@[simp] theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
@[simp, grind] theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) (h : dom c i) : c[i]? = some (c[i]'h) := by
have : Decidable (dom c i) := .isTrue h
rw [getElem?_def]
exact dif_pos h
@[simp] theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
@[simp, grind] theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
(c : cont) (i : idx) (h : ¬dom c i) : c[i]? = none := by
have : Decidable (dom c i) := .isFalse h
rw [getElem?_def]
exact dif_neg h
@[simp] theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
@[simp, grind] theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
[Inhabited elem] (c : cont) (i : idx) (h : dom c i) :
c[i]! = c[i]'h := by
have : Decidable (dom c i) := .isTrue h
simp [getElem!_def, getElem?_def, h]
@[simp] theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
@[simp, grind] theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
[Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) : c[i]! = default := by
have : Decidable (dom c i) := .isFalse h
simp [getElem!_def, getElem?_def, h]

2
tests/lean/run/grind_list2.lean
View file

@ -1075,7 +1075,7 @@ theorem map_dropLast {f : α → β} {l : List α} : l.dropLast.map f = (l.map f
theorem dropLast_append {l₁ l₂ : List α} :
(l₁ ++ l₂).dropLast = if l₂.isEmpty then l₁.dropLast else l₁ ++ l₂.dropLast := by
grind +extAll (splits := 10) [length_eq_zero_iff]
grind +extAll (splits := 12) [length_eq_zero_iff]
theorem dropLast_append_cons : dropLast (l₁ ++ b :: l₂) = l₁ ++ dropLast (b :: l₂) := by
grind +extAll