6. Discrete Mathematics

Discrete Mathematics is the study of finite sets, objects, and structures. We can count the elements of a finite set, and we can compute finite sums or products over its elements, we can compute maximums and minimums, and so on. We can also study objects that are generated by finitely many applications of certain generating functions, we can define functions by structural recursion, and prove theorems by structural induction. This chapters describes parts of Mathlib that support these activities.

6.1. Finsets and Fintypes

Dealing with finite sets and types in Mathlib can be confusing, because the library offers multiple ways of handling them. In this section we will discuss the most common ones.

We have already come across the type Finset in Section 5.2 and Section 5.3. As the name suggests, an element of type Finset α is a finite set of elements of type α. We will call these “finsets.” The Finset data type is designed to have a computational interpretation, and many basic operations on Finset α assume that α has decidable equality, which guarantees that there is an algorithm for testing whether a : α is an element of a finset s.

section
variable {α : Type*} [DecidableEq α] (a : α) (s t : Finset α)

#check a ∈ s
#check s ∩ t

end

If you remove the declaration [DecidableEq α], Lean will complain on the line #check s ∩ t because it cannot compute the intersection. All of the data types that you should expect to be able to compute with have decidable equality, however, and if you work classically by opening the Classical namespace and declaring noncomputable section, you can reason about finsets of elements of any type at all.

Finsets support most of the set-theoretic operations that sets do:

open Finset

variable (a b c : Finset ℕ)
variable (n : ℕ)

#check a ∩ b
#check a ∪ b
#check a \ b
#check (∅ : Finset ℕ)

example : a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) := by
  ext x; simp only [mem_inter, mem_union]; tauto

example : a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) := by rw [inter_union_distrib_left]

Note that we have opened the Finset namespace, where theorems specific to finsets are found. If you step through the last example below, you will see applying ext followed by simp reduces the identity to a problem in propositional logic. As an exercise, you can try proving some of set identities from Chapter 4, transported to finsets.

You have already seen the notation Finset.range n for the finite set of natural numbers \(\{ 0, 1, \ldots, n-1 \}\). Finset also allows you to define finite sets by enumerating the elements:

#check ({0, 2, 5} : Finset Nat)

def example1 : Finset ℕ := {0, 1, 2}

There are various ways to get Lean to recognize that order of elements and duplicates do not matter in a set presented in this way.

example : ({0, 1, 2} : Finset ℕ) = {1, 2, 0} := by decide

example : ({0, 1, 2} : Finset ℕ) = {0, 1, 1, 2} := by decide

example : ({0, 1} : Finset ℕ) = {1, 0} := by rw [Finset.pair_comm]

example (x : Nat) : ({x, x} : Finset ℕ) = {x} := by simp

example (x y z : Nat) : ({x, y, z, y, z, x} : Finset ℕ) = {x, y, z} := by
  ext i; simp [or_comm, or_assoc, or_left_comm]

example (x y z : Nat) : ({x, y, z, y, z, x} : Finset ℕ) = {x, y, z} := by
  ext i; simp; tauto

You can use insert to add a single element to a Finset, and Finset.erase to delete a single element. Note that erase is in the Finset namespace, but insert is in the root namespace.

example (s : Finset ℕ) (a : ℕ) (h : a ∉ s) : (insert a s |>.erase a) = s :=
  Finset.erase_insert h

example (s : Finset ℕ) (a : ℕ) (h : a ∈ s) : insert a (s.erase a) = s :=
  Finset.insert_erase h

In fact, {0, 1, 2} is just notation for insert 0 (insert 1 (singleton 2)).

set_option pp.notation false in
#check ({0, 1, 2} : Finset ℕ)

Given a finset s and a predicate P, we can use set-builder notation {x ∈ s | P x} to define the set of elements of s that satisfy P. This is notation for Finset.filter P s, which can also be written s.filter P.

example : {m ∈ range n | Even m} = (range n).filter Even := rfl
example : {m ∈ range n | Even m ∧ m ≠ 3} = (range n).filter (fun m ↦ Even m ∧ m ≠ 3) := rfl

example : {m ∈ range 10 | Even m} = {0, 2, 4, 6, 8} := by decide

Mathlib knows that the image of a finset under a function is a finset.

