From dfd84666e2f8802b6c811de387dd8b3dd056d794 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 22 Mar 2017 16:33:56 +0100
Subject: [PATCH] feat(library): add functor, applicative, and monad laws, and
 prove them correct for non-meta instances

---
 library/init/category/applicative.lean        | 35 +++++++--
 library/init/category/functor.lean            |  5 ++
 library/init/category/monad.lean              | 59 +++++++++++++--
 library/init/category/state.lean              | 37 +++++++++-
 library/init/classical.lean                   | 16 -----
 library/init/data/list/instances.lean         | 37 +++++++++-
 library/init/data/option/instances.lean       | 46 ++----------
 library/init/data/option_t.lean               | 71 +++++++++++++++++++
 library/init/data/set.lean                    | 16 ++++-
 library/init/meta/converter.lean              |  4 +-
 library/init/meta/exceptional.lean            |  4 +-
 library/init/meta/interaction_monad.lean      |  4 +-
 library/init/meta/interactive.lean            |  8 +--
 library/init/meta/tactic.lean                 |  7 +-
 library/init/meta/transfer.lean               |  1 +
 library/init/meta/vm.lean                     |  6 +-
 library/init/native/result.lean               | 32 ++++++++-
 library/init/propext.lean                     | 16 +++++
 tests/lean/run/isabelle.lean                  |  3 +-
 .../type_error_at_eval_expr.lean.expected.out |  2 +-
 20 files changed, 318 insertions(+), 91 deletions(-)
 create mode 100644 library/init/data/option_t.lean

diff --git a/library/init/category/applicative.lean b/library/init/category/applicative.lean
index 95143d6982..a4d264fa30 100644
--- a/library/init/category/applicative.lean
+++ b/library/init/category/applicative.lean
@@ -14,11 +14,31 @@ set_option auto_param.check_exists false
 class applicative (f : Type u → Type v) extends functor f :=
 (pure : Π {α : Type u}, α → f α)
 (seq  : Π {α β : Type u}, f (α → β) → f α → f β)
-(map := λ _ _ x y, seq (pure x) y)
+(infixr ` <$> `:100 := map)
+(infixl ` <*> `:60 := seq)
+(map := λ _ _ x y, pure x <*> y)
+-- ` <* `
 (seq_left : Π {α β : Type u}, f α → f β → f α := λ α β a b, seq (map (const β) a) b)
-(seq_right : Π {α β : Type u}, f α → f β → f β := λ α β a b, seq (map (const α id) a) b)
 (seq_left_eq : ∀ {α β : Type u} (a : f α) (b : f β), seq_left a b = seq (map (const β) a) b . control_laws_tac)
+-- ` *> `
+(seq_right : Π {α β : Type u}, f α → f β → f β := λ α β a b, seq (map (const α id) a) b)
 (seq_right_eq : ∀ {α β : Type u} (a : f α) (b : f β), seq_right a b = seq (map (const α id) a) b . control_laws_tac)
+-- applicative laws
+(pure_seq_eq_map : ∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x) -- . control_laws_tac)
+(map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x))
+(seq_pure : ∀ {α β : Type u} (g : f (α → β)) (x : α),
+  g <*> pure x = (λ g : α → β, g x) <$> g)
+(seq_assoc : ∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)),
+  h <*> (g <*> x) = (@comp α β γ <$> h) <*> g <*> x)
+-- defaulted functor law
+(map_comp := λ α β γ g h x, calc
+  (h ∘ g) <$> x = pure (h ∘ g) <*> x                        : eq.symm $ pure_seq_eq_map _ _
+            ... = (comp h <$> pure g) <*> x                 : eq.rec rfl $ map_pure (comp h) g
+            ... = pure (@comp α β γ h) <*> pure g <*> x     : eq.rec rfl $ eq.symm $ pure_seq_eq_map (comp h) (pure g)
+            ... = (@comp α β γ <$> pure h) <*> pure g <*> x : eq.rec rfl $ map_pure (@comp α β γ) h
+            ... = pure h <*> (pure g <*> x)                 : eq.symm $ seq_assoc _ _ _
+            ... = h <$> (pure g <*> x)                      : pure_seq_eq_map _ _
+            ... = h <$> g <$> x                             : congr_arg _ $ pure_seq_eq_map _ _)
 end
 
 section
