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

fix(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT mode

Browse source 
closes #481
This commit is contained in:
Leonardo de Moura 2015-03-23 18:06:11 -07:00
parent 98cc325695
commit 5bf46d1226
6 changed files with 65 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
hott/init/path.hlean
View file

@ -106,6 +106,10 @@ namespace eq
definition inv_inv (p : x = y) : p⁻¹⁻¹ = p :=
eq.rec_on p idp
-- auxiliary definition used by 'cases' tactic
definition elim_inv_inv {A : Type} {a b : A} {C : a = b → Type} (H₁ : a = b) (H₂ : C (H₁⁻¹⁻¹)) : C H₁ :=
eq.rec_on (inv_inv H₁) H₂
/- Theorems for moving things around in equations -/
definition con_eq_of_eq_inv_con (p : x = z) (q : y = z) (r : y = x) :

4
src/library/constants.cpp
View file

@ -15,6 +15,7 @@ name const * g_char = nullptr;
name const * g_char_mk = nullptr;
name const * g_dite = nullptr;
name const * g_eq = nullptr;
name const * g_eq_elim_inv_inv = nullptr;
name const * g_eq_intro = nullptr;
name const * g_eq_rec = nullptr;
name const * g_eq_rec_eq = nullptr;
@ -126,6 +127,7 @@ void initialize_constants() {
g_char_mk = new name{"char", "mk"};
g_dite = new name{"dite"};
g_eq = new name{"eq"};
g_eq_elim_inv_inv = new name{"eq", "elim_inv_inv"};
g_eq_intro = new name{"eq", "intro"};
g_eq_rec = new name{"eq", "rec"};
g_eq_rec_eq = new name{"eq_rec_eq"};
@ -238,6 +240,7 @@ void finalize_constants() {
delete g_char_mk;
delete g_dite;
delete g_eq;
delete g_eq_elim_inv_inv;
delete g_eq_intro;
delete g_eq_rec;
delete g_eq_rec_eq;
@ -349,6 +352,7 @@ name const & get_char_name() { return *g_char; }
name const & get_char_mk_name() { return *g_char_mk; }
name const & get_dite_name() { return *g_dite; }
name const & get_eq_name() { return *g_eq; }
name const & get_eq_elim_inv_inv_name() { return *g_eq_elim_inv_inv; }
name const & get_eq_intro_name() { return *g_eq_intro; }
name const & get_eq_rec_name() { return *g_eq_rec; }
name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; }

1
src/library/constants.h
View file

@ -17,6 +17,7 @@ name const & get_char_name();
name const & get_char_mk_name();
name const & get_dite_name();
name const & get_eq_name();
name const & get_eq_elim_inv_inv_name();
name const & get_eq_intro_name();
name const & get_eq_rec_name();
name const & get_eq_rec_eq_name();

1
src/library/constants.txt
View file

@ -10,6 +10,7 @@ char
char.mk
dite
eq
eq.elim_inv_inv
eq.intro
eq.rec
eq_rec_eq

57
src/library/tactic/inversion_tactic.cpp
View file

@ -708,12 +708,12 @@ class inversion_tac {
buffer<expr> hyps;
g.get_hyps(hyps);
lean_assert(!hyps.empty());
expr eq = hyps.back();
buffer<expr> eq_args;
get_app_args(mlocal_type(eq), eq_args);
expr const & A = whnf(eq_args[0]);
expr lhs = whnf(eq_args[1]);
expr rhs = whnf(eq_args[2]);
expr Heq = hyps.back();
buffer<expr> Heq_args;
get_app_args(mlocal_type(Heq), Heq_args);
expr const & A = whnf(Heq_args[0]);
expr lhs = whnf(Heq_args[1]);
expr rhs = whnf(Heq_args[2]);
constraint_seq cs;
if (m_proof_irrel && m_tc.is_def_eq(lhs, rhs, justification(), cs) && !cs) {
// deletion transition: t == t
@ -744,7 +744,7 @@ class inversion_tac {
else
throw inversion_exception();
}
expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(g_lvl, const_levels(A_fn))), A_args), g_type, lhs, rhs, eq);
expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(g_lvl, const_levels(A_fn))), A_args), g_type, lhs, rhs, Heq);
if (const_name(lhs_fn) == const_name(rhs_fn)) {
// injectivity transition
expr new_type = binding_domain(whnf(infer_type(no_confusion)));
@ -759,14 +759,14 @@ class inversion_tac {
lean_assert(lhs_args.size() >= A_nparams);
return unify_eqs(new_g, neqs - 1 + lhs_args.size() - A_nparams);
} else {
// conflict transition, eq is of the form c_1 ... = c_2 ..., where c_1 and c_2 are different constructors/intro rules.
// conflict transition, Heq is of the form c_1 ... = c_2 ..., where c_1 and c_2 are different constructors/intro rules.
expr val = lift_down(no_confusion);
assign(g, val);
return optional<goal>(); // goal has been solved
}
}
if (is_local(rhs)) {
// solution transition, eq is of the form t = y, where y is a local constant
// solution transition, Heq is of the form t = y, where y is a local constant
// assume the current goal is of the form
//
@ -806,7 +806,7 @@ class inversion_tac {
if (m_proof_irrel)
tformer = Fun(rhs, deps_g_type);
else
tformer = Fun(rhs, Fun(eq, deps_g_type));
tformer = Fun(rhs, Fun(Heq, deps_g_type));
expr eq_rec = mk_constant(get_eq_rec_name(), {eq_rec_lvl1, eq_rec_lvl2});
eq_rec = mk_app(eq_rec, A, lhs, tformer);
buffer<expr> new_hyps;
@ -815,7 +815,7 @@ class inversion_tac {
store_rename(rhs, lhs);
replace(m_imps, rhs, lhs);
if (!m_proof_irrel) {
new_type = abstract_local(new_type, eq);
new_type = abstract_local(new_type, Heq);
new_type = instantiate(new_type, mk_refl(m_tc, lhs));
}
buffer<expr> new_deps;
@ -833,24 +833,49 @@ class inversion_tac {
expr new_meta = mk_app(new_mvar, new_hyps);
goal new_g(new_meta, new_type);
expr eq_rec_minor = mk_app(new_mvar, non_deps);
eq_rec = mk_app(eq_rec, eq_rec_minor, rhs, eq);
eq_rec = mk_app(eq_rec, eq_rec_minor, rhs, Heq);
expr val = mk_app(eq_rec, deps);
assign(g, val);
return unify_eqs(new_g, neqs-1);
}
} else if (is_local(lhs)) {
// flip equation and reduce to previous case
if (m_proof_irrel || !depends_on(g_type, hyps.back()))
hyps.pop_back(); // remove processed equality
expr symm_eq = mk_eq(rhs, lhs).first;
hyps.pop_back(); // remove processed equality
if (!depends_on(g_type, Heq)) {
expr new_type = mk_arrow(symm_eq, g_type);
expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type));
expr new_meta = mk_app(new_mvar, hyps);
goal new_g(new_meta, new_type);
expr eq_inv = mk_symm(m_tc, eq);
expr val = mk_app(new_meta, eq_inv);
expr Heq_inv = mk_symm(m_tc, Heq);
expr val = mk_app(new_meta, Heq_inv);
assign(g, val);
return unify_eqs(new_g, neqs);
} else {
// Let C[Heq] be the original conclusion which depends on the equality eq being processed.
expr new_Heq = update_mlocal(Heq, symm_eq);
expr new_Heq_inv = mk_symm(m_tc, new_Heq);
expr new_type = Pi(new_Heq, instantiate(abstract_local(g_type, Heq), new_Heq_inv));
expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type));
expr new_meta = mk_app(new_mvar, hyps);
goal new_g(new_meta, new_type);
// Then, we have
// new_meta : Pi (new_Heq : rhs = lhs), C[symm new_Heq]
expr Heq_inv = mk_symm(m_tc, Heq);
expr val = mk_app(new_meta, Heq_inv);
// val : C[symm (symm Heq)]
// Remark: in proof irrelevant mode (symm (symm Heq)) is definitionally equal to Heq
if (!m_proof_irrel) {
expr C = Fun(Heq, g_type);
level A_lvl = sort_level(m_tc.ensure_type(A).first);
level g_lvl = sort_level(m_tc.ensure_type(g_type).first);
expr elim_inv_inv = mk_constant(get_eq_elim_inv_inv_name(), {A_lvl, g_lvl});
val = mk_app({elim_inv_inv, A, lhs, rhs, C, Heq, val});
// val : C[Heq] as we wanted
}
assign(g, val);
return unify_eqs(new_g, neqs);
}
}
if (m_throw_tactic_exception) {
throw tactic_exception([=](formatter const & fmt) {

8
tests/lean/hott/481.hlean Normal file
View file

@ -0,0 +1,8 @@
open equiv eq is_equiv is_trunc
definition foo {A B : Type} (f : A ≃ B) (f' : A → B)
(H' : is_equiv f') (p : to_fun f = f') : p = p :=
begin
cases p,
esimp
end