/-
Port of `Lattice/FiniteMap.agda` (and the parts of `Lattice/Map.agda` it was
built on).

Representation change enabled by dropping the setoid: a finite map over a
*fixed* key list `ks` is an association list whose key spine is *exactly* `ks`:

    FiniteMap A B ks := { l : List (A × B) // l.map Prod.fst = ks }

Since the spine (including order) is pinned by the type, the representation is
canonical and propositional equality coincides with the Agda `_≈_` (pointwise
value equality). The 1100-line `Lattice/Map.agda` — whose unordered-keys
union/intersection and `Provenance` machinery existed to make `_≈_` workable —
collapses into the positional `combine` below.

Correspondence (Agda ↦ Lean):
  FiniteMap, _≈_, ≈-Decidable    ↦ FiniteMap, `=`, DecidableEq instance
  _⊔_/_⊓_ (via Map union/inter)  ↦ Max/Min via `combine`
  isUnionSemilattice,
  isIntersectSemilattice,
  isLattice, lattice             ↦ instance Lattice (FiniteMap A B ks) (Lattice.mk',
                                   i.e. the same "two semilattices + absorption" data)
  _∈_, _∈k_, ∈k-dec, forget      ↦ Membership instance, MemKey (+ Decidable),
                                   mem_key_of_mem
  locate                         ↦ locate (computable)
  all-equal-keys                 ↦ spine_eq
  ∈k-exclusive                   ↦ immediate from memKey_iff (both sides ↔ k ∈ ks)
  m₁≼m₂⇒m₁[k]≼m₂[k]              ↦ le_of_mem_mem (takes `ks.Nodup`; the Agda Map
                                   carried key-uniqueness intrinsically)
  m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂         ↦ trivial with `=` (congruence)
  _updating_via_ + Map lemmas:
    updating-via-keys-≡          ↦ (the `property` field of `updating`)
    updating-via-∈k-forward      ↦ memKey_updating
    updating-via-k∈ks            ↦ mem_updating
    updating-via-k∈ks-≡          ↦ eq_of_mem_updating
    updating-via-k∉ks-forward    ↦ mem_updating_of_not_mem
    updating-via-k∉ks-backward   ↦ mem_of_mem_updating
    f'-Monotonic (Map)           ↦ updating_mono
  GeneralizedUpdate:
    f'                           ↦ generalizedUpdate
    f'-Monotonic                 ↦ generalizedUpdate_monotone
    f'-∈k-forward                ↦ generalizedUpdate_memKey
    f'-k∈ks                      ↦ generalizedUpdate_mem
    f'-k∈ks-≡                    ↦ generalizedUpdate_mem_eq
    f'-k∉ks-forward, -backward   ↦ generalizedUpdate_not_mem_forward, _backward
  _[_], []-∈                     ↦ valuesAt, mem_valuesAt (takes `ks.Nodup`)
  m₁≼m₂⇒m₁[ks]≼m₂[ks]            ↦ valuesAt_le
  Provenance-union               ↦ mem_sup
  ⊔-combines                     ↦ (omitted: only used inside the Agda
                                   isomorphism proofs, which simplified away)
  IterProdIsomorphism.from/to    ↦ toIter / ofIter — no `Unique ks` needed: the
                                   spine-pinned representation is already
                                   canonical, so the isomorphism is exact
  from/to-preserves-≈, -⊔-distr  ↦ toIter_monotone / ofIter_monotone (with `≼`
                                   being `≤`, the transport interface consumes
                                   monotonicity directly)
  from-to-inverseˡ/ʳ             ↦ toIter_ofIter / ofIter_toIter
  to-build                       ↦ mem_ofIter_build
  FixedHeight.fixedHeight        ↦ FiniteMap.fixedHeight (still obtained by
                                   transport along the IterProd isomorphism)
  ⊥-contains-bottoms             ↦ bot_contains_bots
-/
import Spa.Lattice.IterProd
import Spa.Isomorphism

namespace Spa

/-- Agda: `FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)`. -/
def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
  { l : List (A × B) // l.map Prod.fst = ks }

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

/-- Agda: `all-equal-keys`. -/
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

/-! ### The lattice structure (`combine` replaces Map union/intersection) -/

/-- Positional combination of two maps with equal spines. -/
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

/-- Agda: `isLattice`/`lattice` (built like the Agda record from the two
semilattices plus absorption; `Lattice.mk'` defines `a ≤ b ↔ a ⊔ b = b`). -/
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)))

/-! ### Membership -/

instance : Membership (A × B) (FiniteMap A B ks) :=
  ⟨fun fm p => p ∈ fm.val⟩

omit [Lattice B] in
theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val :=
  Iff.rfl

/-- Agda: `_∈k_`. -/
def MemKey (k : A) (fm : FiniteMap A B ks) : Prop :=
  k ∈ fm.val.map Prod.fst

omit [Lattice B] in
/-- A key is in the map iff it is in the (fixed) key list
(Agda: `∈k-exclusive` becomes a special case). -/
theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by
  rw [MemKey, fm.property]

/-- Agda: `∈k-dec`. -/
instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] :
    Decidable (MemKey k fm) :=
  decidable_of_iff _ memKey_iff.symm

