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

feat(simplifier): detect refl proofs from simp extensions

Browse source
This commit is contained in:
Daniel Selsam 2016-07-06 09:21:08 -07:00 • committed by Leonardo de Moura
parent a354973fee
commit ea19bb40dd
2 changed files with 37 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/tactic/simplifier/simplifier.cpp
View file

@ -514,8 +514,11 @@ simp_result simplifier::simplify_extensions(expr const & _e) {
expr proof = m_tctx.instantiate_mvars(goal_mvar);
lean_trace(name({"simplifier", "extensions"}),
tout() << proof << " : " << e << " " << m_rel << " " << result << "\n";);
// TODO(dhs): detect refl proofs
r = join(r, simp_result(result, proof));
if (is_app_of(proof, get_eq_refl_name(), 2) || is_app_of(proof, get_rfl_name(), 2)) {
r.update(result);
} else {
r = join(r, simp_result(result, proof));
}
} else {
lean_trace(name({"simplifier", "extensions"}),
tout() << "extension failed on goal " << goal_type << "\n";);

32
tests/lean/run/simp_ext_refl.lean Normal file
View file

@ -0,0 +1,32 @@
open tactic
constants (A : Type.{1}) (x y z : A) (g : A → A) (Hg : g y = z)
attribute Hg [simp]
definition f (a : A) := y
lemma f.def : ∀ (a), f a = y := λ a, rfl
meta_definition simp_f_to_y : tactic unit := mk_eq_simp_ext $
λ e, if expr.get_app_num_args e = 1
then do res ← mk_const "y",
pf ← mk_app "rfl" [e],
return (res, pf)
else fail "expected f applied to one arg"
meta_definition simp_f_to_y₂ : tactic unit := mk_eq_simp_ext $
λ e, if expr.get_app_num_args e = 1
then do res ← mk_const "y",
pf ← mk_app ("f" <.> "def") [expr.app_arg e],
return (res, pf)
else fail "expected f applied to one arg"
register_simp_ext f simp_f_to_y
definition foo : g (f x) = z := by simp >> triv
register_simp_ext f simp_f_to_y₂
definition foo₂ : g (f x) = z := by simp >> triv
print foo
print foo₂