Normalizing an index list.

The normalization of an index list, is the corresponding index list where all id are set to 0, 1, 2, ... determined by the order of indices without duals, followed by the order of indices with duals.

TODO: Replace with Mathlib lemma.

theorem IndexNotation.IndexList.dedup_map_of_injective' {α : Type} [DecidableEq α] (f : α → ℕ) (l : List α) (hf : ∀ I ∈ l, ∀ J ∈ l, f I = f J ↔ I = J) : (List.map f l).dedup = List.map f l.dedup

TODO: Replace with Mathlib lemma.

theorem IndexNotation.IndexList.indexOf_map {α : Type} [DecidableEq α] (f : α → ℕ) (l : List α) (n : α) (hf : ∀ I ∈ l, ∀ (J : α), f I = f J ↔ I = J) : List.indexOf n l = List.indexOf (f n) (List.map f l)

theorem IndexNotation.IndexList.indexOf_map_fin {α : Type} {m : ℕ} [DecidableEq α] (f : α → Fin m) (l : List α) (n : α) (hf : ∀ I ∈ l, ∀ (J : α), f I = f J ↔ I = J) : List.indexOf n l = List.indexOf (f n) (List.map f l)

theorem IndexNotation.IndexList.indexOf_map' {α : Type} [DecidableEq α] (f : α → ℕ) (g : α → α) (l : List α) (n : α) (hf : ∀ I ∈ l, ∀ (J : α), f I = f J ↔ g I = g J) (hg : ∀ I ∈ l, g I = I) (hs : ∀ (I : α), f I = f (g I)) : List.indexOf (g n) l = List.indexOf (f n) (List.map f l)

theorem IndexNotation.IndexList.filter_dedup {α : Type} [DecidableEq α] (l : List α) (p : α → Prop) [DecidablePred p] : (List.filter (fun (b : α) => decide (p b)) l).dedup = List.filter (fun (b : α) => decide (p b)) l.dedup

theorem IndexNotation.IndexList.findIdx?_map {α : Type} {β : Type} (p : α → Bool) (f : β → α) (l : List β) : List.findIdx? p (List.map f l) = List.findIdx? (p ∘ f) l

theorem IndexNotation.IndexList.findIdx?_on_finRange {n : ℕ} (p : Fin n.succ → Prop) [DecidablePred p] (hp : ¬p 0) : List.findIdx? (fun (b : Fin n.succ) => decide (p b)) (List.finRange n.succ) = Option.map (fun (i : ℕ) => i + 1) (List.findIdx? ((fun (b : Fin n.succ) => decide (p b)) ∘ Fin.succ) (List.finRange n))

theorem IndexNotation.IndexList.findIdx?_on_finRange_eq_findIdx {n : ℕ} (p : Fin n → Prop) [DecidablePred p] : List.findIdx? (fun (b : Fin n) => decide (p b)) (List.finRange n) = Option.map Fin.val (Fin.find p)

idList

def IndexNotation.IndexList.idListFin {X : Type} (l : IndexNotation.IndexList X) : List (Fin l.length)

The list of elements of Fin l.length i is in idListFin if l.idMap i appears for the first time in the ith spot.

For example, for the list ['ᵘ¹', 'ᵘ²', 'ᵤ₁'] the idListFin is [0, 1].

Equations

• One or more equations did not get rendered due to their size.

theorem IndexNotation.IndexList.idListFin_getDualInOther? {X : Type} (l : IndexNotation.IndexList X) : l.idListFin = List.filter (fun (i : Fin l.length) => decide (l.getDualInOther? l i = some i)) (List.finRange l.length)

def IndexNotation.IndexList.idList {X : Type} (l : IndexNotation.IndexList X) : List ℕ

The list of ids keeping only the first appearance of each id.

Equations

• l.idList = List.map l.idMap l.idListFin

theorem IndexNotation.IndexList.idList_getDualInOther? {X : Type} (l : IndexNotation.IndexList X) : l.idList = List.map l.idMap (List.filter (fun (i : Fin l.length) => decide (l.getDualInOther? l i = some i)) (List.finRange l.length))

