michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/definitional/equations): improve detection of infeasible cases in the definitional package

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-22 14:05:28 -08:00
parent 431ce6ff2d
commit 49661a043d
2 changed files with 29 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/library/definitional/equations.cpp
View file

@ -734,17 +734,14 @@ class equation_compiler_fn {
return true;
}
// Return true if there are no equations, and the next variable is an indexed inductive datatype.
// In this case, it is worth trying the cases tactic, since this may be a conflicting state.
/** Return true if there are no equations, and the next variable is an inductive datatype.
In this case, it is worth trying the cases tactic, since this may be a conflicting state. */
bool is_no_equation_constructor_transition(program const & p) {
lean_assert(p.m_var_stack);
if (!p.m_eqns && head(p.m_var_stack)) {
expr const & x = p.get_var(*head(p.m_var_stack));
expr const & I = get_app_fn(mlocal_type(x));
return
is_constant(I) &&
inductive::is_inductive_decl(env(), const_name(I)) &&
*inductive::get_num_indices(env(), const_name(I)) > 0;
return is_constant(I) && inductive::is_inductive_decl(env(), const_name(I));
} else {
return false;
}
@ -943,7 +940,13 @@ class equation_compiler_fn {
}
expr compile_no_equations(program const & p) {
bool fail_if_subgoals = true;
lean_assert(head(p.m_var_stack));
expr const & x = p.get_var(*head(p.m_var_stack));
expr const & I = get_app_fn(mlocal_type(x));
lean_assert(is_constant(I) && inductive::is_inductive_decl(env(), const_name(I)));
/* If the head variable is a recursive datatype, then we want to fail if subgoals are generated.
Reason: avoid non-termination. */
bool fail_if_subgoals = is_recursive_datatype(env(), const_name(I));
if (auto r = compile_constructor_core(p, fail_if_subgoals))
return *r;
else

19
tests/lean/run/unreachable_cases.lean Normal file
View file

@ -0,0 +1,19 @@
open nat prod
inductive ifin : ℕ → Type := -- inductively defined fin-type
| fz : Π n, ifin (succ n)
| fs : Π {n}, ifin n → ifin (succ n)
open ifin
definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n)
| (succ k) n (fz k) := sorry
| (succ k) n (fs x) := sorry
definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
| ⌞succ k⌟ (n, fz k) := sorry
| ⌞succ k⌟ (n, fs x) := sorry
definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
| (succ k) (n, fz k) := sorry
| (succ k) (n, fs x) := sorry