@@ -38,7 +58,12 @@ applicative.seq_left
 @[inline] def seq_right : f α → f β → f β :=
 applicative.seq_right
 
-infixl ` <*> `:2 := seq_app
-infixl ` <* `:2  := seq_left
-infixl ` *> `:2  := seq_right
+infixl ` <*> `:60 := seq_app
+infixl ` <* `:60  := seq_left
+infixl ` *> `:60  := seq_right
+
 end
+
+-- applicative "law" derivable from other laws
+theorem applicative.pure_id_seq {α β : Type u} {f : Type u → Type v} [applicative f] (x : f α) : pure id <*> x = x :=
+eq.trans (applicative.pure_seq_eq_map _ _) (functor.id_map _)
diff --git a/library/init/category/functor.lean b/library/init/category/functor.lean
index 241037b6e5..2a7e2a75a5 100644
--- a/library/init/category/functor.lean
+++ b/library/init/category/functor.lean
@@ -13,8 +13,13 @@ set_option auto_param.check_exists false
 
 class functor (f : Type u → Type v) : Type (max u+1 v) :=
 (map : Π {α β : Type u}, (α → β) → f α → f β)
+(infixr ` <$> `:100 := map)
+-- ` <$ `
 (map_const : Π {α : Type u} (β : Type u), α → f β → f α := λ α β, map ∘ const β)
 (map_const_eq : ∀ {α β : Type u}, @map_const α β = map ∘ const β . control_laws_tac)
+-- `functor` is indeed a categorical functor
+(id_map : Π {α : Type u} (x : f α), id <$> x = x)
+(map_comp : Π {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x)
 end
 
 @[inline] def fmap {f : Type u → Type v} [functor f] {α β : Type u} : (α → β) → f α → f β :=
diff --git a/library/init/category/monad.lean b/library/init/category/monad.lean
index f81eae6b05..3065e1df17 100644
--- a/library/init/category/monad.lean
+++ b/library/init/category/monad.lean
@@ -7,6 +7,8 @@ prelude
 import init.category.applicative
 universes u v
 
+open function
+
 class has_bind (m : Type u → Type v) :=
 (bind : Π {α β : Type u}, m α → (α → m β) → m β)
 
@@ -16,16 +18,63 @@ has_bind.bind
 @[inline] def has_bind.and_then {α β : Type u} {m : Type u → Type v} [has_bind m] (x : m α) (y : m β) : m β :=
 do x, y
 
-infixl ` >>= `:2 := bind
-infixl ` >> `:2  := has_bind.and_then
+infixl ` >>= `:55 := bind
+infixl ` >> `:55  := has_bind.and_then
+
+section
+set_option auto_param.check_exists false
 
 class monad (m : Type u → Type v) extends applicative m, has_bind m : Type (max u+1 v) :=
-(map := λ α β f x, bind x $ λ x, pure (f x))
-(seq := λ α β f x, bind f $ λ f, map f x)
+(infixr ` <$> `:100 := map)
+(infixl ` <*> `:60 := seq)
+(infixl ` >>= `:55 := bind)
+(map := λ α β f x, x >>= pure ∘ f)
+(seq := λ α β f x, f >>= (<$> x))
+(bind_pure_comp_eq_map : ∀ {α β : Type u} (f : α → β) (x : m α), x >>= pure ∘ f = f <$> x  . control_laws_tac)
+(bind_map_eq_seq : ∀ {α β : Type u} (f : m (α → β)) (x : m α), f >>= (<$> x) = f <*> x  . control_laws_tac)
+-- monad laws
+(pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x)
+(bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ),
+  x >>= f >>= g = x >>= λ x, f x >>= g)
+-- all applicative laws are derivable from the monad laws + id_map
+(pure_seq_eq_map := λ α β g x, eq.trans (eq.symm $ bind_map_eq_seq _ _) (pure_bind _ _))
+(map_pure := λ α β g x, eq.trans (eq.symm $ bind_pure_comp_eq_map _ _) (pure_bind _ _))
+(seq_pure := λ α β g x, calc
+  g <*> pure x = g >>= (<$> pure x)            : eq.symm $ bind_map_eq_seq _ _
+           ... = g >>= λ g : α → β, pure (g x) : congr_arg _ $ funext $ λ g, map_pure _ _
+           ... = (λ g : α → β, g x) <$> g      : bind_pure_comp_eq_map _ _)
+(seq_assoc := λ α β γ x g h, calc
+  h <*> (g <*> x)
+      = h >>= (<$> g <*> x) : eq.symm $ bind_map_eq_seq _ _
+  ... = h >>= λ h, pure (@comp α β γ h) >>= (<$> g) >>= (<$> x) : congr_arg _ $ funext $ λ h, (calc
+    h <$> (g <*> x)
+        = g <*> x >>= pure ∘ h : eq.symm $ bind_pure_comp_eq_map _ _
+    ... = g >>= (<$> x) >>= pure ∘ h                    : eq.rec rfl $ eq.symm $ bind_map_eq_seq g x
+    ... = g >>= λ g, g <$> x >>= pure ∘ h               : bind_assoc _ _ _
+    ... = g >>= λ g, pure (h ∘ g) >>= (<$> x)        : congr_arg _ $ funext $ λ g, (calc
+      g <$> x >>= pure ∘ h
+          = x >>= pure ∘ g >>= pure ∘ h        : eq.rec rfl $ eq.symm $ bind_pure_comp_eq_map g x
+      ... = x >>= λ x, pure (g x) >>= pure ∘ h : bind_assoc _ _ _
+      ... = x >>= λ x, pure (h (g x)) : congr_arg _ $ funext $ λ x, pure_bind _ _
+      ... = (h ∘ g) <$> x : bind_pure_comp_eq_map _ _
+      ... = pure (h ∘ g) >>= (<$> x) : eq.symm $ pure_bind _ _)
+    ... = g >>= pure ∘ (@comp α β γ h) >>= (<$> x) : eq.symm $ bind_assoc _ _ _
+    ... = @comp α β γ h <$> g >>= (<$> x) : eq.rec rfl $ bind_pure_comp_eq_map (comp h) g
+    ... = pure (@comp α β γ h) >>= (<$> g) >>= (<$> x) : eq.rec rfl $ eq.symm $ pure_bind (@comp α β γ h) (<$> g))
+  ... = h >>= (λ h, pure (@comp α β γ h) >>= (<$> g)) >>= (<$> x) : eq.symm $ bind_assoc _ _ _
+  ... = h >>= pure ∘ @comp α β γ >>= (<$> g) >>= (<$> x) : eq.rec rfl $ eq.symm $ bind_assoc h (pure ∘ @comp α β γ) (<$> g)
+  ... = (@comp α β γ <$> h) >>= (<$> g) >>= (<$> x) : eq.rec rfl $ bind_pure_comp_eq_map (@comp α β γ) h
+  ... = ((@comp α β γ <$> h) >>= (<$> g)) <*> x : bind_map_eq_seq _ _
+  ... = (@comp α β γ <$> h) <*> g <*> x : eq.rec rfl $ bind_map_eq_seq (@comp α β γ <$> h) g)
+end
 
