From 3ead6be9ca0c5a5c52fa615f156dd0f612651ab7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 13 Mar 2017 11:23:47 +0100
Subject: [PATCH] feat(init): add default value proofs to the monadic hierarchy

---
 library/init/category/applicative.lean    |  8 ++-
 library/init/category/functor.lean        |  7 ++-
 library/init/category/state.lean          |  2 +-
 library/init/data/list/basic.lean         |  5 +-
 library/init/data/list/instances.lean     |  1 -
 library/init/data/option/basic.lean       | 57 +-------------------
 library/init/data/option/instances.lean   | 65 +++++++++++++++++++++++
 library/init/data/set.lean                |  2 +-
 library/init/meta/comp_value_tactics.lean |  2 +-
 library/init/meta/exceptional.lean        |  5 +-
 library/init/meta/expr.lean               |  2 +-
 library/init/meta/format.lean             |  2 +-
 library/init/meta/interaction_monad.lean  |  3 +-
 library/init/meta/lean/parser.lean        |  3 +-
 library/init/meta/rec_util.lean           |  2 +-
 library/init/meta/simp_tactic.lean        |  1 +
 library/init/meta/smt/smt_tactic.lean     |  1 +
 library/init/meta/tactic.lean             | 10 ++++
 library/init/meta/task.lean               |  7 +--
 library/init/native/result.lean           |  2 +-
 library/init/util.lean                    |  4 +-
 21 files changed, 109 insertions(+), 82 deletions(-)
 create mode 100644 library/init/data/option/instances.lean

diff --git a/library/init/category/applicative.lean b/library/init/category/applicative.lean
index 6f15a56b76..95143d6982 100644
--- a/library/init/category/applicative.lean
+++ b/library/init/category/applicative.lean
@@ -8,12 +8,18 @@ import init.category.functor
 open function
 universes u v
 
+section
+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)
 (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)
-(map := λ _ _ x y, seq (pure x) y)
+(seq_left_eq : ∀ {α β : Type u} (a : f α) (b : f β), seq_left a b = seq (map (const β) a) b . control_laws_tac)
+(seq_right_eq : ∀ {α β : Type u} (a : f α) (b : f β), seq_right a b = seq (map (const α id) a) b . control_laws_tac)
+end
 
 section
 variables {f : Type u → Type v} [applicative f] {α β : Type u}
diff --git a/library/init/category/functor.lean b/library/init/category/functor.lean
index 7e4d925e73..241037b6e5 100644
--- a/library/init/category/functor.lean
+++ b/library/init/category/functor.lean
@@ -4,13 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch, Sebastian Ullrich
 -/
 prelude
-import init.core init.function
+import init.core init.function init.meta.name
 open function
 universes u v
 
+section
+set_option auto_param.check_exists false
+
 class functor (f : Type u → Type v) : Type (max u+1 v) :=
 (map : Π {α β : Type u}, (α → β) → f α → f β)
 (map_const : Π {α : Type u} (β : Type u), α → f β → f α := λ α β, map ∘ const β)
+(map_const_eq : ∀ {α β : Type u}, @map_const α β = map ∘ const β . control_laws_tac)
+end
 
 @[inline] def fmap {f : Type u → Type v} [functor f] {α β : Type u} : (α → β) → f α → f β :=
 functor.map
diff --git a/library/init/category/state.lean b/library/init/category/state.lean
index 2531dce267..00ae7f8e05 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.logic init.category.monad init.category.alternative
+import init.meta.tactic
 universes u v
 
 def state (σ α : Type u) : Type u :=
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index 8f01340f50..ec9763bbbd 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.logic init.data.nat.basic init.category.monad
+import init.logic init.data.nat.basic
 open decidable list
 
 universes u v w
@@ -224,6 +224,3 @@ join (map b a)
 @[inline] def ret {α : Type u} (a : α) : list α :=
 [a]
 end list
-
-instance : monad list :=
-{map := @list.map, pure := @list.ret, bind := @list.bind}
diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
index a02490ac26..c1320f2070 100644
--- a/library/init/data/list/instances.lean
+++ b/library/init/data/list/instances.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.category.monad init.category.alternative init.data.list.basic
 import init.meta.mk_dec_eq_instance
 open list
 
diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean
index aa98a6cb1e..ee6826880c 100644
--- a/library/init/data/option/basic.lean
+++ b/library/init/data/option/basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.logic init.category
+import init.logic init.category.monad init.category.alternative
 open decidable
 
 universes u v
@@ -53,58 +53,3 @@ instance {α : Type u} [d : decidable_eq α] : decidable_eq (option α)
   | (is_false n) := is_false (λ h, option.no_confusion h (λ e, absurd e n))
   end
 
-@[inline] def option_bind {α : Type u} {β : Type v} : option α → (α → option β) → option β
-| none     b := none
-| (some a) b := b a
-
-instance : monad option :=
-{pure := @some, bind := @option_bind}
-
-def option_orelse {α : Type u} : option α → option α → option α
-| (some a) o         := some a
-| none     (some a)  := some a
-| none     none      := none
-
-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/instances.lean b/library/init/data/option/instances.lean
new file mode 100644
index 0000000000..c19a3817c3
--- /dev/null
+++ b/library/init/data/option/instances.lean
@@ -0,0 +1,65 @@
+/-
+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 .basic
+
+universes u v
+
+@[inline] def option_bind {α : Type u} {β : Type v} : option α → (α → option β) → option β
+| none     b := none
+| (some a) b := b a
+
+instance : monad option :=
+{pure := @some, bind := @option_bind}
+
+def option_orelse {α : Type u} : option α → option α → option α
+| (some a) o         := some a
+| none     (some a)  := some a
+| none     none      := none
+
+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/set.lean b/library/init/data/set.lean
index f4fd527986..7545a612d6 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.logic init.category.functor
+import init.meta.tactic
 
 universes u v
 def set (α : Type u) := α → Prop
diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean
index cd98b98c35..cc0dc329b6 100644
--- a/library/init/meta/comp_value_tactics.lean
+++ b/library/init/meta/comp_value_tactics.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.tactic init.data.option.instances
 
 meta constant mk_nat_val_ne_proof : expr → expr → option expr
 meta constant mk_nat_val_lt_proof : expr → expr → option expr
diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean
index f3db6d8085..ea1fdc1753 100644
--- a/library/init/meta/exceptional.lean
+++ b/library/init/meta/exceptional.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.category.monad init.meta.format
+import init.category.monad init.meta.format init.util
 /-
 Remark: we use a function that produces a format object as the exception information.
 Motivation: the formatting object may be big, and we may create it on demand.
@@ -50,4 +50,5 @@ exception α (λ u, f)
 end exceptional
 
 meta instance : monad exceptional :=
-{pure := @exceptional.return, bind := @exceptional.bind}
+{pure := @exceptional.return, bind := @exceptional.bind,
+ map_const_eq := undefined, seq_left_eq := undefined, seq_right_eq := undefined}
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index fd0dee0751..dfacd0648c 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.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.level
+import init.meta.level init.category.monad
 
 structure pos :=
 (line   : nat)
diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean
index edcfaea44b..37eb548193 100644
--- a/library/init/meta/format.lean
+++ b/library/init/meta/format.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.options
+import init.meta.options init.function
 
 universes u v
 
diff --git a/library/init/meta/interaction_monad.lean b/library/init/meta/interaction_monad.lean
index 72ffe87855..25bbb2f26c 100644
--- a/library/init/meta/interaction_monad.lean
+++ b/library/init/meta/interaction_monad.lean
@@ -68,7 +68,8 @@ meta def interaction_monad_orelse {α : Type u} (t₁ t₂ : m α) : m α :=
 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 := @interaction_monad_fmap, pure := @interaction_monad_return, bind := @interaction_monad_bind,
+ map_const_eq := undefined, seq_left_eq := undefined, seq_right_eq := 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/lean/parser.lean b/library/init/meta/lean/parser.lean
index 90830a20fb..98456b8b0d 100644
--- a/library/init/meta/lean/parser.lean
+++ b/library/init/meta/lean/parser.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
 prelude
-import init.data.option.basic init.category.monad init.category.alternative
-import init.meta.pexpr init.meta.interaction_monad
+import init.meta.tactic
 
 namespace lean
 
diff --git a/library/init/meta/rec_util.lean b/library/init/meta/rec_util.lean
index dab27522d3..9731319c2b 100644
--- a/library/init/meta/rec_util.lean
+++ b/library/init/meta/rec_util.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 Helper tactic for showing that a type has decidable equality.
 -/
 prelude
-import init.meta.tactic
+import init.meta.tactic init.data.option.instances
 
 namespace tactic
 open expr
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index f654fd0f69..af6b038d83 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.tactic init.meta.attribute init.meta.constructor_tactic
 import init.meta.relation_tactics init.meta.occurrences init.meta.quote
+import init.data.option.instances
 
 open tactic
 
diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean
index c3535a5b5c..4cb5195b81 100644
--- a/library/init/meta/smt/smt_tactic.lean
+++ b/library/init/meta/smt/smt_tactic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import init.category
 import init.meta.simp_tactic
 import init.meta.smt.congruence_closure
 import init.meta.smt.ematch
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 235c9000a4..908dcb67cc 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -988,3 +988,13 @@ run_cmd do
 
 lemma id_locked_eq {α : Type u} (a : α) : id_locked α a = a :=
 rfl
+
+/- Install monad laws tactic and use it to prove some instances. -/
+
+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}
diff --git a/library/init/meta/task.lean b/library/init/meta/task.lean
index 43c9331dd9..5f24661398 100644
--- a/library/init/meta/task.lean
+++ b/library/init/meta/task.lean
@@ -1,5 +1,5 @@
 prelude
-import init.category
+import init.logic
 
 meta constant {u} task : Type u → Type u
 
@@ -13,11 +13,8 @@ protected meta constant {u} flatten {α : Type u} : task (task α) → task α
 protected meta def {u v} bind {α : Type u} {β : Type v} (t : task α) (f : α → task β) : task β :=
 task.flatten (task.map f t)
 
-meta instance : monad task :=
-{ map := @task.map, bind := @task.bind, pure := @task.pure }
-
 @[inline]
 meta def {u} delay {α : Type u} (f : unit → α) : task α :=
-task.map f (return ())
+task.map f (task.pure ())
 
 end task
diff --git a/library/init/native/result.lean b/library/init/native/result.lean
index bc867ac8e3..b8ef565547 100644
--- a/library/init/native/result.lean
+++ b/library/init/native/result.lean
@@ -5,7 +5,7 @@ Authors: Jared Roesch
 -/
 prelude
 
-import init.category.monad
+import init.meta.tactic
 
 namespace native
 
diff --git a/library/init/util.lean b/library/init/util.lean
index 8c56da878b..f7762c8f9a 100644
--- a/library/init/util.lean
+++ b/library/init/util.lean
@@ -32,6 +32,6 @@ f ()
 meta def try_for {α : Type u} (max : nat) (f : thunk α) : option α :=
 some (f ())
 
-meta constant undefined_core {α : Type u} (message : string) : α
+meta constant undefined_core {α : Sort u} (message : string) : α
 
-meta def undefined {α : Type u} : α := undefined_core "undefined"
+meta def undefined {α : Sort u} : α := undefined_core "undefined"