#check (range 5).image (fun x ↦ x * 2)

example : (range 5).image (fun x ↦ x * 2) = {x ∈ range 10 | Even x} := by decide

Lean also knows that the cartesian product s ×ˢ t of two finsets is a finset, and that the powerset of a finset is a finset. (Note that the notation s ×ˢ t also works for sets.)

#check s ×ˢ t
#check s.powerset

Defining operations on finsets in terms of their elements is tricky, because any such definition has to be independent of the order in which the elements are presented. Of course, you can always define functions by composing existing operations. Another thing you can do is use Finset.fold to fold a binary operation over the elements, provided that the operation is associative and commutative, since these properties guarantee that the result is independent of the order that the operation is applied. Finite sums, products, and unions are defined in that way. In the last example below, biUnion stands for “bounded indexed union.” With conventional mathematical notation, the expression would be written \(\bigcup_{i ∈ s} g(i)\).

#check Finset.fold

def f (n : ℕ) : Int := (↑n)^2

#check (range 5).fold (fun x y : Int ↦ x + y) 0 f
#eval (range 5).fold (fun x y : Int ↦ x + y) 0 f

#check ∑ i ∈ range 5, i^2
#check ∏ i ∈ range 5, i + 1

variable (g : Nat → Finset Int)

#check (range 5).biUnion g

There is a natural principle of induction on finsets: to prove that every finset has a property, show that the empty set has the property and that the property is preserved when we add one new element to a finset. (The @ symbol in @insert is needed in the induction step of the next example to give names to the parameters a and s because they have been marked implicit. )

#check Finset.induction

example {α : Type*} [DecidableEq α] (f : α → ℕ)  (s : Finset α) (h : ∀ x ∈ s, f x ≠ 0) :
    ∏ x ∈ s, f x ≠ 0 := by
  induction s using Finset.induction_on with
  | empty => simp
  | @insert a s anins ih =>
    rw [prod_insert anins]
    apply mul_ne_zero
    · apply h; apply mem_insert_self
    apply ih
    intros x xs
    exact h x (mem_insert_of_mem xs)

If s is a finset, Finset.Nonempty s is defined to be ∃ x, x ∈ s. You can use classical choice to pick an element of a nonempty finset. Similarly, the library defines Finset.toList s which uses choice to pick the elements of s in some order.

noncomputable example (s : Finset ℕ) (h : s.Nonempty) : ℕ := Classical.choose h

example (s : Finset ℕ) (h : s.Nonempty) : Classical.choose h ∈ s := Classical.choose_spec h

noncomputable example (s : Finset ℕ) : List ℕ := s.toList

example (s : Finset ℕ) (a : ℕ) : a ∈ s.toList ↔ a ∈ s := mem_toList

You can use Finset.min and Finset.max to choose the minimum or maximum element of a finset of elements of a linear order, and similarly you can use Finset.inf and Finset.sup with finsets of elements of a lattice, but there is a catch. What should the minimum element of an empty finset be? You can check that the primed versions of the functions below add a precondition that the finset is nonempty. The non-primed versions Finset.min and Finset.max add a top or bottom element, respectively, to the output type, to handle the case where the finset is empty. The non-primed versions Finset.inf and Finset.sup assume that the lattice comes equipped with a top or bottom element, respectively.

#check Finset.min
#check Finset.min'
#check Finset.max
#check Finset.max'
#check Finset.inf
#check Finset.inf'
#check Finset.sup
#check Finset.sup'

example : Finset.Nonempty {2, 6, 7} := ⟨6, by trivial⟩
example : Finset.min' {2, 6, 7} ⟨6, by trivial⟩ = 2 := by trivial

Every finset s has a finite cardinality, Finset.card s, which can be written #s when the Finset namespace is open.

#check Finset.card

#eval (range 5).card

example (s : Finset ℕ) : s.card = #s := by rfl

example (s : Finset ℕ) : s.card = ∑ i ∈ s, 1 := by rw [card_eq_sum_ones]

example (s : Finset ℕ) : s.card = ∑ i ∈ s, 1 := by simp

The next section is all about reasoning about cardinality.