-def return {m : Type u → Type v} [monad m] {α : Type u} : α → m α :=
+@[reducible] def return {m : Type u → Type v} [monad m] {α : Type u} : α → m α :=
 pure
 
 /- Identical to has_bind.and_then, but it is not inlined. -/
 def has_bind.seq {α β : Type u} {m : Type u → Type v} [has_bind m] (x : m α) (y : m β) : m β :=
 do x, y
+
+-- monad "law" derivable from other laws
+theorem monad.bind_pure {α β : Type u} {m : Type u → Type v} [monad m] (x : m α) : x >>= pure = x :=
+eq.trans (monad.bind_pure_comp_eq_map _ _ _) (functor.id_map _)
diff --git a/library/init/category/state.lean b/library/init/category/state.lean
index 00ae7f8e05..ed3f243b64 100644
--- a/library/init/category/state.lean
+++ b/library/init/category/state.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.tactic
+import init.meta.interactive
 universes u v
 
 def state (σ α : Type u) : Type u :=
@@ -20,7 +20,18 @@ variables {σ α β : Type u}
 λ s, match (a s) with (a', s') := b a' s' end
 
 instance (σ : Type u) : monad (state σ) :=
-{pure := @state_return σ, bind := @state_bind σ}
+{pure := @state_return σ, bind := @state_bind σ,
+ id_map := begin
+   intros, apply funext, intro s,
+   dsimp [state_bind], cases x s,
+   apply rfl
+ end,
+ pure_bind := by intros; apply rfl,
+ bind_assoc := begin
+   intros, apply funext, intro s,
+   dsimp [state_bind], cases x s,
+   apply rfl
+ end}
 end
 
 namespace state
