feat(library/tactic/rewrite_tactic): treat iff.refl as trivial step in the rewrite tactic

src/library/constants.cpp

@@ -26,6 +26,8 @@ name const * g_false = nullptr;
 name const * g_heq = nullptr;
 name const * g_heq_refl = nullptr;
 name const * g_heq_to_eq = nullptr;
+name const * g_iff = nullptr;
+name const * g_iff_refl = nullptr;
 name const * g_ite = nullptr;
 name const * g_lift = nullptr;
 name const * g_lift_down = nullptr;
@@ -134,6 +136,8 @@ void initialize_constants() {
     g_heq = new name{"heq"};
     g_heq_refl = new name{"heq", "refl"};
     g_heq_to_eq = new name{"heq", "to_eq"};
+    g_iff = new name{"iff"};
+    g_iff_refl = new name{"iff", "refl"};
     g_ite = new name{"ite"};
     g_lift = new name{"lift"};
     g_lift_down = new name{"lift", "down"};
@@ -243,6 +247,8 @@ void finalize_constants() {
     delete g_heq;
     delete g_heq_refl;
     delete g_heq_to_eq;
+    delete g_iff;
+    delete g_iff_refl;
     delete g_ite;
     delete g_lift;
     delete g_lift_down;
@@ -351,6 +357,8 @@ name const & get_false_name() { return *g_false; }
 name const & get_heq_name() { return *g_heq; }
 name const & get_heq_refl_name() { return *g_heq_refl; }
 name const & get_heq_to_eq_name() { return *g_heq_to_eq; }
+name const & get_iff_name() { return *g_iff; }
+name const & get_iff_refl_name() { return *g_iff_refl; }
 name const & get_ite_name() { return *g_ite; }
 name const & get_lift_name() { return *g_lift; }
 name const & get_lift_down_name() { return *g_lift_down; }

src/library/constants.h

@@ -28,6 +28,8 @@ name const & get_false_name();
 name const & get_heq_name();
 name const & get_heq_refl_name();
 name const & get_heq_to_eq_name();
+name const & get_iff_name();
+name const & get_iff_refl_name();
 name const & get_ite_name();
 name const & get_lift_name();
 name const & get_lift_down_name();

src/library/constants.txt

@@ -21,6 +21,8 @@ false
 heq
 heq.refl
 heq.to_eq
+iff
+iff.refl
 ite
 lift
 lift.down

src/library/tactic/rewrite_tactic.cpp

@@ -1108,12 +1108,12 @@ class rewrite_fn {
 
     bool check_trivial_goal() {
         expr type = m_g.get_type();
-        if (is_eq(type)) {
+        if (is_eq(type) || (is_iff(type) && m_env.impredicative())) {
             constraint_seq cs;
             expr lhs = app_arg(app_fn(type));
             expr rhs = app_arg(type);
             if (m_unifier_tc->is_def_eq(lhs, rhs, justification(), cs) && !cs) {
-                expr H = mk_refl(*m_tc, lhs);
+                expr H = is_eq(type) ? mk_refl(*m_tc, lhs) : mk_iff_refl(lhs);
                 m_subst.assign(m_g.get_name(), m_g.abstract(H));
                 return true;
             } else {

src/library/util.cpp

@@ -335,6 +335,18 @@ expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop) {
 expr mk_pr1(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_left(tc, p) : mk_pr1(tc, p); }
 expr mk_pr2(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_right(tc, p) : mk_pr2(tc, p); }
 
+bool is_iff(expr const & e) {
+    expr const & fn = get_app_fn(e);
+    return is_constant(fn) && const_name(fn) == get_iff_name();
+}
+expr mk_iff(expr const & lhs, expr const & rhs) {
+    return mk_app(mk_constant(get_iff_name()), lhs, rhs);
+}
+
+expr mk_iff_refl(expr const & a) {
+    return mk_app(mk_constant(get_iff_refl_name()), a);
+}
+
 expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) {
     expr A    = tc.whnf(tc.infer(lhs).first).first;
     level lvl = sort_level(tc.ensure_type(A).first);

src/library/util.h

@@ -133,6 +133,10 @@ bool is_eq_a_a(expr const & e);
 /** \brief Return true iff \c e is of the form (eq A a a') where \c a and \c a' are definitionally equal */
 bool is_eq_a_a(type_checker & tc, expr const & e);
 
+bool is_iff(expr const & e);
+expr mk_iff(expr const & lhs, expr const & rhs);
+expr mk_iff_refl(expr const & a);
+
 /** \brief Create a telescope equality for HoTT library.
     This procedure assumes eq supports dependent elimination.
     For HoTT, we can't use heterogeneous equality.