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

feat(library/tactic/congruence/congruence_closure): merge annotated term with term being annotated

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-26 16:30:18 -08:00
parent cf32e25f68
commit 148d34b3bf
2 changed files with 19 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/library/tactic/congruence/congruence_closure.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "library/string.h"
#include "library/trace.h"
#include "library/fun_info.h"
#include "library/annotation.h"
#include "library/comp_val.h"
#include "library/app_builder.h"
#include "library/defeq_canonizer.h"
@ -499,8 +500,13 @@ void congruence_closure::add_occurrence(expr const & parent, expr const & child,
m_state.m_parents.insert(child, ps);
}
static expr * g_congr_mark = nullptr; // dummy congruence proof, it is just a placeholder.
static expr * g_eq_true_mark = nullptr; // dummy eq_true proof, it is just a placeholder.
static expr * g_congr_mark = nullptr; // dummy congruence proof, it is just a placeholder.
static expr * g_eq_true_mark = nullptr; // dummy eq_true proof, it is just a placeholder.
static expr * g_refl_mark = nullptr; // dummy refl proof, it is just a placeholder.
void congruence_closure::push_refl_eq(expr const & lhs, expr const & rhs) {
m_todo.emplace_back(lhs, rhs, *g_refl_mark, false);
}
void congruence_closure::add_congruence_table(expr const & e) {
lean_assert(is_app(e));
@ -662,6 +668,8 @@ void congruence_closure::internalize_core(expr const & e, bool toplevel, bool to
for (unsigned i = 0; i < macro_num_args(e); i++)
internalize_core(macro_arg(e, i), false, false);
mk_entry_core(e, to_propagate);
if (is_annotation(e))
push_refl_eq(e, get_annotation_arg(e));
}
break;
case expr_kind::Pi:
@ -850,7 +858,7 @@ bool congruence_closure::has_heq_proofs(expr const & root) const {
}
expr congruence_closure::flip_proof(expr const & H, bool flipped, bool heq_proofs) const {
if (H == *g_congr_mark || H == *g_eq_true_mark) {
if (H == *g_congr_mark || H == *g_eq_true_mark || H == *g_refl_mark) {
return H;
} else {
expr new_H = H;
@ -1021,6 +1029,10 @@ expr congruence_closure::mk_proof(expr const & lhs, expr const & rhs, expr const
return mk_eq_symm(m_ctx, a_R_b_eq_true);
else
return a_R_b_eq_true;
} else if (H == *g_refl_mark) {
expr type = heq_proofs ? mk_heq(m_ctx, lhs, rhs) : mk_eq(m_ctx, lhs, rhs);
expr proof = heq_proofs ? mk_heq_refl(m_ctx, lhs) : mk_eq_refl(m_ctx, lhs);
return mk_app(mk_constant(get_id_locked_name(), {mk_level_zero()}), type, proof);
} else {
return H;
}
@ -1511,13 +1523,15 @@ format congruence_closure::state::pp_eqcs(formatter const & fmt, bool nonsinglet
void initialize_congruence_closure() {
register_trace_class("cc");
register_trace_class({"cc", "merge"});
name prefix = name::mk_internal_unique_name();
name prefix = name::mk_internal_unique_name();
g_congr_mark = new expr(mk_constant(name(prefix, "[congruence]")));
g_eq_true_mark = new expr(mk_constant(name(prefix, "[iff-true]")));
g_refl_mark = new expr(mk_constant(name(prefix, "[refl]")));
}
void finalize_congruence_closure() {
delete g_congr_mark;
delete g_eq_true_mark;
delete g_refl_mark;
}
}

1
src/library/tactic/congruence/congruence_closure.h
View file

@ -176,6 +176,7 @@ private:
void mk_entry(expr const & e, bool to_propagate);
void internalize_core(expr const & e, bool toplevel, bool to_propagate);
void push_todo(expr const & lhs, expr const & rhs, expr const & H, bool heq_proof);
void push_refl_eq(expr const & lhs, expr const & rhs);
void invert_trans(expr const & e, bool new_flipped, optional<expr> new_target, optional<expr> new_proof);
void invert_trans(expr const & e);
void remove_parents(expr const & e);