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

feat(library/init/meta/congruence_tactics): add option for retrieving only non-singleton equivalence classes, add auxiliary functions

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-23 18:35:44 -08:00
parent a2850ac050
commit ca261b7fa8
5 changed files with 53 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
library/init/meta/congruence_tactics.lean
View file

@ -13,14 +13,38 @@ meta constant cc_state.mk : cc_state
meta constant cc_state.mk_using_hs : tactic cc_state
meta constant cc_state.next : cc_state → expr → expr
meta constant cc_state.inconsistent : cc_state → bool
meta constant cc_state.roots : cc_state → list expr
meta constant cc_state.roots_core : cc_state → bool → list expr
meta constant cc_state.root : cc_state → expr → expr
meta constant cc_state.mt : cc_state → expr → nat
meta constant cc_state.is_cg_root : cc_state → expr → bool
meta constant cc_state.pp_eqc : cc_state → expr → tactic format
meta constant cc_state.pp : cc_state → tactic format
meta constant cc_state.pp_core : cc_state → bool → tactic format
meta constant cc_state.internalize : cc_state → expr → bool → tactic cc_state
meta constant cc_state.add : cc_state → expr → tactic cc_state
meta constant cc_state.is_eqv : cc_state → expr → expr → tactic bool
meta constant cc_state.is_not_eqv : cc_state → expr → expr → tactic bool
meta constant cc_state.eqv_proof : cc_state → expr → expr → tactic expr
namespace cc_state
meta def roots (s : cc_state) : list expr :=
cc_state.roots_core s tt
meta def pp (s : cc_state) : tactic format :=
cc_state.pp_core s tt
meta def eqc_of_core (s : cc_state) : expr → expr → list expr → list expr
| e f r :=
let n := s^.next e in
if n = f then e::r else eqc_of_core n f (e::r)
meta def eqc_of (s : cc_state) (e : expr) : list expr :=
s^.eqc_of_core e e []
meta def in_singlenton_eqc (s : cc_state) (e : expr) : bool :=
to_bool (s^.next e = e)
meta def eqc_size (s : cc_state) (e : expr) : nat :=
(s^.eqc_of e)^.length
end cc_state

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

