diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 7767d3d9e..6b98187dc 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -106,6 +106,10 @@ namespace eq definition inv_inv (p : x = y) : p⁻¹⁻¹ = p := eq.rec_on p idp + -- auxiliary definition used by 'cases' tactic + definition elim_inv_inv {A : Type} {a b : A} {C : a = b → Type} (H₁ : a = b) (H₂ : C (H₁⁻¹⁻¹)) : C H₁ := + eq.rec_on (inv_inv H₁) H₂ + /- Theorems for moving things around in equations -/ definition con_eq_of_eq_inv_con (p : x = z) (q : y = z) (r : y = x) : diff --git a/src/library/constants.cpp b/src/library/constants.cpp index f177ae7fa..74d6051a7 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -15,6 +15,7 @@ name const * g_char = nullptr; name const * g_char_mk = nullptr; name const * g_dite = nullptr; name const * g_eq = nullptr; +name const * g_eq_elim_inv_inv = nullptr; name const * g_eq_intro = nullptr; name const * g_eq_rec = nullptr; name const * g_eq_rec_eq = nullptr; @@ -126,6 +127,7 @@ void initialize_constants() { g_char_mk = new name{"char", "mk"}; g_dite = new name{"dite"}; g_eq = new name{"eq"}; + g_eq_elim_inv_inv = new name{"eq", "elim_inv_inv"}; g_eq_intro = new name{"eq", "intro"}; g_eq_rec = new name{"eq", "rec"}; g_eq_rec_eq = new name{"eq_rec_eq"}; @@ -238,6 +240,7 @@ void finalize_constants() { delete g_char_mk; delete g_dite; delete g_eq; + delete g_eq_elim_inv_inv; delete g_eq_intro; delete g_eq_rec; delete g_eq_rec_eq; @@ -349,6 +352,7 @@ name const & get_char_name() { return *g_char; } name const & get_char_mk_name() { return *g_char_mk; } name const & get_dite_name() { return *g_dite; } name const & get_eq_name() { return *g_eq; } +name const & get_eq_elim_inv_inv_name() { return *g_eq_elim_inv_inv; } name const & get_eq_intro_name() { return *g_eq_intro; } name const & get_eq_rec_name() { return *g_eq_rec; } name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; } diff --git a/src/library/constants.h b/src/library/constants.h index 2e31f5ddc..cc706c778 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -17,6 +17,7 @@ name const & get_char_name(); name const & get_char_mk_name(); name const & get_dite_name(); name const & get_eq_name(); +name const & get_eq_elim_inv_inv_name(); name const & get_eq_intro_name(); name const & get_eq_rec_name(); name const & get_eq_rec_eq_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index c60daae77..ccbe1cb8d 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -10,6 +10,7 @@ char char.mk dite eq +eq.elim_inv_inv eq.intro eq.rec eq_rec_eq diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 31a8265a3..07fba1c70 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -708,12 +708,12 @@ class inversion_tac { buffer hyps; g.get_hyps(hyps); lean_assert(!hyps.empty()); - expr eq = hyps.back(); - buffer eq_args; - get_app_args(mlocal_type(eq), eq_args); - expr const & A = whnf(eq_args[0]); - expr lhs = whnf(eq_args[1]); - expr rhs = whnf(eq_args[2]); + expr Heq = hyps.back(); + buffer Heq_args; + get_app_args(mlocal_type(Heq), Heq_args); + expr const & A = whnf(Heq_args[0]); + expr lhs = whnf(Heq_args[1]); + expr rhs = whnf(Heq_args[2]); constraint_seq cs; if (m_proof_irrel && m_tc.is_def_eq(lhs, rhs, justification(), cs) && !cs) { // deletion transition: t == t @@ -744,7 +744,7 @@ class inversion_tac { else throw inversion_exception(); } - expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(g_lvl, const_levels(A_fn))), A_args), g_type, lhs, rhs, eq); + expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(g_lvl, const_levels(A_fn))), A_args), g_type, lhs, rhs, Heq); if (const_name(lhs_fn) == const_name(rhs_fn)) { // injectivity transition expr new_type = binding_domain(whnf(infer_type(no_confusion))); @@ -759,14 +759,14 @@ class inversion_tac { lean_assert(lhs_args.size() >= A_nparams); return unify_eqs(new_g, neqs - 1 + lhs_args.size() - A_nparams); } else { - // conflict transition, eq is of the form c_1 ... = c_2 ..., where c_1 and c_2 are different constructors/intro rules. + // conflict transition, Heq is of the form c_1 ... = c_2 ..., where c_1 and c_2 are different constructors/intro rules. expr val = lift_down(no_confusion); assign(g, val); return optional(); // goal has been solved } } if (is_local(rhs)) { - // solution transition, eq is of the form t = y, where y is a local constant + // solution transition, Heq is of the form t = y, where y is a local constant // assume the current goal is of the form // @@ -806,7 +806,7 @@ class inversion_tac { if (m_proof_irrel) tformer = Fun(rhs, deps_g_type); else - tformer = Fun(rhs, Fun(eq, deps_g_type)); + tformer = Fun(rhs, Fun(Heq, deps_g_type)); expr eq_rec = mk_constant(get_eq_rec_name(), {eq_rec_lvl1, eq_rec_lvl2}); eq_rec = mk_app(eq_rec, A, lhs, tformer); buffer new_hyps; @@ -815,7 +815,7 @@ class inversion_tac { store_rename(rhs, lhs); replace(m_imps, rhs, lhs); if (!m_proof_irrel) { - new_type = abstract_local(new_type, eq); + new_type = abstract_local(new_type, Heq); new_type = instantiate(new_type, mk_refl(m_tc, lhs)); } buffer new_deps; @@ -833,24 +833,49 @@ class inversion_tac { expr new_meta = mk_app(new_mvar, new_hyps); goal new_g(new_meta, new_type); expr eq_rec_minor = mk_app(new_mvar, non_deps); - eq_rec = mk_app(eq_rec, eq_rec_minor, rhs, eq); + eq_rec = mk_app(eq_rec, eq_rec_minor, rhs, Heq); expr val = mk_app(eq_rec, deps); assign(g, val); return unify_eqs(new_g, neqs-1); } } else if (is_local(lhs)) { // flip equation and reduce to previous case - if (m_proof_irrel || !depends_on(g_type, hyps.back())) - hyps.pop_back(); // remove processed equality expr symm_eq = mk_eq(rhs, lhs).first; - expr new_type = mk_arrow(symm_eq, g_type); - expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type)); - expr new_meta = mk_app(new_mvar, hyps); - goal new_g(new_meta, new_type); - expr eq_inv = mk_symm(m_tc, eq); - expr val = mk_app(new_meta, eq_inv); - assign(g, val); - return unify_eqs(new_g, neqs); + hyps.pop_back(); // remove processed equality + if (!depends_on(g_type, Heq)) { + expr new_type = mk_arrow(symm_eq, g_type); + expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type)); + expr new_meta = mk_app(new_mvar, hyps); + goal new_g(new_meta, new_type); + expr Heq_inv = mk_symm(m_tc, Heq); + expr val = mk_app(new_meta, Heq_inv); + assign(g, val); + return unify_eqs(new_g, neqs); + } else { + // Let C[Heq] be the original conclusion which depends on the equality eq being processed. + expr new_Heq = update_mlocal(Heq, symm_eq); + expr new_Heq_inv = mk_symm(m_tc, new_Heq); + expr new_type = Pi(new_Heq, instantiate(abstract_local(g_type, Heq), new_Heq_inv)); + expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type)); + expr new_meta = mk_app(new_mvar, hyps); + goal new_g(new_meta, new_type); + // Then, we have + // new_meta : Pi (new_Heq : rhs = lhs), C[symm new_Heq] + expr Heq_inv = mk_symm(m_tc, Heq); + expr val = mk_app(new_meta, Heq_inv); + // val : C[symm (symm Heq)] + // Remark: in proof irrelevant mode (symm (symm Heq)) is definitionally equal to Heq + if (!m_proof_irrel) { + expr C = Fun(Heq, g_type); + level A_lvl = sort_level(m_tc.ensure_type(A).first); + level g_lvl = sort_level(m_tc.ensure_type(g_type).first); + expr elim_inv_inv = mk_constant(get_eq_elim_inv_inv_name(), {A_lvl, g_lvl}); + val = mk_app({elim_inv_inv, A, lhs, rhs, C, Heq, val}); + // val : C[Heq] as we wanted + } + assign(g, val); + return unify_eqs(new_g, neqs); + } } if (m_throw_tactic_exception) { throw tactic_exception([=](formatter const & fmt) { diff --git a/tests/lean/hott/481.hlean b/tests/lean/hott/481.hlean new file mode 100644 index 000000000..48b156c7e --- /dev/null +++ b/tests/lean/hott/481.hlean @@ -0,0 +1,8 @@ +open equiv eq is_equiv is_trunc + +definition foo {A B : Type} (f : A ≃ B) (f' : A → B) + (H' : is_equiv f') (p : to_fun f = f') : p = p := +begin + cases p, + esimp +end