theorem IndexNotation.IndexList.mem_idList_of_mem {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) {I : IndexNotation.Index X} (hI : I ∈ l.val) : I.id ∈ l.idList

theorem IndexNotation.IndexList.idMap_mem_idList {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) (i : Fin l.length) : l.idMap i ∈ l.idList

@[simp]

theorem IndexNotation.IndexList.idList_indexOf_mem {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) {I : IndexNotation.Index X} {J : IndexNotation.Index X} (hI : I ∈ l.val) (hJ : J ∈ l.val) : List.indexOf I.id l.idList = List.indexOf J.id l.idList ↔ I.id = J.id

theorem IndexNotation.IndexList.idList_indexOf_get {X : Type} (l : IndexNotation.IndexList X) (i : Fin l.length) : List.indexOf (l.idMap i) l.idList = List.indexOf ((l.getDualInOther? l i).get ⋯) l.idListFin

GetDualCast

def IndexNotation.IndexList.GetDualCast {X : Type} (l : IndexNotation.IndexList X) (l2 : IndexNotation.IndexList X) : Prop

Two IndexLists are related by GetDualCast if they are the same length, and have the same dual structure.

For example, ['ᵘ¹', 'ᵘ²', 'ᵤ₁'] and ['ᵤ₄', 'ᵘ⁵', 'ᵤ₄'] are related by GetDualCast, but ['ᵘ¹', 'ᵘ²', 'ᵤ₁'] and ['ᵘ¹', 'ᵘ²', 'ᵤ₃'] are not.

Equations

• l.GetDualCast l2 = (l.length = l2.length ∧ ∀ (h : l.length = l2.length), l.getDual? = Option.map (Fin.cast ⋯) ∘ l2.getDual? ∘ Fin.cast h)

theorem IndexNotation.IndexList.GetDualCast.symm {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) : l2.GetDualCast l

