feat(data/W/cardinal): results about cardinality of W-types (#9210)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

archive/examples/prop_encodable.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 
-import data.W
+import data.W.basic
 
 /-!
 # W types

src/data/W.lean → src/data/W/basic.lean

@@ -37,7 +37,73 @@ instance : inhabited (W_type (λ (_ : unit), empty)) :=
 
 namespace W_type
 
-variables {α : Type*} {β : α → Type*} [Π a : α, fintype (β a)]
+variables {α : Type*} {β : α → Type*}
+
+/-- The canonical map to the corresponding sigma type, returning the label of a node as an
+  element `a` of `α`, and the children of the node as a function `β a → W_type β`. -/
+def to_sigma : W_type β → Σ a : α, β a → W_type β
+| ⟨a, f⟩ := ⟨a, f⟩
+
+/-- The canonical map from the sigma type into a `W_type`. Given a node `a : α`, and
+  its children as a function `β a → W_type β`, return the corresponding tree. -/
+def of_sigma : (Σ a : α, β a → W_type β) → W_type β
+| ⟨a, f⟩ := W_type.mk a f
+
+@[simp] lemma of_sigma_to_sigma : Π (w : W_type β),
+  of_sigma (to_sigma w) = w
+| ⟨a, f⟩ := rfl
+
+@[simp] lemma to_sigma_of_sigma : Π (s : Σ a : α, β a → W_type β),
+  to_sigma (of_sigma s) = s
+| ⟨a, f⟩ := rfl
+
+variable (β)
+
+/-- The canonical bijection with the sigma type, showing that `W_type` is a fixed point of
+  the polynomial `Σ a : α, β a → W_type β`.  -/
+@[simps] def equiv_sigma : W_type β ≃ Σ a : α, β a → W_type β :=
+{ to_fun := to_sigma,
+  inv_fun := of_sigma,
+  left_inv := of_sigma_to_sigma,
+  right_inv := to_sigma_of_sigma }
+
+variable {β}
+
+/-- The canonical map from `W_type β` into any type `γ` given a map `(Σ a : α, β a → γ) → γ`. -/
+def elim (γ : Type*) (fγ : (Σ a : α, β a → γ) → γ) : W_type β → γ
+| ⟨a, f⟩ := fγ ⟨a, λ b, elim (f b)⟩
+
+lemma elim_injective (γ : Type*) (fγ : (Σ a : α, β a → γ) → γ)
+  (fγ_injective : function.injective fγ) :
+  function.injective (elim γ fγ)
+| ⟨a₁, f₁⟩ ⟨a₂, f₂⟩ h := begin
+  obtain ⟨rfl, h⟩ := sigma.mk.inj (fγ_injective h),
+  congr' with x,
+  exact elim_injective (congr_fun (eq_of_heq h) x : _),
+end
+
+instance [hα : is_empty α] : is_empty (W_type β) :=
+⟨λ w, W_type.rec_on w (is_empty.elim hα)⟩
+
+lemma infinite_of_nonempty_of_is_empty (a b : α) [ha : nonempty (β a)]
+  [he : is_empty (β b)] : infinite (W_type β) :=
+⟨begin
+  introsI hf,
+  have hba : b ≠ a, from λ h, ha.elim (is_empty.elim' (show is_empty (β a), from h ▸ he)),
+  refine not_injective_infinite_fintype
+    (λ n : ℕ, show W_type β, from nat.rec_on n
+      ⟨b, is_empty.elim' he⟩
+      (λ n ih, ⟨a, λ _, ih⟩)) _,
+  intros n m h,
+  induction n with n ih generalizing m h,
+  { cases m with m; simp * at * },
+  { cases m with m,
+    { simp * at * },
+    { refine congr_arg nat.succ (ih _),
+      simp [function.funext_iff, *] at * } }
+end⟩
+
+variables [Π a : α, fintype (β a)]
 
 /-- The depth of a finitely branching tree. -/
 def depth : W_type β → ℕ

src/data/W/cardinal.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2021 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import set_theory.cardinal_ordinal
+import data.W.basic
+/-!
+# Cardinality of W-types
+
+This file proves some theorems about the cardinality of W-types. The main result is
+`cardinal_mk_le_max_omega_of_fintype` which says that if for any `a : α`,
+`β a` is finite, then the cardinality of `W_type β` is at most the maximum of the
+cardinality of `α` and `cardinal.omega`.
+This can be used to prove theorems about the cardinality of algebraic constructions such as
+polynomials. There is a surjection from a `W_type` to `mv_polynomial` for example, and
+this surjection can be used to put an upper bound on the cardinality of `mv_polynomial`.
+
+## Tags
+
+W, W type, cardinal, first order
+-/
+universe u
+
+variables {α : Type u} {β : α → Type u}
+
+noncomputable theory
+
+namespace W_type
+
+open_locale cardinal
+
+open cardinal
+
+lemma cardinal_mk_eq_sum : #(W_type β) = sum (λ a : α, #(W_type β) ^ #(β a)) :=
+begin
+  simp only [cardinal.lift_mk, cardinal.power_def, cardinal.sum_mk],
+  exact cardinal.eq.2 ⟨equiv_sigma β⟩
+end
+
+/-- `#(W_type β)` is the least cardinal `κ` such that `sum (λ a : α, κ ^ #(β a)) ≤ κ` -/
+lemma cardinal_mk_le_of_le {κ : cardinal.{u}} (hκ : sum (λ a : α, κ ^ #(β a)) ≤ κ) :
+  #(W_type β) ≤ κ :=
+begin
+  conv_rhs { rw ← cardinal.mk_out κ},
+  rw [← cardinal.mk_out κ] at hκ,
+  simp only [cardinal.power_def, cardinal.sum_mk, cardinal.le_def] at hκ,
+  cases hκ,
+  exact cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)
+end
+
+/-- If, for any `a : α`, `β a` is finite, then the cardinality of `W_type β`
+  is at most the maximum of the cardinality of `α` and `ω`  -/
+lemma cardinal_mk_le_max_omega_of_fintype [Π a, fintype (β a)] : #(W_type β) ≤ max (#α) ω :=
+(is_empty_or_nonempty α).elim
+  (begin
+    introI h,
+    rw [@cardinal.eq_zero_of_is_empty (W_type β)],
+    exact zero_le _
+  end) $
+λ hn,
+let m := max (#α) ω in
+cardinal_mk_le_of_le $
+calc cardinal.sum (λ a : α, m ^ #(β a))
+    ≤ #α * cardinal.sup.{u u}
+      (λ a : α, m ^ cardinal.mk (β a)) :
+  cardinal.sum_le_sup _
+... ≤ m * cardinal.sup.{u u}
+      (λ a : α, m ^ #(β a)) :
+  mul_le_mul' (le_max_left _ _) (le_refl _)
+... = m : mul_eq_left.{u} (le_max_right _ _)
+  (cardinal.sup_le.2 (λ i, begin
+    cases lt_omega.1 (lt_omega_iff_fintype.2 ⟨show fintype (β i), by apply_instance⟩) with n hn,
+    rw [hn],
+    exact power_nat_le (le_max_right _ _)
+  end))
+  (pos_iff_ne_zero.1 (succ_le.1
+    begin
+      rw [succ_zero],
+      obtain ⟨a⟩ : nonempty α, from hn,
+      refine le_trans _ (le_sup _ a),
+      rw [← @power_zero m],
+      exact power_le_power_left (pos_iff_ne_zero.1
+        (lt_of_lt_of_le omega_pos (le_max_right _ _))) (zero_le _)
+    end))
+
+end W_type

src/data/pfunctor/univariate/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
-import data.W
+import data.W.basic
 
 /-!
 # Polynomial functors