max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/tactic/cases_tactic): use inj_arrow instead no_confusion when index is a nested and/or mutually recursive datatype

Browse source 
The `no_confusion` construction is only generated for inductive
datatypes supported in the kernel.
Before this commit, given `h : T`, `cases h` could leak the internal encoding
used by the inductive compiler WHEN a nested and/or mutual inductive
datatype is used to index the inductive datatype `T`.
The new test exposes the problem.

The solution implemented in this commit uses inj_arrow lemmas
generated by the inductive compiler. We only use the lemmas
if the target is a proposition. If it is not, we sign an error.
The reason for this limitation is documented in the source code.

cc @jroesch @dselsam

Jared: the information leakage has been fixed. So, students will not be
confused by the internal encoding used in the inductive compiler.
I added the example I posted on slack as a new test.
Note that, the workaround I used has been removed.
This commit is contained in:
Leonardo de Moura 2017-11-27 21:12:58 -08:00
parent 7c63b2f046
commit 641a4548b6
5 changed files with 250 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/inductive_compiler/ginductive.cpp
View file

@ -15,6 +15,13 @@ Author: Daniel Selsam
#include "library/kernel_serializer.h"
namespace lean {
optional<name> is_gintro_rule_app(environment const & env, expr const & e) {
expr const & fn = get_app_fn(e);
if (!is_constant(fn)) return optional<name>();
if (!is_ginductive_intro_rule(env, const_name(fn))) return optional<name>();
return optional<name>(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<expr> args;
unsigned idx = 0;

8
src/library/inductive_compiler/ginductive.h
View file

@ -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<name> 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<name> is_gintro_rule_app(environment const & env, expr const & e);
/* \brief Returns the offset of a simulated introduction rule.
Example:

123
src/library/tactic/cases_tactic.cpp
View file

@ -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<name> c1 = is_constructor_app(m_env, lhs);
optional<name> c2 = is_constructor_app(m_env, rhs);
A = ctx.whnf(A);
buffer<expr> 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<name> c1 = is_gintro_rule_app(m_env, lhs);
optional<name> 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<declaration> 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<expr> 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");

96
tests/lean/cases_ginductive.lean Normal file
View file

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

37
tests/lean/cases_ginductive.lean.expected.out Normal file
View file

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