From 05f7917ad239ac2836ab2fa8bcdb905509dbec5f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 14 Jun 2023 11:55:57 +0000 Subject: [PATCH 1/3] fix: use semireducible transparency when producing `no_confusion_type` and injectivity lemmas --- src/library/constructions/injective.cpp | 4 ++-- src/library/constructions/no_confusion.cpp | 4 +++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp index da2a2ac356..612e846487 100644 --- a/src/library/constructions/injective.cpp +++ b/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::Semireducible); buffer 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); diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index df79e3068a..9a032f92d5 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -75,6 +75,7 @@ optional 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::Semireducible); expr t1 = tc.infer(cases_on1); expr t2 = tc.infer(cases_on2); buffer outer_cases_on_args; @@ -104,7 +105,8 @@ optional 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); From ef0371baa1b2362fdc40b2e6e1ec4ab08ef30582 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 14 Jun 2023 12:05:38 +0000 Subject: [PATCH 2/3] fix and add test --- src/library/constructions/no_confusion.cpp | 1 + tests/lean/no_confusion_type.lean | 15 +++++++++++++++ tests/lean/no_confusion_type.lean.expected.out | 2 ++ 3 files changed, 18 insertions(+) diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 9a032f92d5..83219ddb42 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/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" diff --git a/tests/lean/no_confusion_type.lean b/tests/lean/no_confusion_type.lean index cbcfeae1b9..59a6fd43a7 100644 --- a/tests/lean/no_confusion_type.lean +++ b/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 : fin n1) (m2 : fin n2) +#reduce with_wrapped.no_confusion_type P (with_wrapped.mk _ m1) (with_wrapped.mk _ m2) + +end Ex diff --git a/tests/lean/no_confusion_type.lean.expected.out b/tests/lean/no_confusion_type.lean.expected.out index 089ba2260f..aa9fb08ba8 100644 --- a/tests/lean/no_confusion_type.lean.expected.out +++ b/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 From db2dcfb1006c12534cc8f5b80d230b4c7ff0693d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 14 Jun 2023 12:27:39 +0000 Subject: [PATCH 3/3] fix --- src/library/constructions/injective.cpp | 2 +- src/library/constructions/no_confusion.cpp | 2 +- tests/lean/no_confusion_type.lean | 4 ++-- tests/lean/run/simp_constructor.lean | 11 +++++++++++ 4 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp index 612e846487..e85aaa21b7 100644 --- a/src/library/constructions/injective.cpp +++ b/src/library/constructions/injective.cpp @@ -60,7 +60,7 @@ 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 one in `no_confusion` - type_context_old ctx(env, transparency_mode::Semireducible); + type_context_old ctx(env, transparency_mode::Reducible); buffer 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); diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 83219ddb42..429d516a78 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -76,7 +76,7 @@ optional 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::Semireducible); + type_context_old ctx(env, transparency_mode::Reducible); expr t1 = tc.infer(cases_on1); expr t2 = tc.infer(cases_on2); buffer outer_cases_on_args; diff --git a/tests/lean/no_confusion_type.lean b/tests/lean/no_confusion_type.lean index 59a6fd43a7..0d6f75f5b4 100644 --- a/tests/lean/no_confusion_type.lean +++ b/tests/lean/no_confusion_type.lean @@ -22,7 +22,7 @@ structure with_wrapped : Type := (m : wrapped_nat n) #check with_wrapped.no_confusion_type -constants (P : Type) (n1 n2 : nat) (m1 : fin n1) (m2 : fin n2) +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 Ex +end ExSemiReducible diff --git a/tests/lean/run/simp_constructor.lean b/tests/lean/run/simp_constructor.lean index 281d6ff35c..a389c4dc04 100644 --- a/tests/lean/run/simp_constructor.lean +++ b/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