@@ -54,7 +65,27 @@ section
 end
 
 instance (σ : Type u) (m : Type u → Type v) [monad m] : monad (state_t σ m) :=
-{pure := @state_t_return σ m _, bind := @state_t_bind σ m _}
+{pure := @state_t_return σ m _, bind := @state_t_bind σ m _,
+ id_map := begin
+   intros, apply funext, intro,
+   dsimp [state_t_bind, state_t_return],
+   assert h : state_t_bind._match_1 (λ (x : α) (s : σ), @return m _ _ (x, s)) = pure,
+   { apply funext, intro s, cases s, apply rfl },
+   { rw h, apply @monad.bind_pure _ σ },
+ end,
+ pure_bind := begin
+   intros, apply funext, intro,
+   dsimp [state_t_bind, state_t_return],
+   dsimp [return, pure, bind], -- TODO: fix signature of `pure_bind`
+   rw [monad.pure_bind], apply rfl
+ end,
+ bind_assoc := begin
+   intros, apply funext, intro s,
+   dsimp [state_t_bind, state_t_return, bind],
+   rw [monad.bind_assoc],
+   apply congr_arg, apply funext, intro r,
+   cases r, apply rfl
+ end}
 
 section
   variable  {σ : Type u}
diff --git a/library/init/classical.lean b/library/init/classical.lean
index 9e5dc34dce..4c7781f711 100644
--- a/library/init/classical.lean
+++ b/library/init/classical.lean
@@ -175,22 +175,6 @@ cases_true_false (λ x, x = false ∨ x = true)
   (or.inr rfl)
   (or.inl rfl)
   a
-
-theorem iff.to_eq {a b : Prop} (h : a ↔ b) : a = b :=
-iff.elim (assume h1 h2, propext (iff.intro h1 h2)) h
-
-theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
-propext (iff.intro
-  (assume h, iff.to_eq h)
-  (assume h, h^.to_iff))
-
-lemma eq_false {a : Prop} : (a = false) = (¬ a) :=
-have (a ↔ false) = (¬ a), from propext (iff_false a),
-eq.subst (@iff_eq_eq a false) this
-
-lemma eq_true {a : Prop} : (a = true) = a :=
-have (a ↔ true) = a, from propext (iff_true a),
-eq.subst (@iff_eq_eq a true) this
 end aux
 
 end classical
diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
index c1320f2070..2e5ecdb5ea 100644
--- a/library/init/data/list/instances.lean
+++ b/library/init/data/list/instances.lean
@@ -4,14 +4,49 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
+import init.data.list.lemmas
 import init.meta.mk_dec_eq_instance
 open list
 
 universes u v
 
+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
+
+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] },
+end
+end
+
+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
+ end,
+ bind_assoc := begin
+   intros _ _ _ xs _ _, induction xs with x xs ih,
+   { apply rfl },
+   { simp [cons_bind, append_bind, ih] },
+ end}
+
 instance : alternative list :=
 { list.monad with
-  failure := @nil,
+  failure := @list.nil,
   orelse  := @list.append }
 
 instance {α : Type u} [decidable_eq α] : decidable_eq (list α) :=
diff --git a/library/init/data/option/instances.lean b/library/init/data/option/instances.lean
index c19a3817c3..5cee35bbbd 100644
--- a/library/init/data/option/instances.lean
+++ b/library/init/data/option/instances.lean
@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import .basic
+import init.meta.tactic
+
 
 universes u v
 
@@ -13,7 +15,10 @@ universes u v
 | (some a) b := b a
 
 instance : monad option :=
-{pure := @some, bind := @option_bind}
+{pure := @some, bind := @option_bind,
+ id_map := λ α x, option.rec rfl (λ x, rfl) x,
+ pure_bind := λ α β x f, rfl,
+ bind_assoc := λ α β γ x f g, option.rec rfl (λ x, rfl) x}
 
 def option_orelse {α : Type u} : option α → option α → option α
 | (some a) o         := some a
@@ -24,42 +29,3 @@ instance : alternative option :=
 { option.monad with
   failure := @none,
   orelse  := @option_orelse }
