feat(frontends/lean): calculational proofs

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

src/builtin/kernel.lean

@@ -106,6 +106,15 @@ Theorem Absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
 Theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b
 := Subst H2 H1.
 
+Theorem ImpTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c
+:= assume Ha, MP H2 (MP H1 Ha).
+
+Theorem ImpEqTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b == c) : a ⇒ c
+:= assume Ha, EqMP H2 (MP H1 Ha).
+
+Theorem EqImpTrans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c
+:= assume Ha, MP H2 (EqMP H1 Ha).
+
 Theorem DoubleNeg (a : Bool) : (¬ ¬ a) == a
 := Case (λ x, (¬ ¬ x) == x) Trivial Trivial a.
 
@@ -224,7 +233,6 @@ effectiveness of Lean's elaborator.
 *)
 
 SetOpaque implies true.
-SetOpaque iff     true.
 SetOpaque not     true.
 SetOpaque or      true.
 SetOpaque and     true.

src/frontends/lean/CMakeLists.txt

@@ -1,7 +1,7 @@
 add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp
   parser.cpp parser_imp.cpp parser_expr.cpp parser_error.cpp
   parser_imp.cpp parser_cmds.cpp parser_level.cpp parser_tactic.cpp
-  parser_macros.cpp pp.cpp frontend_elaborator.cpp register_module.cpp
-  environment_scope.cpp coercion.cpp shell.cpp)
+  parser_macros.cpp parser_calc.cpp pp.cpp frontend_elaborator.cpp
+  register_module.cpp environment_scope.cpp coercion.cpp shell.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/parser_calc.cpp

