Geb.Mathlib.Data.Vector.Scatter

Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

import Geb.Mathlib.Data.Vector.OfFn

Writing a list of index-value pairs into a vector

Vector.scatter writes a list of index-value pairs into a vector in one left-to-right pass, each pair overwriting the entry at its index. Repeated indices are allowed, the last pair carrying an index being the one whose value survives, so the entry at an index is determined by the pairs whenever they all carry the same value there.

Main definitions

Vector.scatter — the pass.

Main statements

Vector.get_scatter_of_not_mem — an index no pair carries keeps its entry.

Vector.get_scatter_of_mem — an index carried with one value takes that value.

Implementation notes

The determinacy condition covers a list of constant value and a list of distinct indices alike, neither paying for the other's hypothesis. Both lemmas quantify over the starting vector, so they apply part-way through a pass as well as at its start.

Tags

vector, scatter, fold, choice-free

              @[expose] public sectionuniverse unamespace Vector

One pass writing each pair's value into the vector at the pair's index.

def scatter {α : Type u} {n : Nat} (P : List (Fin n × α)) (v : Vector α n) :
    Vector α n :=
  P.foldl (fun w p ↦ w.set p.1.val p.2 p.1.isLt) v

The pass leaves untouched every index no pair carries.

theorem get_scatter_of_not_mem {α : Type u} {n : Nat} (P : List (Fin n × α))
    (v : Vector α n) (j : Fin n) (hj : j ∉ P.map Prod.fst) :
    (scatter P v).get j = v.get j :=
  P.rec (motive := fun P ↦ ∀ (v : Vector α n), j ∉ P.map Prod.fst →
      (scatter P v).get j = v.get j)
    (fun _ _ ↦ rfl)
    (fun p P ih v hj ↦ byα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin nhj✝:¬j ∈ List.map Prod.fst P✝p:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), ¬j ∈ List.map Prod.fst P → (scatter P v).get j = v.get jv:Vector α nhj:¬j ∈ List.map Prod.fst (p :: P)⊢ (scatter (p :: P) v).get j = v.get j
      rw [List.map_cons,α:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin nhj✝:¬j ∈ List.map Prod.fst P✝p:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), ¬j ∈ List.map Prod.fst P → (scatter P v).get j = v.get jv:Vector α nhj:¬j ∈ p.fst :: List.map Prod.fst P⊢ (scatter (p :: P) v).get j = v.get j List.mem_cons,α:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin nhj✝:¬j ∈ List.map Prod.fst P✝p:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), ¬j ∈ List.map Prod.fst P → (scatter P v).get j = v.get jv:Vector α nhj:¬(j = p.fst ∨ j ∈ List.map Prod.fst P)⊢ (scatter (p :: P) v).get j = v.get j not_orα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin nhj✝:¬j ∈ List.map Prod.fst P✝p:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), ¬j ∈ List.map Prod.fst P → (scatter P v).get j = v.get jv:Vector α nhj:¬j = p.fst ∧ ¬j ∈ List.map Prod.fst P⊢ (scatter (p :: P) v).get j = v.get j] at hjα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin nhj✝:¬j ∈ List.map Prod.fst P✝p:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), ¬j ∈ List.map Prod.fst P → (scatter P v).get j = v.get jv:Vector α nhj:¬j = p.fst ∧ ¬j ∈ List.map Prod.fst P⊢ (scatter (p :: P) v).get j = v.get j
      refine (ih (v.set p.1.val p.2 p.1.isLt) hj.2).trans ?_α:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin nhj✝:¬j ∈ List.map Prod.fst P✝p:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), ¬j ∈ List.map Prod.fst P → (scatter P v).get j = v.get jv:Vector α nhj:¬j = p.fst ∧ ¬j ∈ List.map Prod.fst P⊢ (v.set (↑p.fst) p.snd ⋯).get j = v.get j
      simp only [get_eq_getElem]α:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin nhj✝:¬j ∈ List.map Prod.fst P✝p:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), ¬j ∈ List.map Prod.fst P → (scatter P v).get j = v.get jv:Vector α nhj:¬j = p.fst ∧ ¬j ∈ List.map Prod.fst P⊢ (v.set (↑p.fst) p.snd ⋯)[↑j] = v[↑j]
      exact getElem_set_ne p.1.isLt j.isLt fun he ↦ hj.1 (Fin.ext he).symmAll goals completed! 🐙)
    v hj

The pass writes the value of a pair whose index no other pair carries with a different value.

