LeanPool.QuasiBorelSpaces.RoseTree.Basic

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.RoseTree.Basic.

@[simp]

theorem Rose.eta {A : Type u_1} (t : Rose A) : { label := t.label, children := t.children } = t

@[simp]

theorem Rose.label_bind {A : Type u_1} {B : Type u_2} (f : A → Rose B) (t : Rose A) : (bind f t).label = (f t.label).label

@[simp]

theorem Rose.children_bind {A : Type u_1} {B : Type u_2} (f : A → Rose B) (t : Rose A) : (bind f t).children = (f t.label).children ++ List.map (bind f) t.children

@[simp]

theorem Rose.label_map {A : Type u_1} {B : Type u_2} (f : A → B) (t : Rose A) : (map f t).label = f t.label

@[simp]

theorem Rose.children_map {A : Type u_1} {B : Type u_2} (f : A → B) (t : Rose A) : (map f t).children = List.map (map f) t.children

theorem Rose.induction {A : Type u_1} (motive : Rose A → Prop) (mk : ∀ (label : A) (children : List (Rose A)), (∀ t ∈ children, motive t) → motive { label := label, children := children }) (t : Rose A) : motive t

theorem Rose.induction' {A : Type u_1} (motive : Rose A → Prop) (mk : ∀ (label : A) (children : List (Rose A)), (∀ (i : Fin children.length), motive children[i]) → motive { label := label, children := children }) (t : Rose A) : motive t

theorem Rose.bind_pure {A : Type u_1} (t : Rose A) : bind (fun (x : A) => { label := x, children := [] }) t = t

@[simp]

theorem Rose.bind_pure_fun {A : Type u_1} : (bind fun (x : A) => { label := x, children := [] }) = id

@[simp]

theorem Rose.bind_bind {A : Type u_1} {B : Type u_2} {C : Type u_3} (f : B → Rose C) (g : A → Rose B) (t : Rose A) : bind f (bind g t) = bind (fun (x : A) => bind f (g x)) t

@[simp]

theorem Rose.bind_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} (f : B → Rose C) (g : A → Rose B) : bind f ∘ bind g = bind (bind f ∘ g)

@[simp]

theorem Rose.bind_comp_r {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} (f : B → Rose C) (g : A → Rose B) (h : D → Rose A) : bind f ∘ bind g ∘ h = bind (bind f ∘ g) ∘ h

@[simp]

theorem Rose.fold_eq_bind {A : Type u_1} {B : Type u_2} (f : A → Rose B) : (fold fun (x : A) (xs : List (Rose B)) => { label := (f x).label, children := (f x).children ++ xs }) = bind f

@[simp]

theorem Rose.map_mk {A : Type u_1} {B : Type u_2} (f : A → B) (x : A) (xs : List (Rose A)) : map f { label := x, children := xs } = { label := f x, children := List.map (map f) xs }

@[simp]

theorem Rose.map_id {A : Type u_1} {f : A → A} (hf : ∀ (x : A), f x = x) (t : Rose A) : map f t = t

@[simp]

theorem Rose.map_map {A : Type u_1} {B : Type u_2} {C : Type u_3} (f : B → C) (g : A → B) (t : Rose A) : map f (map g t) = map (fun (x : A) => f (g x)) t

@[simp]

theorem Rose.map_bind {A : Type u_1} {B : Type u_2} {C : Type u_3} (f : B → C) (g : A → Rose B) (t : Rose A) : map f (bind g t) = bind (fun (x : A) => map f (g x)) t

@[simp]

theorem Rose.bind_map {A : Type u_1} {B : Type u_2} {C : Type u_3} (f : B → Rose C) (g : A → B) (t : Rose A) : bind f (map g t) = bind (fun (x : A) => f (g x)) t

@[simp]

theorem Rose.bind_eq_map {A : Type u_1} {B : Type u_2} (f : A → B) (t : Rose A) : bind (fun (x : A) => { label := f x, children := [] }) t = map f t

@[simp]

theorem Rose.fold_map {A : Type u_1} {B : Type u_2} {C : Type u_3} (f : B → List C → C) (g : A → B) (t : Rose A) : fold f (map g t) = fold (fun (x : A) => f (g x)) t

@[simp]

theorem Rose.bind_eq {A B : Type u_1} (t : Rose A) (f : A → Rose B) : t >>= f = bind f t

@[simp]

theorem Rose.pure_eq {A : Type u_1} (x : A) : pure x = { label := x, children := [] }

@[simp]

theorem Rose.seq_eq {A B : Type u_1} (f : Rose (A → B)) (t : Rose A) : f <*> t = bind (fun (f : A → B) => map f t) f

@[simp]

theorem Rose.map_eq {A B : Type u_1} (f : A → B) (t : Rose A) : f <$> t = map f t

@[simp]

theorem Rose.seqLeft_eq {A B : Type u_1} (t : Rose A) (u : Rose B) : t <* u = bind (fun (x : A) => map (fun (x_1 : B) => x) u) t

@[simp]

theorem Rose.seqRight_eq {A B : Type u_1} (t : Rose A) (u : Rose B) : t *> u = bind (fun (x : A) => u) t

instance Rose.instLawfulMonad : LawfulMonad Rose

@[simp]

theorem Rose.decode_encode {A : Type u_1} [Encodable A] (t : Rose A) : decode t.encode = some t

@[implicit_reducible]

instance Rose.instEncodable {A : Type u_1} [Encodable A] : Encodable (Rose A)

Equations

• Rose.instEncodable = { encode := Rose.encode, decode := Rose.decode, encodek := ⋯ }

instance Rose.instCountable {A : Type u_1} [Countable A] : Countable (Rose A)

@[simp]

theorem Rose.le_mk {A : Type u_1} [LE A] (x y : A) (xs ys : List (Rose A)) : { label := x, children := xs } ≤ { label := y, children := ys } ↔ x ≤ y ∧ List.Forall₂ (fun (x1 x2 : Rose A) => x1 ≤ x2) xs ys

@[implicit_reducible]

instance Rose.instPreorder {A : Type u_1} [Preorder A] : Preorder (Rose A)

Equations

• Rose.instPreorder = { toLE := Rose.instLE, lt := fun (a b : Rose A) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[implicit_reducible]

instance Rose.instPartialOrder {A : Type u_1} [PartialOrder A] : PartialOrder (Rose A)

Equations

• Rose.instPartialOrder = { toPreorder := Rose.instPreorder, le_antisymm := ⋯ }