@@ -0,0 +1,142 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/builtin.h"
+#include "library/placeholder.h"
+#include "frontends/lean/parser_calc.h"
+#include "frontends/lean/parser_imp.h"
+#include "frontends/lean/operator_info.h"
+#include "frontends/lean/frontend.h"
+
+namespace lean {
+bool calc_proof_parser::supports(expr const & op1) const {
+    return
+        std::find_if(m_supported_operators.begin(), m_supported_operators.end(), [&](op_data const & op2) { return op1 == op2.m_fn; })
+        != m_supported_operators.end();
+}
+
+void calc_proof_parser::add_supported_operator(op_data const & op1) {
+    if (supports(op1.m_fn))
+        throw exception("operator already supported in the calculational proof manager");
+    m_supported_operators = cons(op1, m_supported_operators);
+}
+
+optional<trans_data> calc_proof_parser::find_trans_data(expr const & op1, expr const & op2) const {
+    auto it = std::find_if(m_trans_ops.begin(), m_trans_ops.end(),
+                           [&](std::tuple<expr, expr, trans_data> const & entry) { return std::get<0>(entry) == op1 && std::get<1>(entry) == op2; });
+    if (it == m_trans_ops.end())
+        return optional<trans_data>();
+    else
+        return optional<trans_data>(std::get<2>(*it));
+}
+
+void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans_data const & d) {
+    if (!supports(op1) || !supports(op2) || !supports(d.m_rop))
+        throw exception("invalid transitivity step in calculational proof manager, operator not supported");
+    if (find_trans_data(op1, op2))
+        throw exception("transitivity step is already supported in the calculational proof manager");
+    if (d.m_num_args < 5)
+        throw exception("transitivity step must have at least 5 arguments");
+    m_trans_ops.emplace_front(op1, op2, d);
+}
+
+calc_proof_parser::calc_proof_parser() {
+    expr imp = mk_implies_fn();
+    expr eq  = mk_homo_eq_fn();
+    expr iff = mk_iff_fn();
+    add_supported_operator(op_data(imp, 2));
+    add_supported_operator(op_data(eq, 3));
+    add_supported_operator(op_data(iff, 2));
+    add_trans_step(eq, eq,    trans_data(mk_trans_fn(), 6, eq));
+    add_trans_step(eq, imp,   trans_data(mk_constant("EqImpTrans"), 5, imp));
+    add_trans_step(imp, eq,   trans_data(mk_constant("ImpEqTrans"), 5, imp));
+    add_trans_step(imp, imp,  trans_data(mk_constant("ImpTrans"), 5, imp));
+    add_trans_step(iff, iff,  trans_data(mk_trans_fn(), 6, iff));
+    add_trans_step(iff, imp,  trans_data(mk_constant("EqImpTrans"), 5, imp));
+    add_trans_step(imp, iff,  trans_data(mk_constant("ImpEqTrans"), 5, imp));
+    add_trans_step(eq, iff,   trans_data(mk_trans_fn(), 6, iff));
+    add_trans_step(iff, eq,   trans_data(mk_trans_fn(), 6, iff));
+}
+
+optional<expr> calc_proof_parser::find_op(operator_info const & op, pos_info const & p) const {
+    if (!op)
+        return none_expr();
+    for (auto d : op.get_denotations()) {
+        // TODO(Leo): I'm ignoring overloading.
+        if (supports(d))
+            return some_expr(d);
+    }
+    throw parser_error("invalid calculational proof, operator is not supported", p);
+    return none_expr();
+}
+
+expr calc_proof_parser::parse_op(parser_imp & imp) const {
+    environment const & env = imp.get_environment();
+    auto p   = imp.pos();
+    name id  = imp.check_identifier_next("invalid calculational proof, identifier expected");
+    if (auto r = find_op(find_led(env, id), p))
+        return *r;
+    if (auto r = find_op(find_nud(env, id), p))
+        return *r;
+    expr e = imp.get_name_ref(id, p, false /* do not process implicit args */);
+    if (!supports(e))
+        throw parser_error("invalid calculational proof, operator is not supported", p);
+    return e;
+}
+
+/**
+   \brief Parse
+
+   calc expr op expr : proof1
+        ...  op expr : proof2
+
+        ...  op expr : proofn
+*/
+expr calc_proof_parser::parse(parser_imp & imp) const {
+    auto p = imp.pos();
+    expr first = imp.parse_expr();
+    if (!is_app(first))
+        throw parser_error("invalid calculational proof, first expression must be an application", p);
+    expr op      = arg(first, 0);
+    if (!supports(op))
+        throw parser_error("invalid calculational proof, first expression is not an application of a supported operator", p);
+    if (num_args(first) < 3)
+        throw parser_error("invalid calculational proof, first expression must be an application of a binary operator (modulo implicit arguments)", p);
+    imp.check_colon_next("invalid calculational proof, ':' expected");
+    unsigned num = num_args(first);
+    expr result  = imp.parse_expr();
+    expr rhs     = arg(first, num - 2);
+    expr lhs     = arg(first, num - 1);
+    while (imp.curr() == scanner::token::Ellipsis) {
+        imp.next();
+        p = imp.pos();
+        expr new_op  = parse_op(imp);
+        auto tdata = find_trans_data(op, new_op);
+        if (!tdata)
+            throw parser_error("invalid calculational proof, operators cannot be combined", p);
+        expr new_lhs = imp.parse_expr();
+        p = imp.pos();
+        imp.check_colon_next("invalid calculational proof, ':' expected");
+        expr step_pr = imp.parse_expr();
+        buffer<expr> args;
+        args.push_back(tdata->m_fn);
+        for (unsigned i = 0; i < tdata->m_num_args - 5; i++) {
+            // transitivity step has implicit arguments
+            args.push_back(imp.save(mk_placeholder(), p));
+        }
+        args.push_back(rhs);
+        args.push_back(lhs);
+        args.push_back(new_lhs);
+        args.push_back(result);
+        args.push_back(step_pr);
+        result = mk_app(args);
+        op  = tdata->m_rop;
+        lhs = new_lhs;
+    }
+    std::cout << result << "\n";
+    return result;
+}
+}

src/frontends/lean/parser_calc.h