theorem get_scatter_of_mem {α : Type u} {n : Nat} (P : List (Fin n × α))
    (v : Vector α n) (j : Fin n) (a : α) (hm : (j, a) ∈ P)
    (hu : ∀ b, (j, b) ∈ P → b = a) : (scatter P v).get j = a :=
  P.rec (motive := fun P ↦ ∀ (v : Vector α n), (j, a) ∈ P →
      (∀ b, (j, b) ∈ P → b = a) → (scatter P v).get j = a)
    (fun _ hm _ ↦ absurd hm List.not_mem_nil)
    (fun p P ih v hm hu ↦ byα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = a⊢ (scatter (p :: P) v).get j = a
      by_cases hjP : j ∈ P.map Prod.fstposα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:j ∈ List.map Prod.fst P⊢ (scatter (p :: P) v).get j = anegα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:¬j ∈ List.map Prod.fst P⊢ (scatter (p :: P) v).get j = a
      ·posα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:j ∈ List.map Prod.fst P⊢ (scatter (p :: P) v).get j = a obtain ⟨q, hq, hqj⟩ := List.mem_map.mp hjPposα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:j ∈ List.map Prod.fst Pq:Fin n × αhq:q ∈ Phqj:q.fst = j⊢ (scatter (p :: P) v).get j = a
        have hq' : (j, q.2) ∈ P := by rw [← hqjα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:j ∈ List.map Prod.fst Pq:Fin n × αhq:q ∈ Phqj:q.fst = j⊢ (q.fst, q.snd) ∈ P]α:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:j ∈ List.map Prod.fst Pq:Fin n × αhq:q ∈ Phqj:q.fst = j⊢ (q.fst, q.snd) ∈ P; exact hqposα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:j ∈ List.map Prod.fst Pq:Fin n × αhq:q ∈ Phqj:q.fst = jhq':(j, q.snd) ∈ P⊢ (scatter (p :: P) v).get j = a
        exact ih (v.set p.1.val p.2 p.1.isLt)
          (hu q.2 (List.mem_cons_of_mem p hq') ▸ hq')
          fun b hb ↦ hu b (List.mem_cons_of_mem p hb)All goals completed! 🐙
      ·negα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:¬j ∈ List.map Prod.fst P⊢ (scatter (p :: P) v).get j = a rcases List.mem_cons.mp hm with he | hmPneg.inlα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:¬j ∈ List.map Prod.fst Phe:(j, a) = p⊢ (scatter (p :: P) v).get j = aneg.inrα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:¬j ∈ List.map Prod.fst PhmP:(j, a) ∈ P⊢ (scatter (p :: P) v).get j = a
        ·neg.inlα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:¬j ∈ List.map Prod.fst Phe:(j, a) = p⊢ (scatter (p :: P) v).get j = a subst heneg.inlα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = aP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhjP:¬j ∈ List.map Prod.fst Phm:(j, a) ∈ (j, a) :: Phu:∀ (b : α), (j, b) ∈ (j, a) :: P → b = a⊢ (scatter ((j, a) :: P) v).get j = a
          refine (get_scatter_of_not_mem P (v.set j.val a j.isLt) j hjP).trans ?_neg.inlα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = aP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhjP:¬j ∈ List.map Prod.fst Phm:(j, a) ∈ (j, a) :: Phu:∀ (b : α), (j, b) ∈ (j, a) :: P → b = a⊢ (v.set (↑j) a ⋯).get j = a
          simp only [get_eq_getElem]neg.inlα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = aP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhjP:¬j ∈ List.map Prod.fst Phm:(j, a) ∈ (j, a) :: Phu:∀ (b : α), (j, b) ∈ (j, a) :: P → b = a⊢ (v.set (↑j) a ⋯)[↑j] = a
          exact getElem_set_self j.isLtAll goals completed! 🐙
        ·neg.inrα:Type un:NatP✝:List (Fin n × α)v✝:Vector α nj:Fin na:αhm✝:(j, a) ∈ P✝hu✝:∀ (b : α), (j, b) ∈ P✝ → b = ap:Fin n × αP:List (Fin n × α)ih:∀ (v : Vector α n), (j, a) ∈ P → (∀ (b : α), (j, b) ∈ P → b = a) → (scatter P v).get j = av:Vector α nhm:(j, a) ∈ p :: Phu:∀ (b : α), (j, b) ∈ p :: P → b = ahjP:¬j ∈ List.map Prod.fst PhmP:(j, a) ∈ P⊢ (scatter (p :: P) v).get j = a exact absurd (List.mem_map_of_mem (f := Prod.fst) hmP) hjPAll goals completed! 🐙)
    v hm hu

end Vector