feat(frontends/lean): 'by' is now also using interactive mode syntax

src/frontends/lean/CMakeLists.txt

@@ -7,4 +7,4 @@ pp.cpp structure_cmd.cpp structure_instance.cpp
 init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp
 opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
-brackets.cpp begin_end_block.cpp)
+brackets.cpp tactic_notation.cpp)

src/frontends/lean/builtin_exprs.cpp

@@ -33,7 +33,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/match_expr.h"
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/brackets.h"
-#include "frontends/lean/begin_end_block.h"
+#include "frontends/lean/tactic_notation.h"
 
 #ifndef LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE
 #define LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE true
@@ -155,17 +155,6 @@ static expr parse_unit(parser & p, unsigned, expr const *, pos_info const & pos)
     return p.save_pos(mk_constant(get_unit_star_name()), pos);
 }
 
-static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
-    p.next();
-    parser::local_scope scope(p);
-    p.clear_locals();
-    expr tac  = p.parse_expr();
-    expr type = mk_app(mk_constant(get_tactic_name()), mk_constant(get_unit_name()));
-    p.update_pos(tac, pos);
-    expr r    = p.save_pos(mk_typed_expr(type, tac), pos);
-    return p.save_pos(mk_by(r), pos);
-}
-
 static expr parse_proof(parser & p);
 
 static expr parse_proof(parser & p) {

src/frontends/lean/elaborator.cpp

@@ -43,7 +43,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 #include "frontends/lean/prenum.h"
 #include "frontends/lean/elaborator.h"
-#include "frontends/lean/begin_end_block.h"
+#include "frontends/lean/tactic_notation.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/structure_instance.h"
 

src/frontends/lean/init_module.cpp

@@ -23,7 +23,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/match_expr.h"
 #include "frontends/lean/notation_cmd.h"
-#include "frontends/lean/begin_end_block.h"
+#include "frontends/lean/tactic_notation.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
@@ -46,10 +46,10 @@ void initialize_frontend_lean_module() {
     initialize_match_expr();
     initialize_elaborator();
     initialize_notation_cmd();
-    initialize_begin_end_block();
+    initialize_tactic_notation();
 }
 void finalize_frontend_lean_module() {
-    finalize_begin_end_block();
+    finalize_tactic_notation();
     finalize_notation_cmd();
     finalize_elaborator();
     finalize_match_expr();

src/frontends/lean/tactic_notation.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "library/annotation.h"
 #include "library/constants.h"
 #include "library/quote.h"
+#include "library/typed_expr.h"
 #include "library/placeholder.h"
 #include "library/tactic/elaborate.h"
 #include "frontends/lean/parser.h"
@@ -212,6 +213,14 @@ static expr parse_tactic_interactive(parser & p, name const & decl_name) {
     return p.rec_save_pos(mk_app(mk_constant(decl_name), args), pos);
 }
 
+static expr parse_tactic(parser & p) {
+    if (auto dname = is_tactic_interactive(p)) {
+        return parse_tactic_interactive(p, *dname);
+    } else {
+        return p.parse_expr();
+    }
+}
+
 expr parse_begin_end_core(parser & p, pos_info const & start_pos,
                           name const & end_token, bool nested = false) {
     p.next();
@@ -233,10 +242,8 @@ expr parse_begin_end_core(parser & p, pos_info const & start_pos,
                 next_tac = parse_begin_end_core(p, pos, get_rcurly_tk(), true);
             } else if (p.curr_is_token(end_token)) {
                 break;
-            } else if (auto dname = is_tactic_interactive(p)) {
-                next_tac = parse_tactic_interactive(p, *dname);
             } else {
-                next_tac = p.parse_expr();
+                next_tac = parse_tactic(p);
             }
             r = concat(p, r, next_tac, start_pos, pos);
         }
@@ -258,7 +265,19 @@ expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) {
     return parse_begin_end_core(p, pos, get_end_tk());
 }
 
-void initialize_begin_end_block() {
+expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
+    p.next();
+    parser::local_scope scope(p);
+    p.clear_locals();
+    expr tac  = parse_tactic(p);
+    expr type = mk_tactic_unit();
+    p.update_pos(tac, pos);
+    expr r    = p.save_pos(mk_typed_expr(type, tac), pos);
+    return p.save_pos(mk_by(r), pos);
+}
+
+
+void initialize_tactic_notation() {
     g_begin_end  = new name("begin_end");
     register_annotation(*g_begin_end);
 
@@ -266,7 +285,7 @@ void initialize_begin_end_block() {
     register_annotation(*g_begin_end_element);
 }
 
-void finalize_begin_end_block() {
+void finalize_tactic_notation() {
     delete g_begin_end;
     delete g_begin_end_element;
 }

src/frontends/lean/tactic_notation.h

@@ -9,10 +9,11 @@ Author: Leonardo de Moura
 namespace lean {
 expr parse_begin_end_core(parser & p, pos_info const & start_pos, name const & end_token, bool nested = false);
 expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos);
+expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos);
 bool is_begin_end_block(expr const & e);
 bool is_begin_end_element(expr const & e);
 void get_begin_end_block_elements(expr const & e, buffer<expr> & elems);
 expr update_begin_end_block(expr const & e, buffer<expr> const & elems);
-void initialize_begin_end_block();
-void finalize_begin_end_block();
+void initialize_tactic_notation();
+void finalize_tactic_notation();
 }

tests/lean/run/back_chaining2.lean

@@ -5,7 +5,7 @@ attribute [intro] Huq Hur Hus Hut
 
 open tactic
 
-definition lemma1 : (P → Q) → P → Q := by intros >> back_chaining_using_hs
-definition lemma2 : (P → Q) → (Q → R) → P → R := by intros >> back_chaining_using_hs
-definition lemma3 : (P → Q) → (Q → R) → (R → S) → P → S := by intros >> back_chaining_using_hs
-definition lemma4 : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by intros >> back_chaining_using_hs
+definition lemma1 : (P → Q) → P → Q := by (intros >> back_chaining_using_hs)
+definition lemma2 : (P → Q) → (Q → R) → P → R := by (intros >> back_chaining_using_hs)
+definition lemma3 : (P → Q) → (Q → R) → (R → S) → P → S := by (intros >> back_chaining_using_hs)
+definition lemma4 : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by (intros >> back_chaining_using_hs)

tests/lean/run/back_chaining3.lean

@@ -12,7 +12,7 @@ constant subtype_trans : ∀ S T U, subtype S T → subtype T U → subtype S U
 attribute [intro] subtype_refl subtype_trans
 
 lemma L1 : ∀ T1 T2 T3 T4, subtype T1 T2 → subtype T2 T3 → subtype T3 T4 → subtype T1 T4 :=
-by intros >> back_chaining_using_hs
+by (intros >> back_chaining_using_hs)
 
 lemma L2 : ∀ T1 T2 T3 T4, subtype T1 T2 → subtype T2 T3 → subtype T3 T4 → subtype T1 T4 :=
 by do
@@ -24,6 +24,6 @@ by do
 set_option back_chaining.max_depth 10
 
 lemma L3 : ∀ T1 T2 T3 T4 T5 T6 (H1 :subtype T1 T2) (H2 : subtype T2 T3) (H3 : subtype T3 T4) (H3 : subtype T4 T5) (H4 : subtype T5 T6), subtype T1 T6 :=
-by intros >> back_chaining_using_hs
+by (intros >> back_chaining_using_hs)
 
 end ex

tests/lean/run/calc_tac.lean

@@ -0,0 +1,8 @@
+axiom add_zero {A : Type} [has_add A] [has_zero A] : ∀ a : A, a + 0 = a
+axiom add_comm {A : Type} [has_add A] : ∀ a b : A, a + b = b + a
+
+example {A : Type} [has_add A] [has_zero A] [has_one A] (a b c : A) : b = 0 → a + b + c = c + a :=
+assume h,
+calc a + b + c = a + 0 + c : by rw h
+           ... = a + c     : by rw add_zero
+           ... = c + a     : by rw add_comm