From b39fe17dee32a9d9023cd54e1a7eeef619590561 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 May 2015 15:48:25 -0700
Subject: [PATCH] feat(library/tactic): add 'transitiviy', 'reflexivity' and
 'symmetry' tactics

closes #500
---
 hott/init/tactic.hlean                     |  4 +
 library/init/tactic.lean                   |  4 +
 src/emacs/lean-syntax.el                   |  2 +-
 src/library/tactic/CMakeLists.txt          |  2 +-
 src/library/tactic/equivalence_tactics.cpp | 95 ++++++++++++++++++++++
 src/library/tactic/equivalence_tactics.h   | 11 +++
 src/library/tactic/init_module.cpp         |  3 +
 tests/lean/run/eqv_tacs.lean               | 34 ++++++++
 8 files changed, 153 insertions(+), 2 deletions(-)
 create mode 100644 src/library/tactic/equivalence_tactics.cpp
 create mode 100644 src/library/tactic/equivalence_tactics.h
 create mode 100644 tests/lean/run/eqv_tacs.lean

diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean
index 1317ef586..71bed84f5 100644
--- a/hott/init/tactic.hlean
+++ b/hott/init/tactic.hlean
@@ -112,6 +112,10 @@ opaque definition injection (e : expr) (ids : opt_identifier_list) : tactic := b
 
 opaque definition subst (ids : identifier_list) : tactic := builtin
 
+opaque definition reflexivity             : tactic := builtin
+opaque definition symmetry                : tactic := builtin
+opaque definition transitivity (e : expr) : tactic := builtin
+
 definition try         (t : tactic) : tactic := or_else t id
 definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
 definition focus       (t : tactic) : tactic := focus_at t 0
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index cbbd88c96..71f8da35b 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -112,6 +112,10 @@ opaque definition injection (e : expr) (ids : opt_identifier_list) : tactic := b
 
 opaque definition subst (ids : identifier_list) : tactic := builtin
 
+opaque definition reflexivity             : tactic := builtin
+opaque definition symmetry                : tactic := builtin
+opaque definition transitivity (e : expr) : tactic := builtin
+
 definition try         (t : tactic) : tactic := or_else t id
 definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
 definition focus       (t : tactic) : tactic := focus_at t 0
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 892eb0aa6..d26fdfd85 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -136,7 +136,7 @@
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
                 "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp"
                 "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "left" "right"