theorem IndexNotation.IndexList.GetDualCast.getDual?_isSome_iff {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (i : Fin l.length) : (l.getDual? i).isSome = true ↔ (l2.getDual? (Fin.cast ⋯ i)).isSome = true

theorem IndexNotation.IndexList.GetDualCast.getDual?_get {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (i : Fin l.length) (h1 : (l.getDual? i).isSome = true) : (l.getDual? i).get h1 = Fin.cast ⋯ ((l2.getDual? (Fin.cast ⋯ i)).get ⋯)

theorem IndexNotation.IndexList.GetDualCast.areDualInSelf_of {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (i : Fin l.length) (j : Fin l.length) (hA : l.AreDualInSelf i j) : l2.AreDualInSelf (Fin.cast ⋯ i) (Fin.cast ⋯ j)

theorem IndexNotation.IndexList.GetDualCast.areDualInSelf_iff {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (i : Fin l.length) (j : Fin l.length) : l.AreDualInSelf i j ↔ l2.AreDualInSelf (Fin.cast ⋯ i) (Fin.cast ⋯ j)

theorem IndexNotation.IndexList.GetDualCast.idMap_eq_of {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (i : Fin l.length) (j : Fin l.length) (hm : l.idMap i = l.idMap j) : l2.idMap (Fin.cast ⋯ i) = l2.idMap (Fin.cast ⋯ j)

theorem IndexNotation.IndexList.GetDualCast.idMap_eq_iff {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (i : Fin l.length) (j : Fin l.length) : l.idMap i = l.idMap j ↔ l2.idMap (Fin.cast ⋯ i) = l2.idMap (Fin.cast ⋯ j)

theorem IndexNotation.IndexList.GetDualCast.iff_idMap_eq {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} : l.GetDualCast l2 ↔ l.length = l2.length ∧ ∀ (h : l.length = l2.length) (i j : Fin l.length), l.idMap i = l.idMap j ↔ l2.idMap (Fin.cast h i) = l2.idMap (Fin.cast h j)

theorem IndexNotation.IndexList.GetDualCast.refl {X : Type} (l : IndexNotation.IndexList X) : l.GetDualCast l

theorem IndexNotation.IndexList.GetDualCast.trans {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} {l3 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (h' : l2.GetDualCast l3) : l.GetDualCast l3

theorem IndexNotation.IndexList.GetDualCast.getDualInOther?_get {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (i : Fin l.length) : (l.getDualInOther? l i).get ⋯ = Fin.cast ⋯ ((l2.getDualInOther? l2 (Fin.cast ⋯ i)).get ⋯)

theorem IndexNotation.IndexList.GetDualCast.countId_cast {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (i : Fin l.length) : l.countId (l.val.get i) = l2.countId (l2.val.get (Fin.cast ⋯ i))

theorem IndexNotation.IndexList.GetDualCast.idListFin_cast {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) : List.map (Fin.cast ⋯) l.idListFin = l2.idListFin

theorem IndexNotation.IndexList.GetDualCast.idList_indexOf {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) (i : Fin l.length) : List.indexOf (l2.idMap (Fin.cast ⋯ i)) l2.idList = List.indexOf (l.idMap i) l.idList

Normalized index list

def IndexNotation.IndexList.normalize {X : Type} (l : IndexNotation.IndexList X) : IndexNotation.IndexList X

Given an index list l, the corresponding index list where id's are set to sequentially lowest values.

E.g. on ['ᵘ¹', 'ᵘ³', 'ᵤ₁'] this gives ['ᵘ⁰', 'ᵘ¹', 'ᵤ₀'].

Equations

• l.normalize = { val := List.ofFn fun (i : Fin l.length) => (l.colorMap i, List.indexOf (l.idMap i) l.idList) }

theorem IndexNotation.IndexList.normalize_eq_map {X : Type} (l : IndexNotation.IndexList X) : l.normalize.val = List.map (fun (I : IndexNotation.Index X) => (I.toColor, List.indexOf I.id l.idList)) l.val

@[simp]

theorem IndexNotation.IndexList.normalize_length {X : Type} (l : IndexNotation.IndexList X) : l.normalize.length = l.length

@[simp]

theorem IndexNotation.IndexList.normalize_val_length {X : Type} (l : IndexNotation.IndexList X) : l.normalize.val.length = l.val.length

@[simp]

theorem IndexNotation.IndexList.normalize_colorMap {X : Type} (l : IndexNotation.IndexList X) : l.normalize.colorMap = l.colorMap ∘ Fin.cast ⋯

theorem IndexNotation.IndexList.colorMap_normalize {X : Type} (l : IndexNotation.IndexList X) : l.colorMap = l.normalize.colorMap ∘ Fin.cast ⋯

@[simp]

theorem IndexNotation.IndexList.normalize_countId {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) (i : Fin l.normalize.length) : l.normalize.countId l.normalize.val[↑i] = l.countId (l.val.get ⟨↑i, ⋯⟩)

@[simp]

theorem IndexNotation.IndexList.normalize_countId' {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) (i : Fin l.length) (hi : ↑i < l.normalize.length) : l.normalize.countId l.normalize.val[↑i] = l.countId (l.val.get i)

@[simp]

theorem IndexNotation.IndexList.normalize_countId_mem {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) (I : IndexNotation.Index X) (h : I ∈ l.val) : l.normalize.countId (I.toColor, List.indexOf I.id l.idList) = l.countId I

theorem IndexNotation.IndexList.normalize_filter_countId_eq_one {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) : List.map IndexNotation.Index.id (List.filter (fun (I : IndexNotation.Index X) => decide (l.normalize.countId I = 1)) l.normalize.val) = List.map (fun (a : ℕ) => List.indexOf a l.idList) (List.map IndexNotation.Index.id (List.filter (fun (I : IndexNotation.Index X) => decide (l.countId I = 1)) l.val))

@[simp]

theorem IndexNotation.IndexList.normalize_idMap_apply {X : Type} (l : IndexNotation.IndexList X) (i : Fin l.normalize.length) : l.normalize.idMap i = List.indexOf (l.val.get ⟨↑i, ⋯⟩).id l.idList

@[simp]

theorem IndexNotation.IndexList.normalize_getDualCast_self {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) : l.normalize.GetDualCast l

@[simp]

theorem IndexNotation.IndexList.self_getDualCast_normalize {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) : l.GetDualCast l.normalize

theorem IndexNotation.IndexList.normalize_filter_countId_not_eq_one {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) : List.map IndexNotation.Index.id (List.filter (fun (I : IndexNotation.Index X) => decide ¬l.normalize.countId I = 1) l.normalize.val) = List.map (fun (a : ℕ) => List.indexOf a l.idList) (List.map IndexNotation.Index.id (List.filter (fun (I : IndexNotation.Index X) => decide ¬l.countId I = 1) l.val))

theorem IndexNotation.IndexList.GetDualCast.to_normalize {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) : l.normalize.GetDualCast l2.normalize

theorem IndexNotation.IndexList.GetDualCast.normalize_idMap_eq {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.GetDualCast l2) : l.normalize.idMap = l2.normalize.idMap ∘ Fin.cast ⋯

theorem IndexNotation.IndexList.GetDualCast.iff_normalize {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} : l.GetDualCast l2 ↔ l.normalize.length = l2.normalize.length ∧ ∀ (h : l.normalize.length = l2.normalize.length), l.normalize.idMap = l2.normalize.idMap ∘ Fin.cast h

@[simp]

theorem IndexNotation.IndexList.normalize_normalize {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) : l.normalize.normalize = l.normalize

Equality of normalized forms

theorem IndexNotation.IndexList.normalize_length_eq_of_eq_length {X : Type} (l : IndexNotation.IndexList X) (l2 : IndexNotation.IndexList X) (h : l.length = l2.length) : l.normalize.length = l2.normalize.length

theorem IndexNotation.IndexList.normalize_colorMap_eq_of_eq_colorMap {X : Type} (l : IndexNotation.IndexList X) (l2 : IndexNotation.IndexList X) (h : l.length = l2.length) (hc : l.colorMap = l2.colorMap ∘ Fin.cast h) : l.normalize.colorMap = l2.normalize.colorMap ∘ Fin.cast ⋯

Reindexing

def IndexNotation.IndexList.Reindexing {X : Type} (l : IndexNotation.IndexList X) (l2 : IndexNotation.IndexList X) : Prop

Two ColorIndexList are said to be reindexes of one another if they:

1. have the same length.
2. every corresponding index has the same color, and duals which correspond.

Note: This does not allow for reordering of indices.

Equations

• l.Reindexing l2 = (l.length = l2.length ∧ ∀ (h : l.length = l2.length), l.colorMap = l2.colorMap ∘ Fin.cast h ∧ l.getDual? = Option.map (Fin.cast ⋯) ∘ l2.getDual? ∘ Fin.cast h)

theorem IndexNotation.IndexList.Reindexing.iff_getDualCast {X : Type} {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} : l.Reindexing l2 ↔ l.GetDualCast l2 ∧ ∀ (h : l.length = l2.length), l.colorMap = l2.colorMap ∘ Fin.cast h

theorem IndexNotation.IndexList.Reindexing.iff_normalize {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} : l.Reindexing l2 ↔ l.normalize = l2.normalize

theorem IndexNotation.IndexList.Reindexing.refl {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) : l.Reindexing l

theorem IndexNotation.IndexList.Reindexing.symm {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} (h : l.Reindexing l2) : l2.Reindexing l

theorem IndexNotation.IndexList.Reindexing.trans {X : Type} [DecidableEq X] {l : IndexNotation.IndexList X} {l2 : IndexNotation.IndexList X} {l3 : IndexNotation.IndexList X} (h : l.Reindexing l2) (h' : l2.Reindexing l3) : l.Reindexing l3

@[simp]

theorem IndexNotation.IndexList.normalize_reindexing_self {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) : l.normalize.Reindexing l

@[simp]

theorem IndexNotation.IndexList.self_reindexing_normalize {X : Type} [DecidableEq X] (l : IndexNotation.IndexList X) : l.Reindexing l.normalize