-
-def option_t (m : Type u → Type v) [monad m] (α : Type u) : Type v :=
-m (option α)
-
-@[inline] def option_t_bind {m : Type u → Type v} [monad m] {α β : Type u} (a : option_t m α) (b : α → option_t m β)
-                               : option_t m β :=
-show m (option β), from
-do o ← a,
-   match o with
-   | none     := return none
-   | (some a) := b a
-   end
-
-@[inline] def option_t_return {m : Type u → Type v} [monad m] {α : Type u} (a : α) : option_t m α :=
-show m (option α), from
-return (some a)
-
-instance {m : Type u → Type v} [monad m] : monad (option_t m) :=
-{pure := @option_t_return m _, bind := @option_t_bind m _}
-
-def option_t_orelse {m : Type u → Type v} [monad m] {α : Type u} (a : option_t m α) (b : option_t m α) : option_t m α :=
-show m (option α), from
-do o ← a,
-   match o with
-   | none     := b
-   | (some v) := return (some v)
-   end
-
-def option_t_fail {m : Type u → Type v} [monad m] {α : Type u} : option_t m α :=
-show m (option α), from
-return none
-
-instance {m : Type u → Type v} [monad m] : alternative (option_t m) :=
-{ option_t.monad with
-  failure := @option_t_fail m _,
-  orelse  := @option_t_orelse m _ }
-
-def option_t.lift {m : Type u → Type v} [monad m] {α : Type u} (a : m α) : option_t m α :=
-(some <$> a : m (option α))
diff --git a/library/init/data/option_t.lean b/library/init/data/option_t.lean
new file mode 100644
index 0000000000..890520fba3
--- /dev/null
+++ b/library/init/data/option_t.lean
@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.interactive
+
+universes u v
+
+def option_t (m : Type u → Type v) [monad m] (α : Type u) : Type v :=
+m (option α)
+
+@[inline] def option_t_bind {m : Type u → Type v} [monad m] {α β : Type u} (a : option_t m α) (b : α → option_t m β)
+                               : option_t m β :=
+show m (option β), from
+do o ← a,
+   match o with
+   | none     := return none
+   | (some a) := b a
+   end
+
+@[inline] def option_t_return {m : Type u → Type v} [monad m] {α : Type u} (a : α) : option_t m α :=
+show m (option α), from
+return (some a)
+
+instance {m : Type u → Type v} [monad m] : monad (option_t m) :=
+{pure := @option_t_return m _, bind := @option_t_bind m _,
+ id_map := begin
+   intros,
+   dsimp [option_t_bind],
+   assert h : option_t_bind._match_1 option_t_return = @pure m _ (option α),
+   { apply funext, intro s, cases s, apply rfl, apply rfl },
+   { rw h, apply @monad.bind_pure _ (option α) m },
+ end,
+ pure_bind := begin
+   intros,
+   dsimp [option_t_bind, option_t_return],
+   dsimp [return, pure, bind], -- TODO: fix signature of `pure_bind`
+   rw [monad.pure_bind], apply rfl
+ end,
+ bind_assoc := begin
+   intros,
+   dsimp [option_t_bind, option_t_return, bind],
+   rw [monad.bind_assoc],
+   apply congr_arg, apply funext, intro x,
+   cases x,
+   { dsimp [option_t_bind._match_1, return, pure],
+     rw [monad.pure_bind], apply rfl },
+   { apply rfl }
+ end}
+
+def option_t_orelse {m : Type u → Type v} [monad m] {α : Type u} (a : option_t m α) (b : option_t m α) : option_t m α :=
+show m (option α), from
+do o ← a,
+   match o with
+   | none     := b
+   | (some v) := return (some v)
+   end
+
+def option_t_fail {m : Type u → Type v} [monad m] {α : Type u} : option_t m α :=
+show m (option α), from
+return none
+
+instance {m : Type u → Type v} [monad m] : alternative (option_t m) :=
+{ @option_t.monad m _ with
+  failure := @option_t_fail m _,
+  orelse  := @option_t_orelse m _ }
+
+def option_t.lift {m : Type u → Type v} [monad m] {α : Type u} (a : m α) : option_t m α :=
+(some <$> a : m (option α))
diff --git a/library/init/data/set.lean b/library/init/data/set.lean
index 7545a612d6..8994a8ee6f 100644
--- a/library/init/data/set.lean
+++ b/library/init/data/set.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.tactic
+import init.meta.interactive
 
 universes u v
 def set (α : Type u) := α → Prop
