diff --git a/src/library/inductive_compiler/ginductive.cpp b/src/library/inductive_compiler/ginductive.cpp index db19901d68..c18645dac3 100644 --- a/src/library/inductive_compiler/ginductive.cpp +++ b/src/library/inductive_compiler/ginductive.cpp @@ -15,6 +15,13 @@ Author: Daniel Selsam #include "library/kernel_serializer.h" namespace lean { +optional is_gintro_rule_app(environment const & env, expr const & e) { + expr const & fn = get_app_fn(e); + if (!is_constant(fn)) return optional(); + if (!is_ginductive_intro_rule(env, const_name(fn))) return optional(); + return optional(const_name(fn)); +} + expr whnf_ginductive(type_context & ctx, expr const & e) { return ctx.whnf_head_pred(e, [&](expr const & e) { if (is_macro(e)) return true; @@ -24,6 +31,13 @@ expr whnf_ginductive(type_context & ctx, expr const & e) { }); } +expr whnf_gintro_rule(type_context & ctx, expr const & e) { + return ctx.whnf_head_pred(e, [&](expr const & e) { + if (is_macro(e)) return true; + return !is_gintro_rule_app(ctx.env(), e); + }); +} + static unsigned compute_idx_number(expr const & e) { buffer args; unsigned idx = 0; diff --git a/src/library/inductive_compiler/ginductive.h b/src/library/inductive_compiler/ginductive.h index c62a7118b7..ec037a498d 100644 --- a/src/library/inductive_compiler/ginductive.h +++ b/src/library/inductive_compiler/ginductive.h @@ -32,9 +32,15 @@ unsigned get_ginductive_num_indices(environment const & env, name const & ind_na /* \brief Returns the names of all types that are mutually inductive with \e ind_name */ list get_ginductive_mut_ind_names(environment const & env, name const & ind_name); -/* Return \c e until it is in weak head normal form OR the head is a ginductive datatype. */ +/* Normalize \c e until it is in weak head normal form OR the head is a ginductive datatype. */ expr whnf_ginductive(type_context & ctx, expr const & e); +/* Normalize \c e until it is in weak head normal form OR the head is a ginductive intro rule (aka constructor) */ +expr whnf_gintro_rule(type_context & ctx, expr const & e); + +/* Similar to is_constructor_app, but takes generalized introduction rules into account. */ +optional is_gintro_rule_app(environment const & env, expr const & e); + /* \brief Returns the offset of a simulated introduction rule. Example: diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 79aab83c7c..87ad496a47 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/app_builder.h" #include "library/inverse.h" #include "library/trace.h" +#include "library/constructions/injective.h" #include "library/vm/vm_list.h" #include "library/vm/vm_name.h" #include "library/vm/vm_expr.h" @@ -331,8 +332,8 @@ struct cases_tactic_fn { lean_assert(is_pi(target) && is_arrow(target)); if (is_eq(binding_domain(target), lhs, rhs)) { type_context ctx = mk_type_context_for(mvar); - expr lhs_n = ctx.whnf(lhs); - expr rhs_n = ctx.whnf(rhs); + expr lhs_n = whnf_gintro_rule(ctx, lhs); + expr rhs_n = whnf_gintro_rule(ctx, rhs); if (lhs != lhs_n || rhs != rhs_n) { expr new_eq = ::lean::mk_eq(ctx, lhs_n, rhs_n); expr new_target = mk_arrow(new_eq, binding_body(target)); @@ -410,23 +411,99 @@ struct cases_tactic_fn { throw_exception(mvar, "cases tactic failed, unexpected failure when using inverse"); } } else { - optional c1 = is_constructor_app(m_env, lhs); - optional c2 = is_constructor_app(m_env, rhs); - A = ctx.whnf(A); - buffer A_args; - expr const & A_fn = get_app_args(A, A_args); - if (!is_constant(A_fn) || !inductive::is_inductive_decl(m_env, const_name(A_fn))) - throw_ill_formed_datatype(); - name no_confusion_name(const_name(A_fn), "no_confusion"); - if (!m_env.find(no_confusion_name)) { - throw exception(sstream() << "cases tactic failed, construction '" - << no_confusion_name << "' is not available in the environment"); + optional c1 = is_gintro_rule_app(m_env, lhs); + optional c2 = is_gintro_rule_app(m_env, rhs); + if (!c1 || !c2) { + auto s = mk_tactic_state(mvar); + throw cases_tactic_exception { s, [=] { + return format("cases tactic failed, unsupported equality between type and constructor indices") + line() + + format("(only equalities between constructors and/or variables are supported, try cases on the indices):") + line() + + s.pp_expr(H_type) + line(); + }}; } - expr target = g1.get_type(); - level target_lvl = get_level(ctx, target); - expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(target_lvl, const_levels(A_fn))), - A_args), target, lhs, rhs, H); - if (c1 && c2) { + + if (!is_constructor_app(m_env, lhs) || !is_constructor_app(m_env, rhs)) { + /* lhs or rhs is not a kernel constructor application, + that is, it is a generalized constructor generated by + the inductive compiler. */ + if (*c1 == *c2) { + /* + lhs and rhs are of the form (C ...) where C is a generalized constructor. + We use the inj_arrow lemma to break equation into pieces. + We cannot use no_confusion because it would leak the internal encoding + used in the kernel. + */ + A = whnf_ginductive(ctx, A); + expr const & A_fn = get_app_fn(A); + if (!is_constant(A_fn) || !is_ginductive(m_env, const_name(A_fn))) + throw_ill_formed_datatype(); + name inj_arrow_name = mk_injective_arrow_name(*c1); + optional inj_arrow_decl = m_env.find(inj_arrow_name); + if (!inj_arrow_decl) { + throw exception(sstream() << "cases tactic failed, construction '" + << inj_arrow_name << "' is not available in the environment"); + } + unsigned inj_arrow_arity = get_arity(inj_arrow_decl->get_type()); + expr target = g1.get_type(); + if (!ctx.is_prop(target)) { + /* TODO(Leo): refine this limitation. + Actually, we only need to disallow this case if the cases tactic + is being used by the equation compiler. + Reason: we don't have support for inj_arrow in the code that + generate proofs for equational lemmas produced by equational compiler. + */ + throw exception(sstream() << "cases tactic failed, target is not a proposition, " + "dependent elimination is currently not supported in this cases because one of the indices " + "is an inductive datatype of '" << const_name(A_fn) << "', and this is a nested and/or mutually " + "recursive datatype"); + } + expr inj_arrow = mk_app(ctx, inj_arrow_name, inj_arrow_arity - 1, H, target); + lean_cases_trace(mvar, tout() << "injection\n";); + expr new_target = binding_domain(ctx.whnf(ctx.infer(inj_arrow))); + expr mvar2 = m_mctx.mk_metavar_decl(lctx, new_target); + expr val = mk_app(inj_arrow, mvar2); + m_mctx.assign(*mvar1, val); + unsigned A_nparams = get_ginductive_num_params(m_env, const_name(A_fn)); + lean_assert(get_app_num_args(lhs) >= A_nparams); + return unify_eqs(mvar2, num_eqs - 1 + get_app_num_args(lhs) - A_nparams, + updating, new_intros, subst); + } else { + lean_assert(*c1 != *c2); + /* + lhs and rhs are generalized constructor applications, but with different constructors. + Thus, we normalize both of them to make sure we can use no_confusion + */ + expr lhs_n = ctx.whnf(lhs); + expr rhs_n = ctx.whnf(rhs); + lean_assert(lhs != lhs_n || rhs != rhs_n); + expr new_eq = ::lean::mk_eq(ctx, lhs_n, rhs_n); + expr new_target = mk_arrow(new_eq, binding_body(target)); + expr new_mvar = m_mctx.mk_metavar_decl(lctx, new_target); + m_mctx.assign(mvar, new_mvar); + lean_cases_trace(mvar, tout() << "normalize generalized constructors at lhs/rhs:\n" << pp_goal(mvar) << "\n";); + return unify_eqs(new_mvar, num_eqs, updating, new_intros, subst); + } + } else { + /* + lhs and rhs are kernel constructor applications. + We use no_confusion to perform dependent elimination. + */ + lean_assert(is_constructor_app(lhs)); + lean_assert(is_constructor_app(rhs)); + A = ctx.whnf(A); + buffer A_args; + expr const & A_fn = get_app_args(A, A_args); + if (!is_constant(A_fn) || !inductive::is_inductive_decl(m_env, const_name(A_fn))) + throw_ill_formed_datatype(); + name no_confusion_name(const_name(A_fn), "no_confusion"); + if (!m_env.find(no_confusion_name)) { + throw exception(sstream() << "cases tactic failed, construction '" + << no_confusion_name << "' is not available in the environment"); + } + expr target = g1.get_type(); + level target_lvl = get_level(ctx, target); + expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(target_lvl, const_levels(A_fn))), + A_args), target, lhs, rhs, H); if (*c1 == *c2) { lean_cases_trace(mvar, tout() << "injection\n";); expr new_target = binding_domain(ctx.whnf(ctx.infer(no_confusion))); @@ -438,19 +515,11 @@ struct cases_tactic_fn { return unify_eqs(mvar2, num_eqs - 1 + get_app_num_args(lhs) - A_nparams, updating, new_intros, subst); } else { - /* conflict, closes the goal */ - lean_cases_trace(*mvar1, tout() << "conflicting equality detected, " - "closing goal using no_confusion\n";); + lean_assert(*c1 != *c2); m_mctx.assign(*mvar1, no_confusion); return none_expr(); } } - auto s = mk_tactic_state(mvar); - throw cases_tactic_exception { s, [=] { - return format("cases tactic failed, unsupported equality between type and constructor indices") + line() - + format("(only equalities between constructors and/or variables are supported, try cases on the indices):") + line() - + s.pp_expr(H_type) + line(); - }}; } } else { throw_exception(mvar, "cases tactic failed, equality expected"); diff --git a/tests/lean/cases_ginductive.lean b/tests/lean/cases_ginductive.lean new file mode 100644 index 0000000000..c985346b15 --- /dev/null +++ b/tests/lean/cases_ginductive.lean @@ -0,0 +1,96 @@ +inductive term +| const (c : string) : term +| app (fn : string) (ts : list term) : term + +mutual inductive is_rename, is_rename_lst +with is_rename : term → string → string → term → Prop +| const_eq (c₁ c₂) : is_rename (term.const c₁) c₁ c₂ (term.const c₂) +| const_ne (c₁ c₂ c₃) (hne : c₁ ≠ c₂) : is_rename (term.const c₁) c₂ c₃ (term.const c₁) +| app (fn c₁ c₂ ts₁ ts₂) (h₁ : is_rename_lst ts₁ c₁ c₂ ts₂) : is_rename (term.app fn ts₁) c₁ c₂ (term.app fn ts₂) +with is_rename_lst : list term → string → string → list term → Prop +| nil (c₁ c₂) : is_rename_lst [] c₁ c₂ [] +| cons (t₁ ts₁ t₂ ts₂ c₁ c₂) (h₁ : is_rename t₁ c₁ c₂ t₂) (h₂ : is_rename_lst ts₁ c₁ c₂ ts₂) : is_rename_lst (t₁::ts₁) c₁ c₂ (t₂::ts₂) + +mutual def term.ind, term_list.ind + (p : term → Prop) (ps : list term → Prop) + (h₁ : ∀ c, p (term.const c)) + (h₂ : ∀ fn ts, ps ts → p (term.app fn ts)) + (h₃ : ps []) + (h₄ : ∀ t ts, p t → ps ts → ps (t::ts)) +with term.ind : ∀ t : term, p t +| (term.const c) := h₁ c +| (term.app fn ts) := h₂ fn ts (term_list.ind ts) +with term_list.ind : ∀ ts : list term, ps ts +| [] := h₃ +| (t::ts) := h₄ t ts (term.ind t) (term_list.ind ts) + +lemma term.ind_on + (p : term → Prop) (ps : list term → Prop) + (t : term) + (h₁ : ∀ c, p (term.const c)) + (h₂ : ∀ fn ts, ps ts → p (term.app fn ts)) + (h₃ : ps []) + (h₄ : ∀ t ts, p t → ps ts → ps (t::ts)) : p t := +term.ind p ps h₁ h₂ h₃ h₄ t + +lemma is_rename_det : ∀ t₁ t₂ t₂' c₁ c₂, is_rename t₁ c₁ c₂ t₂ → is_rename t₁ c₁ c₂ t₂' → t₂ = t₂' := +begin + intro t₁, + apply term.ind_on + (λ t₁ : term, ∀ t₂ t₂' c₁ c₂, is_rename t₁ c₁ c₂ t₂ → is_rename t₁ c₁ c₂ t₂' → t₂ = t₂') + (λ ts₁ : list term, ∀ ts₂ ts₂' c₁ c₂, is_rename_lst ts₁ c₁ c₂ ts₂ → is_rename_lst ts₁ c₁ c₂ ts₂' → ts₂ = ts₂') + t₁, + { intros c₁ t₂ t₂' c₁' c₂ h₁ h₂, + cases h₁; cases h₂; trace_state; { refl <|> contradiction } }, + { intros fn ts ih t₂ t₂' c₁ c₂ h₁ h₂, cases h₁; cases h₂, trace_state, + have := ih _ _ _ _ h₁_1 h₁_2, + simp [*] }, + { intros ts₂ ts₂' c₁ c₂ h₁ h₂, + cases h₁; cases h₂; refl }, + { intros t ts ih₁ ih₂ ts₂ ts₂' c₁ c₂ h₁ h₂, + cases h₁; cases h₂, + have := ih₁ _ _ _ _ h₁_1 h₁_2, + have := ih₂ _ _ _ _ h₂_1 h₂_2, + simp [*] } +end + +mutual def is_rename.ind, is_rename_lst.ind + (p : ∀ {t₁ c₁ c₂ t₂}, is_rename t₁ c₁ c₂ t₂ → Prop) + (ps : ∀ {ts₁ c₁ c₂ ts₂}, is_rename_lst ts₁ c₁ c₂ ts₂ → Prop) + (h₁ : ∀ (c₁ c₂ : string), p (is_rename.const_eq c₁ c₂)) + (h₂ : ∀ (c₁ c₂ c₃ : string) (hne : c₁ ≠ c₂), p (is_rename.const_ne c₁ c₂ c₃ hne)) + (h₃ : ∀ (fn c₁ c₂ ts₁ ts₂ h) (ih : ps h), p (is_rename.app fn c₁ c₂ ts₁ ts₂ h)) + (h₄ : ∀ (c₁ c₂ : string), ps (is_rename_lst.nil c₁ c₂)) + (h₅ : ∀ (t₁ ts₁ t₂ ts₂ c₁ c₂ h₁ h₂) (ih₁ : p h₁) (ih₂ : ps h₂), ps (is_rename_lst.cons t₁ ts₁ t₂ ts₂ c₁ c₂ h₁ h₂)) +with is_rename.ind : ∀ (t₁ c₁ c₂ t₂) (h : is_rename t₁ c₁ c₂ t₂), p h +| (term.const c) := + begin + intros c₁ c₂ t₂ hr, + cases t₂; cases hr, + { apply h₁ }, + { apply h₂, assumption } + end +| (term.app fn ts₁) := + have ih : ∀ (c₁ c₂ ts₂) (h : is_rename_lst ts₁ c₁ c₂ ts₂), ps h, from is_rename_lst.ind ts₁, + begin + intros c₁ c₂ t₂ hr, + cases t₂; cases hr, + apply h₃, apply ih, assumption + end + +with is_rename_lst.ind : ∀ (ts₁ c₁ c₂ ts₂) (h : is_rename_lst ts₁ c₁ c₂ ts₂), ps h +| [] := + begin + intros c₁ c₂ ts₂ hr, + cases ts₂; cases hr, apply h₄ + end +| (t₁::ts₁) := + have ih₁ : ∀ (c₁ c₂ t₂) (h : is_rename t₁ c₁ c₂ t₂), p h, from is_rename.ind t₁, + have ih₂ : ∀ (c₁ c₂ ts₂) (h : is_rename_lst ts₁ c₁ c₂ ts₂), ps h, from is_rename_lst.ind ts₁, + begin + intros c₁ c₂ ts₂ hr, + cases ts₂; cases hr, + fapply h₅, exact h₁_1, exact h₂_1, + exact ih₁ _ _ _ h₁_1, + exact ih₂ _ _ _ h₂_1 + end diff --git a/tests/lean/cases_ginductive.lean.expected.out b/tests/lean/cases_ginductive.lean.expected.out new file mode 100644 index 0000000000..153fb0d70a --- /dev/null +++ b/tests/lean/cases_ginductive.lean.expected.out @@ -0,0 +1,37 @@ +t₁ : term, +c₁ c₂ : string, +h₁ h₂ : is_rename (term.const c₁) c₁ c₂ (term.const c₂) +⊢ term.const c₂ = term.const c₂ +t₁ : term, +c₁ c₂ : string, +h₁ : is_rename (term.const c₁) c₁ c₂ (term.const c₂), +hne : c₁ ≠ c₁, +h₂ : is_rename (term.const c₁) c₁ c₂ (term.const c₁) +⊢ term.const c₂ = term.const c₁ +t₁ : term, +c₁ c₂ : string, +hne : c₁ ≠ c₁, +h₁ : is_rename (term.const c₁) c₁ c₂ (term.const c₁), +h₂ : is_rename (term.const c₁) c₁ c₂ (term.const c₂) +⊢ term.const c₁ = term.const c₂ +t₁ : term, +c₁ c₁' c₂ : string, +hne : c₁ ≠ c₁', +h₁ : is_rename (term.const c₁) c₁' c₂ (term.const c₁), +hne_1 : c₁ ≠ c₁', +h₂ : is_rename (term.const c₁) c₁' c₂ (term.const c₁) +⊢ term.const c₁ = term.const c₁ +t₁ : term, +fn : string, +ts : list term, +ih : + ∀ (ts₂ ts₂' : list term) (c₁ c₂ : string), + is_rename_lst ts c₁ c₂ ts₂ → is_rename_lst ts c₁ c₂ ts₂' → ts₂ = ts₂', +c₁ c₂ : string, +ts₂ : list term, +h₁_1 : is_rename_lst ts c₁ c₂ ts₂, +h₁ : is_rename (term.app fn ts) c₁ c₂ (term.app fn ts₂), +ts₂_1 : list term, +h₁_2 : is_rename_lst ts c₁ c₂ ts₂_1, +h₂ : is_rename (term.app fn ts) c₁ c₂ (term.app fn ts₂_1) +⊢ term.app fn ts₂ = term.app fn ts₂_1