DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Use alpha and beta for FiniteMap type variables

Browse Source
This commit is contained in:
Danila Fedorin
2026-06-29 08:59:37 -05:00
parent 2598df690c
commit d1a11a9b2c
1 changed files with 51 additions and 51 deletions
Download Patch File Download Diff File Expand all files Collapse all files

102
lean/Spa/Lattice/FiniteMap.lean
View File

@@ -3,62 +3,62 @@ import Mathlib.Data.List.Nodup
namespace Spa namespace Spa
def FiniteMap (A B : Type*) (ks : List A) : Type _ := Fin ks.length → B def FiniteMap (α β : Type*) (ks : List α) : Type _ := Fin ks.length → β
namespace FiniteMap namespace FiniteMap
variable {A B : Type*} {ks : List A} variable {α β : Type*} {ks : List α}
instance [Lattice B] : Lattice (FiniteMap A B ks) := instance [Lattice β] : Lattice (FiniteMap α β ks) :=
inferInstanceAs (Lattice (Fin ks.length → B)) inferInstanceAs (Lattice (Fin ks.length → β))
instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) := instance [FiniteHeightLattice β] : FiniteHeightLattice (FiniteMap α β ks) :=
inferInstanceAs (FiniteHeightLattice (Fin ks.length → B)) inferInstanceAs (FiniteHeightLattice (Fin ks.length → β))
instance [DecidableEq B] : DecidableEq (FiniteMap A B ks) := instance [DecidableEq β] : DecidableEq (FiniteMap α β ks) :=
inferInstanceAs (DecidableEq (Fin ks.length → B)) inferInstanceAs (DecidableEq (Fin ks.length → β))
instance : Membership (A × B) (FiniteMap A B ks) := instance : Membership (α × β) (FiniteMap α β ks) :=
⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩ ⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩
lemma mem_iff {fm : FiniteMap A B ks} {p : A × B} : lemma mem_iff {fm : FiniteMap α β ks} {p : α × β} :
p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl
def MemKey (k : A) (_fm : FiniteMap A B ks) : Prop := k ∈ ks def MemKey (k : α) (_fm : FiniteMap α β ks) : Prop := k ∈ ks
lemma MemKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl lemma MemKey_iff {k : α} {fm : FiniteMap α β ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] : Decidable (MemKey k fm) := instance {k : α} {fm : FiniteMap α β ks} [DecidableEq α] : Decidable (MemKey k fm) :=
decidable_of_iff _ MemKey_iff.symm decidable_of_iff _ MemKey_iff.symm
lemma mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks} lemma mem_key_of_mem {k : α} {v : β} {fm : FiniteMap α β ks}
(h : (k, v) ∈ fm) : MemKey k fm := by (h : (k, v) ∈ fm) : MemKey k fm := by
obtain ⟨i, hi, _⟩ := h obtain ⟨i, hi, _⟩ := h
have hik : ks.get i = k := hi have hik : ks.get i = k := hi
exact hik ▸ ks.get_mem i exact hik ▸ ks.get_mem i
def toList (fm : FiniteMap A B ks) : List (A × B) := def toList (fm : FiniteMap α β ks) : List (α × β) :=
(List.finRange ks.length).map fun i => (ks.get i, fm i) (List.finRange ks.length).map fun i => (ks.get i, fm i)
lemma le_def [Lattice B] {fm₁ fm₂ : FiniteMap A B ks} : lemma le_def [Lattice β] {fm₁ fm₂ : FiniteMap α β ks} :
fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl
section Locate section Locate
variable [DecidableEq A] variable [DecidableEq α]
/-- Recover the value stored under a present key. -/ /-- Recover the value stored under a present key. -/
def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) : def locate {k : α} {fm : FiniteMap α β ks} (h : MemKey k fm) :
{v : B // (k, v) ∈ fm} := {v : β // (k, v) ∈ fm} :=
let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩ let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩
⟨fm i, i, List.idxOf_get _, rfl⟩ ⟨fm i, i, List.idxOf_get _, rfl⟩
end Locate end Locate
variable [Lattice B] variable [Lattice β]
lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks} lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap α β ks}
(hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B} (hle : fm₁ ≤ fm₂) {k : α} {v₁ v₂ : β}
(h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by
obtain ⟨i, hi, rfl⟩ := h₁ obtain ⟨i, hi, rfl⟩ := h₁
obtain ⟨j, hj, rfl⟩ := h₂ obtain ⟨j, hj, rfl⟩ := h₂
@@ -66,13 +66,13 @@ lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
subst hij subst hij
exact le_def.mp hle i exact le_def.mp hle i
lemma mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B} lemma mem_sup {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
(h : (k, v) ∈ fm₁ ⊔ fm₂) : (h : (k, v) ∈ fm₁ ⊔ fm₂) :
∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
obtain ⟨i, hi, rfl⟩ := h obtain ⟨i, hi, rfl⟩ := h
exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩ exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩
lemma mem_inf {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B} lemma mem_inf {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
(h : (k, v) ∈ fm₁ ⊓ fm₂) : (h : (k, v) ∈ fm₁ ⊓ fm₂) :
∃ v₁ v₂, v = v₁ ⊓ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by ∃ v₁ v₂, v = v₁ ⊓ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
obtain ⟨i, hi, rfl⟩ := h obtain ⟨i, hi, rfl⟩ := h
@@ -80,30 +80,30 @@ lemma mem_inf {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
section Updating section Updating
variable [DecidableEq A] variable [DecidableEq α]
def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) : FiniteMap A B ks := def updating (fm : FiniteMap α β ks) (ks' : List α) (g : α → β) : FiniteMap α β ks :=
fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i
omit [Lattice B] in omit [Lattice β] in
lemma eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks} lemma eq_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
{ks' : List A} {g : A → B} (hk : k ∈ ks') {ks' : List α} {g : α → β} (hk : k ∈ ks')
(h : (k, v) ∈ updating fm ks' g) : v = g k := by (h : (k, v) ∈ updating fm ks' g) : v = g k := by
obtain ⟨i, hi, rfl⟩ := h obtain ⟨i, hi, rfl⟩ := h
show (if ks.get i ∈ ks' then g (ks.get i) else fm i) = g k show (if ks.get i ∈ ks' then g (ks.get i) else fm i) = g k
rw [if_pos (by rw [hi]; exact hk), hi] rw [if_pos (by rw [hi]; exact hk), hi]
omit [Lattice B] in omit [Lattice β] in
lemma mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks} lemma mem_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
{ks' : List A} {g : A → B} (hk : k ∉ ks') {ks' : List α} {g : α → β} (hk : k ∉ ks')
(h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
obtain ⟨i, hi, rfl⟩ := h obtain ⟨i, hi, rfl⟩ := h
refine ⟨i, hi, ?_⟩ refine ⟨i, hi, ?_⟩
show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i) show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i)
rw [if_neg (by rw [hi]; exact hk)] rw [if_neg (by rw [hi]; exact hk)]
lemma updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A} lemma updating_mono {fm₁ fm₂ : FiniteMap α β ks} {ks' : List α}
{g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) : {g₁ g₂ : α → β} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
rw [le_def] rw [le_def]
intro i intro i
@@ -117,25 +117,25 @@ end Updating
section GeneralizedUpdate section GeneralizedUpdate
variable [DecidableEq A] {L : Type*} [Lattice L] variable [DecidableEq α] {L : Type*} [Lattice L]
def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B) def generalizedUpdate (f : L → FiniteMap α β ks) (g : α → L → β)
(ks' : List A) : L → FiniteMap A B ks := fun l => (ks' : List α) : L → FiniteMap α β ks := fun l =>
(f l).updating ks' (fun k => g k l) (f l).updating ks' (fun k => g k l)
variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A} variable {f : L → FiniteMap α β ks} {g : α → L → β} {ks' : List α}
lemma generalizedUpdate_monotone (hf : Monotone f) lemma generalizedUpdate_monotone (hf : Monotone f)
(hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') := (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl) fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
omit [Lattice B] [Lattice L] in omit [Lattice β] [Lattice L] in
lemma generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks') lemma generalizedUpdate_mem_eq {k : α} {v : β} {l : L} (hk : k ∈ ks')
(h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l :=
eq_of_mem_updating (g := fun k => g k l) hk h eq_of_mem_updating (g := fun k => g k l) hk h
omit [Lattice B] [Lattice L] in omit [Lattice β] [Lattice L] in
lemma generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks') lemma generalizedUpdate_not_mem_backward {k : α} {v : β} {l : L} (hk : k ∉ ks')
(h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l :=
mem_of_mem_updating hk h mem_of_mem_updating hk h
@@ -143,19 +143,19 @@ end GeneralizedUpdate
section ValuesAt section ValuesAt
variable [DecidableEq A] variable [DecidableEq α]
/-- The value stored under `k`, if `k` is a key. -/ /-- The value stored under `k`, if `k` is a key. -/
private def lookup (fm : FiniteMap A B ks) (k : A) : Option B := private def lookup (fm : FiniteMap α β ks) (k : α) : Option β :=
if h : k ∈ ks then some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none if h : k ∈ ks then some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none
/-- The values stored under the keys `ks'` (skipping any that are not keys). -/ /-- The values stored under the keys `ks'` (skipping any that are not keys). -/
def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B := def valuesAt (fm : FiniteMap α β ks) (ks' : List α) : List β :=
ks'.filterMap fm.lookup ks'.filterMap fm.lookup
omit [Lattice B] in omit [Lattice β] in
lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B} lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap α β ks} {k : α} {v : β}
{ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by {ks' : List α} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩ refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩
obtain ⟨i, hi, rfl⟩ := h obtain ⟨i, hi, rfl⟩ := h
have hik : ks.get i = k := hi have hik : ks.get i = k := hi
@@ -167,7 +167,7 @@ lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
hks.get_inj_iff.mp (by rw [List.idxOf_get, hi]) hks.get_inj_iff.mp (by rw [List.idxOf_get, hi])
rw [this] rw [this]
private lemma lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) (k : A) : private lemma lookup_rel {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂) (k : α) :
Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by
show Option.Rel _ show Option.Rel _
(if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) (if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
@@ -176,8 +176,8 @@ private lemma lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂
· rw [dif_pos hk, dif_pos hk]; exact Option.Rel.some (le_def.mp hle _) · rw [dif_pos hk, dif_pos hk]; exact Option.Rel.some (le_def.mp hle _)
· rw [dif_neg hk, dif_neg hk]; exact Option.Rel.none · rw [dif_neg hk, dif_neg hk]; exact Option.Rel.none
lemma valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) lemma valuesAt_le {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂)
(ks' : List A) : (ks' : List α) :
List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
induction ks' with induction ks' with
| nil => exact List.Forall₂.nil | nil => exact List.Forall₂.nil