Commit graph

3201 commits

Author SHA1 Message Date
Leonardo de Moura
e3ab0a1d10 feat(frontends/lean): improve error messages when users forget to import 'tactic'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 08:33:29 -07:00
Leonardo de Moura
6b8b5f3dd8 feat(library/tactic): expose more builtin tactics, cleanup expr_to_tactic procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 08:06:28 -07:00
Leonardo de Moura
a7d660f875 feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 20:45:10 -07:00
Leonardo de Moura
5527955ba8 feat(frontends/lean): add 'proof-qed' notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 19:30:48 -07:00
Leonardo de Moura
138267b53a feat(frontends/lean/elaborator) add trick for improving error messages when mixing tactics, elaboration and exact tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:58:32 -07:00
Leonardo de Moura
c3abf81382 chore(emacs): update emacs mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:37:53 -07:00
Leonardo de Moura
60c637fb9d feat(library/tactic): add 'exact' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:37:32 -07:00
Leonardo de Moura
37b5b7c4c2 feat(library/tactic): rename 'exact' to 'assumption', 'exact' is a different tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:10:42 -07:00
Leonardo de Moura
04b2a620f8 fix(frontends/lean/elaborator): instantiate metavariables before displaying error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:07:11 -07:00
Leonardo de Moura
3809a3cc2c chore(frontends/lean): code cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 17:32:13 -07:00
Leonardo de Moura
181a739a5e feat(frontends/lean/elaborator): report unassigned metavariables as goals
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 16:26:06 -07:00
Leonardo de Moura
6a6ebd5c2d refactor(kernel/metavar): add method instantiate as alias for instantiate_metavars_wo_jst
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 15:39:25 -07:00
Leonardo de Moura
d46ade94a7 refactor(frontends/lean): remove unnecessary code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 14:47:41 -07:00
Leonardo de Moura
3e1bb96935 feat(library/tactic/goal): propagate tag (for position information) from goal to subgoal
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 14:47:18 -07:00
Leonardo de Moura
ee531ec0e2 feat(frontends/parser): improve error message when an apply tactic refers a local constant that is not marked as [fact]
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 14:09:01 -07:00
Leonardo de Moura
0f27856e4a feat(library/tactic): new apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 13:14:50 -07:00
Leonardo de Moura
cc3fb0c51f feat(util/name_generator): allow name generator to be created without providing any argument in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 12:39:41 -07:00
Leonardo de Moura
6ab46396d8 feat(library/tactic): expose 'trace' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 10:52:45 -07:00
Leonardo de Moura
e1d909455c refactor(library/tactic): add namespace 'tactic', improve expr_to_tactic failure error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 10:45:09 -07:00
Leonardo de Moura
a66a08c89e feat(frontends/lean): parse strings as expressions of type 'string.string'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 10:00:55 -07:00
Leonardo de Moura
8b8881deae fix(util/hash): relax pre-condition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 09:56:50 -07:00
Leonardo de Moura
f464775af6 fix(frontends/lean/parser): bug when parsing identifiers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 08:36:25 -07:00
Leonardo de Moura
9f9f93645b feat(library/standard): add bit, char, and string types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 08:36:05 -07:00
Leonardo de Moura
0198dfc7c5 feat(frontends/lean): parse numerals as expressions of type 'num.num'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 08:09:33 -07:00
Leonardo de Moura
7593ee1468 refactor(library/standard): remove parameter from 'tactic' inductive type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 08:09:24 -07:00
Leonardo de Moura
b2b76b078f feat(frontends/lean): remove build_tactic_cmds, and use expressions for representing tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 20:43:53 -07:00
Leonardo de Moura
cbac21ec7f feat(library/tactic): add trick for 'embedding' tactics inside Lean expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 19:05:22 -07:00
Leonardo de Moura
2df92b0701 refactor(library/tactic): simplify proof_state
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 18:02:17 -07:00
Leonardo de Moura
7abe2e7242 fix(frontends/lean/token_table): precedence for '@'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 17:06:09 -07:00
Leonardo de Moura
5b69f88664 feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 16:55:41 -07:00
Leonardo de Moura
ec3743dede fix(frontends/lean/parser): avoid nontermination
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 16:46:58 -07:00
Leonardo de Moura
8cdf44b87b feat(frontends/lean/notation_cmd): allow 'max' to use as a precedence level
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 16:46:32 -07:00
Leonardo de Moura
4cb5f97038 refactor(library/tactic): simplify tactic framework, no more proof builders
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 16:11:19 -07:00
Leonardo de Moura
d4b29cd132 feat(library/standard/logic): add exists unique
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 18:22:28 -07:00
Leonardo de Moura
ad12abcdb4 fix(library/unifier): bug in process_eq_constraint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 18:22:05 -07:00
Leonardo de Moura
abe12b0631 fix(shell/lean): only save .olean file if there are no errors
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 18:04:18 -07:00
Leonardo de Moura
eff59211ce feat(library/standard): add more basic theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 18:01:31 -07:00
Leonardo de Moura
c84218e24a chore(frontends/lean/inductive_cmd): cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 17:16:10 -07:00
Leonardo de Moura
3e299a1d5a refactor(frontends/lean/parser): move parser Lua bindings to a separate file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 17:00:10 -07:00
Leonardo de Moura
bccc3df1aa chore(frontends/lean): reduce code duplication
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 16:52:20 -07:00
Leonardo de Moura
af230e73c6 feat(library/standard): define heq, and configure 'calc' for '='
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 14:35:57 -07:00
Leonardo de Moura
e3f9b21c30 fix(kernel/inductive): bug in inductive datatype computational rule, we *must* first instantiate universe variables, *and then* the arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 14:15:16 -07:00
Leonardo de Moura
6e6f778ecf fix(kernel/converter): missing case for local constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 12:57:25 -07:00
Leonardo de Moura
2ea1e68f25 feat(library/standard): add equal_f theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 12:00:47 -07:00
Leonardo de Moura
c5828dcf6c feat(library/standard): add function extensionality axiom
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 11:53:04 -07:00
Leonardo de Moura
15e4b18d62 chore(library/standard): add copyright to library files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 11:44:47 -07:00
Leonardo de Moura
cb000eda13 refactor(kernel): store binder_infor in local constants
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 11:37:46 -07:00
Leonardo de Moura
c2ab31113f refactor(library/tactic): remove cex_builder and 'precision' for proof_state's
These two features make sense for solvers, but not in a general purpose tactic framework for building proofs like the one in Lean.

In most cases, we cannot build a counterexample anyway. These two features should be added in a custom framework for combining preprocessing techniques like in Z3.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 08:48:07 -07:00
Leonardo de Moura
8d584e54da feat(frontends/lean): add exact_apply
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 00:51:11 -07:00
Leonardo de Moura
3650ffdd4f feat(library/standard): add iff_mp_right and iff_mp_left
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 00:29:42 -07:00