feat(library/tactic): rename 'exact' to 'assumption', 'exact' is a different tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/standard/tactic.lean

@@ -20,7 +20,7 @@ definition and_then   (t1 t2 : tactic) : tactic := tactic_value
 definition or_else    (t1 t2 : tactic) : tactic := tactic_value
 definition repeat     (t : tactic) : tactic := tactic_value
 definition now        : tactic := tactic_value
-definition exact      : tactic := tactic_value
+definition assumption : tactic := tactic_value
 definition state      : tactic := tactic_value
 definition fail       : tactic := tactic_value
 definition id         : tactic := tactic_value

src/library/tactic/expr_to_tactic.cpp

@@ -83,7 +83,7 @@ register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tact
 static name g_tac("tactic");
 static register_simple_tac reg_id(name(g_tac, "id"), []() { return id_tactic(); });
 static register_simple_tac reg_now(name(g_tac, "now"), []() { return now_tactic(); });
-static register_simple_tac reg_exact(name(g_tac, "exact"), []() { return assumption_tactic(); });
+static register_simple_tac reg_assumption(name(g_tac, "assumption"), []() { return assumption_tactic(); });
 static register_simple_tac reg_fail(name(g_tac, "fail"), []() { return fail_tactic(); });
 static register_simple_tac reg_beta(name(g_tac, "beta"), []() { return beta_tactic(); });
 static register_bin_tac reg_then(name(g_tac, "and_then"), [](tactic const & t1, tactic const & t2) { return then(t1, t2); });

tests/lean/run/have5.lean

@@ -5,8 +5,8 @@ axiom Ha : a
 axiom Hb : b
 axiom Hc : c
 print raw
-  have H1 : a, by exact,
-  then have H2 : b, by exact,
-  have H3 : c, by exact,
-  then have H4 : d, by exact,
+  have H1 : a, by assumption,
+  then have H2 : b, by assumption,
+  have H3 : c, by assumption,
+  then have H4 : d, by assumption,
   H4

tests/lean/run/t8.lean

@@ -1,3 +1,3 @@
 import standard
 using tactic
-print raw (by exact)
+print raw (by assumption)

tests/lean/run/tactic1.lean

@@ -2,4 +2,4 @@ import standard
 using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by exact
+:= by assumption

tests/lean/run/tactic2.lean

@@ -2,6 +2,6 @@ import standard
 using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
-:= by state; exact
+:= by state; assumption
 
 check tst

tests/lean/run/tactic3.lean

@@ -4,6 +4,6 @@ using tactic
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
 := by trace "first";  state; now  |
       trace "second"; state; fail |
-      trace "third";  exact
+      trace "third";  assumption
 
 check tst

tests/lean/run/tactic4.lean

@@ -4,7 +4,7 @@ using tactic (renaming id->id_tac)
 definition id {A : Type} (a : A) := a
 
 definition simple {A : Bool} : tactic
-:= unfold @id.{1}; exact
+:= unfold @id.{1}; assumption
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
 := by simple

tests/lean/run/tactic5.lean

@@ -4,6 +4,6 @@ using tactic (renaming id->id_tac)
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by !(unfold @id; state); exact
+:= by !(unfold @id; state); assumption
 
 check tst

tests/lean/run/tactic6.lean

@@ -4,6 +4,6 @@ using tactic (renaming id->id_tac)
 definition id {A : Type} (a : A) := a
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
-:= by unfold id; exact
+:= by unfold id; assumption
 
 check tst

tests/lean/run/tactic7.lean

@@ -2,11 +2,11 @@ import standard
 using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
-:= by apply and_intro; state; exact; apply and_intro; !exact
+:= by apply and_intro; state; assumption; apply and_intro; !assumption
 check tst
 
 theorem tst2 {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
-:= by !((apply @and_intro | exact) ; trace "STEP"; state; trace "----------")
+:= by !((apply @and_intro | assumption) ; trace "STEP"; state; trace "----------")
 
 check tst2
 

tests/lean/run/tactic9.lean

@@ -2,5 +2,5 @@ import standard
 using tactic
 
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : ((fun x : Bool, x) A) ∧ B ∧ A
-:= by apply and_intro; beta; exact; apply and_intro; !exact
+:= by apply and_intro; beta; assumption; apply and_intro; !assumption