When formalizing mathematics, one often has to make a decision as to whether to express one’s definitions and theorems in terms of sets or types. Using types often simplifies notation and proofs, but working with subsets of a type can be more flexible. The type-based analogue of a finset is a fintype, that is, a type Fintype α for some α. By definition, a fintype is just a data type that comes equipped with a finset univ that contains all its elements.

variable {α : Type*} [Fintype α]

example : ∀ x : α, x ∈ Finset.univ := by
  intro x; exact mem_univ x

Fintype.card α is equal to the cardinality of the corresponding finset.

example : Fintype.card α = (Finset.univ : Finset α).card := rfl

We have already seen a prototypical example of a fintype, namely, the types Fin n for each n. Lean recognizes that the fintypes are closed under operations like the product operation.

example : Fintype.card (Fin 5) = 5 := by simp
example : Fintype.card ((Fin 5) × (Fin 3)) = 15 := by simp

Any element s of Finset α can be coercied to a type (↑s : Finset α), namely, the subtype of elements of α that are contained in s.

variable (s : Finset ℕ)

example : (↑s : Type) = {x : ℕ // x ∈ s} := rfl
example : Fintype.card ↑s = s.card := by simp

Lean and Mathlib use type class inference to track the additional structure on fintypes, namely, the universal finset that contains all the elements. In other words, you can think of a fintype as an algebraic structure equipped with that extra data. Chapter 7 explains how this works.

6.2. Counting Arguments

The art of counting things is a central part of combinatorics. Mathlib contains several basic identities for counting elements of finsets:

open Finset

variable {α β : Type*} [DecidableEq α] [DecidableEq β] (s t : Finset α) (f : α → β)

example : #(s ×ˢ t) = #s * #t := by rw [card_product]
example : #(s ×ˢ t) = #s * #t := by simp

example : #(s ∪ t) = #s + #t - #(s ∩ t) := by rw [card_union]

example (h : Disjoint s t) : #(s ∪ t) = #s + #t := by rw [card_union_of_disjoint h]
example (h : Disjoint s t) : #(s ∪ t) = #s + #t := by simp [h]

example (h : Function.Injective f) : #(s.image f) = #s := by rw [card_image_of_injective _ h]

example (h : Set.InjOn f s) : #(s.image f) = #s := by rw [card_image_of_injOn h]

Opening the Finset namespace allows us to use the notation #s for s.card, as well as to use the shortened names card_union and so on.

Mathlib can also count elements of fintypes:

open Fintype

variable {α β : Type*} [Fintype α] [Fintype β]

example : card (α × β) = card α * card β := by simp

example : card (α ⊕ β) = card α + card β := by simp

example (n : ℕ) : card (Fin n → α) = (card α)^n := by simp

variable {n : ℕ} {γ : Fin n → Type*} [∀ i, Fintype (γ i)]

example : card ((i : Fin n) → γ i) = ∏ i, card (γ i) := by simp

example : card (Σ i, γ i) = ∑ i, card (γ i) := by simp

When the Fintype namespace is not open, we have to use Fintype.card instead of card.

The following is an example of calculating the cardinality of a finset, namely, the union of range n with a copy of range n that has been shifted by more than n. The calculation requires showing the the two sets in the union are disjoint; the first line of the proof yields the side condition Disjoint (range n) (image (fun i ↦ m + i) (range n)), which is established at the end of the proof. The Disjoint predicate is too general to be directly useful to us, but the theorem disjoint_iff_ne puts it in a form we can use.

#check Disjoint

example (m n : ℕ) (h : m ≥ n) :
    card (range n ∪ (range n).image (fun i ↦ m + i)) = 2 * n := by
  rw [card_union_of_disjoint, card_range, card_image_of_injective, card_range]; omega
  . apply add_right_injective
  . simp [disjoint_iff_ne]; omega

Throughout this section, omega will be a workhorse for us, for dealing with arithmetic calculations and inequalities.

Here is a more interesting example. Consider the subset of \(\{0, \ldots, n\} \times \{0, \ldots, n\}\) consisting of pairs \((i, j)\) such that \(i < j\). If you think of these as lattice points in the coordinate plane, they constitute an upper triangle of the square with corners \((0, 0)\) and \((n, n)\), not including the diagonal. The cardinality of the full square is \((n + 1)^2\), and removing the size of the diagonal and halving the result shows us that the cardinality of the triangle is \(n (n + 1) / 2\).

Alternatively, we note that the rows of the triangle have sizes \(0, 1, \ldots, n\), so the cardinality is the sum of the first \(n\) natural numbers. The first have of the proof below describes the triangle as the union of the rows, where row \(j\) consists of the numbers \(0, 1, ..., j - 1\) paired with \(j\). In the proof below, the notation (., j) abbreviates the function fun i ↦ (i, j). The rest of the proof is just a calculation with finset cardinalities.

def triangle (n : ℕ) : Finset (ℕ × ℕ) := {p ∈ range (n+1) ×ˢ range (n+1) | p.1 < p.2}

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  have : triangle n = (range (n+1)).biUnion (fun j ↦ (range j).image (., j)) := by
    ext p
    simp only [triangle, mem_filter, mem_product, mem_range, mem_biUnion, mem_image]
    constructor
    . rintro ⟨⟨hp1, hp2⟩, hp3⟩
      use p.2, hp2, p.1, hp3
    . rintro ⟨p1, hp1, p2, hp2, rfl⟩
      omega
  rw [this, card_biUnion]; swap
  · -- take care of disjointness first
    intro x _ y _ xney
    simp [disjoint_iff_ne, xney]
  -- continue the calculation
  transitivity (∑ i in range (n+1), i)
  · congr; ext i
    rw [card_image_of_injective, card_range]
    intros i1 i2; simp
  rw [sum_range_id]; rfl

The following variation on the proof does the calculation with fintypes instead of finsets. The type α ≃ β is the type of equivalences between α and β, consisting of a map in the forward direction, the map in the backward direction, and proofs that these two are inverse to one another. The first have in the proof shows that triangle n is equivalent to the disjoint union of Fin i as i ranges over Fin (n + 1). Interestingly, the forward function and the reverse function are constructed with tactics, rather than written explicitly. Since they do nothing more than move data and information around, rfl establishes that they are inverses.

After that, rw [←Fintype.card_coe] rewrites #(triangle n) as the cardinality of the subtype { x // x ∈ triangle n }, and the rest of the proof is a calculation.

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  have : triangle n ≃ Σ i : Fin (n + 1), Fin i.val :=
    { toFun := by
        rintro ⟨⟨i, j⟩, hp⟩
        simp [triangle] at hp
        exact ⟨⟨j, hp.1.2⟩, ⟨i, hp.2⟩⟩
      invFun := by
        rintro ⟨i, j⟩
        use ⟨j, i⟩
        simp [triangle]
        exact j.isLt.trans i.isLt
      left_inv := by intro i; rfl
      right_inv := by intro i; rfl }
  rw [←Fintype.card_coe]
  trans; apply (Fintype.card_congr this)
  rw [Fintype.card_sigma, sum_fin_eq_sum_range]
  convert Finset.sum_range_id (n + 1)
  simp_all

Here is yet another approach. The first line of the proof below reduces the problem to showing 2 * #(triangle n) = (n + 1) * n. We can do that by showing that two copies of the triangle exactly fill the rectangle range n ×ˢ range (n + 1). As an exercise, see if you can fill in the steps of the calculation. In the solutions, we rely on omega extensively in the second-to-last step, but we unfortunately have to do a fair amount of work by hand.

example (n : ℕ) : #(triangle n) = (n + 1) * n / 2 := by
  apply Nat.eq_div_of_mul_eq_right (by norm_num)
  let turn (p : ℕ × ℕ) : ℕ × ℕ := (n - 1 - p.1, n - p.2)
  calc 2 * #(triangle n)
      = #(triangle n) + #(triangle n) := by
          sorry
    _ = #(triangle n) + #(triangle n |>.image turn) := by
          sorry
    _ = #(range n ×ˢ range (n + 1)) := by
          sorry
    _ = (n + 1) * n := by
          sorry

You can convince yourself that we get the same triangle, shifted down, if we replace n by n + 1 and replace < by ≤ in the definition of triangle. The exercise below asks you to use this fact to show that the two triangles have the same size.

def triangle' (n : ℕ) : Finset (ℕ × ℕ) := {p ∈ range n ×ˢ range n | p.1 ≤ p.2}

example (n : ℕ) : #(triangle' n) = #(triangle n) := by sorry

Let us close this section with an example and an exercise from a tutorial on combinatorics given by Bhavik Mehta at Lean for the Curious Mathematician in 2023. Suppose we have a bipartite graph with vertex sets s and t, such that for every a in s, there are at least three edges leaving a, and for every b in t, there is at most one edge entering b. Then the total number of edges in the graph is at least three times the cardinality of s and at most the cardinality of t, from which is follows that three times the cardinality of s is at most the cardinality of t. The following theorem implements this argument, where we use the relation r to represent the edges of the graph. The proof is an elegant calculation.

open Classical
variable (s t : Finset Nat) (a b : Nat)

theorem doubleCounting {α β : Type*} (s : Finset α) (t : Finset β)
    (r : α → β → Prop)
    (h_left : ∀ a ∈ s, 3 ≤ #{b ∈ t | r a b})
    (h_right : ∀ b ∈ t, #{a ∈ s | r a b} ≤ 1) :
    3 * #(s) ≤ #(t) := by
  calc 3 * #(s)
      = ∑ a ∈ s, 3                               := by simp [sum_const_nat, mul_comm]
    _ ≤ ∑ a ∈ s, #({b ∈ t | r a b})              := sum_le_sum h_left
    _ = ∑ a ∈ s, ∑ b ∈ t, if r a b then 1 else 0 := by simp
    _ = ∑ b ∈ t, ∑ a ∈ s, if r a b then 1 else 0 := sum_comm
    _ = ∑ b ∈ t, #({a ∈ s | r a b})              := by simp
    _ ≤ ∑ b ∈ t, 1                               := sum_le_sum h_right
    _ ≤ #(t)                                     := by simp

The following exercise is also taken from Mehta’s tutorial. Suppose A is a subset of range (2 * n) with n + 1 elements. It’s easy to see that A must contain two consecutive integers, and hence two elements that are coprime. If you watch the tutorial, you will see that a good deal of effort was spent in establishing the following fact, which is now proved automatically by omega.

example (m k : ℕ) (h : m ≠ k) (h' : m / 2 = k / 2) : m = k + 1 ∨ k = m + 1 := by omega

The solution to Mehta’s exercise uses the pigeonhole principle, in the form exists_lt_card_fiber_of_mul_lt_card_of_maps_to, to show that there are two distinct elements m and k in A such that m / 2 = k / 2. See if you can complete the justification of that fact and then use it to finish the proof.

example {n : ℕ} (A : Finset ℕ)
    (hA : #(A) = n + 1)
    (hA' : A ⊆ range (2 * n)) :
    ∃ m ∈ A, ∃ k ∈ A, Nat.Coprime m k := by
  have : ∃ t ∈ range n, 1 < #({u ∈ A | u / 2 = t}) := by
    apply exists_lt_card_fiber_of_mul_lt_card_of_maps_to
    · sorry
    · sorry
  rcases this with ⟨t, ht, ht'⟩
  simp only [one_lt_card, mem_filter] at ht'
  sorry

6.3. Inductively Defined Types

Lean’s foundation allows us to define inductive types, that is, data types whose instances are generated from the bottom up. For example, the data type List α of lists of elements of α is generated by starting with the empty list, nil, and successively adding elements to the front the list. Below we will define a type of binary trees, BinTree, whose elements are generated by starting with the empty tree and building new trees by attaching a new node to two existing trees.

In Lean, one can define inductive types whose objects are infinite, like countably branching well-founded trees. Finite inductive definitions are commonly used in discrete mathematics, however, especially in those branches of discrete mathematics that are relevant to computer science. Lean provides not only the means to define such types, but also principles of induction and definition by recursion. For example, the data type List α is defined inductively:

namespace MyListSpace

inductive List (α : Type*) where
  | nil  : List α
  | cons : α → List α → List α

end MyListSpace

The inductive definition says that every element of List α is either nil, the empty list, or cons a as, where a is an element of α and as is a list of elements of α. The constructors are properly named List.nil and List.cons, but you can use the shorter notation with the List namespace is open. When the List namespace is not open, you can write .nil and .cons a as anywhere that Lean expects a list, and Lean will automatically insert the List qualifier. Throughout this section, we will put temporary definitions in separate namespaces like MyListSpace to avoid conflicts with the standard library. Outside the temporary namespace, we revert to using the standard library definitions.

Lean defines the notation [] for nil and :: for cons, and you can write [a, b, c] for a :: b :: c :: []. The append and map functions are defined recursively as follows:

def append {α : Type*} : List α → List α → List α
  | [],      bs => bs
  | a :: as, bs => a :: (append as bs)

def map {α β : Type*} (f : α → β) : List α → List β
  | []      => []
  | a :: as => f a :: map f as

#eval append [1, 2, 3] [4, 5, 6]
#eval map (fun n => n^2) [1, 2, 3, 4, 5]

Notice that there is a base case and a recursive case. In each case, the two defining clauses hold definitionally:

theorem nil_append {α : Type*} (as : List α) : append [] as = as := rfl

theorem cons_append {α : Type*} (a : α) (as : List α) (bs : List α) :
    append (a :: as) bs = a :: (append as bs) := rfl

theorem map_nil {α β : Type*} (f : α → β) : map f [] = [] := rfl

theorem map_cons {α β : Type*} (f : α → β) (a : α) (as : List α) :
    map f (a :: as) = f a :: map f as := rfl

The functions append and map are defined in the standard library, and append as bs can be written as as ++ bs.

Lean allows you to write proofs by induction following the structure of the definition.

variable {α β γ : Type*}
variable (as bs cs : List α)
variable (a b c : α)

open List

theorem append_nil : ∀ as : List α, as ++ [] = as
  | [] => rfl
  | a :: as => by rw [cons_append, append_nil as]

theorem map_map (f : α → β) (g : β → γ) :
    ∀ as : List α, map g (map f as) = map (g ∘ f) as
  | [] => rfl
  | a :: as => by rw [map_cons, map_cons, map_cons, map_map f g as]; rfl

You can also use the induction' tactic.

Of course, these theorems are already in the standard library. As an exercise, try defining a function reverse in the MyListSpace3 namespace (to avoid conflicting with the standard List.reverse) that reverses a list. You can use #eval reverse [1, 2, 3, 4, 5] to test it out. The most straightforward definition of reverse requires quadratic time, but don’t worry about that. You can jump to the definition of List.reverse in the standard library to see a linear-time implementation. Try proving reverse (as ++ bs) = reverse bs ++ reverse as and reverse (reverse as) = as. You can use cons_append and append_assoc, but you You may need to come up with auxiliary lemmas and prove them.

def reverse : List α → List α := sorry

theorem reverse_append (as bs : List α) : reverse (as ++ bs) = reverse bs ++ reverse as := by
  sorry

theorem reverse_reverse (as : List α) : reverse (reverse as) = as := by sorry

For another example, consider the following inductive definition of binary trees together with functions to compute the size and depth of a binary tree.

inductive BinTree where
  | empty : BinTree
  | node  : BinTree → BinTree → BinTree

namespace BinTree

def size : BinTree → ℕ
  | empty    => 0
  | node l r => size l + size r + 1

def depth : BinTree → ℕ
  | empty    => 0
  | node l r => max (depth l) (depth r) + 1

It is convenient to count the empty binary tree as a binary tree of size 0 and depth 0. In the literature, this data type is sometimes called the extended binary trees. Including the empty tree means, for example, that we can define the tree node empty (node empty empty) consisting of a root node, and empty left subtree, and a right subtree consisting of a single node.

Here is an important inequality relating the size and the depth:

theorem size_le : ∀ t : BinTree, size t ≤ 2^depth t - 1
  | empty    => Nat.zero_le _
  | node l r => by
    simp only [depth, size]
    calc l.size + r.size + 1
      ≤ (2^l.depth - 1) + (2^r.depth - 1) + 1 := by
          gcongr <;> apply size_le
    _ ≤ (2 ^ max l.depth r.depth - 1) + (2 ^ max l.depth r.depth - 1) + 1 := by
          gcongr <;> simp
    _ ≤ 2 ^ (max l.depth r.depth + 1) - 1 := by
          have : 0 < 2 ^ max l.depth r.depth := by simp
          omega

Try proving the following inequality, which is somewhat easier. Remember, if you do a proof by induction as in the previous theorem, you have to delete the := by.

theorem depth_le_size : ∀ t : BinTree, depth t ≤ size t := by sorry

Also define the flip operation on binary trees, which recursively swaps the left and right subtrees.

def flip : BinTree → BinTree := sorry

If you did it right, the proof of the following should be rfl.

example: flip  (node (node empty (node empty empty)) (node empty empty)) =
    node (node empty empty) (node (node empty empty) empty) := sorry

Prove the following:

theorem size_flip : ∀ t, size (flip t) = size t := by sorry

We close this section with some formal logic. The following is an inductive definition of propositional formulas.

inductive PropForm : Type where
  | var (n : ℕ)           : PropForm
  | fls                   : PropForm
  | conj (A B : PropForm) : PropForm
  | disj (A B : PropForm) : PropForm
  | impl (A B : PropForm) : PropForm

Every propositional formula is either a variable var n, the constant false fls, or a compound formula of the form conj A B, disj A B, or impl A B. With ordinary mathematical notation, these are commonly written \(p_n\), \(\bot\), \(A \wedge B\), \(A \vee B\), and \(A \to B\), respectively. The other propositional connectives can be defined in terms of these; for example, we can define \(\neg A\) as \(A \to \bot\) and \(A \leftrightarrow B\) as \((A \to B) \wedge (B \to A)\).

Having defined the data type of propositional formulas, we define what it means to evaluate a propositional formula with respect to an assignment v of Boolean truth values to the variables.

def eval : PropForm → (ℕ → Bool) → Bool
  | var n,    v => v n
  | fls,      _ => false
  | conj A B, v => A.eval v && B.eval v
  | disj A B, v => A.eval v || B.eval v
  | impl A B, v => ! A.eval v || B.eval v

The next definition specifies the set of variables occurring in a formula, and the subsequent theorem shows that evaluating a formula on two truth assignments that agree on its variables yields that same value.

def vars : PropForm → Finset ℕ
  | var n    => {n}
  | fls      => ∅
  | conj A B => A.vars ∪ B.vars
  | disj A B => A.vars ∪ B.vars
  | impl A B => A.vars ∪ B.vars

theorem eval_eq_eval : ∀ (A : PropForm) (v1 v2 : ℕ → Bool),
    (∀ n ∈ A.vars, v1 n = v2 n) → A.eval v1 = A.eval v2
  | var n, v1, v2, h    => by simp_all [vars, eval, h]
  | fls, v1, v2, h      => by simp_all [eval]
  | conj A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]
  | disj A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]
  | impl A B, v1, v2, h => by
      simp_all [vars, eval, eval_eq_eval A v1 v2, eval_eq_eval B v1 v2]

Noticing the repetition, we can be clever about the use of automation.

theorem eval_eq_eval' (A : PropForm) (v1 v2 : ℕ → Bool) (h : ∀ n ∈ A.vars, v1 n = v2 n) :
    A.eval v1 = A.eval v2 := by
  cases A <;> simp_all [eval, vars, fun A => eval_eq_eval' A v1 v2]

The function subst A m C describes the result of substituting the formula C for every occurrence of the variable var m in the formula A.

def subst : PropForm → ℕ → PropForm → PropForm
  | var n,    m, C => if n = m then C else var n
  | fls,      _, _ => fls
  | conj A B, m, C => conj (A.subst m C) (B.subst m C)
  | disj A B, m, C => disj (A.subst m C) (B.subst m C)
  | impl A B, m, C => impl (A.subst m C) (B.subst m C)

As an example, show that substituting for a variable that does not occur in a formula has no effect:

theorem subst_eq_of_not_mem_vars :
    ∀ (A : PropForm) (n : ℕ) (C : PropForm), n ∉ A.vars → A.subst n C = A := sorry

The following theorem says something more subtle and interesting: evaluating A.subst n C on a truth assignment v is the same as evaluating A on a truth assignment that assigns the value of C to var n. See if you can prove it.

theorem subst_eval_eq : ∀ (A : PropForm) (n : ℕ) (C : PropForm) (v : ℕ → Bool),
  (A.subst n C).eval v = A.eval (fun m => if m = n then C.eval v else v m) := sorry