@@ -74,6 +74,18 @@ def image (f : α → β) (s : set α) : set β :=
 {b | ∃ a, a ∈ s ∧ f a = b}
 
 instance : functor set :=
-{map := @set.image}
+{map := @set.image,
+ id_map := begin
+   intros _ s, apply funext, intro b,
+   dsimp [image, set_of],
+   exact propext ⟨λ ⟨b', ⟨_, _⟩⟩, ‹b' = b› ▸ ‹s b'›,
+                  λ _, ⟨b, ⟨‹s b›, rfl⟩⟩⟩,
+ end,
+ map_comp := begin
+   intros, apply funext, intro c,
+   dsimp [image, set_of],
+   exact propext ⟨λ ⟨a, ⟨h₁, h₂⟩⟩, ⟨g a, ⟨⟨a, ⟨h₁, rfl⟩⟩, h₂⟩⟩,
+                  λ ⟨b, ⟨⟨a, ⟨h₁, h₂⟩⟩, h₃⟩⟩, ⟨a, ⟨h₁, h₂^.symm ▸ h₃⟩⟩⟩
+ end}
 
 end set
diff --git a/library/init/meta/converter.lean b/library/init/meta/converter.lean
index 7b15d87617..c3f4687796 100644
--- a/library/init/meta/converter.lean
+++ b/library/init/meta/converter.lean
@@ -70,7 +70,9 @@ protected meta def bind {α β : Type} (c₁ : conv α) (c₂ : α → conv β)
 meta instance : monad conv :=
 { map  := @conv.map,
   pure := @conv.pure,
-  bind := @conv.bind }
+  bind := @conv.bind,
+  id_map := undefined, pure_bind := undefined, bind_assoc := undefined,
+  bind_pure_comp_eq_map := undefined, bind_map_eq_seq := undefined }
 
 meta instance : alternative conv :=
 { conv.monad with
diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean
index ea1fdc1753..80134b6aff 100644
--- a/library/init/meta/exceptional.lean
+++ b/library/init/meta/exceptional.lean
@@ -51,4 +51,6 @@ end exceptional
 
 meta instance : monad exceptional :=
 {pure := @exceptional.return, bind := @exceptional.bind,
- map_const_eq := undefined, seq_left_eq := undefined, seq_right_eq := undefined}
+ map_const_eq := undefined, seq_left_eq := undefined, seq_right_eq := undefined,
+ id_map := undefined, pure_bind := undefined, bind_assoc := undefined,
+ bind_pure_comp_eq_map := undefined, bind_map_eq_seq := undefined}
diff --git a/library/init/meta/interaction_monad.lean b/library/init/meta/interaction_monad.lean
index 25bbb2f26c..dee7d83d18 100644
--- a/library/init/meta/interaction_monad.lean
+++ b/library/init/meta/interaction_monad.lean
@@ -69,7 +69,9 @@ interaction_monad_bind t₁ (λ a, t₂)
 
 meta instance interaction_monad.monad : monad m :=
 {map := @interaction_monad_fmap, pure := @interaction_monad_return, bind := @interaction_monad_bind,
- map_const_eq := undefined, seq_left_eq := undefined, seq_right_eq := undefined}
+ map_const_eq := undefined, seq_left_eq := undefined, seq_right_eq := undefined,
+ id_map := undefined, pure_bind := undefined, bind_assoc := undefined,
+ bind_pure_comp_eq_map := undefined, bind_map_eq_seq := undefined}
 
 meta def interaction_monad.mk_exception {α : Type u} {β : Type v} [has_to_format β] (msg : β) (ref : option expr) (s : state) : result state α :=
 exception (some (λ _, to_fmt msg)) none s
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index e54969d052..ac81d25053 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -40,7 +40,7 @@ meta def without_ident_list := (tk "without" *> ident*) <|> return []
 meta def location := (tk "at" *> ident*) <|> return []
 meta def qexpr_list := list_of (qexpr 0)
 meta def opt_qexpr_list := qexpr_list <|> return []
-meta def qexpr_list_or_texpr := qexpr_list <|> return <$> texpr
+meta def qexpr_list_or_texpr := qexpr_list <|> list.ret <$> texpr
 end types
 
 /-- Use `desc` as the interactive description of `p`. -/