@@ -0,0 +1,82 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/list.h"
+#include "util/optional.h"
+#include "kernel/expr.h"
+#include "frontends/lean/parser_types.h"
+
+namespace lean {
+class parser_imp;
+class operator_info;
+/**
+   \brief Information for a operator available in the
+   calculational proof module. It must have at least two arguments.
+   It may have implicit ones. We assume the implicit arguments
+   occur in the beginning.
+*/
+struct op_data {
+    expr     m_fn;
+    unsigned m_num_args;
+    op_data(expr const & f, unsigned n): m_fn(f), m_num_args(n) {}
+};
+
+/**
+   \brief Information about a transitivity-like proof step.
+
+   The m_fn  function must have at least 5 arguments.
+   We assume the implicit ones occur in the beginning.
+   The last five are a, b, c and a proof for 'a op1 b' and 'b op2 c'.
+   The function m_fn  produces a proof for 'a rop b'.
+   The resultant operator must be in the list of supported operators.
+*/
+struct trans_data {
+    expr       m_fn;
+    unsigned   m_num_args; // number of arguments of m_fn .
+    expr       m_rop;     // resultant operator
+    trans_data(expr const & f, unsigned n, expr const & rop):
+        m_fn (f), m_num_args(n), m_rop(rop) {
+    }
+};
+
+/**
+   \brief Calculational proof support in the Lean parser.
+
+   It parses expression of the form:
+
+   calc expr op expr : proof1
+        ...  op expr : proof2
+
+        ...  op expr : proofn
+*/
+class calc_proof_parser {
+    /**
+       \brief List of supported operators in calculational proofs.
+    */
+    list<op_data> m_supported_operators;
+
+    /**
+       \brief Maps to operators to the corresponding transitivity operator.
+       For example, the pair (=, =>) maps to
+
+           Theorem EqImpTrans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c
+          := assume Ha, MP H2 (EqMP H1 Ha).
+    */
+    list<std::tuple<expr, expr, trans_data>> m_trans_ops;
+    optional<trans_data> find_trans_data(expr const & op1, expr const & op2) const;
+    optional<expr> find_op(operator_info const & op, pos_info const & p) const;
+    expr parse_op(parser_imp & imp) const;
+public:
+    calc_proof_parser();
+
+    bool supports(expr const & op1) const;
+    void add_supported_operator(op_data const & op);
+    void add_trans_step(expr const & op1, expr const & op2, trans_data const & d);
+
+    expr parse(parser_imp & p) const;
+};
+}

src/frontends/lean/parser_expr.cpp

