michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
4824 commits 3 branches 0 tags 28 MiB
Commit graph

4824 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
7fb2b0f6d8 feat(kernel): add method 'may_reduce_later' to normalizer_extension, and improve unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 22:31:05 -07:00
Leonardo de Moura
ce282a549a feat(frontends/lean): add 'prefix' notation declaration command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 21:37:56 -07:00
Leonardo de Moura
6d773a2ba4 fix(library/standard): not notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 21:29:15 -07:00
Leonardo de Moura
855ffcba34 feat(library/standard): add pairs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 20:43:16 -07:00
Leonardo de Moura
110b622b83 feat(library/unifier): add support for unification constraints of the form "(elim ... (?m ...)) =?= t", where elim is an eliminator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 20:41:51 -07:00
Leonardo de Moura
c854ad3d65 refactor(library/unifier): add is_def_eq alias 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 18:01:59 -07:00
Leonardo de Moura
b5f63e78ca feat(frontends/lean/notation_cmd): reuse existing precedence to increase compatibility with existing notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 17:23:29 -07:00
Leonardo de Moura
fa1857e6a9 fix(frontends/lean/notation_cmd): fix default, add 'prev' action 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 16:44:44 -07:00
Leonardo de Moura
9ec4f23522 fix(library/standard): congr1 and congr2 theorem definition, we should allow A and B to inhabit different universes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 16:25:14 -07:00
Leonardo de Moura
7d27368708 refactor(library/standard): use inductive datatype to define inhabited 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 15:05:19 -07:00
Leonardo de Moura
aba4534acb feat(library/unifier): 'forget' justifications after finding a solution, the justifications are only needed inside the unifier (for implementing nonchronological backtracking) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 14:14:07 -07:00
Leonardo de Moura
a009225435 feat(kernel/metavar): expose destructive assign 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 14:07:47 -07:00
Leonardo de Moura
b49902807c refactor(kernel/metavar): separate substitution from their justifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 14:01:22 -07:00
Leonardo de Moura
abbd054b51 feat(library/tactic): add eassumption tactic, and remove redundant 'subgoals' from apply tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 13:04:46 -07:00
Leonardo de Moura
079592c446 feat(library/unifier): eagerly apply substitution to improve quick failure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 12:58:30 -07:00
Leonardo de Moura
db0ef64c04 feat(util/lazy_list_fn): handle the 'is_nil' case more efficiently 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 11:29:04 -07:00
Leonardo de Moura
c9cfb844f1 feat(library/unifier): add 'quick' failure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 11:28:21 -07:00
Leonardo de Moura
dd96bb151b refactor(library/unifier): reduce the number unify procedure 'flavors' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 11:15:43 -07:00
Leonardo de Moura
d63ccbcf94 fix(library/unifier): missing case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 10:51:59 -07:00
Leonardo de Moura
528d51bc57 feat(library/standard): add congr theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 09:44:36 -07:00
Leonardo de Moura
0ff145e59b feat(library/tactic): add apply tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 09:20:01 -07:00
Leonardo de Moura
c1538bfc40 test(tests/lean/run): add 'apply subst' test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 09:07:56 -07:00
Leonardo de Moura
c9994ca00c feat(library/unifier): when projecting give preference to most recent locals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 09:01:29 -07:00
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