@@ -66,13 +66,13 @@ private meta def parser_desc_aux : expr → tactic (list format)
 | ```(ident)  := return ["id"]
 | ```(ident_) := return ["id"]
 | ```(qexpr) := return ["expr"]
-| ```(tk %%c) := return <$> to_fmt <$> eval_expr string c
+| ```(tk %%c) := list.ret <$> to_fmt <$> eval_expr string c
 | ```(cur_pos) := return []
 | ```(return ._) := return []
 | ```(._ <$> %%p) := parser_desc_aux p
 | ```(skip_info %%p) := parser_desc_aux p
 | ```(set_goal_info_pos %%p) := parser_desc_aux p
-| ```(with_desc %%desc %%p) := return <$> eval_expr format desc
+| ```(with_desc %%desc %%p) := list.ret <$> eval_expr format desc
 | ```(%%p₁ <*> %%p₂) := do
   f₁ ← parser_desc_aux p₁,
   f₂ ← parser_desc_aux p₂,
@@ -306,7 +306,7 @@ meta def rw_rules : parser rw_rules_t :=
 (tk "[" *>
  rw_rules_t.mk <$> sep_by (skip_info (tk ",")) (set_goal_info_pos $ rw_rule_p (qexpr 0))
                <*> (some <$> cur_pos <* set_goal_info_pos (tk "]")))
-<|> rw_rules_t.mk <$> (return <$> rw_rule_p texpr) <*> return none
+<|> rw_rules_t.mk <$> (list.ret <$> rw_rule_p texpr) <*> return none
 
 private meta def rw_core (m : transparency) (rs : parse rw_rules) (loc : parse location) : tactic unit :=
 match loc with
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 908dcb67cc..683fdc4358 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -994,7 +994,6 @@ rfl
 meta def control_laws_tac := whnf_target >> intros >> to_expr ``(rfl) >>= exact
 
 meta instance : monad task :=
-{map := @task.map, bind := @task.bind, pure := @task.pure}
-
-instance : monad list :=
-{map := @list.map, pure := @list.ret, bind := @list.bind}
+{map := @task.map, bind := @task.bind, pure := @task.pure,
+ id_map := undefined, pure_bind := undefined, bind_assoc := undefined,
+ bind_pure_comp_eq_map := undefined}
diff --git a/library/init/meta/transfer.lean b/library/init/meta/transfer.lean
index 699df48186..b487e9bd83 100644
--- a/library/init/meta/transfer.lean
+++ b/library/init/meta/transfer.lean
@@ -5,6 +5,7 @@ Author: Johannes Hölzl (CMU)
 -/
 prelude
 import init.meta.tactic init.meta.match_tactic init.relator init.meta.mk_dec_eq_instance
+import init.data.list.instances
 
 namespace transfer
 open tactic expr list monad
diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean
index 9415001968..2a8a8b485f 100644
--- a/library/init/meta/vm.lean
+++ b/library/init/meta/vm.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.meta.tactic init.data.option.basic
+import init.meta.tactic init.data.option_t
 import init.meta.mk_dec_eq_instance
 
 meta constant vm_obj : Type
@@ -77,7 +77,9 @@ meta constant vm_core.ret {α : Type} : α → vm_core α
 meta constant vm_core.bind {α β : Type} : vm_core α → (α → vm_core β) → vm_core β
 
 meta instance : monad vm_core :=
-{map := @vm_core.map, pure := @vm_core.ret, bind := @vm_core.bind}
+{map := @vm_core.map, pure := @vm_core.ret, bind := @vm_core.bind,
+ id_map := undefined, pure_bind := undefined, bind_assoc := undefined,
+ bind_pure_comp_eq_map := undefined, bind_map_eq_seq := undefined}
 
 @[reducible] meta def vm (α : Type) : Type := option_t vm_core α
 
diff --git a/library/init/native/result.lean b/library/init/native/result.lean
index b8ef565547..72f22417f6 100644
--- a/library/init/native/result.lean
+++ b/library/init/native/result.lean
@@ -5,7 +5,7 @@ Authors: Jared Roesch
 -/
 prelude
 
-import init.meta.tactic
+import init.meta.interactive
 
 namespace native
 
@@ -22,7 +22,10 @@ def result.and_then {E T U : Type} : result E T → (T → result E U) → resul
 | (result.ok t) f := f t
 
 instance result_monad (E : Type) : monad (result E) :=
-{pure := @result.ok E, bind := @result.and_then E}
+{pure := @result.ok E, bind := @result.and_then E,
+ id_map := by intros; cases x; dsimp [result.and_then]; apply rfl,
+ pure_bind := by intros; apply rfl,
+ bind_assoc := by intros; cases x; simp [result.and_then]}
 
 inductive resultT (M : Type → Type) (E : Type) (A : Type) : Type
 | run : M (result E A) → resultT
@@ -43,7 +46,30 @@ section resultT
   end)
 
   instance resultT_monad [m : monad M] (E : Type) : monad (resultT M E) :=
-  {pure := @resultT.pure M m E, bind := @resultT.and_then M m E}
+  {pure := @resultT.pure M m E, bind := @resultT.and_then M m E,
+   id_map := begin
+     intros, cases x,
+     dsimp [resultT.and_then],
+     assert h : @resultT.and_then._match_1 _ m E α _ resultT.pure = pure,
+     { apply funext, intro x,
+       cases x; simp [resultT.and_then._match_1, resultT.pure, resultT.and_then._match_2] },
+     { rw [h, @monad.bind_pure _ (result E α) _] },
+   end,
+   pure_bind := begin
+     intros,
+     dsimp [resultT.pure, resultT.and_then, return, pure, bind],
+     rw [monad.pure_bind], dsimp [resultT.and_then._match_1],
+     cases f x, dsimp [resultT.and_then._match_2], apply rfl,
+   end,
+   bind_assoc := begin
+     intros,
+     cases x, dsimp [resultT.and_then, bind],
+     apply congr_arg, rw [monad.bind_assoc],
+     apply congr_arg, apply funext, intro,
+     cases x with e a; dsimp [resultT.and_then._match_1, pure],
+     { rw [monad.pure_bind], apply rfl },
+     { cases f a, apply rfl },
+   end}
 end resultT
 
 end native
diff --git a/library/init/propext.lean b/library/init/propext.lean
index 474eb40490..87d080adbd 100644
--- a/library/init/propext.lean
+++ b/library/init/propext.lean
@@ -25,3 +25,19 @@ propext (iff_true_intro h)
 
 lemma eq_false_intro {a : Prop} (h : ¬a) : a = false :=
 propext (iff_false_intro h)
+
+theorem iff.to_eq {a b : Prop} (h : a ↔ b) : a = b :=
+propext h
+
+theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
+propext (iff.intro
+  (assume h, iff.to_eq h)
+  (assume h, h^.to_iff))
+
+lemma eq_false {a : Prop} : (a = false) = (¬ a) :=
+have (a ↔ false) = (¬ a), from propext (iff_false a),
+eq.subst (@iff_eq_eq a false) this
+
+lemma eq_true {a : Prop} : (a = true) = a :=
+have (a ↔ true) = a, from propext (iff_true a),
+eq.subst (@iff_eq_eq a true) this
diff --git a/tests/lean/run/isabelle.lean b/tests/lean/run/isabelle.lean
index 3d5f25966b..38103e5c12 100644
--- a/tests/lean/run/isabelle.lean
+++ b/tests/lean/run/isabelle.lean
@@ -33,8 +33,7 @@ protected meta def failure {α} : lazy_tactic α :=
 λ s, nil
 
 meta instance : monad lazy_tactic :=
-{ pure := @lazy_tactic.return,
-  bind := @lazy_tactic.bind }
+unsafe_monad_from_pure_bind @lazy_tactic.return @lazy_tactic.bind
 
 meta instance : alternative lazy_tactic :=
 { lazy_tactic.monad with
diff --git a/tests/lean/type_error_at_eval_expr.lean.expected.out b/tests/lean/type_error_at_eval_expr.lean.expected.out
index 6ec01aaa84..aff914bac0 100644
--- a/tests/lean/type_error_at_eval_expr.lean.expected.out
+++ b/tests/lean/type_error_at_eval_expr.lean.expected.out
@@ -1,6 +1,6 @@
 type_error_at_eval_expr.lean:3:0: error: eval_expr failed due to type error
 nested exception message:
-type mismatch at definition '_eval_expr.16.440', has type
+type mismatch at definition '_eval_expr.16.500', has type
   list ℕ
 but is expected to have type
   ℕ