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

feat: add simp-friendly, Ord-based tree map lemmas (#7697)

Browse source 
This PR is a follow-up to #7695, which removed `simp` attributes from
tree map lemmas with bad discrimination patterns. In this PR, we
introduce some `Ord`-based lemmas that are more simp-friendly.

---------

Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
This commit is contained in:
Paul Reichert 2025-03-28 09:29:16 +01:00 • committed by GitHub
parent 060b2fe46f
commit e4968ae854
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 106 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/Std/Data/DTreeMap/Lemmas.lean
View file

@ -3128,6 +3128,12 @@ theorem compare_minKey_modify_eq [TransCmp cmp] {k f he} :
(t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
Impl.Const.compare_minKey_modify_eq t.wf
@[simp]
theorem ordCompare_minKey_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} {k f he} :
compare (modify t k f |>.minKey he)
(t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
compare_minKey_modify_eq
theorem minKey_alter_eq_self [TransCmp cmp] {k f he} :
(alter t k f).minKey he = k ↔
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
@ -3266,6 +3272,11 @@ theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
cmp (modify t k f).minKey! t.minKey! = .eq :=
Impl.Const.compare_minKey!_modify_eq t.wf (instOrd := ⟨cmp⟩)
@[simp]
theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} [Inhabited α] {k f} :
compare (modify t k f).minKey! t.minKey! = .eq :=
compare_minKey!_modify_eq
theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
(he : (alter t k f).isEmpty = false) :
(alter t k f).minKey! = k ↔
@ -3403,6 +3414,11 @@ theorem compare_minKeyD_modify_eq [TransCmp cmp] {k f fallback} :
cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
Impl.Const.compare_minKeyD_modify_eq t.wf (instOrd := ⟨cmp⟩)
@[simp]
theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} {k f fallback} :
compare (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
compare_minKeyD_modify_eq
theorem minKeyD_alter_eq_self [TransCmp cmp] {k f}
(he : (alter t k f).isEmpty = false) {fallback} :
(alter t k f |>.minKeyD fallback) = k ↔
@ -3754,6 +3770,12 @@ theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
(t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
Impl.Const.compare_maxKey_modify_eq t.wf
@[simp]
theorem ordCompare_maxKey_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} {k f he} :
compare (modify t k f |>.maxKey he)
(t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
compare_maxKey_modify_eq
theorem maxKey_alter_eq_self [TransCmp cmp] {k f he} :
(alter t k f).maxKey he = k ↔
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
@ -3892,6 +3914,11 @@ theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
cmp (modify t k f).maxKey! t.maxKey! = .eq :=
Impl.Const.compare_maxKey!_modify_eq t.wf (instOrd := ⟨cmp⟩)
@[simp]
theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} [Inhabited α] {k f} :
compare (modify t k f).maxKey! t.maxKey! = .eq :=
compare_maxKey!_modify_eq
theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
(he : (alter t k f).isEmpty = false) :
(alter t k f).maxKey! = k ↔
@ -4029,6 +4056,11 @@ theorem compare_maxKeyD_modify_eq [TransCmp cmp] {k f fallback} :
cmp (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
Impl.Const.compare_maxKeyD_modify_eq t.wf (instOrd := ⟨cmp⟩)
@[simp]
theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : DTreeMap α β} {k f fallback} :
compare (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
compare_maxKeyD_modify_eq
theorem maxKeyD_alter_eq_self [TransCmp cmp] {k f}
(he : (alter t k f).isEmpty = false) {fallback} :
(alter t k f |>.maxKeyD fallback) = k ↔

22
src/Std/Data/DTreeMap/Raw/Lemmas.lean
View file

@ -3120,6 +3120,12 @@ theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
cmp (modify t k f).minKey! t.minKey! = .eq :=
Impl.Const.compare_minKey!_modify_eq h (instOrd := ⟨cmp⟩)
@[simp]
theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inhabited α] (h : t.WF)
{k f} :
compare (modify t k f).minKey! t.minKey! = .eq :=
compare_minKey!_modify_eq h
theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
(he : (alter t k f).isEmpty = false) :
(alter t k f).minKey! = k ↔
@ -3257,6 +3263,11 @@ theorem compare_minKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
Impl.Const.compare_minKeyD_modify_eq h (instOrd := ⟨cmp⟩)
@[simp]
theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h : t.WF) {k f fallback} :
compare (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
compare_minKeyD_modify_eq h
theorem minKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
(he : (alter t k f).isEmpty = false) {fallback} :
(alter t k f |>.minKeyD fallback) = k ↔
@ -3594,6 +3605,12 @@ theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
cmp (modify t k f).maxKey! t.maxKey! = .eq :=
Impl.Const.compare_maxKey!_modify_eq h (instOrd := ⟨cmp⟩)
@[simp]
theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inhabited α] (h : t.WF)
{k f} :
compare (modify t k f).maxKey! t.maxKey! = .eq :=
compare_maxKey!_modify_eq h
theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
(he : (alter t k f).isEmpty = false) :
(alter t k f).maxKey! = k ↔
@ -3731,6 +3748,11 @@ theorem compare_maxKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
cmp (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
Impl.Const.compare_maxKeyD_modify_eq h (instOrd := ⟨cmp⟩)
@[simp]
theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h : t.WF) {k f fallback} :
compare (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
compare_maxKeyD_modify_eq h
theorem maxKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
(he : (alter t k f).isEmpty = false) {fallback} :
(alter t k f |>.maxKeyD fallback) = k ↔

32
src/Std/Data/TreeMap/Lemmas.lean
View file

@ -2063,6 +2063,12 @@ theorem compare_minKey_modify_eq [TransCmp cmp] {k f he} :
(t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
DTreeMap.Const.compare_minKey_modify_eq
@[simp]
theorem ordCompare_minKey_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} {k f he} :
compare (modify t k f |>.minKey he)
(t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
compare_minKey_modify_eq
theorem minKey_alter_eq_self [TransCmp cmp] {k f he} :
(alter t k f).minKey he = k ↔
(f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
@ -2185,6 +2191,11 @@ theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
cmp (modify t k f).minKey! t.minKey! = .eq :=
DTreeMap.Const.compare_minKey!_modify_eq
@[simp]
theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} [Inhabited α] {k f} :
compare (modify t k f).minKey! t.minKey! = .eq :=
compare_minKey!_modify_eq
theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
(he : (alter t k f).isEmpty = false) :
(alter t k f).minKey! = k ↔
@ -2306,6 +2317,11 @@ theorem compare_minKeyD_modify_eq [TransCmp cmp] {k f fallback} :
cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
DTreeMap.Const.compare_minKeyD_modify_eq
@[simp]
theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} {k f fallback} :
compare (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
compare_minKeyD_modify_eq
theorem minKeyD_alter_eq_self [TransCmp cmp] {k f}
(he : (alter t k f).isEmpty = false) {fallback} :
(alter t k f |>.minKeyD fallback) = k ↔
@ -2619,6 +2635,12 @@ theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
(t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
DTreeMap.Const.compare_maxKey_modify_eq
@[simp]
theorem ordCompare_maxKey_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} {k f he} :
compare (modify t k f |>.maxKey he)
(t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
compare_maxKey_modify_eq
theorem maxKey_alter_eq_self [TransCmp cmp] {k f he} :
(alter t k f).maxKey he = k ↔
(f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
@ -2741,6 +2763,11 @@ theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
cmp (modify t k f).maxKey! t.maxKey! = .eq :=
DTreeMap.Const.compare_maxKey!_modify_eq
@[simp]
theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} [Inhabited α] {k f} :
compare (modify t k f).maxKey! t.maxKey! = .eq :=
compare_maxKey!_modify_eq
theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
(he : (alter t k f).isEmpty = false) :
(alter t k f).maxKey! = k ↔
@ -2862,6 +2889,11 @@ theorem compare_maxKeyD_modify_eq [TransCmp cmp] {k f fallback} :
cmp (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
DTreeMap.Const.compare_maxKeyD_modify_eq
@[simp]
theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : TreeMap α β} {k f fallback} :
compare (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
compare_maxKeyD_modify_eq
theorem maxKeyD_alter_eq_self [TransCmp cmp] {k f}
(he : (alter t k f).isEmpty = false) {fallback} :
(alter t k f |>.maxKeyD fallback) = k ↔

20
src/Std/Data/TreeMap/Raw/Lemmas.lean
View file

@ -2059,6 +2059,11 @@ theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
cmp (modify t k f).minKey! t.minKey! = .eq :=
DTreeMap.Raw.Const.compare_minKey!_modify_eq h
@[simp]
theorem ordCompare_minKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inhabited α] (h : t.WF) {k f} :
compare (modify t k f).minKey! t.minKey! = .eq :=
compare_minKey!_modify_eq h
theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
(he : (alter t k f).isEmpty = false) :
(alter t k f).minKey! = k ↔
@ -2180,6 +2185,11 @@ theorem compare_minKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
DTreeMap.Raw.Const.compare_minKeyD_modify_eq h
@[simp]
theorem ordCompare_minKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h : t.WF) {k f fallback} :
compare (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
compare_minKeyD_modify_eq h
theorem minKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
(he : (alter t k f).isEmpty = false) {fallback} :
(alter t k f |>.minKeyD fallback) = k ↔
@ -2480,6 +2490,11 @@ theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
cmp (modify t k f).maxKey! t.maxKey! = .eq :=
DTreeMap.Raw.Const.compare_maxKey!_modify_eq h
@[simp]
theorem ordCompare_maxKey!_modify_eq [Ord α] [TransOrd α] {t : Raw α β} [Inhabited α] (h : t.WF) {k f} :
compare (modify t k f).maxKey! t.maxKey! = .eq :=
compare_maxKey!_modify_eq h
theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
(he : (alter t k f).isEmpty = false) :
(alter t k f).maxKey! = k ↔
@ -2601,6 +2616,11 @@ theorem compare_maxKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
cmp (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
DTreeMap.Raw.Const.compare_maxKeyD_modify_eq h
@[simp]
theorem ordCompare_maxKeyD_modify_eq [Ord α] [TransOrd α] {t : Raw α β} (h : t.WF) {k f fallback} :
compare (modify t k f |>.maxKeyD fallback) (t.maxKeyD fallback) = .eq :=
compare_maxKeyD_modify_eq h
theorem maxKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
(he : (alter t k f).isEmpty = false) {fallback} :
(alter t k f |>.maxKeyD fallback) = k ↔