From 705670807ed8b9960d84b8524b10f65aaeb017b2 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 31 May 2017 09:17:02 -0400
Subject: [PATCH 1/7] feat(init/data/cached): Caching mechanism

This still needs more work on the VM side.
---
 library/init/data/cached.lean | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 library/init/data/cached.lean

diff --git a/library/init/data/cached.lean b/library/init/data/cached.lean
new file mode 100644
index 0000000000..8d2fa91ca8
--- /dev/null
+++ b/library/init/data/cached.lean
@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+-/
+prelude
+import init.data.quot
+universes u v
+
+structure cached (α : Type u) [inhabited α] := mk' :: (val : quot (λ x y : α, true))
+
+namespace cached
+
+variables {α : Type u} [inhabited α] {β : Type v}
+
+def mk (v : α) : cached α := ⟨quot.mk _ v⟩
+
+def empty : cached α := mk (default α)
+
+def lift (f : α → β) (h : ∀ x y, f x = f y) (c : cached α) : β :=
+quot.lift f (λx y _, h x y) c.val
+
+def lift_eq {f : α → β} {h} (x) : lift f h (mk x) = f x := rfl
+
+-- This function has a VM implementation to change the value of the cache `c` to `v`
+def update (c : cached α) (v : α) (f : thunk β) : β := f ()
+
+def reset (c : cached α) : thunk β → β := update c (default α)
+
+theorem cache_eq_empty : ∀ (c : cached α), c = empty
+| ⟨q⟩ := congr_arg mk' $ quot.ind (λx, quot.sound trivial) q
+
+end cached
\ No newline at end of file

From e21f362d6b7a17ac9fc694b2f6a8d5bc20e09b2a Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 1 Jun 2017 00:52:59 -0400
Subject: [PATCH 2/7] feat(init/data/cached): Constructions based on cached

---
 library/data/hash_map.lean     | 18 +++++++++++
 library/data/hashed_func.lean  | 52 ++++++++++++++++++++++++++++++++
 library/init/data/cached.lean  | 55 +++++++++++++++++++++++++---------
 library/init/data/default.lean |  2 +-
 4 files changed, 112 insertions(+), 15 deletions(-)
 create mode 100644 library/data/hashed_func.lean

diff --git a/library/data/hash_map.lean b/library/data/hash_map.lean
index b59532a435..4388a1e26e 100644
--- a/library/data/hash_map.lean
+++ b/library/data/hash_map.lean
@@ -480,6 +480,15 @@ theorem contains_iff (m : hash_map α β) (a : α) (b : β a) :
   m.contains a ↔ a ∈ m.keys :=
 m.is_valid.contains_aux_iff _ _
 
