Switch FiniteMap Fin n -> L representation

This helps automatically derive lattice laws for it

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

lean/Spa/Analysis/Constant.lean

@@ -77,12 +77,12 @@ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
     intro vs₁ vs₂ h
     simp only [eval]
     by_cases hk : k ∈ prog.vars
-    · rw [dif_pos (FiniteMap.memKey_iff.mpr hk),
-          dif_pos (FiniteMap.memKey_iff.mpr hk)]
+    · rw [dif_pos (FiniteMap.MemKey_iff.mpr hk),
+          dif_pos (FiniteMap.MemKey_iff.mpr hk)]
       exact FiniteMap.le_of_mem_mem prog.vars_nodup h
         (FiniteMap.locate _).2 (FiniteMap.locate _).2
-    · rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)),
-          dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))]
+    · rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)),
+          dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
   | num n =>
     intro vs₁ vs₂ _
     exact le_refl _

lean/Spa/Analysis/Forward/Lattices.lean

@@ -20,7 +20,7 @@ variable {L prog}
 omit [Lattice L] in
 theorem states_memKey (s : prog.State) (sv : StateVariables L prog) :
     FiniteMap.MemKey s sv :=
-  FiniteMap.memKey_iff.mpr (prog.states_complete s)
+  FiniteMap.MemKey_iff.mpr (prog.states_complete s)
 
 def variablesAt (s : prog.State) (sv : StateVariables L prog) :
     VariableValues L prog :=

lean/Spa/Analysis/Sign.lean

@@ -137,12 +137,12 @@ theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
     intro vs₁ vs₂ h
     simp only [eval]
     by_cases hk : k ∈ prog.vars
-    · rw [dif_pos (FiniteMap.memKey_iff.mpr hk),
-          dif_pos (FiniteMap.memKey_iff.mpr hk)]
+    · rw [dif_pos (FiniteMap.MemKey_iff.mpr hk),
+          dif_pos (FiniteMap.MemKey_iff.mpr hk)]
       exact FiniteMap.le_of_mem_mem prog.vars_nodup h
         (FiniteMap.locate _).2 (FiniteMap.locate _).2
-    · rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)),
-          dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))]
+    · rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)),
+          dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
   | num n =>
     intro vs₁ vs₂ _
     cases n <;> exact le_refl _

lean/Spa/Lattice/FiniteMap.lean

@@ -1,318 +1,111 @@
-import Spa.Lattice.IterProd
-import Spa.Isomorphism
+import Spa.Lattice.Tuple
+import Mathlib.Data.List.Nodup
 
 namespace Spa
 
