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

feat(frontends/lean/definition_cmds): make sure copied lemma is a rfl lemma if source is a rfl lemma

Browse source 
The idea is to allow the defeq simplifier to use the copied lemma.
This commit is contained in:
Leonardo de Moura 2016-10-06 15:49:38 -07:00
parent c745519e50
commit e473d7cefc
1 changed files with 25 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/frontends/lean/definition_cmds.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/replace_fn.h"
#include "library/trace.h"
#include "library/constants.h"
#include "library/explicit.h"
#include "library/typed_expr.h"
#include "library/private.h"
@ -445,6 +446,14 @@ static void get_args_for_instantiating_lemma(unsigned arity,
}
}
/* Return true iff e is of the form (fun (a_1 : A_1) ... (a_n : A_n), eq.refl ...) */
static bool is_refl_lemma(expr e) {
while (is_lambda(e))
e = binding_body(e);
expr const & fn = get_app_fn(e);
return is_constant(fn, get_eq_refl_name()) || is_constant(fn, get_rfl_name());
}
/**
Given a declaration d defined as
(fun (a_1 : A_1) ... (a_n : A_n), d._main a_1' ... a_n')
@ -510,7 +519,22 @@ static environment copy_equation_lemmas(environment const & env, name const & d_
});
new_eqn_type = locals.mk_pi(new_eqn_type);
name new_eqn_name = d_name + eqn_suffix;
expr new_eqn_value = locals.mk_lambda(mk_app(mk_constant(eqn_name, eqn_levels), args));
expr new_eqn_value;
if (is_refl_lemma(eqn_decl->get_value())) {
/* Create a refl-lemma to make sure it can be used by the defeq simplifier. */
type_context::tmp_locals extra_locals(ctx);
while (is_pi(eqn_type)) {
expr local = locals.push_local_from_binding(eqn_type);
eqn_type = instantiate(binding_body(eqn_type), local);
}
expr lhs, rhs;
lean_verify(is_eq(eqn_type, lhs, rhs));
new_eqn_value = mk_eq_refl(ctx, lhs);
new_eqn_value = extra_locals.mk_lambda(new_eqn_value);
} else {
new_eqn_value = mk_app(mk_constant(eqn_name, eqn_levels), args);
}
new_eqn_value = locals.mk_lambda(new_eqn_value);
declaration new_decl = mk_theorem(new_eqn_name, d.get_univ_params(), new_eqn_type, new_eqn_value);
new_env = module::add(new_env, check(new_env, new_decl));
// TODO(Leo): tag lemmas