Properties of list canonicalization

This file contains lemmas about list canonicalization.

insertCanonical

theorem List.insertCanonical_singleton {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] (f : α → β) (x : α) : insertCanonical f x [] = [x]

theorem List.insertCanonical_not_nil {β : Type u_1} {α : Type u_2} [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) : insertCanonical f x xs ≠ []

theorem List.insertCanonical_mem {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] {f : α → β} {xs : List α} (x : α) : x ∈ insertCanonical f x xs

@[irreducible]

theorem List.insertCanonical_find? {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] [BEq β] [LawfulBEq β] {f : α → β} {xs : List α} (x : α) : find? (fun (e : α) => f e == f x) (insertCanonical f x xs) = some x

@[irreducible]

theorem List.insertCanonical_preserves_find_other_element {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] [BEq α] [Cedar.Data.StrictLT α] (k : α) (x : α × β) (xs : List (α × β)) : (x.fst == k) = false → find? (fun (x : α × β) => x.fst == k) (insertCanonical Prod.fst x xs) = find? (fun (x : α × β) => x.fst == k) xs

theorem List.insertCanonical_sortedBy {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] {f : α → β} {xs : List α} (x : α) : SortedBy f xs → SortedBy f (insertCanonical f x xs)

theorem List.insertCanonical_subset {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) : insertCanonical f x xs ⊆ x :: xs

theorem List.insertCanonical_equiv {α : Type u_1} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (x : α) (xs : List α) : x :: xs ≡ insertCanonical id x xs

theorem List.insertCanonical_preserves_forallᵥ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] {p : β → γ → Prop} {kv₁ : α × β} {kv₂ : α × γ} {kvs₁ : List (α × β)} {kvs₂ : List (α × γ)} (h₁ : kv₁.fst = kv₂.fst ∧ p kv₁.snd kv₂.snd) (h₂ : Forallᵥ p kvs₁ kvs₂) : Forallᵥ p (insertCanonical Prod.fst kv₁ kvs₁) (insertCanonical Prod.fst kv₂ kvs₂)

theorem List.insertCanonical_map_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) : insertCanonical Prod.fst (Prod.map id f x) (map (Prod.map id f) xs) = map (Prod.map id f) (insertCanonical Prod.fst x xs)

theorem List.insertCanonical_map_fst_canonicalize {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (xs : List (α × β)) (f : β → γ) (x : α × β) : insertCanonical Prod.fst (Prod.map id f x) (canonicalize Prod.fst (map (Prod.map id f) xs)) = map (Prod.map id f) (insertCanonical Prod.fst x (canonicalize Prod.fst xs))

canonicalize

theorem List.canonicalize_nil {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] (f : α → β) : canonicalize f [] = []

theorem List.canonicalize_nil' {β : Type u_1} {α : Type u_2} [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (xs : List α) : xs = [] ↔ canonicalize f xs = []

theorem List.canonicalize_not_nil {β : Type u_1} {α : Type u_2} [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (xs : List α) : xs ≠ [] ↔ canonicalize f xs ≠ []

theorem List.canonicalize_cons {β : Type u_1} {α : Type u_2} {ys : List α} [LT β] [DecidableLT β] (f : α → β) (xs : List α) (a : α) : canonicalize f xs = canonicalize f ys → canonicalize f (a :: xs) = canonicalize f (a :: ys)

theorem List.canonicalize_singleton {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] (f : α → β) (x : α) : canonicalize f [x] = [x]

theorem List.canonicalize_sortedBy {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] (f : α → β) (xs : List α) : SortedBy f (canonicalize f xs)

theorem List.sortedBy_implies_canonicalize_eq {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] {f : α → β} {xs : List α} : SortedBy f xs → canonicalize f xs = xs

theorem List.canonicalize_subseteq {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] (f : α → β) (xs : List α) : canonicalize f xs ⊆ xs

theorem List.in_canonicalize_in_list {β : Type u_1} {α : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] {f : α → β} {x : α} {xs : List α} : x ∈ canonicalize f xs → x ∈ xs

Corollary of canonicalize_subseteq

theorem List.canonicalize_equiv {α : Type u_1} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (xs : List α) : xs ≡ canonicalize id xs

theorem List.equiv_implies_canonical_eq {α : Type u_1} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (xs ys : List α) : xs ≡ ys → canonicalize id xs = canonicalize id ys

theorem List.canonicalize_idempotent {α : Type u_1} {β : Type u_2} [LT β] [Cedar.Data.StrictLT β] [DecidableLT β] (f : α → β) (xs : List α) : canonicalize f (canonicalize f xs) = canonicalize f xs

theorem List.canonicalize_id_filter {α : Type u_1} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (p : α → Bool) (xs : List α) : filter p (canonicalize id xs) = canonicalize id (filter p xs)

theorem List.canonicalize_preserves_forallᵥ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) : Forallᵥ p kvs₁ kvs₂ → Forallᵥ p (canonicalize Prod.fst kvs₁) (canonicalize Prod.fst kvs₂)

theorem List.canonicalize_of_map_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (xs : List (α × β)) (f : β → γ) : canonicalize Prod.fst (map (Prod.map id f) xs) = map (Prod.map id f) (canonicalize Prod.fst xs)