From efabd2280ca0daa06cef24d6610932a59769a4b2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Jul 2014 00:43:10 -0700
Subject: [PATCH] feat(library/unifier): allow unifier to unfold opaque
 definitions of the current module

It is not clear whether this is a good idea or not. In some cases, it seems to do more harm than good.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/bit.lean    | 15 +++++++++++++++
 library/standard/logic.lean  |  5 ++++-
 src/library/unifier.cpp      |  2 +-
 tests/lean/run/tactic23.lean |  2 +-
 4 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/library/standard/bit.lean b/library/standard/bit.lean
index ac963a1131..227b144969 100644
--- a/library/standard/bit.lean
+++ b/library/standard/bit.lean
@@ -20,4 +20,19 @@ theorem cond_b0 {A : Type} (t e : A) : cond b0 t e = e
 
 theorem cond_b1 {A : Type} (t e : A) : cond b1 t e = t
 := refl (cond b1 t e)
+
+definition bor (a b : bit)
+:= bit_rec (bit_rec b0 b1 b) b1 a
+
+theorem bor_b1_left (a : bit) : bor b1 a = b1
+:= refl (bor b1 a)
+
+theorem bor_b1_right (a : bit) : bor a b1 = b1
+:= bit_rec (refl (bor b0 b1)) (refl (bor b1 b1)) a
+
+theorem bor_b0_left (a : bit) : bor b0 a = a
+:= bit_rec (refl (bor b0 b0)) (refl (bor b0 b1)) a
+
+theorem bor_b0_right (a : bit) : bor a b0 = a
+:= bit_rec (refl (bor b0 b0)) (refl (bor b1 b0)) a
 end
diff --git a/library/standard/logic.lean b/library/standard/logic.lean
index 682466ddbe..f528877922 100644
--- a/library/standard/logic.lean
+++ b/library/standard/logic.lean
@@ -226,8 +226,11 @@ definition cast {A B : Type} (H : A = B) (a : A) : B
 theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a
 := refl (cast (refl A) a)
 
+theorem cast_proof_irrel {A B : Type} (H1 H2 : A = B) (a : A) : cast H1 a = cast H2 a
+:= refl (cast H1 a)
+
 theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a
-:= calc cast H a = cast (refl A) a : refl (cast H a) -- by proof irrelevance
+:= calc cast H a = cast (refl A) a : cast_proof_irrel H (refl A) a
             ...  = a               : cast_refl a
 
 definition heq {A B : Type} (a : A) (b : B) := ∃ H, cast H a = b
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index f3d2fb2d8f..ac362e5642 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -335,7 +335,7 @@ struct unifier_fn {
                name_generator const & ngen, substitution const & s, unifier_plugin const & p,
                bool use_exception, unsigned max_steps):
         m_env(env), m_ngen(ngen), m_subst(s), m_plugin(p),
-        m_tc(env, m_ngen.mk_child()),
+        m_tc(env, m_ngen.mk_child(), mk_default_converter(env, optional<module_idx>(0))),
         m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) {
         m_next_assumption_idx = 0;
         m_next_cidx = 0;
diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean
index b61029e682..163cecb25a 100644
--- a/tests/lean/run/tactic23.lean
+++ b/tests/lean/run/tactic23.lean
@@ -29,7 +29,7 @@ definition assump : tactic := eassumption
 theorem T1 {p : nat → Bool} {a : nat } (H : p (a+2)) : ∃ x, p (succ x)
 := by apply exists_intro; assump
 
-definition is_zero [inline] (n : nat)
+definition is_zero (n : nat)
 := nat_rec true (λ n r, false) n
 
 theorem T2 : ∃ a, (is_zero a) = true