feat(frontends/lean): add type notation for referencing hypotheses

library/theories/number_theory/primes.lean

@@ -65,10 +65,10 @@ assume h d, obtain h₁ h₂, from h, h₂ m d
 
 lemma gt_one_of_pos_of_prime_dvd {i p : nat} : prime p → 0 < i → i mod p = 0 → 1 < i :=
 assume ipp pos h,
-have h₁ : p ≥ 2, from ge_two_of_prime ipp,
+have p ≥ 2,  from ge_two_of_prime ipp,
-have p ∣ i,       from dvd_of_mod_eq_zero h,
+have p ∣ i,   from dvd_of_mod_eq_zero h,
-have p ≤ i,      from le_of_dvd pos this,
+have p ≤ i,  from le_of_dvd pos this,
-lt_of_succ_le (le.trans h₁ this)
+lt_of_succ_le (le.trans `2 ≤ p` this)
 
 definition sub_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≠ 1 ∧ m ≠ n} :=
 assume h₁ h₂,
@@ -124,30 +124,30 @@ definition infinite_primes (n : nat) : {p | p ≥ n ∧ prime p} :=
 let m := fact (n + 1) in
 have m ≥ 1,     from le_of_lt_succ (succ_lt_succ (fact_pos _)),
 have m + 1 ≥ 2, from succ_le_succ this,
-obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd this,
+obtain p (pp : prime p) (pd : p ∣ m + 1), from sub_prime_and_dvd this,
-have p_ge_2 : p ≥ 2, from ge_two_of_prime prime_p,
+have p ≥ 2, from ge_two_of_prime `prime p`,
-have p_gt_0 : p > 0, from lt_of_succ_lt (lt_of_succ_le p_ge_2),
+have p > 0, from lt_of_succ_lt (lt_of_succ_le `p ≥ 2`),
 have p ≥ n, from by_contradiction
   (suppose ¬ p ≥ n,
     have p < n,     from lt_of_not_ge this,
     have p ≤ n + 1, from le_of_lt (lt.step this),
-    have p ∣ m,      from dvd_fact p_gt_0 this,
+    have p ∣ m,      from dvd_fact `p > 0` this,
-    have p ∣ 1,      from dvd_of_dvd_add_right (!add.comm ▸ p_dvd_m1) this,
+    have p ∣ 1,      from dvd_of_dvd_add_right (!add.comm ▸ `p ∣ m + 1`) this,
     have p ≤ 1,     from le_of_dvd zero_lt_one this,
-    absurd (le.trans p_ge_2 this) dec_trivial),
+    absurd (le.trans `2 ≤ p` `p ≤ 1`) dec_trivial),
-subtype.tag p (and.intro this prime_p)
+subtype.tag p (and.intro this `prime p`)
 
 lemma ex_infinite_primes (n : nat) : ∃ p, p ≥ n ∧ prime p :=
 ex_of_sub (infinite_primes n)
 
 lemma odd_of_prime {p : nat} : prime p → p > 2 → odd p :=
 λ pp p_gt_2, by_contradiction (λ hn,
-  have even_p : even p, from even_of_not_odd hn,
+  have even p, from even_of_not_odd hn,
-  obtain k (hk : p = 2*k), from exists_of_even even_p,
+  obtain k (hk : p = 2*k), from exists_of_even this,
-  assert two_div_p : 2 ∣ p, by rewrite [hk]; apply dvd_mul_right,
+  assert 2 ∣ p, by rewrite [hk]; apply dvd_mul_right,
-  or.elim (eq_one_or_eq_self_of_prime_of_dvd pp two_div_p)
+  or.elim (eq_one_or_eq_self_of_prime_of_dvd pp this)
-    (λ h : 2 = 1, absurd h dec_trivial)
+    (suppose 2 = 1, absurd this dec_trivial)
-    (λ h : 2 = p, by subst h; exact absurd p_gt_2 !lt.irrefl))
+    (suppose 2 = p, by subst this; exact absurd p_gt_2 !lt.irrefl))
 
 theorem dvd_of_prime_of_not_coprime {p n : ℕ} (primep : prime p) (nc : ¬ coprime p n) : p ∣ n :=
 have H : gcd p n = 1 ∨ gcd p n = p, from eq_one_or_eq_self_of_prime_of_dvd primep !gcd_dvd_left,
