Random cleanup and grinding

Changes

2 changed files (+18/-20)

• Monad.lean
  • @@ -26,21 +26,19 @@ class LawfulMonad2 (m : Type → Type)
    ((ma >>= f) >>= g) = (ma >>= (fun a => f a >>= g)) + @[grind] def Set.pure {α : Type} : α → Set α - | a => {a} + | a => {a} + + @[grind] def Set.bind {α β : Type} : Set α → (α → Set β) → Set β - | A, f => {b | ∃a, a ∈ A ∧ b ∈ f a} - instance Set.LawfulMonad : LawfulMonad2 Set := - { pure := Set.pure + | A, f => {b | ∃a, a ∈ A ∧ b ∈ f a} + + instance Set.LawfulMonad : LawfulMonad2 Set where + pure := Set.pure bind := Set.bind - pure_bind := by - intro α β a f - simp [Pure.pure, Bind.bind, Set.pure, Set.bind] - bind_pure := by - intro α ma - simp [Pure.pure, Bind.bind, Set.pure, Set.bind] + pure_bind := by grind + bind_pure := by grind bind_assoc := by - intro α β γ f g ma - simp [Pure.pure, Bind.bind, Set.pure, Set.bind] - apply Set.ext - aesop } + simp only [bind, mem_setOf_eq] + grind
• Tree.lean
  • @@ -2,20 +2,20 @@
    -- namespace blah inductive Tree - | leaf - | branch (children : List Tree) + | leaf + | branch (children : List Tree) def f x := (x - 1) ^ 2 #check id def size : Tree -> Nat - | .leaf => 1 - | .branch children => children.map size |>.sum + | .leaf => 1 + | .branch children => children.map size |>.sum def g (x : Tree) := match x with - | .leaf => 1 - | .branch children => + | .leaf => 1 + | .branch children => -- have : (children.map g |>.map f) = children.map (f ∘ g) := List.map_map -- simp only [List.map_map] children.map g |>.map f |>.sum