From c04c610b7b8915f553f5bcdc2531046c72e13da8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Feb 2015 14:30:42 -0800
Subject: [PATCH] feat(frontends/lean): add 'assert H : A, ...' as notation for
 'have H [visible] : A, ...'

---
 hott/init/tactic.hlean               |  1 -
 hott/types/trunc.hlean               |  8 ++++---
 library/algebra/ordered_group.lean   |  2 +-
 library/data/int/basic.lean          |  4 ++--
 library/data/nat/div.lean            |  8 +++----
 library/data/quotient/basic.lean     |  4 ++--
 library/data/quotient/classical.lean |  2 +-
 library/init/tactic.lean             |  1 -
 library/logic/connectives.lean       |  2 +-
 src/emacs/lean-syntax.el             |  4 ++--
 src/frontends/lean/builtin_exprs.cpp | 34 +++++++++++++++++++++-------
 src/frontends/lean/token_table.cpp   |  2 +-
 src/frontends/lean/tokens.cpp        |  4 ++++
 src/frontends/lean/tokens.h          |  1 +
 tests/lean/assert_fail.lean          |  4 ++--
 tests/lean/run/assert_tac.lean       |  2 +-
 tests/lean/run/have6.lean            |  8 +++----
 17 files changed, 57 insertions(+), 34 deletions(-)

diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean
index d9d133f0e..713dbc31e 100644
--- a/hott/init/tactic.hlean
+++ b/hott/init/tactic.hlean
@@ -92,7 +92,6 @@ opaque definition revert_lst (ids : expr_list) : tactic := builtin
 notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l
 
 opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin
-notation `assert` `(` id `:` ty `)` := assert_hypothesis id ty
 
 infixl `;`:15 := and_then
 notation `[` h:10 `|`:10 r:(foldl:10 `|` (e r, or_else r e) h) `]` := r
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 768ca229d..3184e1435 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -52,9 +52,11 @@ namespace is_trunc
        apply (@is_hprop.elim),
        apply is_trunc_pi, intro a,
        apply is_hprop.mk, intros (w, z),
-       assert (H : is_hset A),
-         {apply is_trunc_succ, apply is_trunc_succ,
-          apply is_contr.mk, exact y.2},
+       have H : is_hset A,
+       begin
+         apply is_trunc_succ, apply is_trunc_succ,
+         apply is_contr.mk, exact y.2
+       end,
        fapply (@is_hset.elim A _ _ _ w z)},
      {intros (n', IH, A),
       apply is_trunc_is_equiv_closed,
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 7c19bc6aa..3264dbe88 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -200,7 +200,7 @@ structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_
 (add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b))
 
 theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
-have H' [visible] : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
+assert H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
 by rewrite *neg_add_cancel_left at H'; exact H'
 
 definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible]
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 75e181c55..275211f43 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -383,9 +383,9 @@ begin
 end
 
 theorem add.assoc (a b c : ℤ) : a + b + c = a + (b + c) :=
-have H1 [visible]: repr (a + b + c) ≡ padd (padd (repr a) (repr b)) (repr c), from
+assert H1 : repr (a + b + c) ≡ padd (padd (repr a) (repr b)) (repr c), from
   equiv.trans (repr_add (a + b) c) (padd_congr !repr_add !equiv.refl),
-have H2 [visible]: repr (a + (b + c)) ≡ padd (repr a) (padd (repr b) (repr c)), from
+assert H2 : repr (a + (b + c)) ≡ padd (repr a) (padd (repr b) (repr c)), from
   equiv.trans (repr_add a (b + c)) (padd_congr !equiv.refl !repr_add),
 begin
   apply eq_of_repr_equiv_repr,
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 37f451971..82ae643a0 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -305,10 +305,10 @@ have H2 : n - k div m ≥ 1, from
   le_sub_of_add_le (calc
     1 + k div m = succ (k div m) : add.comm
             ... ≤ n              : succ_le_of_lt H1),