omit [Lattice B] in
/-- Agda: `forget`. -/
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

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⟩

/-- Agda: `locate`. -/
def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
    {v : B // (k, v) ∈ fm} :=
  locateList k fm.val h

end Locate

/-! ### The pointwise order -/

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

/-- The order on finite maps is the pointwise order on values. -/
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₂'

/-- Agda: `m₁≼m₂⇒m₁[k]≼m₂[k]`. The `Nodup` hypothesis was carried inside the
Agda `Map` type. -/
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₂

/-! ### Provenance of joined values -/

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₂⟩

/-- Agda: `Provenance-union` — a binding of a join comes from bindings of both
maps. -/
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

/-! ### Updating (Agda: `_updating_via_` and `GeneralizedUpdate`) -/

section Updating

variable [DecidableEq A]

/-- Agda: `_updating_via_` — for each key in `ks'`, replace its value by `g k`. -/
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
/-- Agda: `updating-via-∈k-forward` (strengthened to an iff). -/
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]

omit [Lattice B] in
/-- Agda: `updating-via-k∈ks-≡`. -/
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
/-- Agda: `updating-via-k∈ks`. -/
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
/-- Agda: `updating-via-k∉ks-forward`. -/
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]⟩

omit [Lattice B] in
/-- Agda: `updating-via-k∉ks-backward`. -/
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⟩

/-- Agda: `f'-Monotonic` at the `Map` level. -/
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

end Updating

section GeneralizedUpdate

/-! Agda: `GeneralizedUpdate` (the "Exercise 4.26" construction). -/

variable [DecidableEq A] {L : Type*} [Lattice L]

/-- Agda: `GeneralizedUpdate.f'`. -/
def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
    (ks' : List A) (l : L) : FiniteMap A B ks :=
  (f l).updating ks' (fun k => g k l)

variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}

/-- Agda: `f'-Monotonic`. -/
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
/-- Agda: `f'-∈k-forward`. -/
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
/-- Agda: `f'-k∈ks`. -/
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
/-- Agda: `f'-k∈ks-≡`. -/
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
/-- Agda: `f'-k∉ks-forward`. -/
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

omit [Lattice B] [Lattice L] in
/-- Agda: `f'-k∉ks-backward`. -/
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

end GeneralizedUpdate

/-! ### Reading off values at a list of keys (Agda: `_[_]`) -/

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'

/-- Agda: `_[_]`. -/
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

omit [Lattice B] in
/-- Agda: `[]-∈`. -/
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⟩

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

/-- Agda: `m₁≼m₂⇒m₁[ks]≼m₂[ks]`. -/
theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
    (ks' : List A) :
    List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
  induction ks' with
  | nil => exact List.Forall₂.nil
  | cons k ks'' ih =>
    have hrel := lookup?_forall₂ (le_iff.mp 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₂
    intro hrel
    cases hrel with
    | none => simpa [valuesAt] using ih
    | some hv => exact List.Forall₂.cons hv (by simpa [valuesAt] using ih)

end ValuesAt

/-! ### The isomorphism with `IterProd` and the fixed height -/

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

/-- Agda: `pop`. -/
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]

/-- Agda: `IterProdIsomorphism.from`. -/
def toIter : {ks : List A} → FiniteMap A B ks → IterProd B PUnit ks.length
  | [], _ => PUnit.unit
  | _ :: _, fm => (fm.headVal, toIter fm.pop)

/-- Agda: `IterProdIsomorphism.to` (no `Unique ks` needed: the spine-pinned
representation is canonical). -/
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
/-- Agda: `from-to-inverseʳ`. -/
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
/-- Agda: `from-to-inverseˡ`. -/
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

/-- Agda: `from-preserves-≈` and `from-⊔-distr` (see header note). -/
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)⟩

/-- Agda: `to-preserves-≈` and `to-⊔-distr` (see header note). -/
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))

/-- Agda: `FixedHeight.fixedHeight` — a finite map into a lattice of height
`hB` has height `|ks| · hB`, by transport along the `IterProd` isomorphism. -/
def fixedHeight {hB : ℕ} (fhB : FixedHeight B hB) (ks : List A) :
    FixedHeight (FiniteMap A B ks) (ks.length * hB) :=
  ((IterProd.fixedHeight fhB punitFixedHeight ks.length).transport
      (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
      (toIter_ofIter ks) (fun fm => ofIter_toIter fm)).cast (by ring)

omit [Lattice B] in
/-- Agda: `to-build`. -/
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'

/-- Agda: `⊥-contains-bottoms`. -/
theorem bot_contains_bots {hB : ℕ} (fhB : FixedHeight B hB) {k : A} {v : B}
    (h : (k, v) ∈ (fixedHeight fhB ks).bot) : v = fhB.bot := by
  have hbot : (fixedHeight fhB ks).bot
      = ofIter ks (IterProd.build fhB.bot PUnit.unit ks.length) := by
    show ofIter ks (IterProd.fixedHeight fhB punitFixedHeight ks.length).bot = _
    rw [IterProd.bot_fixedHeight]
  rw [hbot] at h
  exact mem_ofIter_build h

end Iso

end FiniteMap

end Spa