feat(library/tactic/rewrite_tactic): rewrite tactic with 'iff' lemmas

src/library/constants.cpp

@@ -61,6 +61,7 @@ name const * g_prod = nullptr;
 name const * g_prod_mk = nullptr;
 name const * g_prod_pr1 = nullptr;
 name const * g_prod_pr2 = nullptr;
+name const * g_propext = nullptr;
 name const * g_sigma = nullptr;
 name const * g_sigma_mk = nullptr;
 name const * g_string = nullptr;
@@ -190,6 +191,7 @@ void initialize_constants() {
     g_prod_mk = new name{"prod", "mk"};
     g_prod_pr1 = new name{"prod", "pr1"};
     g_prod_pr2 = new name{"prod", "pr2"};
+    g_propext = new name{"propext"};
     g_sigma = new name{"sigma"};
     g_sigma_mk = new name{"sigma", "mk"};
     g_string = new name{"string"};
@@ -320,6 +322,7 @@ void finalize_constants() {
     delete g_prod_mk;
     delete g_prod_pr1;
     delete g_prod_pr2;
+    delete g_propext;
     delete g_sigma;
     delete g_sigma_mk;
     delete g_string;
@@ -449,6 +452,7 @@ name const & get_prod_name() { return *g_prod; }
 name const & get_prod_mk_name() { return *g_prod_mk; }
 name const & get_prod_pr1_name() { return *g_prod_pr1; }
 name const & get_prod_pr2_name() { return *g_prod_pr2; }
+name const & get_propext_name() { return *g_propext; }
 name const & get_sigma_name() { return *g_sigma; }
 name const & get_sigma_mk_name() { return *g_sigma_mk; }
 name const & get_string_name() { return *g_string; }

src/library/constants.h

@@ -63,6 +63,7 @@ name const & get_prod_name();
 name const & get_prod_mk_name();
 name const & get_prod_pr1_name();
 name const & get_prod_pr2_name();
+name const & get_propext_name();
 name const & get_sigma_name();
 name const & get_sigma_mk_name();
 name const & get_string_name();

src/library/constants.txt

@@ -56,6 +56,7 @@ prod
 prod.mk
 prod.pr1
 prod.pr2
+propext
 sigma
 sigma.mk
 string

src/library/tactic/rewrite_tactic.cpp

@@ -876,7 +876,7 @@ class rewrite_fn {
         return replace(e, [&](expr const & e, unsigned) {
                 if (!has_metavar(e)) {
                     return some_expr(e); // done
-                } else if (is_binding(e)) {
+                } else if (is_lambda(e)) {
                     unsigned next_idx = m_esubst.size();
                     expr r = mk_idx_meta(next_idx, m_tc->infer(e).first);
                     m_esubst.push_back(none_expr());
@@ -909,14 +909,21 @@ class rewrite_fn {
         } else {
             // Remark: we discard constraints generated producing the pattern.
             // Patterns are only used to locate positions where the rule should be applied.
-            expr rule      = get_rewrite_rule(e);
-            expr rule_type = m_relaxed_tc->whnf(m_relaxed_tc->infer(rule).first).first;
-            while (is_pi(rule_type)) {
-                expr meta  = mk_meta(binding_domain(rule_type));
-                rule_type  = m_relaxed_tc->whnf(instantiate(binding_body(rule_type), meta)).first;
+            expr rule          = get_rewrite_rule(e);
+            expr rule_type     = m_relaxed_tc->infer(rule).first;
+            expr new_rule_type = m_relaxed_tc->whnf(rule_type).first;
+            while (is_pi(new_rule_type)) {
+                rule_type     = new_rule_type;
+                expr meta     = mk_meta(binding_domain(rule_type));
+                rule_type     = instantiate(binding_body(rule_type), meta);
+                new_rule_type = m_relaxed_tc->whnf(rule_type).first;
             }
-            if (!is_eq(rule_type))
+            if (is_standard(m_env)) {
+                if (!is_eq(rule_type) && !is_iff(rule_type))
+                    throw_rewrite_exception("invalid rewrite tactic, given lemma is not an equality or iff");
+            } else if (!is_eq(rule_type)) {
                 throw_rewrite_exception("invalid rewrite tactic, given lemma is not an equality");
+            }
             if (get_rewrite_info(e).symm()) {
                 return to_meta_idx(app_arg(rule_type));
             } else {
@@ -1097,8 +1104,12 @@ class rewrite_fn {
             buffer<constraint> cs;
             to_buffer(rcs.second, cs);
             constraint_seq cs_seq;
-            expr rule_type = m_relaxed_tc->whnf(m_relaxed_tc->infer(rule, cs_seq), cs_seq);
-            while (is_pi(rule_type)) {
+            expr rule_type     = m_relaxed_tc->infer(rule, cs_seq);
+            constraint_seq new_cs_seq;
+            expr new_rule_type = m_relaxed_tc->whnf(rule_type, new_cs_seq);
+            while (is_pi(new_rule_type)) {
+                rule_type = new_rule_type;
+                cs_seq   += new_cs_seq;
                 expr meta;
                 if (binding_info(rule_type).is_inst_implicit()) {
                     auto mc = mk_class_instance_elaborator(binding_domain(rule_type));
@@ -1107,9 +1118,15 @@ class rewrite_fn {
                 } else {
                     meta = mk_meta(binding_domain(rule_type));
                 }
-                rule_type  = m_relaxed_tc->whnf(instantiate(binding_body(rule_type), meta), cs_seq);
+                rule_type     = instantiate(binding_body(rule_type), meta);
+                new_rule_type = m_relaxed_tc->whnf(rule_type , cs_seq);
                 rule       = mk_app(rule, meta);
             }
+            lean_assert(is_eq(rule_type) || (is_standard(m_env) && is_iff(rule_type)));
+            if (is_standard(m_env) && is_iff(rule_type)) {
+                rule      = apply_propext(rule, rule_type);
+                rule_type = mk_eq(*m_relaxed_tc, app_arg(app_fn(rule_type)), app_arg(rule_type));
+            }
             lean_assert(is_eq(rule_type));
             bool symm = get_rewrite_info(orig_elem).symm();
             expr src;

src/library/util.cpp

@@ -393,10 +393,13 @@ bool is_iff(expr const & e) {
 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 apply_propext(expr const & iff_pr, expr const & iff_term) {
+    lean_assert(is_iff(iff_term));
+    return mk_app(mk_constant(get_propext_name()), app_arg(app_fn(iff_term)), app_arg(iff_term), iff_pr);
+}
 
 expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) {
     expr A    = tc.whnf(tc.infer(lhs).first).first;

src/library/util.h

@@ -153,6 +153,10 @@ bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs);
 bool is_iff(expr const & e);
 expr mk_iff(expr const & lhs, expr const & rhs);
 expr mk_iff_refl(expr const & a);
+/** \brief Given <tt>iff_pr : iff_term</tt>, where \c iff_term is of the form <tt>l <-> r</tt>,
+    return the term <tt>propext l r iff_pr</tt>
+*/
+expr apply_propext(expr const & iff_pr, expr const & iff_term);
 
 /** \brief If in HoTT mode, apply lift.down.
     The no_confusion constructions uses lifts in the proof relevant version (aka HoTT mode).

tests/lean/run/iff_rw.lean

@@ -0,0 +1,11 @@
+import logic
+
+example (a b : Prop) : a ∧ b → b ∧ a :=
+begin
+  intros, rewrite and.comm, assumption
+end
+
+example (a b c : Prop) : a ∧ b ∧ c → b ∧ a ∧ c :=
+begin
+  intros, rewrite [-and.assoc, {b ∧ a}and.comm, and.assoc], assumption
+end

tests/lean/run/true_imp_rw.lean

@@ -0,0 +1,7 @@
+import logic
+
+example (a b c : Prop) (h : a) : true → true → a :=
+begin
+  rewrite *true_imp,
+  exact h
+end

tests/lean/run/tut_104.lean

@@ -0,0 +1,42 @@
+import data.set
+namespace function
+section
+open set
+variables {A B : Type}
+set_option pp.beta false
+definition bijective (f : A → B) := injective f ∧ surjective f
+
+lemma injective_eq_inj_on_univ₁ (f : A → B) : injective f = inj_on f univ :=
+  begin
+    esimp [injective, inj_on, univ, mem],
+    apply propext,
+    apply iff.intro,
+      intro Pl a1 a2,
+        rewrite *true_imp,
+        exact Pl a1 a2,
+      intro Pr a1 a2,
+      exact Pr trivial trivial
+  end
+
+lemma injective_eq_inj_on_univ₂ (f : A → B) : injective f = inj_on f univ :=
+  begin
+    esimp [injective, inj_on, univ, mem],
+    apply propext,
+    apply iff.intro,
+      intro Pl a1 a2,
+        rewrite *(propext !true_imp),
+        exact Pl a1 a2,
+      intro Pr a1 a2,
+      exact Pr trivial trivial
+  end
+
+lemma injective_eq_inj_on_univ₃ (f : A → B) : injective f = inj_on f univ :=
+  begin
+    esimp [injective, inj_on, univ, mem],
+    apply propext,
+    repeat (apply forall_congr; intros),
+    rewrite *(propext !true_imp)
+  end
+end
+
+end function