@ -162,9 +162,9 @@ expr congruence_closure::state::get_root(expr const & e) const {
}
}
void congruence_closure::state::get_roots(buffer<expr> & roots) const {
void congruence_closure::state::get_roots(buffer<expr> & roots, bool nonsingleton_only) const {
m_entries.for_each([&](expr const & k, entry const & n) {
if (k == n.m_root)
if (k == n.m_root && (!nonsingleton_only || !in_singleton_eqc(k)))
roots.push_back(k);
});
}
@ -1394,9 +1394,15 @@ format congruence_closure::state::pp_eqc(formatter const & fmt, expr const & e)
return bracket("{", group(r), "}");
}
format congruence_closure::state::pp_eqcs(formatter const & fmt) const {
bool congruence_closure::state::in_singleton_eqc(expr const & e) const {
if (auto it = m_entries.find(e))
return it->m_next == e;
return true;
}
format congruence_closure::state::pp_eqcs(formatter const & fmt, bool nonsingleton_only) const {
buffer<expr> roots;
get_roots(roots);
get_roots(roots, nonsingleton_only);
format r;
bool first = true;
for (expr const & root : roots) {

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

@ -130,15 +130,16 @@ public:
void mk_entry_core(expr const & e, bool to_propagate, bool interpreted, bool constructor);
public:
state(name_set const & ho_fns = name_set(), config const & cfg = config());
void get_roots(buffer<expr> & roots) const;
void get_roots(buffer<expr> & roots, bool nonsingleton_only = true) const;
expr get_root(expr const & e) const;
expr get_next(expr const & e) const;
unsigned get_mt(expr const & e) const;
bool is_congr_root(expr const & e) const;
bool check_invariant() const;
bool inconsistent() const { return m_inconsistent; }
bool in_singleton_eqc(expr const & e) const;
format pp_eqc(formatter const & fmt, expr const & e) const;
format pp_eqcs(formatter const & fmt) const;
format pp_eqcs(formatter const & fmt, bool nonsingleton_only = true) const;
};
private:

14
src/library/tactic/congruence/congruence_tactics.cpp
View file

@ -60,12 +60,12 @@ vm_obj cc_state_mk_using_hs(vm_obj const & _s) {
}
}
vm_obj cc_state_pp(vm_obj const & ccs, vm_obj const & _s) {
vm_obj cc_state_pp_core(vm_obj const & ccs, vm_obj const & nonsingleton, vm_obj const & _s) {
tactic_state const & s = to_tactic_state(_s);
type_context ctx = mk_type_context_for(s);
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
formatter fmt = fmtf(s.env(), s.get_options(), ctx);
format r = to_cc_state(ccs).pp_eqcs(fmt);
format r = to_cc_state(ccs).pp_eqcs(fmt, to_bool(nonsingleton));
return mk_tactic_success(to_obj(r), s);
}
@ -90,9 +90,9 @@ vm_obj cc_state_is_cg_root(vm_obj const & ccs, vm_obj const & e) {
return mk_vm_bool(to_cc_state(ccs).is_congr_root(to_expr(e)));
}
vm_obj cc_state_roots(vm_obj const & ccs) {
vm_obj cc_state_roots_core(vm_obj const & ccs, vm_obj const & nonsingleton) {
buffer<expr> roots;
to_cc_state(ccs).get_roots(roots);
to_cc_state(ccs).get_roots(roots, to_bool(nonsingleton));
return to_obj(roots);
}
@ -124,7 +124,7 @@ vm_obj cc_state_add(vm_obj const & ccs, vm_obj const & H, vm_obj const & _s) {
if (ctx.is_prop(type))
return mk_tactic_exception("cc_state.add failed, given expression is not a proof term", s);
cc.add(type, to_expr(H));
});
});
}
vm_obj cc_state_internalize(vm_obj const & ccs, vm_obj const & e, vm_obj const & top_level, vm_obj const & _s) {
@ -161,13 +161,13 @@ void initialize_congruence_tactics() {
DECLARE_VM_BUILTIN(name({"cc_state", "mk"}), cc_state_mk);
DECLARE_VM_BUILTIN(name({"cc_state", "next"}), cc_state_next);
DECLARE_VM_BUILTIN(name({"cc_state", "mk_using_hs"}), cc_state_mk_using_hs);
DECLARE_VM_BUILTIN(name({"cc_state", "pp"}), cc_state_pp);
DECLARE_VM_BUILTIN(name({"cc_state", "pp_core"}), cc_state_pp_core);
DECLARE_VM_BUILTIN(name({"cc_state", "pp_eqc"}), cc_state_pp_eqc);
DECLARE_VM_BUILTIN(name({"cc_state", "next"}), cc_state_next);
DECLARE_VM_BUILTIN(name({"cc_state", "root"}), cc_state_root);
DECLARE_VM_BUILTIN(name({"cc_state", "mt"}), cc_state_mt);
DECLARE_VM_BUILTIN(name({"cc_state", "is_cg_root"}), cc_state_is_cg_root);
DECLARE_VM_BUILTIN(name({"cc_state", "roots"}), cc_state_roots);
DECLARE_VM_BUILTIN(name({"cc_state", "roots_core"}), cc_state_roots_core);
DECLARE_VM_BUILTIN(name({"cc_state", "internalize"}), cc_state_internalize);
DECLARE_VM_BUILTIN(name({"cc_state", "add"}), cc_state_add);
DECLARE_VM_BUILTIN(name({"cc_state", "is_eqv"}), cc_state_is_eqv);

7
tests/lean/run/cc1.lean
View file

@ -8,9 +8,16 @@ by do intros,
s^.pp >>= trace,
t₁ ← to_expr `(f (b + b) b),
t₂ ← to_expr `(f (a + c) c),
b ← to_expr `(b),
d ← to_expr `(d),
guard (s^.inconsistent),
guard (s^.eqc_size b = 3),
guard (not (s^.in_singlenton_eqc b)),
guard (s^.in_singlenton_eqc d),
trace ">>> Equivalence roots",
trace s^.roots,
trace ">>> b's equivalence class",
trace (s^.eqc_of b),
pr ← s^.eqv_proof t₁ t₂,
note `h pr,
contradiction