@@ -195,8 +195,8 @@ lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p
 | (succ n) hp hd :=
   have p ∣ (m^n)*m, by rewrite [pow_succ at hd]; exact hd,
   or.elim (dvd_or_dvd_of_prime_of_dvd_mul hp this)
-    (λ h : p ∣ m^n, dvd_of_prime_of_dvd_pow hp h)
+    (suppose p ∣ m^n, dvd_of_prime_of_dvd_pow hp this)
-    (λ h : p ∣ m, h)
+    (suppose p ∣ m, this)
 
 lemma coprime_pow_of_prime_of_not_dvd {p m a : nat} : prime p → ¬ p ∣ a → coprime a (p^m) :=
 λ h₁ h₂, coprime_pow_right m (coprime_swap (coprime_of_prime_of_not_dvd h₁ h₂))
@@ -205,21 +205,21 @@ lemma coprime_primes {p q : nat} : prime p → prime q → p ≠ q → coprime p
 λ hp hq hn,
   assert gcd p q ∣ p, from !gcd_dvd_left,
   or.elim (eq_one_or_eq_self_of_prime_of_dvd hp this)
-    (λ h : gcd p q = 1, h)
+    (suppose gcd p q = 1, this)
-    (λ h : gcd p q = p,
+    (assume h : gcd p q = p,
       assert gcd p q ∣ q, from !gcd_dvd_right,
       have   p ∣ q, by rewrite -h; exact this,
       or.elim (eq_one_or_eq_self_of_prime_of_dvd hq this)
-        (λ h₁ : p = 1, by subst p; exact absurd hp not_prime_one)
+        (suppose p = 1, by subst p; exact absurd hp not_prime_one)
-        (λ he : p = q, by contradiction))
+        (suppose p = q, by contradiction))
 
 lemma coprime_pow_primes {p q : nat} (n m : nat) : prime p → prime q → p ≠ q → coprime (p^n) (q^m) :=
 λ hp hq hn, coprime_pow_right m (coprime_pow_left n (coprime_primes hp hq hn))
 
 lemma coprime_or_dvd_of_prime {p} (Pp : prime p) (i : nat) : coprime p i ∨ p ∣ i :=
 by_cases
- (λ h : p ∣ i, or.inr h)
+ (suppose p ∣ i, or.inr this)
- (λ h : ¬ p ∣ i, or.inl (coprime_of_prime_of_not_dvd Pp h))
+ (suppose ¬ p ∣ i, or.inl (coprime_of_prime_of_not_dvd Pp this))
 
 lemma eq_one_or_dvd_of_dvd_prime_pow {p : nat} : ∀ {m i : nat}, prime p → i ∣ (p^m) → i = 1 ∨ p ∣ i
 | 0        := take i, assume Pp, begin rewrite [pow_zero], intro Pdvd, apply or.inl (eq_one_of_dvd_one Pdvd) end

src/frontends/lean/notation_cmd.cpp

@@ -813,6 +813,7 @@ static environment dispatch_notation_cmd(parser & p, bool overload, notation_ent
 }
 
 environment local_notation_cmd(parser & p) {
+    parser::in_notation_ctx ctx(p);
     bool overload   = false; // REMARK: local notation override global one
     notation_entry_group grp = notation_entry_group::Main;
     bool persistent = false;
@@ -820,6 +821,7 @@ environment local_notation_cmd(parser & p) {
 }
 
 static environment reserve_cmd(parser & p) {
+    parser::in_notation_ctx ctx(p);
     bool overload   = false;
     notation_entry_group grp = notation_entry_group::Reserve;
     bool persistent = true;
@@ -849,4 +851,12 @@ void register_notation_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("tactic_notation", "declare a new tacitc notation", tactic_notation_cmd));
     add_cmd(r, cmd_info("reserve",         "reserve notation", reserve_cmd));
 }
+
+bool is_notation_cmd(name const & n) {
+    return
+        n == get_infix_tk() || n == get_infixl_tk() || n == get_infixr_tk() || n == get_postfix_tk() ||
+        n == get_prefix_tk() || n == get_notation_tk() || n == get_precedence_tk() ||
+        n == get_tactic_infix_tk() || n == get_tactic_infixl_tk() || n == get_tactic_infixr_tk() || n == get_tactic_postfix_tk() ||
+        n == get_tactic_prefix_tk() || n == get_tactic_notation_tk();
+}
 }

