mathlib docs: set_theory.lists

source

@[instance]

def lists'.decidable_eq (α : Type u) [a : decidable_eq α] (a_1 : bool) :

decidable_eq (lists' α a_1)

source

inductive lists' :

Type u → bool → Type u

atom : Π (α : Type u), α → lists' α bool.ff
nil : Π (α : Type u), lists' α bool.tt
cons' : Π (α : Type u) {b : bool}, lists' α b → lists' α bool.tt → lists' α bool.tt

source

def lists :

Type u_1 → Type u_1

Equations

lists α = Σ (b : bool), lists' α b

source

@[instance]

def lists'.inhabited {α : Type u_1} [inhabited α] (b : bool) :

inhabited (lists' α b)

Equations

lists'.inhabited bool.tt = {default := lists'.nil α}
lists'.inhabited bool.ff = {default := lists'.atom (inhabited.default α)}

source

def lists'.cons {α : Type u_1} :

lists α → lists' α bool.tt → lists' α bool.tt

Equations

lists'.cons ⟨b, a⟩ l = a.cons' l

source

@[simp]

def lists'.to_list {α : Type u_1} {b : bool} :

lists' α b → list (lists α)

Equations

(a.cons' l).to_list = ⟨a_6, a⟩ :: l.to_list
lists'.nil.to_list = list.nil
(lists'.atom a).to_list = list.nil

source

@[simp]

theorem lists'.to_list_cons {α : Type u_1} (a : lists α) (l : lists' α bool.tt) :

(lists'.cons a l).to_list = a :: l.to_list

source

@[simp]

def lists'.of_list {α : Type u_1} :

list (lists α) → lists' α bool.tt

Equations

lists'.of_list (a :: l) = lists'.cons a (lists'.of_list l)
lists'.of_list list.nil = lists'.nil

source

@[simp]

theorem lists'.to_of_list {α : Type u_1} (l : list (lists α)) :

(lists'.of_list l).to_list = l

source

@[simp]

theorem lists'.of_to_list {α : Type u_1} (l : lists' α bool.tt) :

lists'.of_list l.to_list = l

source

@[instance]

def lists'.has_subset {α : Type u_1} :

has_subset (lists' α bool.tt)

Equations

lists'.has_subset = {subset := lists'.subset α}

source

@[instance]

def lists'.has_mem {α : Type u_1} {b : bool} :

has_mem (lists α) (lists' α b)

Equations

lists'.has_mem = {mem := λ (a : lists α) (l : lists' α b), ∃ (a' : lists α) (H : a' ∈ l.to_list), a.equiv a'}

source

theorem lists'.mem_def {α : Type u_1} {b : bool} {a : lists α} {l : lists' α b} :

a ∈ l ↔ ∃ (a' : lists α) (H : a' ∈ l.to_list), a.equiv a'

source

@[simp]

theorem lists'.mem_cons {α : Type u_1} {a y : lists α} {l : lists' α bool.tt} :

a ∈ lists'.cons y l ↔ a.equiv y ∨ a ∈ l

source

theorem lists'.cons_subset {α : Type u_1} {a : lists α} {l₁ l₂ : lists' α bool.tt} :

lists'.cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

source

theorem lists'.of_list_subset {α : Type u_1} {l₁ l₂ : list (lists α)} :

l₁ ⊆ l₂ → lists'.of_list l₁ ⊆ lists'.of_list l₂

source

theorem lists'.subset_nil {α : Type u_1} {l : lists' α bool.tt} :

l ⊆ lists'.nil → l = lists'.nil

source

theorem lists'.mem_of_subset' {α : Type u_1} {a : lists α} {l₁ l₂ : lists' α bool.tt} :

l₁ ⊆ l₂ → a ∈ l₁.to_list → a ∈ l₂

source

theorem lists'.subset_def {α : Type u_1} {l₁ l₂ : lists' α bool.tt} :

l₁ ⊆ l₂ ↔ ∀ (a : lists α), a ∈ l₁.to_list → a ∈ l₂

source

def lists.atom {α : Type u_1} :

α → lists α