-def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
-  { l : List (A × B) // l.map Prod.fst = ks }
+def FiniteMap (A B : Type*) (ks : List A) : Type _ := Fin ks.length → B
 
 namespace FiniteMap
 
 variable {A B : Type*} {ks : List A}
 
-instance [DecidableEq A] [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
-  fun a b => decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm
+instance [Lattice B] : Lattice (FiniteMap A B ks) :=
+  inferInstanceAs (Lattice (Fin ks.length → B))
 
-theorem spine_eq (fm₁ fm₂ : FiniteMap A B ks) :
-    fm₁.val.map Prod.fst = fm₂.val.map Prod.fst :=
-  fm₁.property.trans fm₂.property.symm
+instance [Lattice B] [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
+  inferInstanceAs (FiniteHeightLattice (Fin ks.length → B))
 
-def combine (f : B → B → B) (l₁ l₂ : List (A × B)) : List (A × B) :=
-  List.zipWith (fun p q => (p.1, f p.2 q.2)) l₁ l₂
-
-theorem combine_spine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)},
-    l₁.map Prod.fst = l₂.map Prod.fst →
-    (combine f l₁ l₂).map Prod.fst = l₁.map Prod.fst
-  | [], [], _ => rfl
-  | p :: l₁, q :: l₂, h => by
-    simp only [List.map_cons, List.cons.injEq] at h
-    simp only [combine, List.zipWith_cons_cons, List.map_cons]
-    exact congrArg _ (combine_spine f h.2)
-  | [], _ :: _, h => by simp at h
-  | _ :: _, [], h => by simp at h
-
-theorem combine_comm (f : B → B → B) (hf : ∀ a b, f a b = f b a) :
-    ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
-      combine f l₁ l₂ = combine f l₂ l₁
-  | [], [], _ => rfl
-  | p :: l₁, q :: l₂, h => by
-    simp only [List.map_cons, List.cons.injEq] at h
-    simp only [combine, List.zipWith_cons_cons]
-    rw [h.1, hf]
-    exact congrArg _ (combine_comm f hf h.2)
-  | [], _ :: _, h => by simp at h
-  | _ :: _, [], h => by simp at h
-
-theorem combine_assoc (f : B → B → B) (hf : ∀ a b c, f (f a b) c = f a (f b c)) :
-    ∀ {l₁ l₂ l₃ : List (A × B)},
-      l₁.map Prod.fst = l₂.map Prod.fst → l₂.map Prod.fst = l₃.map Prod.fst →
-      combine f (combine f l₁ l₂) l₃ = combine f l₁ (combine f l₂ l₃)
-  | [], [], [], _, _ => rfl
-  | p :: l₁, q :: l₂, r :: l₃, h₁₂, h₂₃ => by
-    simp only [List.map_cons, List.cons.injEq] at h₁₂ h₂₃
-    simp only [combine, List.zipWith_cons_cons]
-    rw [hf]
-    exact congrArg _ (combine_assoc f hf h₁₂.2 h₂₃.2)
-  | [], [], _ :: _, _, h => by simp at h
-  | [], _ :: _, _, h, _ => by simp at h
-  | _ :: _, [], _, h, _ => by simp at h
-  | _ :: _, _ :: _, [], _, h => by simp at h
-
-theorem combine_absorb (f g : B → B → B) (hfg : ∀ a b, f a (g a b) = a) :
-    ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
-      combine f l₁ (combine g l₁ l₂) = l₁
-  | [], [], _ => rfl
-  | p :: l₁, q :: l₂, h => by
-    simp only [List.map_cons, List.cons.injEq] at h
-    simp only [combine, List.zipWith_cons_cons, hfg]
-    exact congrArg _ (combine_absorb f g hfg h.2)
-  | [], _ :: _, h => by simp at h
-  | _ :: _, [], h => by simp at h
-
-variable [Lattice B]
-
-instance : Max (FiniteMap A B ks) where
-  max fm₁ fm₂ :=
-    ⟨combine (· ⊔ ·) fm₁.val fm₂.val,
-     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
-
-instance : Min (FiniteMap A B ks) where
-  min fm₁ fm₂ :=
-    ⟨combine (· ⊓ ·) fm₁.val fm₂.val,
-     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
-
-@[simp] theorem sup_val (fm₁ fm₂ : FiniteMap A B ks) :
-    (fm₁ ⊔ fm₂).val = combine (· ⊔ ·) fm₁.val fm₂.val := rfl
-
-@[simp] theorem inf_val (fm₁ fm₂ : FiniteMap A B ks) :
-    (fm₁ ⊓ fm₂).val = combine (· ⊓ ·) fm₁.val fm₂.val := rfl
-
-instance : Lattice (FiniteMap A B ks) :=
-  Lattice.mk'
-    (fun a b => Subtype.ext (combine_comm _ sup_comm (spine_eq a b)))
-    (fun a b c => Subtype.ext (combine_assoc _ sup_assoc (spine_eq a b) (spine_eq b c)))
-    (fun a b => Subtype.ext (combine_comm _ inf_comm (spine_eq a b)))
-    (fun a b c => Subtype.ext (combine_assoc _ inf_assoc (spine_eq a b) (spine_eq b c)))
-    (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => sup_inf_self) (spine_eq a b)))
-    (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => inf_sup_self) (spine_eq a b)))
+instance [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
+  inferInstanceAs (DecidableEq (Fin ks.length → B))
 
 instance : Membership (A × B) (FiniteMap A B ks) :=
-  ⟨fun fm p => p ∈ fm.val⟩
+  ⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩
 
-omit [Lattice B] in
-theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val :=
-  Iff.rfl
+theorem mem_iff {fm : FiniteMap A B ks} {p : A × B} :
+    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 ∈ fm.val.map Prod.fst
+def MemKey (k : A) (_fm : FiniteMap A B ks) : Prop := k ∈ ks
 
-omit [Lattice B] in
-theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by
-  rw [MemKey, fm.property]
+theorem MemKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
 
-instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] :
-    Decidable (MemKey k fm) :=
-  decidable_of_iff _ memKey_iff.symm
+instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] : Decidable (MemKey k fm) :=
+  decidable_of_iff _ MemKey_iff.symm
 
