feat(frontends/lean): allow tactics to be used in axiom/variable declarations and in the type of definitions/theorems; add a new test showing the need for this feature

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

src/frontends/lean/parser_cmds.cpp

@@ -152,12 +152,14 @@ void parser_imp::parse_def_core(bool is_definition) {
     expr type = std::get<0>(r);
     expr val  = std::get<1>(r);
     metavar_env menv = std::get<2>(r);
-    check_no_metavar(type, menv, "invalid definition, type still contains metavariables after elaboration");
-    if (has_metavar(val)) {
-        val = apply_tactics(val, menv);
-    } else {
-        check_no_metavar(val, menv, "invalid definition, value still contains metavariables after elaboration");
+    if (has_metavar(type)) {
+        type = apply_tactics(type, menv);
+        val  = menv->instantiate_metavars(val); // val may contain metavariables instantiated in the previous step
     }
+    check_no_metavar(type, menv, "invalid definition, type still contains metavariables after elaboration");
+    if (has_metavar(val))
+        val = apply_tactics(val, menv);
+    check_no_metavar(val, menv, "invalid definition, value still contains metavariables after elaboration");
     lean_assert(!has_metavar(val));
     name full_id = mk_full_name(id);
     if (is_definition) {
@@ -198,22 +200,24 @@ void parser_imp::parse_theorem() {
 void parser_imp::parse_variable_core(bool is_var) {
     next();
     name id = check_identifier_next("invalid variable/axiom declaration, identifier expected");
+    expr pre_type;
     parameter_buffer parameters;
-    expr type;
     if (curr_is_colon()) {
         next();
-        auto p = m_elaborator(parse_expr());
-        check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
-        type = p.first;
+        pre_type = parse_expr();
     } else {
         mk_scope scope(*this);
         parse_var_decl_parameters(parameters);
         check_colon_next("invalid variable/axiom declaration, ':' expected");
         expr type_body = parse_expr();
-        auto p = m_elaborator(mk_abstraction(false, parameters, type_body));
-        check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
-        type = p.first;
+        pre_type = mk_abstraction(false, parameters, type_body);
     }
+    auto p = m_elaborator(pre_type);
+    expr type = p.first;
+    metavar_env menv = p.second;
+    if (has_metavar(type))
+        type = apply_tactics(type, menv);
+    check_no_metavar(type, menv, "invalid variable/axiom, type still contains metavariables after elaboration");
     name full_id = mk_full_name(id);
     if (is_var)
         m_env->add_var(full_id, type);

tests/lean/tactic_at_types.lean

@@ -0,0 +1,24 @@
+import tactic
+import cast
+set_option pp::implicit true -- to be able to parse output produced by Lean
+variable vec : Nat → Type
+variables n m : Nat
+variable v1 : vec (n + m)
+variable v2 : vec (m + n)
+rewrite_set S
+add_rewrite Nat::add_comm Nat::add_assoc Nat::add_left_comm eq_id : S
+axiom Ax1    : v1 = cast (by simp S) v2
+variable Ax2 : v2 = cast (by simp S) v1
+
+variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m)
+infixl   65 ; : concat
+variable empty : vec 0
+axiom    concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) :
+             (v1 ; v2) ; v3 = cast (by simp S) (v1 ; (v2 ; v3))
+add_rewrite Nat::add_zeror Nat::add_zerol : S
+axiom    concat_empty {n : Nat} (v : vec n) :
+             v ; empty = cast (by simp S) v
+
+theorem T1 (n m : Nat) (v : vec (n + m)) (w : vec (m + n)) (H : v = cast (by simp S) w) :
+                  w = cast (by simp S) v
+:= (by simp S)

tests/lean/tactic_at_types.lean.expected.out

@@ -0,0 +1,17 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'tactic'
+  Imported 'cast'
+  Set: lean::pp::implicit
+  Assumed: vec
+  Assumed: n
+  Assumed: m
+  Assumed: v1
+  Assumed: v2
+  Assumed: Ax1
+  Assumed: Ax2
+  Assumed: concat
+  Assumed: empty
+  Assumed: concat_assoc
+  Assumed: concat_empty
+  Proved: T1