From ac4290739d4ee9cb340f0fea20ad6a8992b6d6d1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 25 Mar 2017 00:56:20 +0100
Subject: [PATCH] refactor(init/data/list/instances): simplify proofs

---
 library/init/data/list/instances.lean | 30 +++++++++++++--------------
 1 file changed, 14 insertions(+), 16 deletions(-)

diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
index 2e5ecdb5ea..4d14cdb482 100644
--- a/library/init/data/list/instances.lean
+++ b/library/init/data/list/instances.lean
@@ -10,38 +10,36 @@ open list
 
 universes u v
 
+local attribute [simp] map join ret list.append
+
 section
 variables {α : Type u} {β : Type v} (x : α) (xs ys : list α) (f : α → list β)
 
 private lemma cons_bind : list.bind (x :: xs) f = f x ++ list.bind xs f :=
-by dsimp [list.bind, join]; apply rfl
+by simp [list.bind]
 
 private lemma append_bind : list.bind (xs ++ ys) f = list.bind xs f ++ list.bind ys f :=
 begin
-  induction xs with x xs ih,
-  { apply rfl },
-  { simp [cons_bind, ih] },
+  induction xs,
+  { refl },
+  { simph [cons_bind] }
 end
 end
 
+local attribute [simp] cons_bind append_bind
+
 instance : monad list :=
 {pure := @list.ret, bind := @list.bind,
  id_map := begin
    intros _ xs, induction xs with x xs ih,
-   { apply rfl },
-   { dsimp [list.bind, map, join, ret, append, list.append],
-     dsimp [list.bind, map, join, ret] at ih,
-     rw ih }
- end,
- pure_bind := begin
-   intros,
-   dsimp [list.bind, ret, map, join],
-   apply append_nil
+   { refl },
+   { dsimp at ih, dsimp, simph }
  end,
+ pure_bind := by intros; dsimp; apply append_nil,
  bind_assoc := begin
-   intros _ _ _ xs _ _, induction xs with x xs ih,
-   { apply rfl },
-   { simp [cons_bind, append_bind, ih] },
+   intros _ _ _ xs _ _, induction xs,
+   { refl },
+   { simph }
  end}
 
 instance : alternative list :=