Lumenary.Collections

Formal library

• basketdefDefinitionNo axioms

  /-- A basket of fruit, written as a list. Lists keep their members in order. -/
  def basket : List String := ["mango", "orange", "banana"]

  Axioms used: No axiomsformal/Lumenary/Collections.leanTry it in the Lean web editor

• mango_in_baskettheoremProved here from basic factsNo axioms

  /-- There is a mango in the basket: it is the very first thing in the list. -/
  theorem mango_in_basket : "mango" ∈ basket :=
    List.Mem.head ["orange", "banana"]

  Axioms used: No axiomsformal/Lumenary/Collections.leanTry it in the Lean web editor

• basket_counttheoremProved here from basic factsNo axioms

  /-- The basket holds three pieces of fruit. Lean counts them itself, so `rfl` is enough. -/
  theorem basket_count : basket.length = 3 := rfl

  Axioms used: No axiomsformal/Lumenary/Collections.leanTry it in the Lean web editor

• order_matters_for_liststheoremProved here from basic factsNo axioms

  /-- For lists, order matters: `[1, 2]` and `[2, 1]` are different lists.
  `decide` asks Lean to compare the two lists element by element. -/
  theorem order_matters_for_lists : ([1, 2] : List Nat) ≠ [2, 1] := by decide

  Axioms used: No axiomsformal/Lumenary/Collections.leanTry it in the Lean web editor

• same_memberstheoremProved here from basic factspropext

  /-- …but `[1, 2]` and `[2, 1]` have exactly the same members. As *sets* they would be equal;
  as *lists* they are not (see `order_matters_for_lists`). -/
  theorem same_members : ∀ x : Nat, x ∈ [1, 2] ↔ x ∈ [2, 1] := by
    intro x
    -- Being in a list means being equal to one of its entries:
    -- `x ∈ [1, 2]` unfolds to `x = 1 ∨ x = 2`, and `x ∈ [2, 1]` to `x = 2 ∨ x = 1`.
    simp only [List.mem_cons, List.not_mem_nil, or_false]
    -- "or" does not care about order.
    exact Or.comm

  Axioms used: propextformal/Lumenary/Collections.leanTry it in the Lean web editor

• nothing_in_emptytheoremProved here from basic factsNo axioms

  /-- The empty list has no members at all. -/
  theorem nothing_in_empty : ∀ x : String, x ∉ ([] : List String) := by
    intro x h
    -- A proof of `x ∈ []` would have to come from one of the ways of building membership,
    -- but none of them produces an empty list, so there is no case left to consider.
    cases h

  Axioms used: No axiomsformal/Lumenary/Collections.leanTry it in the Lean web editor