src/frontends/lean/notation_cmd.h

@@ -21,4 +21,6 @@ notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & n
 environment local_notation_cmd(parser & p);
 
 void register_notation_cmds(cmd_table & r);
+
+bool is_notation_cmd(name const & cmd_name);
 }

src/frontends/lean/parser.cpp

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/scoped_ext.h"
 #include "library/explicit.h"
+#include "library/typed_expr.h"
 #include "library/let.h"
 #include "library/num.h"
 #include "library/string.h"
@@ -111,7 +112,8 @@ parser::parser(environment const & env, io_state const & ios,
     m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
     m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) {
     m_local_decls_size_at_beg_cmd = 0;
-    m_profile    = ios.get_options().get_bool("profile", false);
+    m_in_backtick = false;
+    m_profile     = ios.get_options().get_bool("profile", false);
     if (num_threads > 1 && m_profile)
         throw exception("option --profile cannot be used when theorems are compiled in parallel");
     m_has_params = false;
@@ -961,6 +963,7 @@ local_environment parser::parse_binders(buffer<expr> & r, buffer<notation_entry>
 
 bool parser::parse_local_notation_decl(buffer<notation_entry> * nentries) {
     if (curr_is_notation_decl(*this)) {
+        parser::in_notation_ctx ctx(*this);
         buffer<token_entry> new_tokens;
         bool overload    = false;
         bool allow_local = true;
@@ -1327,6 +1330,19 @@ expr parser::parse_string_expr() {
     return from_string(v);
 }
 
+expr parser::parse_backtick_expr() {
+    auto p = pos();
+    next();
+    flet<bool> set(m_in_backtick, true);
+    expr type = parse_expr();
+    if (curr() != scanner::token_kind::Backtick) {
+        throw parser_error("invalid expression, '`' expected", pos());
+    }
+    next();
+    expr assump = mk_by_plus(save_pos(mk_constant(get_tactic_assumption_name()), p), p);
+    return save_pos(mk_typed_expr(type, assump), p);
+}
+
 expr parser::parse_nud() {
     switch (curr()) {
     case scanner::token_kind::Keyword:     return parse_nud_notation();
@@ -1334,6 +1350,7 @@ expr parser::parse_nud() {
     case scanner::token_kind::Numeral:     return parse_numeral_expr();
     case scanner::token_kind::Decimal:     return parse_decimal_expr();
     case scanner::token_kind::String:      return parse_string_expr();
+    case scanner::token_kind::Backtick:    return parse_backtick_expr();
     default: throw parser_error("invalid expression, unexpected token", pos());
     }
 }
@@ -1355,6 +1372,8 @@ unsigned parser::curr_lbp_core(bool as_tactic) const {
     case scanner::token_kind::CommandKeyword: case scanner::token_kind::Eof:
     case scanner::token_kind::ScriptBlock:    case scanner::token_kind::QuotedSymbol:
         return 0;
+    case scanner::token_kind::Backtick:
+        return m_in_backtick ? 0 : get_max_prec();
     case scanner::token_kind::Identifier:     case scanner::token_kind::Numeral:
     case scanner::token_kind::Decimal:        case scanner::token_kind::String:
         return get_max_prec();
@@ -1636,9 +1655,16 @@ void parser::parse_command() {
     name const & cmd_name = get_token_info().value();
     m_cmd_token = get_token_info().token();
     if (auto it = cmds().find(cmd_name)) {
-        next();
+        if (is_notation_cmd(cmd_name)) {
-        m_local_decls_size_at_beg_cmd = m_local_decls.size();
+            in_notation_ctx ctx(*this);
-        m_env = it->get_fn()(*this);
+            next();
+            m_local_decls_size_at_beg_cmd = m_local_decls.size();
+            m_env = it->get_fn()(*this);
+        } else {
+            next();
+            m_local_decls_size_at_beg_cmd = m_local_decls.size();
+            m_env = it->get_fn()(*this);
+        }
     } else {
         auto p = pos();
         next();

src/frontends/lean/parser.h

@@ -233,6 +233,9 @@ class parser {
     elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp);
     elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp);
 
+    bool m_in_backtick; // true if parser `expr` notation
+    expr parse_backtick_expr();
+
     optional<expr> is_tactic_command(name & id);
     expr parse_tactic_option_num();
     expr parse_tactic_led(expr left);
@@ -511,6 +514,12 @@ public:
 
     /** parse all commands in the input stream */
     bool operator()() { return parse_commands(); }
+
+    class in_notation_ctx {
+        scanner::in_notation_ctx m_ctx;
+    public:
+        in_notation_ctx(parser & p):m_ctx(p.m_scanner) {}
+    };
 };
 
 bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name,

src/frontends/lean/scanner.cpp

@@ -437,7 +437,12 @@ auto scanner::scan(environment const & env) -> token_kind {
         case '\"':
             return read_string();
         case '`':
-            return read_quoted_symbol();
+            if (m_in_notation) {
+                return read_quoted_symbol();
+            } else {
+                next();
+                return token_kind::Backtick;
+            }
         case -1:
             return token_kind::Eof;
         default:
@@ -471,6 +476,7 @@ scanner::scanner(std::istream & strm, char const * strm_name, unsigned line):
     m_line  = line;
     m_spos  = 0;
     m_upos  = 0;
+    m_in_notation = false;
     if (std::getline(m_stream, m_curr_line)) {
         m_last_line = false;
         m_curr_line.push_back('\n');

src/frontends/lean/scanner.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include <iostream>
 #include "util/name.h"
+#include "util/flet.h"
 #include "util/numerics/mpq.h"
 #include "kernel/environment.h"
 #include "frontends/lean/token_table.h"
@@ -22,7 +23,7 @@ namespace lean {
 */
 class scanner {
 public:
-    enum class token_kind {Keyword, CommandKeyword, ScriptBlock, Identifier, Numeral, Decimal, String, QuotedSymbol, Eof};
+    enum class token_kind {Keyword, CommandKeyword, ScriptBlock, Identifier, Numeral, Decimal, String, QuotedSymbol, Backtick, Eof};
 protected:
     token_table const * m_tokens;
     std::istream &      m_stream;
@@ -45,6 +46,9 @@ protected:
     std::string         m_buffer;
     std::string         m_aux_buffer;
 
+    bool                m_in_notation;
+
+
     [[ noreturn ]] void throw_exception(char const * msg);
     void next();
     char curr() const { return m_curr; }
@@ -80,6 +84,12 @@ public:
     token_info const & get_token_info() const { return m_token_info; }
 
     std::string const & get_stream_name() const { return m_stream_name; }
+
+    class in_notation_ctx {
+        flet<bool> m_in_notation;
+    public:
+        in_notation_ctx(scanner & s):m_in_notation(s.m_in_notation, true) {}
+    };
 };
 std::ostream & operator<<(std::ostream & out, scanner::token_kind k);
 void initialize_scanner();

src/frontends/lean/tokens.cpp

@@ -126,12 +126,19 @@ static name const * g_foldr_tk = nullptr;
 static name const * g_foldl_tk = nullptr;
 static name const * g_binder_tk = nullptr;
 static name const * g_binders_tk = nullptr;
+static name const * g_precedence_tk = nullptr;
 static name const * g_infix_tk = nullptr;
 static name const * g_infixl_tk = nullptr;
 static name const * g_infixr_tk = nullptr;
 static name const * g_postfix_tk = nullptr;
 static name const * g_prefix_tk = nullptr;
 static name const * g_notation_tk = nullptr;
+static name const * g_tactic_infix_tk = nullptr;
+static name const * g_tactic_infixl_tk = nullptr;
+static name const * g_tactic_infixr_tk = nullptr;
+static name const * g_tactic_postfix_tk = nullptr;
+static name const * g_tactic_prefix_tk = nullptr;
+static name const * g_tactic_notation_tk = nullptr;
 static name const * g_call_tk = nullptr;
 static name const * g_calc_tk = nullptr;
 static name const * g_obtain_tk = nullptr;
@@ -266,12 +273,19 @@ void initialize_tokens() {
     g_foldl_tk = new name{"foldl"};
     g_binder_tk = new name{"binder"};
     g_binders_tk = new name{"binders"};
+    g_precedence_tk = new name{"precedence"};
     g_infix_tk = new name{"infix"};
     g_infixl_tk = new name{"infixl"};
     g_infixr_tk = new name{"infixr"};
     g_postfix_tk = new name{"postfix"};
     g_prefix_tk = new name{"prefix"};
     g_notation_tk = new name{"notation"};
+    g_tactic_infix_tk = new name{"tactic_infix"};
+    g_tactic_infixl_tk = new name{"tactic_infixl"};
+    g_tactic_infixr_tk = new name{"tactic_infixr"};
+    g_tactic_postfix_tk = new name{"tactic_postfix"};
+    g_tactic_prefix_tk = new name{"tactic_prefix"};
+    g_tactic_notation_tk = new name{"tactic_notation"};
     g_call_tk = new name{"call"};
     g_calc_tk = new name{"calc"};
     g_obtain_tk = new name{"obtain"};
@@ -407,12 +421,19 @@ void finalize_tokens() {
     delete g_foldl_tk;
     delete g_binder_tk;
     delete g_binders_tk;
+    delete g_precedence_tk;
     delete g_infix_tk;
     delete g_infixl_tk;
     delete g_infixr_tk;
     delete g_postfix_tk;
     delete g_prefix_tk;
     delete g_notation_tk;
+    delete g_tactic_infix_tk;
+    delete g_tactic_infixl_tk;
+    delete g_tactic_infixr_tk;
+    delete g_tactic_postfix_tk;
+    delete g_tactic_prefix_tk;
+    delete g_tactic_notation_tk;
     delete g_call_tk;
     delete g_calc_tk;
     delete g_obtain_tk;
@@ -547,12 +568,19 @@ name const & get_foldr_tk() { return *g_foldr_tk; }
 name const & get_foldl_tk() { return *g_foldl_tk; }
 name const & get_binder_tk() { return *g_binder_tk; }
 name const & get_binders_tk() { return *g_binders_tk; }
+name const & get_precedence_tk() { return *g_precedence_tk; }
 name const & get_infix_tk() { return *g_infix_tk; }
 name const & get_infixl_tk() { return *g_infixl_tk; }
 name const & get_infixr_tk() { return *g_infixr_tk; }
 name const & get_postfix_tk() { return *g_postfix_tk; }
 name const & get_prefix_tk() { return *g_prefix_tk; }
 name const & get_notation_tk() { return *g_notation_tk; }
+name const & get_tactic_infix_tk() { return *g_tactic_infix_tk; }
+name const & get_tactic_infixl_tk() { return *g_tactic_infixl_tk; }
+name const & get_tactic_infixr_tk() { return *g_tactic_infixr_tk; }
+name const & get_tactic_postfix_tk() { return *g_tactic_postfix_tk; }
+name const & get_tactic_prefix_tk() { return *g_tactic_prefix_tk; }
+name const & get_tactic_notation_tk() { return *g_tactic_notation_tk; }
 name const & get_call_tk() { return *g_call_tk; }
 name const & get_calc_tk() { return *g_calc_tk; }
 name const & get_obtain_tk() { return *g_obtain_tk; }

src/frontends/lean/tokens.h

@@ -128,12 +128,19 @@ name const & get_foldr_tk();
 name const & get_foldl_tk();
 name const & get_binder_tk();
 name const & get_binders_tk();
+name const & get_precedence_tk();
 name const & get_infix_tk();
 name const & get_infixl_tk();
 name const & get_infixr_tk();
 name const & get_postfix_tk();
 name const & get_prefix_tk();
 name const & get_notation_tk();
+name const & get_tactic_infix_tk();
+name const & get_tactic_infixl_tk();
+name const & get_tactic_infixr_tk();
+name const & get_tactic_postfix_tk();
+name const & get_tactic_prefix_tk();
+name const & get_tactic_notation_tk();
 name const & get_call_tk();
 name const & get_calc_tk();
 name const & get_obtain_tk();

src/frontends/lean/tokens.txt

@@ -121,12 +121,19 @@ foldr        foldr
 foldl        foldl
 binder       binder
 binders      binders
+precedence   precedence
 infix        infix
 infixl       infixl
 infixr       infixr
 postfix      postfix
 prefix       prefix
 notation     notation
+tactic_infix tactic_infix
+tactic_infixl tactic_infixl
+tactic_infixr tactic_infixr
+tactic_postfix tactic_postfix
+tactic_prefix tactic_prefix
+tactic_notation tactic_notation
 call         call
 calc         calc
 obtain       obtain