max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library): add functor, applicative, and monad laws, and prove them correct for non-meta instances

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-22 16:33:56 +01:00 • committed by Leonardo de Moura
parent bf8292cb17
commit dfd84666e2
20 changed files with 318 additions and 91 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
library/init/category/applicative.lean
View file

@ -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 _)

5
library/init/category/functor.lean
View file

@ -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 β :=

59
library/init/category/monad.lean
View file

@ -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 _)

37
library/init/category/state.lean
View file

@ -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}

16
library/init/classical.lean
View file

@ -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

37
library/init/data/list/instances.lean
View file

@ -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 α) :=

46
library/init/data/option/instances.lean
View file

@ -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 α))

71
library/init/data/option_t.lean Normal file
View file

@ -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 α))

16
library/init/data/set.lean
View file

@ -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

4
library/init/meta/converter.lean
View file

@ -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

4
library/init/meta/exceptional.lean
View file

@ -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}

4
library/init/meta/interaction_monad.lean
View file

@ -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

8
library/init/meta/interactive.lean
View file

@ -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

7
library/init/meta/tactic.lean
View file

@ -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}

1
library/init/meta/transfer.lean
View file

@ -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

6
library/init/meta/vm.lean
View file

@ -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 α

32
library/init/native/result.lean
View file

@ -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

16
library/init/propext.lean
View file

@ -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

3
tests/lean/run/isabelle.lean
View file

@ -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

2
tests/lean/type_error_at_eval_expr.lean.expected.out
View file

@ -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
ℕ