diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 50b5ddc59f..af1bf9a2b8 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -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 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 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 C_args; + expr const & C = get_app_args(p, C_args); + list 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 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 C_args; - expr const & C = get_app_args(p, C_args); - list 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 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 diff --git a/src/library/tactic/cases_tactic.h b/src/library/tactic/cases_tactic.h index 028bd3ed8a..c54f068f14 100644 --- a/src/library/tactic/cases_tactic.h +++ b/src/library/tactic/cases_tactic.h @@ -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> cases(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, diff --git a/tests/lean/run/inject.lean b/tests/lean/run/inject.lean new file mode 100644 index 0000000000..2318df1f41 --- /dev/null +++ b/tests/lean/run/inject.lean @@ -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