feat(library/blast/congruence_closure): missing case

src/library/blast/congruence_closure.cpp

@@ -886,8 +886,19 @@ expr congruence_closure::mk_proof(name const & R, expr const & lhs, expr const &
             return *r;
         }
     } else if (H == *g_iff_true_mark) {
-        // TODO(Leo):
-        lean_unreachable();
+        bool flip;
+        name R1; expr a, b;
+        if (lhs == mk_true()) {
+            lean_verify(is_relation_app(rhs, R1, a, b));
+            flip = true;
+        } else {
+            lean_verify(is_relation_app(lhs, R1, a, b));
+            flip = false;
+        }
+        expr H1 = get_app_builder().mk_iff_true_intro(*get_eqv_proof(R1, a, b));
+        if (flip)
+            H1 = get_app_builder().mk_iff_symm(H1);
+        return H1;
     } else if (H == *g_lift_mark) {
         expr H1 = *get_eqv_proof(get_eq_name(), lhs, rhs);
         return get_app_builder().lift_from_eq(R, H1);

tests/lean/run/blast_cc9.lean

@@ -0,0 +1,16 @@
+import data.list
+open perm
+set_option blast.subst false
+set_option blast.simp  false
+
+example (a b : nat) : a = b → (b = a ↔ true) :=
+by blast
+
+example (a b c : nat) : a = b → b = c → (true ↔ a = c) :=
+by blast
+
+example (l₁ l₂ l₃ : list nat) : l₁ ~ l₂ → l₂ ~ l₃ → (true ↔ l₁ ~ l₃) :=
+by blast
+
+example (l₁ l₂ l₃ : list nat) : l₁ ~ l₂ → l₂ = l₃ → (true ↔ l₁ ~ l₃) :=
+by blast