Equations

lists.atom a = ⟨bool.ff, lists'.atom a⟩

source

def lists.of' {α : Type u_1} :

lists' α bool.tt → lists α

Equations

lists.of' l = ⟨bool.tt, l⟩

source

@[simp]

def lists.to_list {α : Type u_1} :

lists α → list (lists α)

Equations

lists.to_list ⟨b, l⟩ = l.to_list

source

def lists.is_list {α : Type u_1} :

lists α → Prop

Equations

l.is_list = ↥(l.fst)

source

def lists.of_list {α : Type u_1} :

list (lists α) → lists α

Equations

lists.of_list l = lists.of' (lists'.of_list l)

source

theorem lists.is_list_to_list {α : Type u_1} (l : list (lists α)) :

(lists.of_list l).is_list

source

theorem lists.to_of_list {α : Type u_1} (l : list (lists α)) :

(lists.of_list l).to_list = l

source

theorem lists.of_to_list {α : Type u_1} {l : lists α} :

l.is_list → lists.of_list l.to_list = l

source

@[instance]

def lists.inhabited {α : Type u_1} :

inhabited (lists α)

Equations

lists.inhabited = {default := lists.of' lists'.nil}

source

@[instance]

def lists.decidable_eq {α : Type u_1} [decidable_eq α] :

decidable_eq (lists α)

Equations

lists.decidable_eq = lists.decidable_eq._proof_1.mpr (λ (a b : Σ (b : bool), lists' α b), sigma.decidable_eq a b)

source

@[instance]

def lists.has_sizeof {α : Type u_1} [has_sizeof α] :

has_sizeof (lists α)

Equations

lists.has_sizeof = lists.has_sizeof._proof_1.mpr (sigma.has_sizeof bool (λ (b : bool), lists' α b))

source

def lists.induction_mut {α : Type u_1} (C : lists α → Sort u_2) (D : lists' α bool.tt → Sort u_3) :

(Π (a : α), C (lists.atom a)) → (Π (l : lists' α bool.tt), D l → C (lists.of' l)) → D lists'.nil → (Π (a : lists α) (l : lists' α bool.tt), C a → D l → D (lists'.cons a l)) → pprod (Π (l : lists α), C l) (Π (l : lists' α bool.tt), D l)

Equations

lists.induction_mut C D C0 C1 D0 D1 = ⟨λ (_x : lists α), lists.induction_mut._match_2 C D (λ (b : bool) (l : lists' α b), lists'.rec (λ (a : α), ⟨C0 a, punit.star⟩) ⟨C1 lists'.nil D0, D0⟩ (λ {b : bool} (a : lists' α b) (l : lists' α bool.tt) (IH₁ : pprod (C ⟨b, a⟩) (lists.induction_mut._match_1 D b a)) (IH₂ : pprod (C ⟨bool.tt, l⟩) (lists.induction_mut._match_1 D bool.tt l)), ⟨C1 (a.cons' l) (D1 ⟨b, a⟩ l IH₁.fst IH₂.snd), D1 ⟨b, a⟩ l IH₁.fst IH₂.snd⟩) l) _x, λ (l : lists' α bool.tt), ((λ (b : bool) (l : lists' α b), lists'.rec (λ (a : α), ⟨C0 a, punit.star⟩) ⟨C1 lists'.nil D0, D0⟩ (λ {b : bool} (a : lists' α b) (l : lists' α bool.tt) (IH₁ : pprod (C ⟨b, a⟩) (lists.induction_mut._match_1 D b a)) (IH₂ : pprod (C ⟨bool.tt, l⟩) (lists.induction_mut._match_1 D bool.tt l)), ⟨C1 (a.cons' l) (D1 ⟨b, a⟩ l IH₁.fst IH₂.snd), D1 ⟨b, a⟩ l IH₁.fst IH₂.snd⟩) l) bool.tt l).snd⟩
lists.induction_mut._match_2 C D this ⟨b, l⟩ = (this l).fst
lists.induction_mut._match_1 D bool.tt l = D l
lists.induction_mut._match_1 D bool.ff l = punit