-                "injection" "congruence"))
+                "injection" "congruence" "reflexivity" "symmetry" "transitivity"))
            word-end)
       (1 'font-lock-constant-face))
      ;; Types
diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index c3058ae21..7e4a4791e 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -6,6 +6,6 @@ assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp
 rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp
 change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp
 exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp
-congruence_tactic.cpp)
+congruence_tactic.cpp equivalence_tactics.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})
diff --git a/src/library/tactic/equivalence_tactics.cpp b/src/library/tactic/equivalence_tactics.cpp
new file mode 100644
index 000000000..0b899c06d
--- /dev/null
+++ b/src/library/tactic/equivalence_tactics.cpp
@@ -0,0 +1,95 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/equivalence_manager.h"
+#include "library/explicit.h"
+#include "library/placeholder.h"
+#include "library/tactic/apply_tactic.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+static optional<name> get_goal_op(proof_state const & s) {
+    goals const & gs = s.get_goals();
+    if (empty(gs)) {
+        throw_no_goal_if_enabled(s);
+        return optional<name>();
+    }
+    goal const & g   = head(gs);
+    expr const & op  = get_app_fn(g.get_type());
+    if (is_constant(op))
+        return optional<name>(const_name(op));
+    else
+        return optional<name>();
+}
+
+tactic refl_tactic(elaborate_fn const & elab) {
+    auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
+        auto op = get_goal_op(s);
+        if (!op)
+            return proof_state_seq();
+        if (auto refl = get_refl_info(env, *op)) {
+            return apply_tactic(elab, mk_constant(*refl))(env, ios, s);
+        } else {
+            throw_tactic_exception_if_enabled(s, sstream() << "invalid 'reflexivity' tactic, operator '" << *op << "' is not marked are reflexive");
+            return proof_state_seq();
+        }
+    };
+    return tactic(fn);
+}
+
+tactic symm_tactic(elaborate_fn const & elab) {
+    auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
+        auto op = get_goal_op(s);
+        if (!op)
+            return proof_state_seq();
+        if (auto symm = get_symm_info(env, *op)) {
+            return apply_tactic(elab, mk_constant(*symm))(env, ios, s);
+        } else {
+            throw_tactic_exception_if_enabled(s, sstream() << "invalid 'symmetry' tactic, operator '" << *op << "' is not marked are symmetric");
+            return proof_state_seq();
+        }
+    };
+    return tactic(fn);
+}
+
+tactic trans_tactic(elaborate_fn const & elab, expr const & e) {
+    auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
+        auto op = get_goal_op(s);
+        if (!op)
+            return proof_state_seq();
+        if (auto info = get_trans_extra_info(env, *op, *op)) {
+            expr pr = mk_explicit(mk_constant(std::get<0>(*info)));
+            unsigned nparams = std::get<2>(*info);
+            lean_assert(nparams >= 5);
+            for (unsigned i = 0; i < nparams - 4; i++)
+                pr = mk_app(pr, mk_expr_placeholder());
+            pr = mk_app(pr, e);
+            return apply_tactic(elab, pr)(env, ios, s);
+        } else {
+            throw_tactic_exception_if_enabled(s, sstream() << "invalid 'transitivity' tactic, operator '" << *op << "' is not marked are transitive");
+            return proof_state_seq();
+        }
+    };
+    return tactic(fn);
+}
+
+void initialize_equivalence_tactics() {
+    register_tac(name{"tactic", "reflexivity"},
+                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                     return refl_tactic(fn);
+                 });
+    register_tac(name{"tactic", "symmetry"},
+                 [](type_checker &, elaborate_fn const & fn, expr const &, pos_info_provider const *) {
+                     return symm_tactic(fn);
+                 });
+    register_tac(name{"tactic", "transitivity"},
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     check_tactic_expr(app_arg(e), "invalid 'transitivity' tactic, invalid argument");
+                     return trans_tactic(fn, get_tactic_expr_expr(app_arg(e)));
+                 });
+}
+void finalize_equivalence_tactics() {}
+}
diff --git a/src/library/tactic/equivalence_tactics.h b/src/library/tactic/equivalence_tactics.h
new file mode 100644
index 000000000..bec7c3dc9
--- /dev/null
+++ b/src/library/tactic/equivalence_tactics.h
@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_equivalence_tactics();
+void finalize_equivalence_tactics();
+}
diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp
index a289a3c66..c1031b46a 100644
--- a/src/library/tactic/init_module.cpp
+++ b/src/library/tactic/init_module.cpp
@@ -28,6 +28,7 @@ Author: Leonardo de Moura
 #include "library/tactic/constructor_tactic.h"
 #include "library/tactic/injection_tactic.h"
 #include "library/tactic/congruence_tactic.h"
+#include "library/tactic/equivalence_tactics.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -55,9 +56,11 @@ void initialize_tactic_module() {
     initialize_constructor_tactic();
     initialize_injection_tactic();
     initialize_congruence_tactic();
+    initialize_equivalence_tactics();
 }
 
 void finalize_tactic_module() {
+    finalize_equivalence_tactics();
     finalize_congruence_tactic();
     finalize_injection_tactic();
     finalize_constructor_tactic();
diff --git a/tests/lean/run/eqv_tacs.lean b/tests/lean/run/eqv_tacs.lean
new file mode 100644
index 000000000..e6eadfbe0
--- /dev/null
+++ b/tests/lean/run/eqv_tacs.lean
@@ -0,0 +1,34 @@
+open nat
+
+example (a : nat) : a + 0 = a :=
+by reflexivity
+
+example (a : Prop) : a ↔ a :=
+by reflexivity
+
+example (a b : Prop) : (a ↔ b) → (b ↔ a) :=
+by intros; symmetry; assumption
+
+example (a b c : nat) : a = b → b = c → c = a :=
+begin
+  intros,
+  symmetry,
+  transitivity b,
+  assumption
+end
+
+example (a b c : Prop) : (a ↔ b) → (b ↔ c) → (c ↔ a) :=
+begin
+  intros,
+  symmetry,
+  transitivity b,
+  assumption
+end
+
+example {A B C : Type} (a : A) (b : B) (c : C) : a == b → b == c → c == a :=
+begin
+  intros,
+  symmetry,
+  transitivity b,
+  assumption
+end