-have H3 [visible] : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹,
-have H4 [visible] : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero _ (!zero_mul ▸ H' ▸ H)),
-have H5 : k mod m + 1 ≤ m, from succ_le_of_lt (mod_lt H4),
-have H6 [visible] : m - (k mod m + 1) < m, from sub_lt_self H4 !succ_pos,
+assert H3 : n - k div m = n - k div m - 1 + 1, from (sub_add_cancel H2)⁻¹,
+assert H4 : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero _ (!zero_mul ▸ H' ▸ H)),
+have H5   : k mod m + 1 ≤ m, from succ_le_of_lt (mod_lt H4),
+assert H6 : m - (k mod m + 1) < m, from sub_lt_self H4 !succ_pos,
 calc
   (m * n - (k + 1)) div m = (m * n - (k div m * m + k mod m + 1)) div m : eq_div_mul_add_mod
      ... = (m * n - k div m * m - (k mod m + 1)) div m                  : by rewrite [*sub_sub]
diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index 0b80b6d3c..537720a00 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -121,9 +121,9 @@ theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) {C : B → Type} {f : forall (a : A), C (abs a)}
   (H : forall (r s : A) (H' : R r s), eq.rec_on (eq_abs Q H') (f r) = f s)
   {a : A} (Ha : R a a) : rec Q f (abs a) = f a :=
-have H2  [visible] : R a (rep (abs a)), from
+assert H2  : R a (rep (abs a)), from
   R_rep_abs Q Ha,
-have Heq [visible] : abs (rep (abs a)) = abs a, from
+assert Heq : abs (rep (abs a)) = abs a, from
   abs_rep Q (abs a),
 calc
   rec Q f (abs a) =  eq.rec_on Heq (f (rep (abs a))) : rfl
diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean
index 88447d6b9..5f00ad1fd 100644
--- a/library/data/quotient/classical.lean
+++ b/library/data/quotient/classical.lean
@@ -35,7 +35,7 @@ have H3 : ∀c, R a c ↔ R b c, from
       (assume H4 : R b c, transR H2 H4),
 have H4 : (fun c, R a c) = (fun c, R b c), from
   funext (take c, eq.of_iff (H3 c)),
-have H5 [visible] : nonempty A, from
+assert H5 : nonempty A, from
   nonempty.intro a,
 show epsilon (λc, R a c) = epsilon (λc, R b c), from
   congr_arg _ H4
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index a5d9088b8..835db2507 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -92,7 +92,6 @@ opaque definition revert_lst (ids : expr_list) : tactic := builtin
 notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l
 
 opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin
-notation `assert` `(` id `:` ty `)` := assert_hypothesis id ty
 
 infixl `;`:15 := and_then
 notation `[` h:10 `|`:10 r:(foldl:10 `|` (e r, or_else r e) h) `]` := r
diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean
index 4be528a36..2810ff2df 100644
--- a/library/logic/connectives.lean
+++ b/library/logic/connectives.lean
@@ -177,6 +177,6 @@ section
   theorem if_congr [H₁ : decidable c₁] {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂)
       (He : e₁ = e₂) :
     (if c₁ then t₁ else e₁) = (@ite c₂ (decidable_of_decidable_of_iff H₁ Hc) A t₂ e₂) :=
-  have H2 [visible] : decidable c₂, from (decidable_of_decidable_of_iff H₁ Hc),
+  assert H2 : decidable c₂, from (decidable_of_decidable_of_iff H₁ Hc),
   if_congr_aux Hc Ht He
 end
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 862c9eba3..f7340f2e6 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -98,7 +98,7 @@
 (defconst lean-font-lock-defaults
   `((;; Keywords
      (,(rx word-start (or "calc" "have" "obtains" "show" "by" "in" "at" "let" "forall" "fun"
-                            "exists" "if" "dif" "then" "else" "assume" "take" "obtain" "from") word-end)
+                            "exists" "if" "dif" "then" "else" "assume" "assert" "take" "obtain" "from") word-end)
       . font-lock-keyword-face)
      ;; String
      ("\"[^\"]*\"" . 'font-lock-string-face)
@@ -131,7 +131,7 @@
             (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply"
                 "apply" "fapply" "rename" "intro" "intros"
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat"
-                "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "assert" "rewrite" "esimp" "unfold"))
+                "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" "unfold"))
            word-end)
       (1 'font-lock-constant-face))
      ;; Types
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index acd6ba027..82a208fe7 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -181,6 +181,14 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
             tacs.push_back(parse_begin_end_core(p, pos, get_rcurly_tk(), true));
         } else if (p.curr_is_token(end_token)) {
             break;
+        } else if (p.curr_is_token(get_assert_tk())) {
+            auto pos = p.pos();
+            p.next();
+            name id  = p.check_id_next("invalid 'assert' tactic, identifier expected");
+            p.check_token_next(get_colon_tk(), "invalid 'assert' tactic, ':' expected");
+            expr A   = p.parse_expr();
+            expr assert_tac = p.save_pos(mk_assert_tactic_expr(id, A), pos);
+            tacs.push_back(mk_begin_end_element_annotation(assert_tac));
         } else if (p.curr_is_token(get_have_tk())) {
             auto pos = p.pos();
             p.next();
@@ -318,9 +326,8 @@ static expr parse_proof(parser & p, expr const & prop) {
     }
 }
 
-static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> const & prev_local) {
+static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> const & prev_local, bool is_visible) {
     auto id_pos       = p.pos();
-    bool is_visible   = false;
     name id;
     expr prop;
     if (p.curr_is_token(get_visible_tk())) {
@@ -333,7 +340,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
         p.next();
         if (p.curr_is_token(get_visible_tk())) {
             p.next();
-            p.check_token_next(get_colon_tk(), "invalid 'have' declaration, ':' expected");
+            p.check_token_next(get_colon_tk(), "invalid 'have/assert' declaration, ':' expected");
             is_visible = true;
             prop       = p.parse_expr();
         } else if (p.curr_is_token(get_colon_tk())) {
@@ -348,7 +355,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
         id            = p.mk_fresh_name();
         prop          = p.parse_expr();
     }
-    p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected");
+    p.check_token_next(get_comma_tk(), "invalid 'have/assert' declaration, ',' expected");
     expr proof;
     if (prev_local) {
         parser::local_scope scope(p);
@@ -360,7 +367,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
     } else {
         proof = parse_proof(p, prop);
     }
-    p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected");
+    p.check_token_next(get_comma_tk(), "invalid 'have/assert' declaration, ',' expected");
     parser::local_scope scope(p);
     binder_info bi = mk_contextual_info(is_visible);
     expr l = p.save_pos(mk_local(id, prop, bi), pos);
@@ -369,8 +376,14 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
     if (p.curr_is_token(get_then_tk())) {
         auto then_pos = p.pos();
         p.next();
-        p.check_token_next(get_have_tk(), "invalid 'then have' declaration, 'have' expected");
-        body  = parse_have_core(p, then_pos, some_expr(l));
+        if (p.curr_is_token(get_assert_tk())) {
+            p.next();
+            is_visible = true;
+        } else {
+            p.check_token_next(get_have_tk(), "invalid 'then' declaration, 'have' or 'assert' expected");
+            is_visible = false;
+        }
+        body  = parse_have_core(p, then_pos, some_expr(l), is_visible);
     } else {
         body  = p.parse_expr();
     }
@@ -381,7 +394,11 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
 }
 
 static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return parse_have_core(p, pos, none_expr());
+    return parse_have_core(p, pos, none_expr(), false);
+}
+
+static expr parse_assert(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return parse_have_core(p, pos, none_expr(), true);
 }
 
 static name * H_show = nullptr;
@@ -539,6 +556,7 @@ parse_table init_nud_table() {
     r = r.add({transition("_", mk_ext_action(parse_placeholder))}, x0);
     r = r.add({transition("by", mk_ext_action_core(parse_by))}, x0);
     r = r.add({transition("have", mk_ext_action(parse_have))}, x0);
+    r = r.add({transition("assert", mk_ext_action(parse_assert))}, x0);
     r = r.add({transition("show", mk_ext_action(parse_show))}, x0);
     r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0);
     r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 7939da1ad..1a7cc2e40 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -74,7 +74,7 @@ static char const * g_decreasing_unicode = "↓";
 
 void init_token_table(token_table & t) {
     pair<char const *, unsigned> builtin[] =
-        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"show", 0}, {"obtain", 0},
+        {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"show", 0}, {"obtain", 0},
          {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 4a999d247..eff3c52a2 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -47,6 +47,7 @@ static name * g_import       = nullptr;
 static name * g_prelude      = nullptr;
 static name * g_show         = nullptr;
 static name * g_have         = nullptr;
+static name * g_assert       = nullptr;
 static name * g_assume       = nullptr;
 static name * g_take         = nullptr;
 static name * g_fun          = nullptr;
@@ -165,6 +166,7 @@ void initialize_tokens() {
     g_prelude      = new name("prelude");
     g_show         = new name("show");
     g_have         = new name("have");
+    g_assert       = new name("assert");
     g_assume       = new name("assume");
     g_take         = new name("take");
     g_fun          = new name("fun");
@@ -321,6 +323,7 @@ void finalize_tokens() {
     delete g_take;
     delete g_assume;
     delete g_have;
+    delete g_assert;
     delete g_show;
     delete g_import;
     delete g_prelude;
@@ -403,6 +406,7 @@ name const & get_import_tk() { return *g_import; }
 name const & get_prelude_tk() { return *g_prelude; }
 name const & get_show_tk() { return *g_show; }
 name const & get_have_tk() { return *g_have; }
+name const & get_assert_tk() { return *g_assert; }
 name const & get_assume_tk() { return *g_assume; }
 name const & get_take_tk() { return *g_take; }
 name const & get_fun_tk() { return *g_fun; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 6dd0dbed6..3fa950980 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -49,6 +49,7 @@ name const & get_import_tk();
 name const & get_prelude_tk();
 name const & get_show_tk();
 name const & get_have_tk();
+name const & get_assert_tk();
 name const & get_assume_tk();
 name const & get_take_tk();
 name const & get_fun_tk();
diff --git a/tests/lean/assert_fail.lean b/tests/lean/assert_fail.lean
index 04fe26782..7471f4958 100644
--- a/tests/lean/assert_fail.lean
+++ b/tests/lean/assert_fail.lean
@@ -1,10 +1,10 @@
 example (a b : Prop) (H : b ∧ a) : a ∧ b :=
 begin
-  assert (H : a)
+  assert  H : a
 end
 
 example (a : Prop) (Ha : a) : a :=
 begin
   exact Ha,
-  assert (H : a)
+  assert  H : a
 end
diff --git a/tests/lean/run/assert_tac.lean b/tests/lean/run/assert_tac.lean
index e4a3ebf61..ad95c5112 100644
--- a/tests/lean/run/assert_tac.lean
+++ b/tests/lean/run/assert_tac.lean
@@ -4,7 +4,7 @@ variables {A : Type} {a a' : A}
 
 definition to_eq₁ (H : a == a') : a = a' :=
 begin
-  assert (H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a),
+  assert H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a,
   intro Ht,
     exact (eq.refl (eq.rec_on Ht a)),
   show a = a', from
diff --git a/tests/lean/run/have6.lean b/tests/lean/run/have6.lean
index b98b07533..1ee7b0d0d 100644
--- a/tests/lean/run/have6.lean
+++ b/tests/lean/run/have6.lean
@@ -9,11 +9,11 @@ axiom Hb : b
 axiom Hc : c
 check
   have a ∧ b, from and_intro a b Ha Hb,
-  have [visible] b ∧ a, from and_intro b a Hb Ha,
+  assert b ∧ a, from and_intro b a Hb Ha,
   have H : a ∧ b, from and_intro a b Ha Hb,
-  have H [visible] : a ∧ b, from and_intro a b Ha Hb,
+  assert H : a ∧ b, from and_intro a b Ha Hb,
   then have a ∧ b, from and_intro a b Ha Hb,
-  then have [visible] b ∧ a, from and_intro b a Hb Ha,
+  then assert b ∧ a, from and_intro b a Hb Ha,
   then have H : a ∧ b, from and_intro a b Ha Hb,
-  then have H [visible] : a ∧ b, from and_intro a b Ha Hb,
+  then assert H : a ∧ b, from and_intro a b Ha Hb,
     Ha