-omit [Lattice B] in
 theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
-    (h : (k, v) ∈ fm) : MemKey k fm :=
-  List.mem_map_of_mem _ h
+    (h : (k, v) ∈ fm) : MemKey k fm := by
+  obtain ⟨i, hi, _⟩ := h
+  have hik : ks.get i = k := hi
+  exact hik ▸ ks.get_mem i
+
+def toList (fm : FiniteMap A B ks) : List (A × B) :=
+  (List.finRange ks.length).map fun i => (ks.get i, fm i)
+
+theorem le_def [Lattice B] {fm₁ fm₂ : FiniteMap A B ks} :
+    fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl
 
 section Locate
 
 variable [DecidableEq A]
 
-private def locateList (k : A) :
-    (l : List (A × B)) → k ∈ l.map Prod.fst → {v : B // (k, v) ∈ l}
-  | [], h => absurd h (by simp)
-  | p :: l', h =>
-    if heq : p.1 = k then
-      ⟨p.2, by rw [← heq]; exact List.mem_cons_self ..⟩
-    else
-      let ⟨v, hv⟩ := locateList k l' (by
-        rcases List.mem_cons.mp h with h' | h'
-        · exact absurd h'.symm heq
-        · exact h')
-      ⟨v, List.mem_cons_of_mem _ hv⟩
-
+/-- Recover the value stored under a present key. -/
 def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
     {v : B // (k, v) ∈ fm} :=
-  locateList k fm.val h
+  let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩
+  ⟨fm i, i, List.idxOf_get _, rfl⟩
 
 end Locate
 
-theorem combine_eq_right_iff : ∀ {l₁ l₂ : List (A × B)},
-    l₁.map Prod.fst = l₂.map Prod.fst →
-    (combine (· ⊔ ·) l₁ l₂ = l₂ ↔
-      List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂)
-  | [], [], _ => by simp [combine]
-  | p :: l₁, q :: l₂, h => by
-    simp only [List.map_cons, List.cons.injEq] at h
-    simp only [combine, List.zipWith_cons_cons, List.cons.injEq,
-               List.forall₂_cons, Prod.ext_iff]
-    rw [show List.zipWith (fun p q : A × B => (p.1, p.2 ⊔ q.2)) l₁ l₂
-          = combine (· ⊔ ·) l₁ l₂ from rfl,
-        combine_eq_right_iff h.2]
-    constructor
-    · rintro ⟨⟨hk, hv⟩, hrest⟩
-      exact ⟨⟨hk, sup_eq_right.mp hv⟩, hrest⟩
-    · rintro ⟨⟨hk, hv⟩, hrest⟩
-      exact ⟨⟨hk, sup_eq_right.mpr hv⟩, hrest⟩
-  | [], _ :: _, h => by simp at h
-  | _ :: _, [], h => by simp at h
-
-theorem le_iff {fm₁ fm₂ : FiniteMap A B ks} :
-    fm₁ ≤ fm₂ ↔
-      List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) fm₁.val fm₂.val := by
-  rw [← sup_eq_right, ← combine_eq_right_iff (spine_eq fm₁ fm₂), Subtype.ext_iff,
-      sup_val]
-
-private theorem forall₂_spine : ∀ {l₁ l₂ : List (A × B)},
-    List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂ →
-    l₁.map Prod.fst = l₂.map Prod.fst
-  | _, _, List.Forall₂.nil => rfl
-  | _, _, List.Forall₂.cons hpq hrest => by
-    simp [List.map_cons, hpq.1, forall₂_spine hrest]
-
-private theorem forall₂_mem_mem {l₁ l₂ : List (A × B)}
-    (hf : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
-    (l₁.map Prod.fst).Nodup →
-    ∀ {k : A} {v₁ v₂ : B}, (k, v₁) ∈ l₁ → (k, v₂) ∈ l₂ → v₁ ≤ v₂ := by
-  induction hf with
-  | nil =>
-    intro _ k v₁ v₂ h₁ _
-    simp at h₁
-  | @cons p q l₁' l₂' hpq hrest ih =>
-    intro hnd k v₁ v₂ h₁ h₂
-    simp only [List.map_cons, List.nodup_cons] at hnd
-    have hspine := forall₂_spine hrest
-    rcases List.mem_cons.mp h₁ with heq₁ | h₁'
-    · rcases List.mem_cons.mp h₂ with heq₂ | h₂'
-      · rw [← heq₁, ← heq₂] at hpq
-        exact hpq.2
-      · exfalso
-        apply hnd.1
-        rw [show p.1 = k from (congrArg Prod.fst heq₁).symm, hspine]
-        exact List.mem_map_of_mem _ h₂'
-    · rcases List.mem_cons.mp h₂ with heq₂ | h₂'
-      · exfalso
-        apply hnd.1
-        rw [hpq.1, show q.1 = k from (congrArg Prod.fst heq₂).symm]
-        exact List.mem_map_of_mem _ h₁'
-      · exact ih hnd.2 h₁' h₂'
+variable [Lattice B]
 
 theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
     (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
-    (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ :=
-  forall₂_mem_mem (le_iff.mp hle) (fm₁.property.symm ▸ hks) h₁ h₂
-
-omit [Lattice B] in
-private theorem mem_combine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)} {k : A} {v : B},
-    l₁.map Prod.fst = l₂.map Prod.fst →
-    (k, v) ∈ combine f l₁ l₂ →
-    ∃ v₁ v₂, v = f v₁ v₂ ∧ (k, v₁) ∈ l₁ ∧ (k, v₂) ∈ l₂
-  | [], [], _, _, _, h => by simp [combine] at h
-  | p :: l₁, q :: l₂, k, v, hsp, h => by
-    simp only [List.map_cons, List.cons.injEq] at hsp
-    simp only [combine, List.zipWith_cons_cons] at h
-    rcases List.mem_cons.mp h with heq | h'
-    · injection heq with hk hv
-      exact ⟨p.2, q.2, hv,
-        by rw [hk]; simp,
-        by rw [hk, hsp.1]; simp⟩
-    · obtain ⟨v₁, v₂, hv, h₁, h₂⟩ := mem_combine f hsp.2 h'
-      exact ⟨v₁, v₂, hv, List.mem_cons_of_mem _ h₁, List.mem_cons_of_mem _ h₂⟩
+    (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by
+  obtain ⟨i, hi, rfl⟩ := h₁
+  obtain ⟨j, hj, rfl⟩ := h₂
+  have hij : i = j := hks.get_inj_iff.mp (hi.trans hj.symm)
+  subst hij
+  exact le_def.mp hle i
 
 theorem mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
     (h : (k, v) ∈ fm₁ ⊔ fm₂) :
-    ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ :=
-  mem_combine _ (spine_eq fm₁ fm₂) h
+    ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
+  obtain ⟨i, hi, rfl⟩ := h
+  exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩
 
 section Updating
 
 variable [DecidableEq A]
 
-def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
-    FiniteMap A B ks :=
-  ⟨fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p), by
-    rw [List.map_map,
-        show (Prod.fst ∘ fun p : A × B => if p.1 ∈ ks' then (p.1, g p.1) else p)
-          = Prod.fst from funext fun p => by by_cases h : p.1 ∈ ks' <;> simp [h]]
-    exact fm.property⟩
-
-omit [Lattice B] in
-@[simp] theorem updating_val (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
-    (updating fm ks' g).val
-      = fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p) := rfl
-
-omit [Lattice B] in
-theorem memKey_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} :
-    MemKey k (updating fm ks' g) ↔ MemKey k fm := by
-  rw [memKey_iff, memKey_iff]
+def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) : FiniteMap A B ks :=
+  fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i
 
 omit [Lattice B] in
 theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
     {ks' : List A} {g : A → B} (hk : k ∈ ks')
     (h : (k, v) ∈ updating fm ks' g) : v = g k := by
-  obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
-  by_cases hmem : p.1 ∈ ks'
-  · rw [if_pos hmem] at heq
-    injection heq with h1 h2
-    rw [← h2, h1]
-  · rw [if_neg hmem] at heq
-    rw [heq] at hmem
-    exact absurd hk hmem
-
-omit [Lattice B] in
-theorem mem_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B}
-    (hk : k ∈ ks') (hmem : MemKey k fm) : (k, g k) ∈ updating fm ks' g := by
-  obtain ⟨v, hv⟩ := locate hmem
-  exact List.mem_map.mpr ⟨(k, v), hv, by simp [hk]⟩
-
-omit [Lattice B] in
-theorem mem_updating_of_not_mem {k : A} {v : B} {fm : FiniteMap A B ks}
-    {ks' : List A} {g : A → B} (hk : k ∉ ks') (h : (k, v) ∈ fm) :
-    (k, v) ∈ updating fm ks' g :=
-  List.mem_map.mpr ⟨(k, v), h, by simp [hk]⟩
+  obtain ⟨i, hi, rfl⟩ := h
+  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]
 
 omit [Lattice B] in
 theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
     {ks' : List A} {g : A → B} (hk : k ∉ ks')
     (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
-  obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
-  by_cases hmem : p.1 ∈ ks'
-  · rw [if_pos hmem] at heq
-    injection heq with h1 _
-    rw [← h1] at hk
-    exact absurd hmem hk
-  · rw [if_neg hmem] at heq
-    exact heq ▸ hp
-
-private theorem updating_mono_list {ks' : List A} {g₁ g₂ : A → B}
-    (hg : ∀ k, g₁ k ≤ g₂ k) {l₁ l₂ : List (A × B)}
-    (hl : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
-    List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2)
-      (l₁.map fun p => if p.1 ∈ ks' then (p.1, g₁ p.1) else p)
-      (l₂.map fun p => if p.1 ∈ ks' then (p.1, g₂ p.1) else p) := by
-  induction hl with
-  | nil => exact List.Forall₂.nil
-  | @cons x y l₁' l₂' hpq hrest ih =>
-    simp only [List.map_cons]
-    refine List.Forall₂.cons ?_ ih
-    obtain ⟨hk, hv⟩ := hpq
-    by_cases h : x.1 ∈ ks'
-    · rw [if_pos h, if_pos (hk ▸ h)]
-      exact ⟨hk, hk ▸ hg x.1⟩
-    · rw [if_neg h, if_neg (fun hy => h (hk.symm ▸ hy))]
-      exact ⟨hk, hv⟩
+  obtain ⟨i, hi, rfl⟩ := h
+  refine ⟨i, hi, ?_⟩
+  show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i)
+  rw [if_neg (by rw [hi]; exact hk)]
 
 theorem updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
     {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
     updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
-  rw [le_iff] at hfm ⊢
-  simp only [updating_val]
-  exact updating_mono_list hg hfm
+  rw [le_def]
+  intro i
+  show (if ks.get i ∈ ks' then g₁ (ks.get i) else fm₁ i)
+     ≤ (if ks.get i ∈ ks' then g₂ (ks.get i) else fm₂ i)
+  split
+  · exact hg (ks.get i)
+  · exact le_def.mp hfm i
 
 end Updating
 
@@ -321,7 +114,7 @@ section GeneralizedUpdate
 variable [DecidableEq A] {L : Type*} [Lattice L]
 
 def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
-    (ks' : List A) (l : L) : FiniteMap A B ks :=
+    (ks' : List A) : L → FiniteMap A B ks := fun l =>
   (f l).updating ks' (fun k => g k l)
 
 variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
@@ -330,35 +123,15 @@ theorem generalizedUpdate_monotone (hf : Monotone f)
     (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
   fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
 
-omit [Lattice B] [Lattice L] in
-theorem generalizedUpdate_memKey {k : A} {l : L}
-    (h : MemKey k (f l)) : MemKey k (generalizedUpdate f g ks' l) := by
-  unfold generalizedUpdate
-  exact memKey_updating.mpr h
-
-omit [Lattice B] [Lattice L] in
-theorem generalizedUpdate_mem {k : A} {l : L} (hk : k ∈ ks')
-    (h : MemKey k (f l)) : (k, g k l) ∈ generalizedUpdate f g ks' l := by
-  unfold generalizedUpdate
-  exact mem_updating hk h
-
 omit [Lattice B] [Lattice L] in
 theorem generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
-    (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := by
-  unfold generalizedUpdate at h
-  exact eq_of_mem_updating (g := fun k => g k l) hk h
-
-omit [Lattice B] [Lattice L] in
-theorem generalizedUpdate_not_mem_forward {k : A} {v : B} {l : L} (hk : k ∉ ks')
-    (h : (k, v) ∈ f l) : (k, v) ∈ generalizedUpdate f g ks' l := by
-  unfold generalizedUpdate
-  exact mem_updating_of_not_mem hk h
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l :=
+  eq_of_mem_updating (g := fun k => g k l) hk h
 
 omit [Lattice B] [Lattice L] in
 theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
-    (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := by
-  unfold generalizedUpdate at h
-  exact mem_of_mem_updating hk h
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l :=
+  mem_of_mem_updating hk h
 
 end GeneralizedUpdate
 
@@ -366,48 +139,36 @@ section ValuesAt
 
 variable [DecidableEq A]
 
-private def lookup? (k : A) : List (A × B) → Option B
-  | [] => none
-  | p :: l' => if p.1 = k then some p.2 else lookup? k l'
+/-- The value stored under `k`, if `k` is a key. -/
+private def lookup (fm : FiniteMap A B ks) (k : A) : Option B :=
+  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). -/
 def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
-  ks'.filterMap (fun k => lookup? k fm.val)
-
-omit [Lattice B] in
-private theorem lookup?_eq_some_of_mem : ∀ {l : List (A × B)},
-    (l.map Prod.fst).Nodup → ∀ {k : A} {v : B}, (k, v) ∈ l →
-    lookup? k l = some v
-  | [], _, _, _, h => by simp at h
-  | p :: l', hnd, k, v, h => by
-    simp only [List.map_cons, List.nodup_cons] at hnd
-    rcases List.mem_cons.mp h with heq | h'
-    · rw [← heq]
-      simp [lookup?]
-    · rw [lookup?, if_neg ?_]
-      · exact lookup?_eq_some_of_mem hnd.2 h'
-      · intro hpk
-        subst hpk
-        have := List.mem_map_of_mem Prod.fst h'
-        exact hnd.1 this
+  ks'.filterMap fm.lookup
 
 omit [Lattice B] in
 theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
-    {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' :=
-  List.mem_filterMap.mpr
-    ⟨k, hk, lookup?_eq_some_of_mem (fm.property.symm ▸ hks) h⟩
+    {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
+  refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩
+  obtain ⟨i, hi, rfl⟩ := h
+  have hik : ks.get i = k := hi
+  have hmem : k ∈ ks := hik ▸ ks.get_mem i
+  show (if h : k ∈ ks then
+          some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) = some (fm i)
+  rw [dif_pos hmem]
+  have : (⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr hmem⟩ : Fin ks.length) = i :=
+    hks.get_inj_iff.mp (by rw [List.idxOf_get, hi])
+  rw [this]
 
-private theorem lookup?_forall₂ {l₁ l₂ : List (A × B)}
-    (h : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) (k : A) :
-    Option.Rel (· ≤ ·) (lookup? k l₁) (lookup? k l₂) := by
-  induction h with
-  | nil => exact Option.Rel.none
-  | @cons p q l₁ l₂ hpq hrest ih =>
-    rw [lookup?, lookup?]
-    by_cases hc : q.1 = k
-    · rw [if_pos hc, if_pos (hpq.1.trans hc)]
-      exact Option.Rel.some hpq.2
-    · rw [if_neg hc, if_neg (fun hp => hc (hpq.1 ▸ hp))]
-      exact ih
+private theorem lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) (k : A) :
+    Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by
+  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)
+  by_cases hk : k ∈ ks
+  · 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
 
 theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
     (ks' : List A) :
@@ -415,11 +176,11 @@ theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
   induction ks' with
   | nil => exact List.Forall₂.nil
   | cons k ks'' ih =>
-    have hrel := lookup?_forall₂ (le_iff.mp hle) k
+    have hrel := lookup_rel hle k
     rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons]
     revert hrel
-    generalize lookup? k fm₁.val = o₁
-    generalize lookup? k fm₂.val = o₂
+    generalize fm₁.lookup k = o₁
+    generalize fm₂.lookup k = o₂
     intro hrel
     cases hrel with
     | none => simpa [valuesAt] using ih
@@ -427,120 +188,6 @@ theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
 
 end ValuesAt
 
-section Iso
-
-omit [Lattice B] in
-theorem val_ne_nil {k : A} {ks' : List A} (fm : FiniteMap A B (k :: ks')) :
-    fm.val ≠ [] := fun h => by
-  have hp := fm.property
-  rw [h] at hp
-  simp at hp
-
-def headVal {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → B
-  | ⟨[], h⟩ => absurd h (by simp)
-  | ⟨p :: _, _⟩ => p.2
-
-def pop {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → FiniteMap A B ks'
-  | ⟨[], h⟩ => absurd h (by simp)
-  | ⟨_ :: l, h⟩ =>
-    ⟨l, by simp only [List.map_cons, List.cons.injEq] at h; exact h.2⟩
-
-omit [Lattice B] in
-theorem val_eq_cons {k : A} {ks' : List A} :
-    ∀ fm : FiniteMap A B (k :: ks'), fm.val = (k, fm.headVal) :: fm.pop.val
-  | ⟨[], h⟩ => absurd h (by simp)
-  | ⟨p :: l, h⟩ => by
-    simp only [List.map_cons, List.cons.injEq] at h
-    simp [headVal, pop, ← h.1]
-
-def toIter : {ks : List A} → FiniteMap A B ks → IterProd B PUnit ks.length
-  | [], _ => PUnit.unit
-  | _ :: _, fm => (fm.headVal, toIter fm.pop)
-
-def ofIter : (ks : List A) → IterProd B PUnit ks.length → FiniteMap A B ks
-  | [], _ => ⟨[], rfl⟩
-  | k :: ks', ip =>
-    ⟨(k, ip.1) :: (ofIter ks' ip.2).val, by
-      simp [(ofIter ks' ip.2).property]⟩
-
-omit [Lattice B] in
-theorem ofIter_toIter : ∀ {ks : List A} (fm : FiniteMap A B ks),
-    ofIter ks (toIter fm) = fm
-  | [], fm => by
-    obtain ⟨val, hprop⟩ := fm
-    cases val with
-    | nil => rfl
-    | cons p l => exact absurd hprop (by simp)
-  | k :: ks', fm => Subtype.ext (by
-      show (k, fm.headVal) :: (ofIter ks' (toIter fm.pop)).val = fm.val
-      rw [ofIter_toIter fm.pop, ← val_eq_cons fm])
-
-omit [Lattice B] in
-theorem toIter_ofIter : ∀ (ks : List A) (ip : IterProd B PUnit ks.length),
-    toIter (ofIter ks ip) = ip
-  | [], _ => rfl
-  | k :: ks', ip => by
-    show (headVal (ofIter (k :: ks') ip), toIter (pop (ofIter (k :: ks') ip))) = ip
-    rw [show pop (ofIter (k :: ks') ip) = ofIter ks' ip.2 from rfl,
-        toIter_ofIter ks' ip.2]
-    rfl
-
-theorem headVal_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
-    (h : fm₁ ≤ fm₂) : fm₁.headVal ≤ fm₂.headVal := by
-  have h' := le_iff.mp h
-  rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
-  exact (List.forall₂_cons.mp h').1.2
-
-theorem pop_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
-    (h : fm₁ ≤ fm₂) : fm₁.pop ≤ fm₂.pop := by
-  rw [le_iff]
-  have h' := le_iff.mp h
-  rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
-  exact (List.forall₂_cons.mp h').2
-
-theorem toIter_monotone : ∀ {ks : List A},
-    Monotone (toIter : FiniteMap A B ks → IterProd B PUnit ks.length)
-  | [] => fun _ _ _ => le_refl _
-  | _ :: _ => fun _ _ h =>
-    Prod.mk_le_mk.mpr ⟨headVal_le h, toIter_monotone (pop_le h)⟩
-
-theorem ofIter_monotone : ∀ (ks : List A), Monotone (ofIter (A := A) (B := B) ks)
-  | [] => fun _ _ _ => le_refl _
-  | k :: ks' => fun ip₁ ip₂ h => by
-    rw [le_iff]
-    show List.Forall₂ _ ((k, ip₁.1) :: (ofIter ks' ip₁.2).val)
-                        ((k, ip₂.1) :: (ofIter ks' ip₂.2).val)
-    exact List.Forall₂.cons ⟨rfl, h.1⟩ (le_iff.mp (ofIter_monotone ks' h.2))
-
-def fixedHeight [FiniteHeightLattice B] (ks : List A) :
-    FiniteHeightLattice (FiniteMap A B ks) :=
-  FiniteHeightLattice.transport
-    (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
-    (toIter_ofIter ks) ofIter_toIter
-
-instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
-  fixedHeight ks
-
-omit [Lattice B] in
-theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B},
-    (k, v) ∈ ofIter ks (IterProd.build b PUnit.unit ks.length) → v = b
-  | [], _, _, h => by simp [ofIter, mem_def] at h
-  | k' :: ks', k, v, h => by
-    rcases List.mem_cons.mp h with heq | h'
-    · exact (Prod.ext_iff.mp heq).2
-    · exact mem_ofIter_build h'
-
-theorem bot_contains_bots [FiniteHeightLattice B] {k : A} {v : B}
-    (h : (k, v) ∈ (fixedHeight ks).bot) : v = (⊥ : B) := by
-  have hbot : (fixedHeight ks).bot
-      = ofIter ks (IterProd.build (⊥ : B) (⊥ : PUnit) ks.length) := by
-    show ofIter ks (IterProd.fixedHeight (A := B) (B := PUnit) ks.length).bot = _
-    rw [IterProd.bot_fixedHeight]
-  rw [hbot] at h
-  exact mem_ofIter_build h
-
-end Iso
-
 end FiniteMap
 
 end Spa

lean/Spa/Lattice/Tuple.lean

@@ -0,0 +1,65 @@
+import Spa.Lattice.IterProd
+import Spa.Isomorphism
+
+namespace Spa
+
+namespace Tuple
+
+universe u
+
+variable {B : Type u}
+
+private def iterOfFun : {n : ℕ} → (Fin n → B) → IterProd B PUnit n
+  | 0, _ => PUnit.unit
+  | _ + 1, f => (f 0, iterOfFun (Fin.tail f))
+
+private def funOfIter : {n : ℕ} → IterProd B PUnit n → (Fin n → B)
+  | 0, _ => Fin.elim0
+  | _ + 1, ip => Fin.cons ip.1 (funOfIter ip.2)
+
+private theorem funOfIter_iterOfFun : ∀ {n : ℕ} (f : Fin n → B),
+    funOfIter (iterOfFun f) = f
+  | 0, _ => funext fun i => i.elim0
+  | _ + 1, f => by
+    show Fin.cons (f 0) (funOfIter (iterOfFun (Fin.tail f))) = f
+    rw [funOfIter_iterOfFun (Fin.tail f), Fin.cons_self_tail]
+
+private theorem iterOfFun_funOfIter : ∀ {n : ℕ} (ip : IterProd B PUnit n),
+    iterOfFun (funOfIter ip) = ip
+  | 0, PUnit.unit => rfl
+  | _ + 1, ip => by
+    show (funOfIter ip 0, iterOfFun (Fin.tail (funOfIter ip))) = ip
+    rw [show funOfIter ip = Fin.cons ip.1 (funOfIter ip.2) from rfl]
+    simp [Fin.cons_zero, Fin.tail_cons, iterOfFun_funOfIter ip.2]
+
+variable [Lattice B]
+
+private theorem funOfIter_mono {n : ℕ} :
+    Monotone (funOfIter : IterProd B PUnit n → (Fin n → B)) := by
+  induction n with
+  | zero => intro _ _ _ i; exact i.elim0
+  | succ n ih =>
+    intro ip₁ ip₂ h i
+    obtain ⟨h1, h2⟩ := Prod.le_def.mp h
+    rw [show funOfIter ip₁ = Fin.cons ip₁.1 (funOfIter ip₁.2) from rfl,
+        show funOfIter ip₂ = Fin.cons ip₂.1 (funOfIter ip₂.2) from rfl]
+    induction i using Fin.cases with
+    | zero => rw [Fin.cons_zero, Fin.cons_zero]; exact h1
+    | succ j => rw [Fin.cons_succ, Fin.cons_succ]; exact ih h2 j
+
+private theorem iterOfFun_mono {n : ℕ} :
+    Monotone (iterOfFun : (Fin n → B) → IterProd B PUnit n) := by
+  induction n with
+  | zero => intro f g _; exact le_of_eq rfl
+  | succ n ih =>
+    intro f g h
+    exact Prod.le_def.mpr ⟨h 0, ih fun i => h i.succ⟩
+
+instance instFiniteHeight {n : ℕ} [FiniteHeightLattice B] :
+    FiniteHeightLattice (Fin n → B) :=
+  FiniteHeightLattice.transport funOfIter iterOfFun
+    funOfIter_mono iterOfFun_mono iterOfFun_funOfIter funOfIter_iterOfFun
+
+end Tuple
+
+end Spa

lean/Spa/Showable.lean

@@ -30,7 +30,8 @@ instance {α : Type*} [Showable α] : Showable (AboveBelow α) :=
 instance {α β : Type*} {ks : List α} [Showable α] [Showable β] :
     Showable (FiniteMap α β ks) :=
   ⟨fun fm =>
-    "{" ++ fm.val.foldr (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) ""
+    "{" ++ (FiniteMap.toList fm).foldr
+        (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) ""
         ++ "}"⟩
 
 end Spa