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

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

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

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;

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