fix: use reducible transparency when producing no_confusion_type and injectivity lemmas

src/library/constructions/injective.cpp

@@ -59,8 +59,8 @@ static void collect_args(type_context_old & tctx, expr const & type, unsigned nu
 }
 
 expr mk_injective_type_core(environment const & env, name const & ir_name, expr const & ir_type, unsigned num_params, level_param_names const & lp_names, bool use_eq) {
-    // The transparency needs to match the kernel since we need to be consistent with the no_confusion construction.
-    type_context_old ctx(env, transparency_mode::All);
+    // The transparency needs to match the one in `no_confusion`
+    type_context_old ctx(env, transparency_mode::Reducible);
     buffer<expr> params, args1, args2, new_args;
     collect_args(ctx, ir_type, num_params, params, args1, args2, new_args);
     expr c_ir_params = mk_app(mk_constant(ir_name, param_names_to_levels(lp_names)), params);

src/library/constructions/no_confusion.cpp

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/normalize.h"
 #include "library/scoped_ext.h"
+#include "library/type_context.h"
 #include "library/aux_recursors.h"
 #include "library/constructions/util.h"
 
@@ -75,6 +76,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
     expr cases_on1 = mk_app(cases_on, v1);
     expr cases_on2 = mk_app(cases_on, v2);
     type_checker tc(env);
+    type_context_old ctx(env, transparency_mode::Reducible);
     expr t1        = tc.infer(cases_on1);
     expr t2        = tc.infer(cases_on2);
     buffer<expr> outer_cases_on_args;
@@ -104,7 +106,8 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
                         expr rhs_type = mlocal_type(rhs);
                         level l       = sort_level(tc.ensure_type(lhs_type));
                         expr h_type;
-                        if (tc.is_def_eq(lhs_type, rhs_type)) {
+                        // use `ctx` not `tc` here, as we want them to be reducibly defeq
+                        if (ctx.is_def_eq(lhs_type, rhs_type)) {
                             h_type = mk_app(mk_constant(get_eq_name(), to_list(l)), lhs_type, lhs, rhs);
                         } else {
                             h_type = mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs);

tests/lean/no_confusion_type.lean

@@ -11,3 +11,18 @@ constants v1 v2 : vector nat 2
 constant  P     : Type
 #reduce vector.no_confusion_type P (vector.vcons a1 v1) (vector.vcons a2 v2)
 end Ex
+
+namespace ExSemiReducible
+open nat
+
+def wrapped_nat (n : nat) := nat
+
+structure with_wrapped : Type :=
+(n : nat)
+(m : wrapped_nat n)
+
+#check with_wrapped.no_confusion_type
+constants (P : Type) (n1 n2 : nat) (m1 : wrapped_nat n1) (m2 : wrapped_nat n2)
+#reduce with_wrapped.no_confusion_type P (with_wrapped.mk _ m1) (with_wrapped.mk _ m2)
+
+end ExSemiReducible

tests/lean/no_confusion_type.lean.expected.out

@@ -1,2 +1,4 @@
 vector.no_confusion_type : Sort u_1 → vector ?M_1 ?M_2 → vector ?M_1 ?M_2 → Sort u_1
 (2 = 2 → a1 = a2 → v1 == v2 → P) → P
+with_wrapped.no_confusion_type : Sort u_1 → with_wrapped → with_wrapped → Sort u_1
+(n1 = n2 → m1 == m2 → P) → P

tests/lean/run/simp_constructor.lean

@@ -19,6 +19,17 @@ inductive vec (α : Type u) : nat → Type u
 
 #check @vec.cons.inj_eq
 
+def wrapped_nat (n : nat) := nat
+
+structure with_wrapped : Type :=
+(n : nat)
+(m : wrapped_nat n)
+
+-- #812: this should use `==` not `=` as `m` and `m'` are not reducibly defeq
+#check (@with_wrapped.mk.inj_eq :
+  ∀ {n : ℕ} {m : wrapped_nat n} {n' : ℕ} {m' : wrapped_nat n'},
+    with_wrapped.mk n m = with_wrapped.mk n' m' = (n = n' ∧ m == m'))
+
 example (a b : nat) (h : a == b) : a + 1 = b + 1 :=
 begin
   subst h