From 4f3da9044332487312ce276489d54578aacfd1d0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Jun 2014 15:04:29 -0700
Subject: [PATCH] feat(frontends/lean/builtin_exprs): add 'have' and 'show'
 expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_exprs.cpp | 44 ++++++++++++++++++++++++++++
 src/kernel/expr.h                    |  1 +
 tests/lean/run/t9.lean               | 15 ++++++++++
 3 files changed, 60 insertions(+)
 create mode 100644 tests/lean/run/t9.lean

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index a91f79e03..42e7304a0 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -18,6 +18,8 @@ static name g_in("in");
 static name g_colon(":");
 static name g_assign(":=");
 static name g_comma(",");
+static name g_from("from");
+static name g_by("by");
 
 static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) {
     if (p.curr_is_token(g_llevel_curly)) {
@@ -97,6 +99,46 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     return r;
 }
 
+static expr parse_proof(parser & p, expr const & prop) {
+    if (p.curr_is_token(g_from)) {
+        p.next();
+        return p.parse_expr();
+    } else if (p.curr_is_token(g_by)) {
+        auto pos = p.pos();
+        p.next();
+        tactic t = p.parse_tactic();
+        expr r = p.save_pos(mk_expr_placeholder(some_expr(prop)), pos);
+        p.save_hint(r, t);
+        return r;
+    } else {
+        throw parser_error("invalid expression, 'by' or 'from' expected", p.pos());
+    }
+}
+
+static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) {
+    name id    = p.check_id_next("invalid 'have' declaration, identifier expected");
+    p.check_token_next(g_colon, "invalid 'have' declaration, ':' expected");
+    expr prop  = p.parse_expr();
+    p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
+    expr proof = parse_proof(p, prop);
+    p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
+    parser::local_scope scope(p);
+    expr l = p.save_pos(mk_local(id, prop), pos);
+    p.add_local(l);
+    expr body  = abstract(p.parse_expr(), l);
+    // remark: mk_contextual_info(false) informs the elaborator that prop should not occur inside metavariables.
+    expr r     = p.save_pos(mk_lambda(id, prop, body, mk_contextual_info(false)), pos);
+    return p.save_pos(mk_app(r, proof), pos);
+}
+
+static name H_show("H_show");
+static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) {
+    expr prop  = p.parse_expr();
+    p.check_token_next(g_comma, "invalid 'show' declaration, ',' expected");
+    expr proof = parse_proof(p, prop);
+    return p.save_pos(mk_let(H_show, prop, proof, Var(0)), pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -105,6 +147,8 @@ parse_table init_nud_table() {
     parse_table r;
     r = r.add({transition("_", mk_ext_action(parse_placeholder))}, x0);
     r = r.add({transition("by", mk_ext_action(parse_by))}, x0);
+    r = r.add({transition("have", mk_ext_action(parse_have))}, x0);
+    r = r.add({transition("show", mk_ext_action(parse_show))}, x0);
     r = r.add({transition("(", Expr), transition(")", Skip)}, x0);
     r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
     r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index a924a4aa7..2dc6e4bd6 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -256,6 +256,7 @@ public:
 
 inline binder_info mk_implicit_binder_info() { return binder_info(true); }
 inline binder_info mk_cast_binder_info() { return binder_info(false, true); }
+inline binder_info mk_contextual_info(bool f) { return binder_info(false, false, f); }
 
 bool operator==(binder_info const & i1, binder_info const & i2);
 inline bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); }
diff --git a/tests/lean/run/t9.lean b/tests/lean/run/t9.lean
new file mode 100644
index 000000000..b57a59d4f
--- /dev/null
+++ b/tests/lean/run/t9.lean
@@ -0,0 +1,15 @@
+definition [inline] bool : Type.{1} := Type.{0}
+definition and (p q : bool) : bool
+:= ∀ c : bool, (p → q → c) →  c
+infixl `∧` 25 := and
+theorem and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q
+:= λ (c : bool) (H : p → q → c), H H1 H2
+theorem and_elim_left (p q : bool) (H : p ∧ q) : p
+:= H p (λ (H1 : p) (H2 : q), H1)
+theorem and_elim_right (p q : bool) (H : p ∧ q) : q
+:= H q (λ (H1 : p) (H2 : q), H2)
+theorem and_comm (p q : bool) (H : p ∧ q) : q ∧ p
+:= have H1 : p, from and_elim_left p q H,
+   have H2 : q, from and_elim_right p q H,
+   show q ∧ p, from and_intro q p H2 H1
+