+theorem entries_empty (hash_fn : α → nat) {n} : entries (@mk_hash_map α _ β hash_fn n) = [] :=
+mk_as_list hash_fn _
+
+theorem find_empty (hash_fn : α → nat) {n} (x) : find (@mk_hash_map α _ β hash_fn n) x = none :=
+by { ginduction find (@mk_hash_map α _ β hash_fn n) x with h y, refl,
+     note := (find_iff _ _ _).1 h,
+     rw entries_empty at this,
+     contradiction }
+
 lemma insert_lemma (hash_fn : α → nat) {n n'}
   {bkts : bucket_array α β n} {sz} (v : valid hash_fn bkts sz) :
   valid hash_fn (bkts.foldl (mk_array _ [] : bucket_array α β n') (reinsert_aux hash_fn)) sz :=
@@ -555,6 +564,15 @@ let n'        : ℕ+ := ⟨n.1 * 2, mul_pos n.2 dec_trivial⟩,
   buckets  := buckets'',
   is_valid := insert_lemma _ valid' }
 
+theorem insert_hash_fn (m : hash_map α β) (a : α) (b : β a) : (m.insert a b).hash_fn = m.hash_fn :=
+begin
+  cases m, unfold hash_map.insert, simp,
+  cases (by apply_instance : decidable
+    (↑(contains_aux a (bucket_array.read hash_fn buckets a)))) with hc hc; dsimp [dite],
+  cases (by apply_instance : decidable (size + 1 ≤ nbuckets.val)) with hsz hsz; dsimp [ite],
+  all_goals {refl}
+end
+
 theorem mem_insert : Π (m : hash_map α β) (a b a' b'),
   sigma.mk a' b' ∈ (m.insert a b).entries ↔
   if a = a' then b == b' else sigma.mk a' b' ∈ m.entries
diff --git a/library/data/hashed_func.lean b/library/data/hashed_func.lean
new file mode 100644
index 0000000000..88d95d1d0c
--- /dev/null
+++ b/library/data/hashed_func.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+-/
+import data.hash_map
+
+universes u v
+
+namespace hashed_func
+  variables {α : Type u} [decidable_eq α] {β : α → Type v}
+
+  def cache_ty (f : Π a, β a) (hash_fn : α → ℕ) :=
+  {m : hash_map α β // ∀ x y, m.find x = some y → f x = y}
+
+  instance (f : Π a, β a) (hash_fn : α → ℕ) : inhabited (cache_ty f hash_fn) :=
+  ⟨⟨mk_hash_map hash_fn, λx y h, by rw hash_map.find_empty at h; contradiction⟩⟩
+end hashed_func
+
+structure hashed_func (α : Type u) [decidable_eq α] (β : α → Type v) := mk' ::
+(func : Π a, β a)
+(hash_fn : α → ℕ)
+(cache : cached (hashed_func.cache_ty func hash_fn))
+
+namespace hashed_func
+  variables {α : Type u} [decidable_eq α] {β : α → Type v}
+
+  def mk (f : Π a, β a) (hash_fn : α → ℕ) : hashed_func α β := ⟨f, hash_fn, default _⟩
+
+  def eval : hashed_func α β → Π a, β a | ⟨f, hash_fn, c⟩ a :=
+  c.lift_on
+    (λ⟨m, H⟩, (m.find a).get_or_else $
+      let v := f a in c.update ⟨m.insert a v, λ x y h,
+      begin
+        by_cases a = x with ax,
+        { revert y, rw -ax, intros y h,
+          rw hash_map.find_insert_eq at h,
+          injection h },
+        { rw hash_map.find_insert_ne _ _ _ _ ax at h,
+          exact H x y h }
+      end⟩ v)
+    (λ⟨m, H⟩, begin
+      unfold default inhabited.default hashed_func.eval._match_1,
+      rw hash_map.find_empty,
+      ginduction m.find a with h b; dsimp [option.get_or_else, cached.update, hashed_func.eval._match_1],
+      { refl },
+      { exact H a b h },
+    end)
+
+  instance : has_coe_to_fun (hashed_func α β) := ⟨_, hashed_func.eval⟩
+
+end hashed_func
diff --git a/library/init/data/cached.lean b/library/init/data/cached.lean
index 8d2fa91ca8..e84ddb18af 100644
--- a/library/init/data/cached.lean
+++ b/library/init/data/cached.lean
@@ -4,30 +4,57 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro
 -/
 prelude
-import init.data.quot
+import init.data.quot init.data.option.basic
 universes u v
 
-structure cached (α : Type u) [inhabited α] := mk' :: (val : quot (λ x y : α, true))
+structure cached (α : Type u) [inhabited α] :=
+mk' :: (val : quot (λ x y : α, true))
 
 namespace cached
+  variables {α : Type u} [inhabited α] {β : Type v}
 
-variables {α : Type u} [inhabited α] {β : Type v}
+  def mk (v : α) : cached α := ⟨quot.mk _ v⟩
 
-def mk (v : α) : cached α := ⟨quot.mk _ v⟩
+  def empty : cached α := mk (default α)
+  instance : inhabited (cached α) := ⟨empty⟩
 
-def empty : cached α := mk (default α)
+  def lift_on (c : cached α) (f : α → β) (h : ∀ x, f (default _) = f x) : β :=
+  quot.lift f (λx y _, (h x).symm.trans (h y)) c.val
 
-def lift (f : α → β) (h : ∀ x y, f x = f y) (c : cached α) : β :=
-quot.lift f (λx y _, h x y) c.val
+  def lift_eq {f : α → β} {h} (x) : lift_on (mk x) f h = f x := rfl
 
-def lift_eq {f : α → β} {h} (x) : lift f h (mk x) = f x := rfl
+  -- This function has a VM implementation to change the value of the cache `c` to `v`
+  def update (c : cached α) (v : α) (f : thunk β) : β := f ()
 
--- This function has a VM implementation to change the value of the cache `c` to `v`
-def update (c : cached α) (v : α) (f : thunk β) : β := f ()
+  def reset (c : cached α) : thunk β → β := update c (default α)
 
-def reset (c : cached α) : thunk β → β := update c (default α)
+  theorem cache_eq_empty : ∀ (c : cached α), c = empty
+  | ⟨q⟩ := congr_arg mk' $ quot.ind (λx, quot.sound trivial) q
 
-theorem cache_eq_empty : ∀ (c : cached α), c = empty
-| ⟨q⟩ := congr_arg mk' $ quot.ind (λx, quot.sound trivial) q
+end cached
 
-end cached
\ No newline at end of file
+structure memoized (α : Type u) := mk' ::
+(func : unit → α)
+(cache : cached (option {a // func () = a}))
+
+namespace memoized
+  variable {α : Type u}
+
+  def mk (f : thunk α) : memoized α := mk' f (default _)
+
+  def eval : memoized α → α | ⟨f, c⟩ :=
+  c.lift_on
+    (λo, match o with
+      | none := let v := f () in c.update (some ⟨v, rfl⟩) v
+      | some ⟨x, h⟩ := x
+      end)
+    (λo, match o with
+      | none        := rfl
+      | some ⟨x, h⟩ := h
+      end)
+
+  instance : has_coe_to_fun (memoized α) := ⟨λ_, thunk α, λm _, m.eval⟩
+
+  instance : has_coe (memoized α) α := ⟨λm, m.eval⟩
+
+end memoized
diff --git a/library/init/data/default.lean b/library/init/data/default.lean
index d6b0d3eb85..4b31ee71ea 100644
--- a/library/init/data/default.lean
+++ b/library/init/data/default.lean
@@ -6,4 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import init.data.basic init.data.sigma init.data.nat init.data.char init.data.string
 import init.data.list init.data.sum init.data.subtype init.data.int init.data.array
-import init.data.bool init.data.fin init.data.unsigned
+import init.data.bool init.data.fin init.data.unsigned init.data.cached

From 9a709b77d85a8d24c0108f60ee13b29e97c55d4c Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 1 Jun 2017 03:32:47 -0400
Subject: [PATCH 3/7] feat(library/vm/vm_cached): cached implementation

---
 library/init/data/cached.lean  |  5 +++
 src/library/vm/CMakeLists.txt  |  2 +-
 src/library/vm/init_module.cpp |  3 ++
 src/library/vm/vm_cached.cpp   | 68 ++++++++++++++++++++++++++++++++++
 src/library/vm/vm_cached.h     | 14 +++++++
 5 files changed, 91 insertions(+), 1 deletion(-)
 create mode 100644 src/library/vm/vm_cached.cpp
 create mode 100644 src/library/vm/vm_cached.h

diff --git a/library/init/data/cached.lean b/library/init/data/cached.lean
index e84ddb18af..e7c92a8824 100644
--- a/library/init/data/cached.lean
+++ b/library/init/data/cached.lean
@@ -10,6 +10,7 @@ universes u v
 structure cached (α : Type u) [inhabited α] :=
 mk' :: (val : quot (λ x y : α, true))
 
+#print cached.val
 namespace cached
   variables {α : Type u} [inhabited α] {β : Type v}
 
@@ -31,6 +32,10 @@ namespace cached
   theorem cache_eq_empty : ∀ (c : cached α), c = empty
   | ⟨q⟩ := congr_arg mk' $ quot.ind (λx, quot.sound trivial) q
 
+  meta constant inspect : cached α → α
+
+  meta instance [has_to_string α] : has_to_string (cached α) := ⟨to_string ∘ inspect⟩
+
 end cached
 
 structure memoized (α : Type u) := mk' ::
diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt
index f7a4c77af0..b8b2c575b7 100644
--- a/src/library/vm/CMakeLists.txt
+++ b/src/library/vm/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
   vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
   vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp vm_task.cpp
-  vm_native.cpp vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp vm_pos_info.cpp)
+  vm_native.cpp vm_int.cpp init_module.cpp vm_parser.cpp vm_array.cpp vm_cached.cpp vm_pos_info.cpp)
diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp
index 226539e26b..ae90bf056c 100644
--- a/src/library/vm/init_module.cpp
+++ b/src/library/vm/init_module.cpp
@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_task.h"
 #include "library/vm/vm_parser.h"
 #include "library/vm/vm_array.h"
+#include "library/vm/vm_cached.h"
 
 namespace lean {
 void initialize_vm_core_module() {
@@ -47,9 +48,11 @@ void initialize_vm_core_module() {
     initialize_vm_environment();
     initialize_vm_parser();
     initialize_vm_array();
+    initialize_vm_cached();
 }
 
 void finalize_vm_core_module() {
+    finalize_vm_cached();
     finalize_vm_array();
     finalize_vm_parser();
     finalize_vm_environment();
diff --git a/src/library/vm/vm_cached.cpp b/src/library/vm/vm_cached.cpp
new file mode 100644
index 0000000000..db92bdfc5b
--- /dev/null
+++ b/src/library/vm/vm_cached.cpp
@@ -0,0 +1,68 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Mario Carneiro
+*/
+#include <vector>
+#include "library/vm/vm.h"
+#include "library/trace.h"
+
+#define lean_cached_trace(CODE) lean_trace(name({"cached", "update"}), CODE)
+
+namespace lean {
+struct vm_cached : public vm_external {
+    vm_obj m_default;
+    vm_obj m_value;
+    vm_cached(vm_obj const & def, vm_obj const & v):m_default(def), m_value(v) {}
+    virtual ~vm_cached() {}
+    virtual void dealloc() override { this->~vm_cached(); get_vm_allocator().deallocate(sizeof(vm_cached), this); }
+    virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_cached(m_default, m_value); }
+    virtual vm_external * clone(vm_clone_fn const &) override { return new (get_vm_allocator().allocate(sizeof(vm_cached))) vm_cached(m_default, m_value); }
+};
+
+vm_obj const & get_cached_default(vm_obj const & o) {
+    lean_vm_check(dynamic_cast<vm_cached*>(to_external(o)));
+    return static_cast<vm_cached*>(to_external(o))->m_default;
+}
+
+vm_obj const & get_cached_value(vm_obj const & o) {
+    lean_vm_check(dynamic_cast<vm_cached*>(to_external(o)));
+    return static_cast<vm_cached*>(to_external(o))->m_value;
+}
+
+vm_obj const & set_cached_value(vm_obj const & o, vm_obj const & v) {
+    lean_vm_check(dynamic_cast<vm_cached*>(to_external(o)));
+    return static_cast<vm_cached*>(to_external(o))->m_value = v;
+}
+
+vm_obj cached_mk(vm_obj const &, vm_obj const & def, vm_obj const & v) {
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_cached))) vm_cached(def, v));
+}
+
+vm_obj cached_update(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & c, vm_obj const & v, vm_obj const & fn) {
+    lean_cached_trace(tout() << "cached update\n";);
+    set_cached_value(c, v);
+    return invoke(fn, mk_vm_unit());
+}
+
+vm_obj cached_val(vm_obj const &, vm_obj const &, vm_obj const & c) {
+    return get_cached_value(c);
+}
+
+unsigned cached_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
+    data.push_back(get_cached_value(o));
+    return 0;
+}
+
+void initialize_vm_cached() {
+    DECLARE_VM_BUILTIN(name({"cached", "mk'"}),              cached_mk);
+    DECLARE_VM_BUILTIN(name({"cached", "val"}),              cached_val);
+    DECLARE_VM_BUILTIN(name({"cached", "update"}),           cached_update);
+    DECLARE_VM_BUILTIN(name({"cached", "inspect"}),          cached_val);
+    DECLARE_VM_CASES_BUILTIN(name({"cached", "cases_on"}),   cached_cases_on);
+}
+
+void finalize_vm_cached() {
+}
+}
diff --git a/src/library/vm/vm_cached.h b/src/library/vm/vm_cached.h
new file mode 100644
index 0000000000..8fad78e35d
--- /dev/null
+++ b/src/library/vm/vm_cached.h
@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Mario Carneiro
+*/
+#pragma once
+
+#include "library/vm/vm.h"
+
+namespace lean {
+void initialize_vm_cached();
+void finalize_vm_cached();
+}

From b90c3cbd842d41ba45adbadc01391d1a7ca5a436 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 1 Jun 2017 03:51:41 -0400
Subject: [PATCH 4/7] refactor(init/data/cached): forgot about unchecked_cast

---
 library/init/data/cached.lean | 5 ++---
 src/library/vm/vm_cached.cpp  | 1 -
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/library/init/data/cached.lean b/library/init/data/cached.lean
index e7c92a8824..8df1e95b1b 100644
--- a/library/init/data/cached.lean
+++ b/library/init/data/cached.lean
@@ -4,13 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Mario Carneiro
 -/
 prelude
-import init.data.quot init.data.option.basic
+import init.data.quot init.data.option.basic init.util
 universes u v
 
 structure cached (α : Type u) [inhabited α] :=
 mk' :: (val : quot (λ x y : α, true))
 
-#print cached.val
 namespace cached
   variables {α : Type u} [inhabited α] {β : Type v}
 
@@ -32,7 +31,7 @@ namespace cached
   theorem cache_eq_empty : ∀ (c : cached α), c = empty
   | ⟨q⟩ := congr_arg mk' $ quot.ind (λx, quot.sound trivial) q
 
-  meta constant inspect : cached α → α
+  meta def inspect (c : cached α) : α := unchecked_cast c.val
 
   meta instance [has_to_string α] : has_to_string (cached α) := ⟨to_string ∘ inspect⟩
 
diff --git a/src/library/vm/vm_cached.cpp b/src/library/vm/vm_cached.cpp
index db92bdfc5b..f0d8c4cd5b 100644
--- a/src/library/vm/vm_cached.cpp
+++ b/src/library/vm/vm_cached.cpp
@@ -59,7 +59,6 @@ void initialize_vm_cached() {
     DECLARE_VM_BUILTIN(name({"cached", "mk'"}),              cached_mk);
     DECLARE_VM_BUILTIN(name({"cached", "val"}),              cached_val);
     DECLARE_VM_BUILTIN(name({"cached", "update"}),           cached_update);
-    DECLARE_VM_BUILTIN(name({"cached", "inspect"}),          cached_val);
     DECLARE_VM_CASES_BUILTIN(name({"cached", "cases_on"}),   cached_cases_on);
 }
 

From 939475d7e495bc4fbd2dca1978446da6e97b56c6 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 21 Jun 2017 02:02:56 -0400
Subject: [PATCH 5/7] fix(init/data/cached): add has_repr instance

---
 library/init/data/cached.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/library/init/data/cached.lean b/library/init/data/cached.lean
index 8df1e95b1b..f9f459b9b4 100644
--- a/library/init/data/cached.lean
+++ b/library/init/data/cached.lean
@@ -35,6 +35,8 @@ namespace cached
 
   meta instance [has_to_string α] : has_to_string (cached α) := ⟨to_string ∘ inspect⟩
 
+  meta instance [has_repr α] : has_repr (cached α) := ⟨repr ∘ inspect⟩
+
 end cached
 
 structure memoized (α : Type u) := mk' ::

From 318e90015db62434b312c9c6becc59e897af7d8c Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 21 Jun 2017 02:03:03 -0400
Subject: [PATCH 6/7] test(tests/lean/run/cached): add test for cached

---
 tests/lean/run/cached.lean | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 tests/lean/run/cached.lean

diff --git a/tests/lean/run/cached.lean b/tests/lean/run/cached.lean
new file mode 100644
index 0000000000..444339cb88
--- /dev/null
+++ b/tests/lean/run/cached.lean
@@ -0,0 +1,2 @@
+#eval let c := cached.mk 2 in c
+#eval let c := cached.mk 2 in c.update 3 c

From 5ffc462b8531992ffa960928e633bad08d3fcfa7 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 21 Jun 2017 04:06:03 -0400
Subject: [PATCH 7/7] feat(init/data/cached): add simp theorems for cached

---
 library/data/hashed_func.lean |  3 +++
 library/init/data/cached.lean | 15 +++++++++++++--
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/library/data/hashed_func.lean b/library/data/hashed_func.lean
index 88d95d1d0c..01b190e162 100644
--- a/library/data/hashed_func.lean
+++ b/library/data/hashed_func.lean
@@ -49,4 +49,7 @@ namespace hashed_func
 
   instance : has_coe_to_fun (hashed_func α β) := ⟨_, hashed_func.eval⟩
 
+  @[simp] theorem eval_val : ∀ hf : hashed_func α β, eval hf = hf.func
+  | ⟨f, hash_fn, c⟩ := funext $ λ a, by rw [c.cache_eq_empty]; refl
+
 end hashed_func
diff --git a/library/init/data/cached.lean b/library/init/data/cached.lean
index f9f459b9b4..f0b7f0a07d 100644
--- a/library/init/data/cached.lean
+++ b/library/init/data/cached.lean
@@ -21,16 +21,22 @@ namespace cached
   def lift_on (c : cached α) (f : α → β) (h : ∀ x, f (default _) = f x) : β :=
   quot.lift f (λx y _, (h x).symm.trans (h y)) c.val
 
-  def lift_eq {f : α → β} {h} (x) : lift_on (mk x) f h = f x := rfl
-
   -- This function has a VM implementation to change the value of the cache `c` to `v`
   def update (c : cached α) (v : α) (f : thunk β) : β := f ()
 
+  @[simp] lemma update_def (c : cached α) (v : α) (f : thunk β) :
+    @update _ _ _ c v f = f () := rfl
+
   def reset (c : cached α) : thunk β → β := update c (default α)
 
+  @[simp] lemma reset_def (c : cached α) (f : thunk β) :
+    @reset _ _ _ c f = f () := rfl
+
   theorem cache_eq_empty : ∀ (c : cached α), c = empty
   | ⟨q⟩ := congr_arg mk' $ quot.ind (λx, quot.sound trivial) q
 
+  @[simp] lemma lift_mk {f : α → β} {h} (x) : lift_on (mk x) f h = f x := rfl
+
   meta def inspect (c : cached α) : α := unchecked_cast c.val
 
   meta instance [has_to_string α] : has_to_string (cached α) := ⟨to_string ∘ inspect⟩
@@ -59,6 +65,11 @@ namespace memoized
       | some ⟨x, h⟩ := h
       end)
 
+  @[simp] theorem mk_eval (f : unit → α) : (@mk _ f).eval = f () := rfl
+
+  @[simp] theorem eval_val : ∀ (f : memoized α), eval f = f.func ()
+  | ⟨f, c⟩ := congr_arg (λ c', eval ⟨f, c'⟩) c.cache_eq_empty
+
   instance : has_coe_to_fun (memoized α) := ⟨λ_, thunk α, λm _, m.eval⟩
 
   instance : has_coe (memoized α) α := ⟨λm, m.eval⟩