[Merged by Bors] - feat(combinatorics/catalan): Connection between Catalan numbers and number of trees

src/algebra/big_operators/basic.lean

@@ -451,6 +451,34 @@ begin
   {intros b hb, use j b hb, use hj b hb, exact (right_inv b hb).symm,},
 end
 
+/--
+  Reorder a product, but only provide an injection and the fact that there are not more terms
+  in the new product.
+-/
+@[to_additive "
+  Reorder a sum, but only provide an injection and the fact that there are not more terms
+  in the new sum.
+"]
+lemma prod_bij_of_inj_of_card_le {s : finset α} {t : finset γ} {f : α → β} {g : γ → β}
+  (i : Π a ∈ s, γ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
+  (i_inj : ∀ a₁ a₂ ha₁ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (card_le : t.card ≤ s.card) :
+  (∏ x in s, f x) = (∏ x in t, g x) :=
+prod_bij i hi h i_inj (surj_on_of_inj_on_of_card_le i hi i_inj card_le)
+
+/--
+  Reorder a product, but only provide a surjection and the fact that there are not fewer terms
+  in the new product.
+-/
+@[to_additive "
+  Reorder a sum, but only provide a surjection and the fact that there are not fewer terms
+  in the new sum.
+"]
+lemma prod_bij_of_surj_of_card_le {s : finset α} {t : finset γ} {f : α → β} {g : γ → β}
+  (i : Π a ∈ s, γ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
+  (i_surj : ∀ b ∈ t, ∃ a ha, b = i a ha) (card_le : s.card ≤ t.card) :
+  (∏ x in s, f x) = (∏ x in t, g x) :=
+prod_bij i hi h (inj_on_of_surj_on_of_card_le i hi i_surj card_le) i_surj
+
 @[to_additive] lemma prod_finset_product
   (r : finset (γ × α)) (s : finset γ) (t : γ → finset α)
   (h : ∀ p : γ × α, p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} :

src/combinatorics/catalan.lean

@@ -7,6 +7,7 @@ import data.nat.choose.central
 import algebra.big_operators.fin
 import tactic.field_simp
 import tactic.linear_combination
+import data.tree
 
 /-!
 # Catalan numbers
@@ -39,7 +40,7 @@ https://math.stackexchange.com/questions/3304415/catalan-numbers-algebraic-proof
 -/
 
 open_locale big_operators
-open finset
+open finset finset.nat.antidiagonal (fst_le snd_le)
 
 /-- The recursive definition of the sequence of Catalan numbers:
 `catalan (n + 1) = ∑ i : fin n.succ, catalan i * catalan (n - i)` -/
@@ -53,6 +54,15 @@ def catalan : ℕ → ℕ
 lemma catalan_succ (n : ℕ) : catalan (n + 1) = ∑ i : fin n.succ, catalan i * catalan (n - i) :=
 by rw catalan
 
+lemma catalan_succ' (n : ℕ) :
+  catalan (n + 1) = ∑ ij in nat.antidiagonal n, catalan ij.1 * catalan ij.2 :=
+begin
+  rw [catalan_succ, ← sum_range (λ i, catalan i * catalan (n - i))], symmetry,
+  exact sum_bij_of_inj_of_card_le (λ (ij : ℕ × ℕ) _, ij.1)
+    (λ _ h, by simpa [nat.lt_succ_iff] using fst_le h) (by tidy)
+    (λ _ _ h₁ h₂, (nat.antidiagonal_congr h₁ h₂).mpr) (by simp),
+end
+
 @[simp] lemma catalan_one : catalan 1 = 1 := by simp [catalan_succ]
 
 /-- A helper sequence that can be used to prove the equality of the recursive and the explicit
@@ -128,3 +138,46 @@ by norm_num [catalan_eq_central_binom_div, nat.central_binom, nat.choose]
 
 lemma catalan_three : catalan 3 = 5 :=
 by norm_num [catalan_eq_central_binom_div, nat.central_binom, nat.choose]
+
+namespace unit_tree
+
+/-- Given two finsets, find all trees that can be formed with
+  left child in `a` and right child in `b` -/
+@[simp] def pairwise_node (a : finset unit_tree) (b : finset unit_tree) : finset unit_tree :=
+  (a ×ˢ b).map ⟨λ x, x.1.node x.2, λ ⟨x₁, x₂⟩ ⟨y₁, y₂⟩, by { simp, tauto, }⟩
+
+/-- A finset of all trees with `n` nodes. See `mem_trees_of_nodes_eq` -/
+def trees_of_nodes_eq : ℕ → finset unit_tree
+| 0 := {nil}
+| (n+1) := (finset.nat.antidiagonal n).attach.bUnion $ λ ijh,
+  have _ := nat.lt_succ_iff.mpr (fst_le ijh.2),
+  have _ := nat.lt_succ_iff.mpr (snd_le ijh.2),
+  pairwise_node (trees_of_nodes_eq ijh.1.1) (trees_of_nodes_eq ijh.1.2)
+
+@[simp] lemma trees_of_nodes_eq_zero : trees_of_nodes_eq 0 = {nil} := by rw [trees_of_nodes_eq]
+
+lemma trees_of_nodes_eq_succ (n : ℕ) : trees_of_nodes_eq (n + 1) =
+  (nat.antidiagonal n).bUnion (λ ij, pairwise_node (trees_of_nodes_eq ij.1)
+    (trees_of_nodes_eq ij.2)) :=
+by { rw trees_of_nodes_eq, ext, simp [-pairwise_node], }
+
+@[simp] theorem mem_trees_of_nodes_eq {x : unit_tree} {n : ℕ} :
+  x ∈ trees_of_nodes_eq n ↔ x.nodes = n :=
+begin
+  induction x generalizing n;
+  cases n;
+  simp [trees_of_nodes_eq_succ, nat.succ_eq_add_one, *],
+  trivial,
+end
+
+lemma trees_of_nodes_eq_card_eq_catalan (n : ℕ) :
+  (trees_of_nodes_eq n).card = catalan n :=
+begin
+  induction n using nat.case_strong_induction_on with n ih,
+  { simp, },
+  rw [trees_of_nodes_eq_succ, card_bUnion, catalan_succ'],
+  { apply sum_congr rfl, rintro ⟨i, j⟩ H, simp [ih _ (fst_le H), ih _ (snd_le H)], },
+  { rintros ⟨i, j⟩ H ⟨i', j'⟩ H' hne a ha, clear_except ha hne, tidy, },
+end
+
+end unit_tree

src/data/list/basic.lean

@@ -3094,6 +3094,25 @@ lemma reduce_option_nth_iff {l : list (option α)} {x : α} :
   (∃ i, l.nth i = some (some x)) ↔ ∃ i, l.reduce_option.nth i = some x :=
 by rw [←mem_iff_nth, ←mem_iff_nth, reduce_option_mem_iff]
 
+/-! ### all_some -/
+
+section all_some
+
+@[simp] lemma all_some_nil {α : Type*} : (@list.nil $ option α).all_some = some [] := rfl
+
+@[simp] lemma all_some_cons_none {α} (x : list (option α)) :
+  (none :: x).all_some = none := rfl
+
+@[simp] lemma all_some_cons_some {α} (x : list (option α)) (y) :
+  (some y :: x).all_some = x.all_some.map (list.cons y) := rfl
+
+@[simp] theorem all_some_of_map_some {α} (x : list α) :
+  (x.map some).all_some = some x :=
+by induction x; simp [*]
+
+end all_some
+
+
 /-! ### filter -/
 
 section filter

src/data/tree.lean

@@ -82,3 +82,76 @@ def map {β} (f : α → β) : tree α → tree β
 | (node a l r) := node (f a) (map l) (map r)
 
 end tree
+
+/-- A unit tree is a binary tree with no data (only units) attached -/
+@[derive [has_reflect, decidable_eq]]
+inductive unit_tree
+| nil : unit_tree
+| node : unit_tree → unit_tree → unit_tree
+
+namespace unit_tree
+
+instance : inhabited unit_tree := ⟨nil⟩
+
+/-- A unit tree is the same thing as `tree unit` -/
+@[simp] def to_tree : unit_tree → tree punit
+| nil := tree.nil
+| (node a b) := tree.node punit.star a.to_tree b.to_tree
+
+/-- A unit tree is the same thing as `tree unit` -/
+@[simp] def of_tree : tree punit → unit_tree
+| tree.nil := nil
+| (tree.node () a b) := node (of_tree a) (of_tree b)
+
+@[simp] lemma to_tree_of_tree : ∀ (x : tree unit), (of_tree x).to_tree = x
+| tree.nil := rfl
+| (tree.node () a b) := by rw [of_tree, to_tree, to_tree_of_tree a, to_tree_of_tree b]
+
+@[simp] lemma of_tree_to_tree (x : unit_tree) : of_tree x.to_tree = x :=
+by induction x; simp [*]
+
+/-- A non-nil ptree; useful when we want an arbitrary value other than `nil` -/
+abbreviation non_nil : unit_tree := node nil nil
+
+@[simp] lemma non_nil_ne : non_nil ≠ nil := by trivial
+
+/-- The number of internal nodes (i.e. not including leaves) of a binary tree -/
+@[simp] def nodes : unit_tree → ℕ
+| nil := 0
+| (node a b) := a.nodes + b.nodes + 1
+
+/-- The number of leaves of a binary tree -/
+@[simp] def leaves : unit_tree → ℕ
+| nil := 1
+| (node a b) := a.leaves + b.leaves
+
+/-- The height - length of the longest path from the root - of a binary tree -/
+@[simp] def height : unit_tree → ℕ
+| nil := 0
+| (node a b) := max a.height b.height + 1
+
+lemma leaves_eq_internal_nodes_succ (x : unit_tree) :
+  x.leaves = x.nodes + 1 :=
+by { induction x; simp [*, nat.add_comm, nat.add_assoc, nat.add_right_comm], }
+
+lemma leaves_pos (x : unit_tree) : 0 < x.leaves :=
+by { induction x, { exact nat.zero_lt_one, }, apply nat.lt_add_left, assumption, }
+
+lemma height_le_nodes : ∀ (x : unit_tree), x.height ≤ x.nodes
+| nil := le_refl _
+| (node a b) := nat.succ_le_succ
+    (max_le
+      (trans a.height_le_nodes $ nat.le_add_right _ _)
+      (trans b.height_le_nodes $ nat.le_add_left _ _))
+
+/-- The left child of the tree, or `nil` if the tree is `nil` -/
+@[simp] def left : unit_tree → unit_tree
+| nil := nil
+| (node l r) := l
+
+/-- The right child of the tree, or `nil` if the tree is `nil` -/
+@[simp] def right : unit_tree → unit_tree
+| nil := nil
+| (node l r) := r
+
+end unit_tree