From 010ecebfeaf17be7e557a41afe6628855046b600 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Sep 2014 18:11:58 -0700 Subject: [PATCH] feat(frontends/lean): add proof-qed expression Remark: we still have to add support to it in the elaborator. Right now, it is just an embellished parenthesis. --- src/emacs/lean-syntax.el | 2 + src/frontends/lean/builtin_exprs.cpp | 17 +++- src/frontends/lean/elaborator.cpp | 10 +++ src/frontends/lean/token_table.cpp | 3 +- src/library/annotation.cpp | 9 ++ src/library/annotation.h | 4 + tests/lean/run/div2.lean | 120 +++++++++++++++++++++++++++ 7 files changed, 163 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/div2.lean diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index a5ce50a58..427185581 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -80,6 +80,8 @@ (,(rx symbol-start (or "bool" "int" "nat" "real" "Prop" "Type" "ℕ" "ℤ") symbol-end) . 'font-lock-type-face) ;; sorry (,(rx symbol-start "sorry" symbol-end) . 'font-lock-warning-face) + ;; extra-keywords + (,(rx (or "∎")) . 'font-lock-keyword-face) ;; lean-keywords (, (concat "\\(" (regexp-opt lean-keywords 'words) "\\)") (1 'font-lock-keyword-face))))) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 663fd9a67..13d7077bb 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -26,7 +26,7 @@ namespace lean { namespace notation { static name g_llevel_curly(".{"), g_rcurly("}"), g_in("in"), g_colon(":"), g_assign(":="); static name g_comma(","), g_visible("[visible]"), g_from("from"), g_using("using"); -static name g_then("then"), g_have("have"), g_by("by"), g_qed("qed"), g_end("end"); +static name g_then("then"), g_have("have"), g_by("by"), g_proof("proof"), g_qed("qed"), g_end("end"); static name g_take("take"), g_assume("assume"), g_show("show"), g_fun("fun"); static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) { @@ -153,11 +153,21 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & } } +static expr parse_proof_qed_core(parser & p, pos_info const & pos) { + expr r = p.save_pos(mk_proof_qed_annotation(p.parse_expr()), pos); + p.check_token_next(g_qed, "invalid proof-qed, 'qed' expected"); + return r; +} + static expr parse_proof(parser & p, expr const & prop) { if (p.curr_is_token(g_from)) { // parse: 'from' expr p.next(); return p.parse_expr(); + } else if (p.curr_is_token(g_proof)) { + auto pos = p.pos(); + p.next(); + return parse_proof_qed_core(p, pos); } else if (p.curr_is_token(g_by)) { // parse: 'by' tactic auto pos = p.pos(); @@ -369,6 +379,10 @@ static expr parse_rparen(parser & p, unsigned, expr const * args, pos_info const return args[0]; } +static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const & pos) { + return parse_proof_qed_core(p, pos); +} + parse_table init_nud_table() { action Expr(mk_expr_action()); action Skip(mk_skip_action()); @@ -390,6 +404,7 @@ parse_table init_nud_table() { r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0); r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0); r = r.add({transition("begin", mk_ext_action(parse_begin_end))}, x0); + r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0); r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0); r = r.add({transition("including", mk_ext_action(parse_including_expr))}, x0); return r; diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c83f2e5cd..3cfbf8d6c 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -315,6 +315,8 @@ public: return visit_choice(e, some_expr(t), cs); } else if (is_by(e)) { return visit_by(e, some_expr(t), cs); + } else if (is_proof_qed_annotation(e)) { + return visit_proof_qed(e, some_expr(t), cs); } else { return visit(e, cs); } @@ -343,6 +345,12 @@ public: return m; } + expr visit_proof_qed(expr const & e, optional const & /* t */, constraint_seq & cs) { + lean_assert(is_proof_qed_annotation(e)); + // TODO(Leo) + return visit(get_annotation_arg(e), cs); + } + /** \brief Make sure \c f is really a function, if it is not, try to apply coercions. The result is a pair new_f, f_type, where new_f is the new value for \c f, and \c f_type is its type (and a Pi-expression) @@ -693,6 +701,8 @@ public: return visit_let_value(e, cs); } else if (is_by(e)) { return visit_by(e, none_expr(), cs); + } else if (is_proof_qed_annotation(e)) { + return visit_proof_qed(e, none_expr(), cs); } else if (is_no_info(e)) { flet let(m_no_info, true); return visit(get_annotation_arg(e), cs); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 930c2865d..75fa51f6d 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -65,6 +65,7 @@ static char const * g_pi_unicode = "\u03A0"; static char const * g_forall_unicode = "\u2200"; static char const * g_arrow_unicode = "\u2192"; static char const * g_cup = "\u2294"; +static char const * g_qed_unicode = "∎"; token_table init_token_table() { token_table t; @@ -87,7 +88,7 @@ token_table init_token_table() { pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, - {nullptr, nullptr}}; + {g_qed_unicode, "qed"}, {nullptr, nullptr}}; pair cmd_aliases[] = {{"parameter", "variable"}, {"parameters", "variables"}, {"lemma", "theorem"}, diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp index e7b9f3cad..3bf523f44 100644 --- a/src/library/annotation.cpp +++ b/src/library/annotation.cpp @@ -136,11 +136,20 @@ name const & get_show_name() { return g_show; } +name const & get_proof_qed_name() { + static name g_proof_qed("proof-qed"); + static register_annotation_fn g_proof_qed_annotation(g_proof_qed); + return g_proof_qed; +} + static name g_have_name = get_have_name(); // force 'have' annotation to be registered static name g_show_name = get_show_name(); // force 'show' annotation to be registered +static name g_proof_qed_name = get_proof_qed_name(); // force 'proof-qed' annotation to be registered expr mk_have_annotation(expr const & e) { return mk_annotation(get_have_name(), e); } expr mk_show_annotation(expr const & e) { return mk_annotation(get_show_name(), e); } +expr mk_proof_qed_annotation(expr const & e) { return mk_annotation(get_proof_qed_name(), e); } bool is_have_annotation(expr const & e) { return is_annotation(e, get_have_name()); } bool is_show_annotation(expr const & e) { return is_annotation(e, get_show_name()); } +bool is_proof_qed_annotation(expr const & e) { return is_annotation(e, get_proof_qed_name()); } } diff --git a/src/library/annotation.h b/src/library/annotation.h index 9e525acfe..da46644fa 100644 --- a/src/library/annotation.h +++ b/src/library/annotation.h @@ -60,10 +60,14 @@ expr copy_annotations(expr const & from, expr const & to); expr mk_have_annotation(expr const & e); /** \brief Tag \c e as a 'show'-expression. 'show' is a pre-registered annotation. */ expr mk_show_annotation(expr const & e); +/** \brief Tag \c e as a 'proof-qed'-expression. 'proof-qed' is a pre-registered annotation. */ +expr mk_proof_qed_annotation(expr const & e); /** \brief Return true iff \c e was created using #mk_have_annotation. */ bool is_have_annotation(expr const & e); /** \brief Return true iff \c e was created using #mk_show_annotation. */ bool is_show_annotation(expr const & e); +/** \brief Return true iff \c e was created using #mk_proof_qed_annotation. */ +bool is_proof_qed_annotation(expr const & e); /** \brief Return the serialization 'opcode' for annotation macros. */ std::string const & get_annotation_opcode(); diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean new file mode 100644 index 000000000..a9439eafb --- /dev/null +++ b/tests/lean/run/div2.lean @@ -0,0 +1,120 @@ +import logic data.nat.sub struc.relation data.prod +import tools.fake_simplifier + +open nat relation relation.iff_ops prod +open fake_simplifier decidable +open eq_ops + +namespace nat + +-- A general recursion principle +-- ----------------------------- +-- +-- Data: +-- +-- dom, codom : Type +-- default : codom +-- measure : dom → ℕ +-- rec_val : dom → (dom → codom) → codom +-- +-- and a proof +-- +-- rec_decreasing : ∀m, m ≥ measure x, rec_val x f = rec_val x (restrict f m) +-- +-- ... which says that the recursive call only depends on f at values with measure less than x, +-- in the sense that changing other values to the default value doesn't change the result. +-- +-- The result is a function f = rec_measure, satisfying +-- +-- f x = rec_val x f + +definition restrict {dom codom : Type} (default : codom) (measure : dom → ℕ) (f : dom → codom) + (m : ℕ) (x : dom) := +if measure x < m then f x else default + +theorem restrict_lt_eq {dom codom : Type} (default : codom) (measure : dom → ℕ) (f : dom → codom) + (m : ℕ) (x : dom) (H : measure x < m) : + restrict default measure f m x = f x := +if_pos H + +theorem restrict_not_lt_eq {dom codom : Type} (default : codom) (measure : dom → ℕ) + (f : dom → codom) (m : ℕ) (x : dom) (H : ¬ measure x < m) : + restrict default measure f m x = default := +if_neg H + +definition rec_measure_aux {dom codom : Type} (default : codom) (measure : dom → ℕ) + (rec_val : dom → (dom → codom) → codom) : ℕ → dom → codom := +rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default) + +definition rec_measure {dom codom : Type} (default : codom) (measure : dom → ℕ) + (rec_val : dom → (dom → codom) → codom) (x : dom) : codom := +rec_measure_aux default measure rec_val (succ (measure x)) x + +theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → ℕ) + (rec_val : dom → (dom → codom) → codom) + (rec_decreasing : ∀g1 g2 x, (∀z, measure z < measure x → g1 z = g2 z) → + rec_val x g1 = rec_val x g2) + (m : ℕ) : + let f' := rec_measure_aux default measure rec_val in + let f := rec_measure default measure rec_val in + ∀x, f' m x = restrict default measure f m x := +let f' := rec_measure_aux default measure rec_val in +let f := rec_measure default measure rec_val in +case_strong_induction_on m + (take x, + have H1 : f' 0 x = default, from rfl, + have H2 : ¬ measure x < 0, from not_lt_zero, + have H3 : restrict default measure f 0 x = default, from if_neg H2, + show f' 0 x = restrict default measure f 0 x, from H1 ⬝ H3⁻¹) + (take m, + assume IH: ∀n, n ≤ m → ∀x, f' n x = restrict default measure f n x, + take x : dom, + show f' (succ m) x = restrict default measure f (succ m) x, from + by_cases -- (measure x < succ m) + (assume H1 : measure x < succ m, + have H2a : ∀z, measure z < measure x → f' m z = f z, + proof + take z, + assume Hzx : measure z < measure x, + calc + f' m z = restrict default measure f m z : IH m le_refl z + ... = f z : restrict_lt_eq _ _ _ _ _ (lt_le_trans Hzx (lt_succ_imp_le H1)) + ∎, + have H2 : f' (succ m) x = rec_val x f, + proof + calc + f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl + ... = rec_val x (f' m) : if_pos H1 + ... = rec_val x f : rec_decreasing (f' m) f x H2a + ∎, + let m' := measure x in + have H3a : ∀z, measure z < m' → f' m' z = f z, + proof + take z, + assume Hzx : measure z < measure x, + calc + f' m' z = restrict default measure f m' z : IH _ (lt_succ_imp_le H1) _ + ... = f z : restrict_lt_eq _ _ _ _ _ Hzx + qed, + have H3 : restrict default measure f (succ m) x = rec_val x f, + proof + calc + restrict default measure f (succ m) x = f x : if_pos H1 + ... = f' (succ m') x : eq.refl _ + ... = if measure x < succ m' then rec_val x (f' m') else default : rfl + ... = rec_val x (f' m') : if_pos self_lt_succ + ... = rec_val x f : rec_decreasing _ _ _ H3a + qed, + show f' (succ m) x = restrict default measure f (succ m) x, + from H2 ⬝ H3⁻¹) + (assume H1 : ¬ measure x < succ m, + have H2 : f' (succ m) x = default, from + calc + f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl + ... = default : if_neg H1, + have H3 : restrict default measure f (succ m) x = default, + from if_neg H1, + show f' (succ m) x = restrict default measure f (succ m) x, + from H2 ⬝ H3⁻¹)) + +end nat