From cf34f75ab5e7a22458de2ce8942cb2b6a294d5e3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Jul 2014 04:08:51 +0100 Subject: [PATCH] feat(frontends/lean): add 'obtains' expression Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 11 ++++---- src/emacs/lean-mode.el | 2 +- src/frontends/lean/builtin_exprs.cpp | 42 ++++++++++++++++++++++++++++ src/frontends/lean/token_table.cpp | 2 +- tests/lean/run/elim.lean | 7 +++++ 5 files changed, 57 insertions(+), 7 deletions(-) create mode 100644 tests/lean/run/elim.lean diff --git a/library/standard/logic.lean b/library/standard/logic.lean index 0436b102c..4e27f85cc 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -204,7 +204,8 @@ theorem exists_unique_intro {A : Type} {p : A → Bool} (w : A) (H1 : p w) (H2 : := exists_intro w (and_intro H1 H2) theorem exists_unique_elim {A : Type} {p : A → Bool} {b : Bool} (H2 : ∃! x, p x) (H1 : ∀ x, p x → (∀ y, y ≠ x → ¬ p y) → b) : b -:= exists_elim H2 (λ w Hw, H1 w (and_elim_left Hw) (and_elim_right Hw)) +:= obtains w Hw, from H2, + H1 w (and_elim_left Hw) (and_elim_right Hw) inductive inhabited (A : Type) : Bool := | inhabited_intro : A → inhabited A @@ -236,15 +237,15 @@ definition heq {A B : Type} (a : A) (b : B) := ∃ H, cast H a = b infixl `==`:50 := heq theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B -:= exists_elim H (λ H Hw, H) +:= obtains w Hw, from H, w theorem eq_to_heq {A : Type} {a b : A} (H : a = b) : a == b := exists_intro (refl A) (trans (cast_refl a) H) theorem heq_to_eq {A : Type} {a b : A} (H : a == b) : a = b -:= exists_elim H (λ (H : A = A) (Hw : cast H a = b), - calc a = cast H a : symm (cast_eq H a) - ... = b : Hw) +:= obtains (w : A = A) (Hw : cast w a = b), from H, + calc a = cast w a : symm (cast_eq w a) + ... = b : Hw theorem heq_refl {A : Type} (a : A) : a == a := eq_to_heq (refl a) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 1ec6ce886..eeb3c98fd 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -26,7 +26,7 @@ '("--") ;; comments start with '("import" "abbreviation" "opaque_hint" "tactic_hint" "definition" "hiding" "exposing" "parameter" "parameters" "proof" "qed" "conjecture" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "axiom" "inductive" "with" "universe" "alias" "help" "environment" "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "including" "class" "instance" "section" "set_option" "add_rewrite") ;; some keywords '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face) - ("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face) + ("\\_<\\(calc\\|have\\|obtains\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face) ("\"[^\"]*\"" . 'font-lock-string-face) ("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face) ("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index dd63e2dfc..4f0399ba7 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -278,6 +278,47 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) return mk_let(p, H_show, prop, proof, Var(0), pos, mk_contextual_info(false)); } +static name g_exists_elim("exists_elim"); +static expr parse_obtains(parser & p, unsigned, expr const *, pos_info const & pos) { + if (!p.env().find(g_exists_elim)) + throw parser_error("invalid use of 'obtains' expression, environment does not contain 'exists_elim' theorem", pos); + // exists_elim {A : Type} {P : A → Bool} {B : Bool} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B) + buffer ps; + auto b_pos = p.pos(); + environment env = p.parse_binders(ps); + unsigned num_ps = ps.size(); + if (num_ps < 2) + throw parser_error("invalid 'obtains' expression, at least 2 binders expected", b_pos); + bool is_fact = false; + if (p.curr_is_token(g_fact)) { + p.next(); + is_fact = true; + } + if (!is_fact) { + expr H = ps[num_ps-1]; + ps[num_ps-1] = update_local(H, mlocal_type(H), local_info(H).update_contextual(false)); + } + p.check_token_next(g_comma, "invalid 'obtains' expression, ',' expected"); + p.check_token_next(g_from, "invalid 'obtains' expression, 'from' expected"); + expr H1 = p.parse_expr(); + p.check_token_next(g_comma, "invalid 'obtains' expression, ',' expected"); + expr b = p.parse_scoped_expr(ps, env); + expr H = ps[num_ps-1]; + unsigned i = num_ps-1; + while (i > 1) { + --i; + expr a = ps[i]; + expr H_aux = mk_local(p.mk_fresh_name(), mk_expr_placeholder(), mk_contextual_info(is_fact)); + expr H2 = Fun({a, H}, b); + b = mk_constant(g_exists_elim)(H_aux, H2); + H = H_aux; + } + expr a = ps[0]; + expr H2 = Fun({a, H}, b); + expr r = mk_constant(g_exists_elim)(H1, H2); + return p.rec_save_pos(r, pos); +} + static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &) { return parse_calc(p); } @@ -329,6 +370,7 @@ parse_table init_nud_table() { 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("obtains", mk_ext_action(parse_obtains))}, 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/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 396fdbbb3..d7c59dea6 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -65,7 +65,7 @@ static char const * g_cup = "\u2294"; token_table init_token_table() { token_table t; std::pair builtin[] = - {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0}, {"then", 0}, + {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtains", 0}, {"by", 0}, {"then", 0}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec}, {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, diff --git a/tests/lean/run/elim.lean b/tests/lean/run/elim.lean new file mode 100644 index 000000000..a3bb4ba72 --- /dev/null +++ b/tests/lean/run/elim.lean @@ -0,0 +1,7 @@ +import standard +using num +variable p : num → num → num → Bool +axiom H1 : ∃ x y z, p x y z +axiom H2 : ∀ {x y z : num}, p x y z → p x x x +theorem tst : ∃ x, p x x x +:= obtains a b c H, from H1, exists_intro a (H2 H)