@@ -20,12 +20,14 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser_imp.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/notation.h"
+#include "frontends/lean/parser_calc.h"
 
 namespace lean {
 // A name that can't be created by the user.
 // It is used as placeholder for parsing A -> B expressions which
 // are syntax sugar for (Pi (_ : A), B)
 static name g_unused = name::mk_internal_unique_name();
+static name g_calc("calc");
 
 /**
    \brief Return the size of the implicit vector associated with the given denotation.
@@ -478,6 +480,10 @@ expr parser_imp::parse_expr_macro(name const & id, pos_info const & p) {
     }
 }
 
+expr parser_imp::parse_calc() {
+    return get_calc_proof_parser().parse(*this);
+}
+
 /**
    \brief Parse an identifier that has a "null denotation" (See
    paper: "Top down operator precedence"). A nud identifier is a
@@ -497,6 +503,8 @@ expr parser_imp::parse_nud_id() {
         return parse_expr_macro(id, p);
     } else if (auto alias = get_alias(m_env, id)) {
         return save(*alias, p);
+    } else if (id == g_calc) {
+        return parse_calc();
     } else {
         operator_info op = find_nud(m_env, id);
         if (op) {
@@ -533,6 +541,8 @@ expr parser_imp::parse_led_id(expr const & left) {
         return save(mk_app(left, parse_expr_macro(id, p)), p2);
     } else if (auto alias = get_alias(m_env, id)) {
         return save(mk_app(left, save(*alias, p)), p2);
+    } else if (id == g_calc) {
+        return save(mk_app(left, parse_calc()), p2);
     } else {
         operator_info op = find_led(m_env, id);
         if (op) {

src/frontends/lean/parser_imp.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include "frontends/lean/parser_imp.h"
 #include "frontends/lean/parser_macros.h"
+#include "frontends/lean/parser_calc.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
@@ -51,6 +52,12 @@ parser_imp::mk_scope::~mk_scope() {
     m_fn.m_num_local_decls = m_old_num_local_decls;
 }
 
+calc_proof_parser & parser_imp::get_calc_proof_parser() {
+    if (!m_calc_proof_parser)
+        m_calc_proof_parser.reset(new calc_proof_parser());
+    return *m_calc_proof_parser;
+}
+
 pos_info parser_imp::pos_of(expr const & e, pos_info default_pos) {
     auto it = m_expr_pos_info.find(e);
     if (it == m_expr_pos_info.end())
@@ -157,6 +164,8 @@ parser_imp::parser_imp(environment const & env, io_state const & st, std::istrea
     scan();
 }
 
+parser_imp::~parser_imp() {}
+
 void parser_imp::show_prompt(bool interactive, io_state const & ios) {
     if (interactive) {
         regular(ios) << "# ";

src/frontends/lean/parser_imp.h

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 class parser_imp;
+class calc_proof_parser;
 
 bool get_parser_verbose(options const & opts);
 bool get_parser_show_errors(options const & opts);
@@ -72,6 +73,10 @@ class parser_imp {
     pos_info            m_last_script_pos;
     tactic_hints        m_tactic_hints;
     std::vector<name>   m_namespace_prefixes;
+
+    std::unique_ptr<calc_proof_parser> m_calc_proof_parser;
+
+
     // If true then return error when parsing identifiers and it is not local or global.
     // We set this flag off when parsing tactics. The apply_tac may reference
     // a hypothesis in the proof state. This hypothesis is not visible until we
@@ -107,7 +112,11 @@ class parser_imp {
         ~mk_scope();
     };
 
+    calc_proof_parser & get_calc_proof_parser();
+
 public:
+    environment const & get_environment() const { return m_env; }
+
     /** \brief Return the current position information */
     pos_info pos() const { return mk_pair(m_scanner.get_line(), m_scanner.get_pos()); }
 
@@ -293,6 +302,7 @@ private:
     expr parse_type(bool level_expected);
     tactic parse_tactic_macro(name tac_id, pos_info const & p);
     expr parse_show_expr();
+    expr parse_calc();
     expr parse_nud_id();
     expr parse_nud();
     expr parse_led(expr const & left);
@@ -412,6 +422,7 @@ private:
 
 public:
     parser_imp(environment const & env, io_state const & st, std::istream & in, script_state * S, bool use_exceptions, bool interactive);
+    ~parser_imp();
     static void show_prompt(bool interactive, io_state const & ios);
     void show_prompt();
     void show_tactic_prompt();

src/frontends/lean/scanner.cpp

@@ -412,7 +412,17 @@ scanner::token scanner::scan() {
                 return token::Colon;
             }
         case ',':  next(); return token::Comma;
-        case '.':  next(); return token::Period;
+        case '.':
+            next();
+            if (curr() == '.') {
+                next();
+                if (curr() != '.')
+                    throw_exception("invalid character sequence, '...' ellipsis expected");
+                next();
+                return token::Ellipsis;
+            } else {
+                return token::Period;
+            }
         case '(':
             next();
             if (curr() == '*') {
@@ -480,6 +490,7 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
     case scanner::token::ScriptBlock:       out << "Script"; break;
     case scanner::token::Show:              out << "show"; break;
     case scanner::token::By:                out << "by"; break;
+    case scanner::token::Ellipsis:          out << "..."; break;
     case scanner::token::Eof:               out << "EOF"; break;
     }
     return out;

src/frontends/lean/scanner.h

@@ -21,7 +21,7 @@ public:
     enum class token {
         LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
         Let, In, Forall, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Eq, Assign, Type, Placeholder,
-        Show, By, ScriptBlock, Eof
+        Show, By, ScriptBlock, Ellipsis, Eof
     };
 protected:
     int                m_spos; // position in the current line of the stream

tests/lean/calc1.lean

@@ -0,0 +1,13 @@
+Import tactic.
+
+Variables a b c d e : Bool.
+Axiom H1 : a => b.
+Axiom H2 : b = c.
+Axiom H3 : c => d.
+Axiom H4 : d <=> e.
+
+Theorem T : a => e
+:= calc a  =>  b : H1
+      ...  =   c : H2
+      ...  =>  d : (by apply H3)
+      ...  <=> e : H4.

tests/lean/calc1.lean.expected.out

@@ -0,0 +1,14 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'tactic'
+  Assumed: a
+  Assumed: b
+  Assumed: c
+  Assumed: d
+  Assumed: e
+  Assumed: H1
+  Assumed: H2
+  Assumed: H3
+  Assumed: H4
+ImpEqTrans a d e (ImpTrans a c d (ImpEqTrans a b c H1 H2) _) H4
+  Proved: T