Skip to content

Generalize ExtTreeMap lemma universes #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dhsorens merged 2 commits into from
Mar 31, 2026
Merged

Generalize ExtTreeMap lemma universes #6

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1c21eb1
fix: grind compiler warning
dhsorens Mar 16, 2026
ed753cf
fix: generalize ExtTreeMap lemma universes
quangvdao Mar 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions ExtTreeMapLemmas/ExtTreeMap.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,13 @@ import Mathlib.Tactic

namespace Std.ExtTreeMap

variable {α β : Type}
universe u v

variable {α : Type u} {β : Type v}

attribute [local instance low] beqOfOrd
attribute [grind ext] ExtTreeMap.ext_getElem?
attribute [grind] ExtTreeMap.distinct_keys_toList ExtTreeMap.getElem?_ofList_of_mem
attribute [grind .] ExtTreeMap.distinct_keys_toList ExtTreeMap.getElem?_ofList_of_mem

@[grind =]
theorem getElem?_pfilter
Expand All @@ -21,7 +23,7 @@ theorem getElem?_pfilter
-- Apply the hypothesis `h_filter_eq` directly to conclude the proof.
apply Std.ExtDTreeMap.get?_filter_with_getKey_pfilter

variable {α β : Type} {cmp : α → α → Ordering}
variable {α : Type u} {β : Type v} {cmp : α → α → Ordering}
variable {k : α} {m m₁ m₂ : Std.ExtTreeMap α β cmp} {f : α → β → β → β}

@[simp, grind =]
Expand Down Expand Up @@ -111,7 +113,7 @@ lemma toList_ofList [BEq α] [LawfulBEq α] : ofList (toList m) cmp = m := by
grind

@[simp, grind =]
lemma getElem?_filter_with_getKey {β : Type} {f : α → β → Bool} {k : α} {m : ExtTreeMap α β cmp} :
lemma getElem?_filter_with_getKey {f : α → β → Bool} {k : α} {m : ExtTreeMap α β cmp} :
(m.filter f)[k]? = m[k]?.filter (f k) := by
simp

Expand Down
Loading