04eaf184a9
@avigad, @fpvandoorn, @rlewis1988, @dselsam
This commit modifies how have-expressions are elaborated.
Now, to process
have H : <type>, from <proof>,
<rest>
we first process the constraints in <type> and <proof> simultaneously.
After all these constraints are solved, the elaborator performs
a Prolog-like cut, and process the constraints in <rest>.
So, all overloads, type classes and coercions in <type> and <proof> are solved
before we start processing <rest>. Moreover, while processing <rest>, we
cannot backtrack to <type> and <proof> anymore.
I fixed all affected proofs in the standard and HoTT libraries in
previous commits pushed today and yesterday. I think most affected proofs were not using a good
style and/or were easy to fix. Here is a common pattern that does not
work anymore.
structure has_scalar [class] (F V : Type) :=
(smul : F → V → V)
infixl ` • `:73 := has_scalar.smul
proposition smul_zero (a : R) : a • (0 : M) = 0 :=
have a • 0 + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
!add.left_cancel this
The `have` doesn't work because Lean can't figure out the type of 0 before
it starts processing `!add.left_cancel this`. This is easy to fix, we just have to
annotate one of the `0`s in the `have`:
proposition smul_zero (a : R) : a • (0 : M) = 0 :=
have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
!add.left_cancel this
BTW, all tactics are still being executed after all constraints are solved.
We may change that in the future. I didn't want to execute
the tactics at <proof> before <rest> because of universe
meta-variables. In Lean, unassigned universe meta-variables become
parameters. Moreover, we perform this conversion *before*
we start processing tactics. Reason: universe meta-variables
create many problems for tactics such as `rewrite`, `blast` and `simp`.
Finally, we can recover the previous behavior using the option
set_option parser.checkpoint_have false
72 lines
2.9 KiB
C++
72 lines
2.9 KiB
C++
/*
|
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#pragma once
|
|
#include <string>
|
|
#include "kernel/expr.h"
|
|
|
|
namespace lean {
|
|
/** \brief Declare a new kind of annotation. It must only be invoked at startup time
|
|
Use helper obect #register_annotation_fn.
|
|
*/
|
|
void register_annotation(name const & n);
|
|
|
|
/** \brief Create an annotated expression with tag \c kind based on \c e.
|
|
|
|
\pre \c kind must have been registered using #register_annotation.
|
|
|
|
\remark Annotations have no real semantic meaning, but are useful for guiding pretty printer and/or automation.
|
|
*/
|
|
expr mk_annotation(name const & kind, expr const & e, tag g);
|
|
expr mk_annotation(name const & kind, expr const & e);
|
|
/** \brief Return true iff \c e was created using #mk_annotation. */
|
|
bool is_annotation(expr const & e);
|
|
/** \brief Return true iff \c e was created using #mk_annotation, and has tag \c kind. */
|
|
bool is_annotation(expr const & e, name const & kind);
|
|
/** \brief Return true iff \c e is of the form (a_1 ... (a_k e') ...)
|
|
where all a_i's are annotations and one of the is \c kind.
|
|
|
|
\remark is_nested_annotation(e, kind) implies is_annotation(e, kind)
|
|
*/
|
|
bool is_nested_annotation(expr const & e, name const & kind);
|
|
|
|
/** \brief Return the annotated expression, \c e must have been created using #mk_annotation.
|
|
|
|
\post get_annotation_arg(mk_annotation(k, e)) == e
|
|
*/
|
|
expr const & get_annotation_arg(expr const & e);
|
|
/** \brief Return the king of the annotated expression, \c e must have been created using #mk_annotation.
|
|
|
|
\post get_annotation_arg(mk_annotation(k, e)) == k
|
|
*/
|
|
name const & get_annotation_kind(expr const & e);
|
|
|
|
/** \brief Return the nested annotated expression, \c e must have been created using #mk_annotation.
|
|
This function is the "transitive" version of #get_annotation_arg.
|
|
It guarantees that the result does not satisfy the predicate is_annotation.
|
|
*/
|
|
expr const & get_nested_annotation_arg(expr const & e);
|
|
|
|
/** \brief Copy annotation from \c from to \c to. */
|
|
expr copy_annotations(expr const & from, expr const & to);
|
|
|
|
/** \brief Tag \c e as a 'have'-expression. 'have' is a pre-registered annotation. */
|
|
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);
|
|
expr mk_checkpoint_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);
|
|
bool is_checkpoint_annotation(expr const & e);
|
|
|
|
/** \brief Return the serialization 'opcode' for annotation macros. */
|
|
std::string const & get_annotation_opcode();
|
|
|
|
void initialize_annotation();
|
|
void finalize_annotation();
|
|
}
|