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

fix(library/equations_compiler/elim_match): skip nonvar + inaccessible

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-21 08:08:36 -07:00
parent fdadada3a9
commit aa68d72fa5
3 changed files with 104 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

77
src/library/equations_compiler/elim_match.cpp
View file

@ -555,6 +555,17 @@ struct elim_match_fn {
return false;
}
/** Return true iff the next pattern of all equations is an inaccessible term */
bool all_inaccessible(problem const & P) const {
for (equation const & eqn : P.m_equations) {
lean_assert(eqn.m_patterns);
expr const & p = head(eqn.m_patterns);
if (!is_inaccessible(p))
return false;
}
return true;
}
/* Return true iff the next pattern in some of the equations is an inaccessible term. */
bool is_inaccessible_transition(problem const & P) const {
return some_inaccessible(P);
@ -927,34 +938,50 @@ struct elim_match_fn {
}
list<lemma> process_non_variable(problem const & P) {
trace_match(tout() << "step: filter equations using constructor\n";);
type_context ctx = mk_type_context(P);
expr p = head(P.m_var_stack);
lean_assert(!is_local(p));
p = whnf_constructor(ctx, p);
if (!is_constructor_app(p)) {
throw_error("dependent pattern matching result is not a constructor application "
"(use 'set_option trace.eqn_compiler.elim_match true' "
"for additional details)");
type_context ctx = mk_type_context(P);
if (all_inaccessible(P)) {
trace_match(tout() << "step: skip inaccessible patterns\n";);
problem new_P;
new_P.m_fn_name = P.m_fn_name;
new_P.m_goal = P.m_goal;
new_P.m_var_stack = tail(P.m_var_stack);
buffer<equation> new_eqns;
for (equation const & eqn : P.m_equations) {
equation new_eqn = eqn;
new_eqn.m_patterns = tail(eqn.m_patterns);
new_eqns.push_back(new_eqn);
}
new_P.m_equations = to_list(new_eqns);
return process(new_P);
} else {
trace_match(tout() << "step: filter equations using constructor\n";);
p = whnf_constructor(ctx, p);
if (!is_constructor_app(p)) {
throw_error("dependent pattern matching result is not a constructor application "
"(use 'set_option trace.eqn_compiler.elim_match true' "
"for additional details)");
}
expr p_type = whnf_inductive(ctx, ctx.infer(p));
lean_assert(is_inductive_app(p_type));
name I_name = const_name(get_app_fn(p_type));
unsigned I_nparams = get_inductive_num_params(I_name);
buffer<expr> C_args;
expr const & C = get_app_args(p, C_args);
list<equation> eqns = normalize_next_pattern(P.m_equations);
problem new_P;
new_P.m_fn_name = P.m_fn_name;
new_P.m_goal = P.m_goal;
buffer<expr> new_var_stack;
for (unsigned i = I_nparams; i < C_args.size(); i++) {
new_var_stack.push_back(whnf_constructor(ctx, C_args[i]));
}
to_buffer(tail(P.m_var_stack), new_var_stack);
new_P.m_var_stack = to_list(new_var_stack);
new_P.m_equations = get_equations_for(const_name(C), I_nparams, hsubstitution(), eqns);
return process(new_P);
}
expr p_type = whnf_inductive(ctx, ctx.infer(p));
lean_assert(is_inductive_app(p_type));
name I_name = const_name(get_app_fn(p_type));
unsigned I_nparams = get_inductive_num_params(I_name);
buffer<expr> C_args;
expr const & C = get_app_args(p, C_args);
list<equation> eqns = normalize_next_pattern(P.m_equations);
problem new_P;
new_P.m_fn_name = P.m_fn_name;
new_P.m_goal = P.m_goal;
buffer<expr> new_var_stack;
for (unsigned i = I_nparams; i < C_args.size(); i++) {
new_var_stack.push_back(whnf_constructor(ctx, C_args[i]));
}
to_buffer(tail(P.m_var_stack), new_var_stack);
new_P.m_var_stack = to_list(new_var_stack);
new_P.m_equations = get_equations_for(const_name(C), I_nparams, hsubstitution(), eqns);
return process(new_P);
}
/* Create (f ... x) with the given arity, where the other arguments are inferred using

2
src/library/tactic/cases_tactic.h
View file

@ -28,7 +28,7 @@ namespace lean {
since some of the goals are discarded.
\remark If unfold_ginductive is true, then we perform cases_on on the basic inductive datatype produced
by the kernel. That is, we used relaxed_whnf to expand generalized inductive datatypes.
by the kernel. That is, we use relaxed_whnf to expand generalized inductive datatypes.
*/
pair<list<expr>, list<name>>
cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx,

51
tests/lean/run/inject.lean Normal file
View file

@ -0,0 +1,51 @@
open nat
inductive fi : nat → Type
| f0 : ∀ {n}, fi (succ n)
| fs : ∀ {n} (j : fi n), fi (succ n)
namespace fi
def lift {m k : nat} (f : fi m → fi k) : ∀ {n} (i : fi (m + n)), fi (k + n)
| 0 v := f v
| (succ n) f0 := f0
| (succ n) (fs i) := fs (lift i)
set_option pp.implicit true
#check @lift.equations._eqn_1
#check @lift.equations._eqn_2
#check @lift.equations._eqn_3
def to_nat : ∀ {n}, fi n → nat
| ._ (@f0 n) := 0
| ._ (@fs n i) := succ (to_nat i)
def fi' {n} (i : fi n) : Type :=
fi (to_nat i)
set_option trace.eqn_compiler true
set_option trace.type_context.is_def_eq true
def inject : ∀ {n} {i : fi n}, fi' i → fi n
| ._ (@fs n i) f0 := f0
| ._ (@fs n i) (fs j) := fs (inject j)
#exit
/- fi (to_nat (fs n i)) =?= fi (succ n) -/
#check @inject.equations._eqn_1
#check @inject.equations._eqn_2
@[unify] def to_nat_hint (n m k : nat) (i : fi (succ n)) (j : fi n) : unification_hint :=
{ pattern := @to_nat (succ n) (@fs n j) ≟ succ m,
constraints := [m ≟ to_nat j] }
def inject' : ∀ {n} {i : fi n}, fi' i → fi n
| ._ (@fs n i) f0 := f0
| ._ (@fs n i) (fs j) := fs (inject' j)
end fi