feat(data/finsupp/basic): alist.lookup as a finitely supported func…

…tion (#15443)

Reworked from #15396. The planned use case for this new definition is to facilitate giving the [Cantor Normal Form](https://leanprover-community.github.io/mathlib_docs/set_theory/ordinal/cantor_normal_form.html#ordinal.CNF) of an ordinal as a finitely supported function. See #15396 (comment) for further discussion of the motivation.

src/data/finsupp/basic.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Scott Morrison
 import algebra.hom.group_action
 import algebra.indicator_function
 import data.finset.preimage
+import data.list.alist
 
 /-!
 # Type of functions with finite support
@@ -774,8 +775,71 @@ end
 @[simp] lemma graph_eq_empty {f : α →₀ M} : f.graph = ∅ ↔ f = 0 :=
 (graph_injective α M).eq_iff' graph_zero
 
+/-- Produce an association list for the finsupp over its support using choice. -/
+@[simps] def to_alist (f : α →₀ M) : alist (λ x : α, M) :=
+⟨f.graph.to_list.map prod.to_sigma, begin
+  rw [list.nodupkeys, list.keys, list.map_map, prod.fst_comp_to_sigma, list.nodup_map_iff_inj_on],
+  { rintros ⟨b, m⟩ hb ⟨c, n⟩ hc (rfl : b = c),
+    rw [mem_to_list, finsupp.mem_graph_iff] at hb hc,
+    dsimp at hb hc,
+    rw [←hc.1, hb.1] },
+  { apply nodup_to_list }
+end⟩
+
+@[simp] lemma to_alist_keys_to_finset (f : α →₀ M) : f.to_alist.keys.to_finset = f.support :=
+by { ext, simp [to_alist, alist.mem_keys, alist.keys, list.keys] }
+
+@[simp] lemma mem_to_alist {f : α →₀ M} {x : α} : x ∈ f.to_alist ↔ f x ≠ 0 :=
+by rw [alist.mem_keys, ←list.mem_to_finset, to_alist_keys_to_finset, mem_support_iff]
+
 end graph
 
+end finsupp
+
+/-! ### Declarations about `alist.lookup_finsupp` -/
+
+section lookup_finsupp
+
+variable [has_zero M]
+
+namespace alist
+open list
+
+/-- Converts an association list into a finitely supported function via `alist.lookup`, sending
+absent keys to zero. -/
+@[simps] def lookup_finsupp (l : alist (λ x : α, M)) : α →₀ M :=
+{ support := (l.1.filter $ λ x, sigma.snd x ≠ 0).keys.to_finset,
+  to_fun := λ a, (l.lookup a).get_or_else 0,
+  mem_support_to_fun := λ a, begin
+    simp_rw [mem_to_finset, list.mem_keys, list.mem_filter, ←mem_lookup_iff],
+    cases lookup a l;
+    simp
+  end }
+
+alias lookup_finsupp_to_fun ← lookup_finsupp_apply
+
+@[simp] lemma to_alist_lookup_finsupp (f : α →₀ M) : f.to_alist.lookup_finsupp = f :=
+begin
+  ext,
+  by_cases h : f a = 0,
+  { suffices : f.to_alist.lookup a = none,
+    { simp [h, this] },
+    { simp [lookup_eq_none, h] } },
+  { suffices : f.to_alist.lookup a = some (f a),
+    { simp [h, this] },
+    { apply mem_lookup_iff.2,
+      simpa using h } }
+end
+
+lemma lookup_finsupp_surjective : surjective (@lookup_finsupp α M _) :=
+λ f, ⟨_, to_alist_lookup_finsupp f⟩
+
+end alist
+
+end lookup_finsupp
+
+namespace finsupp
+
 /-!
 ### Declarations about `sum` and `prod`
 

src/data/list/alist.lean

@@ -122,6 +122,10 @@ theorem lookup_eq_none {a : α} {s : alist β} :
   lookup a s = none ↔ a ∉ s :=
 lookup_eq_none
 
+theorem mem_lookup_iff {a : α} {b : β a} {s : alist β} :
+  b ∈ lookup a s ↔ sigma.mk a b ∈ s.entries :=
+mem_lookup_iff s.nodupkeys
+
 theorem perm_lookup {a : α} {s₁ s₂ : alist β} (p : s₁.entries ~ s₂.entries) :
   s₁.lookup a = s₂.lookup a :=
 perm_lookup _ s₁.nodupkeys s₂.nodupkeys p

src/data/sigma/basic.lean

@@ -143,6 +143,7 @@ rfl
 /-- Convert a product type to a Σ-type. -/
 def prod.to_sigma {α β} (p : α × β) : Σ _ : α, β := ⟨p.1, p.2⟩
 
+@[simp] lemma prod.fst_comp_to_sigma {α β} : sigma.fst ∘ @prod.to_sigma α β = prod.fst := rfl
 @[simp] lemma prod.fst_to_sigma {α β} (x : α × β) : (prod.to_sigma x).fst = x.fst := rfl
 @[simp] lemma prod.snd_to_sigma {α β} (x : α × β) : (prod.to_sigma x).snd = x.snd := rfl
 @[simp] lemma prod.to_sigma_mk {α β} (x : α) (y : β) : (x, y).to_sigma = ⟨x, y⟩ := rfl