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

1530 commits

Author SHA1 Message Date
Leonardo de Moura
00df34a1c4 feat(library/unifier): generalize method process_succ_eq_max_core 2014-11-14 14:25:41 -08:00
Leonardo de Moura
488f989c46 fix(frontends/lean/inductive_cmd): generate error for inductive datatype declarations that will produce an eliminator that can only eliminate to Prop 2014-11-14 13:57:42 -08:00
Leonardo de Moura
58525905d0 fix(frontends/lean/notation_cmd): bugs in 'reserve notation' command 2014-11-13 22:05:55 -08:00
Leonardo de Moura
51719145f9 feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2) 2014-11-12 17:28:33 -08:00
Leonardo de Moura
edd04881ee fix(library/logic): import prod and unit declarations in logic 
Reason: we need them for automatically generating constructions needed
by the definitional package
 2014-11-12 16:54:50 -08:00
Leonardo de Moura
6bc89f0916 feat(library/definitional): define ibelow and below 
These are helper definitions for brec_on and binduction_on
 2014-11-12 16:38:46 -08:00
Leonardo de Moura
97609d1625 test(tests/lean/run/nateq): add example that triggered previous modification 2014-11-12 15:11:08 -08:00
Leonardo de Moura
b07b82cf43 fix(library/definitional): marking cases_on and rec_on as reducible 
The idea is to avoid counter-intuitive behavior
 2014-11-12 15:03:30 -08:00
Leonardo de Moura
a3066e3eaa fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator 2014-11-12 13:10:19 -08:00
Leonardo de Moura
463e70332d test(tests/lean/run): define brec_on and binduction_on for a reflexive type 
We say an inductive type T is reflexive if it contains at least one constructor that
takes as an argument a function returning T.

For reflexive types it doesn't seen to be possible to define a single
brec_on that can eliminate to Type.{>=1} and Prop.
The universe level expressions get too complicated.
Even if we extend the universe constraint solver in the kernel, the
additional complexity might be a problem.

We workaround this issue by defining two versions of brec_on:
  - One (brec_on) that eliminates to Type.{>=1}, and
  - binduction_on that eliminates to Prop.

For non-reflexive types, we can combine both of them.
 2014-11-12 10:52:32 -08:00
Leonardo de Moura
5312afa7ec feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes 
The new test contains examples that required explicit levels.
 2014-11-12 10:52:32 -08:00
Leonardo de Moura
faf90c4b87 test(tests/lean/run): test brec_on on vectors 2014-11-11 17:23:59 -08:00
Leonardo de Moura
f6889951c6 fix(library/definitional/cases_on): bug in inductive datatypes with higher-order recursion 2014-11-11 15:14:08 -08:00
Leonardo de Moura
e65b5884e5 test(tests/lean/run/forest): define brec_on for forests 
Almost everything explicit to get an idea of what needs to be generated automatically.
 2014-11-11 13:16:23 -08:00
Leonardo de Moura
b3e4a689cf test(tests/lean/run): define ackermann function using recursors 2014-11-11 11:06:10 -08:00
Leonardo de Moura
e2ce942513 fix(tests/lean): adjust test to new eval semantics 2014-11-10 21:10:33 -08:00
Leonardo de Moura
1f92751c4d test(tests/lean/run): fibonacci using well_founded recursion 2014-11-10 12:46:55 -08:00
Leonardo de Moura
363d4a7577 fix(library/definitional/no_confusion): assertion violation 2014-11-10 10:32:03 -08:00
Leonardo de Moura
fa26c2301c fix(frontends/lean): fix pretty-printing spacing problem 2014-11-09 14:49:43 -08:00
Leonardo de Moura
3aac26d658 fix(frontends/lean): tactic + variables bug, fixes #315 2014-11-09 14:43:22 -08:00
Leonardo de Moura
eff3c6b774 feat(frontends/lean): add variation of the foldl/foldr notation where initial element is suppressed, closes #314 
See tests/lean/fold.lean for examples
 2014-11-09 14:08:33 -08:00
Leonardo de Moura
ce889ddf60 feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1' 2014-11-09 12:55:13 -08:00
Leonardo de Moura
df5a17cdce feat(frontends/lean/placeholder_elaborator): include type in class-instance resolution trace 2014-11-09 12:06:16 -08:00
Leonardo de Moura
9b9ae128d5 feat(frontends/lean): include file-name and line/col numbers when displaying class-instance resolution trace 2014-11-09 11:47:01 -08:00
Leonardo de Moura
aef1dd9a04 test(tests/lean/run): fibonacci using below_rec_on (aka brec_on) 2014-11-08 22:19:18 -08:00
Leonardo de Moura
1b6e40d3d6 test(tests/lean/run): define below_rec_on (aka brec_on) for vectors 2014-11-08 22:19:18 -08:00
Leonardo de Moura
e8bc0f8249 feat(library/defitional): add no_confusion construction for inductive datatypes that are not propositions 2014-11-08 18:56:52 -08:00
Leonardo de Moura
b5da143fc0 feat(library/defitional): add no_confusion_type construction for inductive datatypes that are not propositions 2014-11-08 15:20:19 -08:00
Leonardo de Moura
c7992f2cac feat(frontends/lean): add [whnf] modifier to eval command 2014-11-08 10:19:29 -08:00
Leonardo de Moura
f16f215c2a refactor(data/num/string): break into pieces to reduce dependencies 2014-11-07 08:53:14 -08:00
Leonardo de Moura
e993486301 refactor(library/data/num): break into pieces to reduce dependencies 2014-11-07 08:24:29 -08:00
Leonardo de Moura
b5e0ded163 feat(frontends/lean): max precedence used by Lean is not max_uint anymore 
The motivation is to allow users to define notation with higher
precedence than function application.
 2014-11-07 07:57:11 -08:00
Leonardo de Moura
85d0521d48 feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305 2014-11-06 21:34:05 -08:00
Leonardo de Moura
781f709bb4 feat(library/logic): import wf.lean in logic/default.lean 
We will use well-founded recursion in the definitional package
 2014-11-06 15:03:13 -08:00
Leonardo de Moura
4fa363adbf fix(tests/lean): avoid 'sorry' in expected output 2014-11-06 14:06:55 -08:00
Leonardo de Moura
af88e34588 fix(kernel/inductive): bug in eliminator for recursive datatypes in Prop 2014-11-06 14:03:28 -08:00
Leonardo de Moura
be52d950f0 fix(frontends/lean): improve error message, addresses issue #299 2014-11-06 12:19:40 -08:00
Leonardo de Moura
e499f8e20a feat(kernel/inductive): relax conditions for an inductive datatype in Prop to be able to eliminate into Type 
The new relaxed version allows us to define the "accessability"
proposition and have an eliminator into Type.

See justification in the new comments at inductive.cpp
 2014-11-06 09:36:54 -08:00
Leonardo de Moura
8723f5b613 fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches. 
Given a datatype C with parameters As, if the declaration contained
(C Bs), the elaborator would silently replace it with (C As).

This bug would confuse users and make them believe they define something
different.
 2014-11-05 23:12:00 -08:00
Leonardo de Moura
b3ad8c704a feat(frontends/lean/structure_cmd): allow inheritance from two identical structures, closes #296 2014-11-05 15:01:05 -08:00
Leonardo de Moura
4650791108 feat(frontends/lean): add 'print fields' command 2014-11-05 14:06:54 -08:00
Leonardo de Moura
354baf4d13 test(tests/lean/run): add structure command test 2014-11-05 12:54:03 -08:00
Leonardo de Moura
f8a2bc41a5 fix(frontends/lean/structure_cmd): bad test output 2014-11-05 12:02:53 -08:00
Leonardo de Moura
677e0aeef6 fix(frontends/lean/structure_cmd): accept ': Type' when universe levels are not specified 2014-11-05 12:02:52 -08:00
Leonardo de Moura
defc2478b5 feat(frontends/lean): add 'record' as an alias for 'structure' command 2014-11-05 12:02:52 -08:00
Leonardo de Moura
5b87d060cf fix(frontends/lean/structure_cmd): universe level validation 2014-11-04 22:19:23 -08:00
Leonardo de Moura
6944c7d902 fix(frontends/lean/placeholder_elaborator): local context must be adjusted when performing class-instance resolution modulo Pi-abstraction, fixes #293 2014-11-04 18:41:27 -08:00
Leonardo de Moura
3bfe5b0b7e fix(frontends/lean): type information for "atomic" notation declaration, fixes #292 2014-11-04 18:01:20 -08:00
Leonardo de Moura
d58c3e498d feat(frontends/lean/builtin_cmds): add 'print prefix' command 2014-11-04 08:40:32 -08:00
Leonardo de Moura
3454e70017 fix(frontends/lean/inductive_cmd): bug in expression position propagation, fixes #289 
Fix incorrect line/column number information in error messages produced
during inductive datatype elaboration.
 2014-11-04 07:44:47 -08:00
Leonardo de Moura
b6722a5d33 feat(frontends/lean/structure_cmd): add 'private' modifier for parent structures 
When it is used coercions/instances to parent structure are to registered
 2014-11-03 23:16:49 -08:00
Leonardo de Moura
b24165dc7b feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on' 2014-11-03 23:06:33 -08:00
Leonardo de Moura
7897e21a14 feat(frontends/lean/structure_cmd): allow fields to be suppresed, but constructor to be provided 2014-11-03 22:55:51 -08:00
Leonardo de Moura
08b4ce2db9 feat(frontends/lean/structure_cmd): use 'mk' as constructor name when it is not provided 2014-11-03 22:40:08 -08:00
Leonardo de Moura
8f3139231b feat(frontends/lean/structure_cmd): allow structure declarations that contains only a header 2014-11-03 22:17:43 -08:00
Leonardo de Moura
91749d2364 fix(frontends/lean/structure_cmd): modify coercion generation 
The previous coercion was more efficient, but the computation was
getting stuck when processing algebraic structures
 2014-11-03 19:37:11 -08:00
Leonardo de Moura
d2b5af237e refactor(library): use new 'structure' command to define prod and sigma 2014-11-03 18:57:55 -08:00
Leonardo de Moura
ea7470375f fix(tests/lean): to reflect changes in the standard library 2014-11-03 18:46:53 -08:00
Leonardo de Moura
c306bfa83c feat(frontends/lean/structure_cmd): add 'eta' theorem for structures 2014-11-03 18:33:44 -08:00
Leonardo de Moura
186d910d0b feat(frontends/lean/structure_cmd): mark coercion to parents as coercions and instances (when both structures as classes) 2014-11-03 17:55:59 -08:00
Leonardo de Moura
9531203d9d feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used 2014-11-03 17:47:08 -08:00
Leonardo de Moura
b112f3c582 feat(frontends/lean/structure_cmd): add coercions to parent structures 2014-11-03 17:39:52 -08:00
Leonardo de Moura
7afa69577e feat(frontends/lean/structure_cmd): add aliases for structure decls 2014-11-03 15:50:41 -08:00
Leonardo de Moura
efe1105eb9 fix(frontends/lean): alias generation for composite names was not working 
This is an issue for declarations that generate composite names such as
the inductive datatype packacke.

The commit also fix a bug in the generate of aliases for recursors
 2014-11-03 15:43:58 -08:00
Leonardo de Moura
594e3ea8fc fix(frontends/lean/structure_cmd): 'rec' must be marked as protected 2014-11-03 14:50:12 -08:00
Leonardo de Moura
0f56b5f5b7 test(tests/lean/run): add structure command test 2014-11-03 14:29:17 -08:00
Leonardo de Moura
a2e75159c8 fix(frontends/lean): process choice-exprs at check_constant_next 2014-11-02 19:42:30 -08:00
Leonardo de Moura
c7406d6ce8 fix(library/scoped_ext): bug when declaring nested namespaces 2014-11-02 15:35:49 -08:00
Leonardo de Moura
df008dc3c3 feat(frontends/lean/inductive_cmd): create a namespace for each declared datatype 2014-11-01 19:15:46 -07:00
Leonardo de Moura
ea55ec4090 feat(frontends/lean/decl_cmds): remove useless name from 'example' commad 2014-11-01 16:12:23 -07:00
Leonardo de Moura
1e6f7cdbb4 chore(frontends/lean/decl_cmds): add 'example' command 
It is like a theorem, but it is discarded after checking
 2014-11-01 11:37:39 -07:00
Leonardo de Moura
94cf10284a fix(frontends/lean/calc_proof_elaborator): bug when inserting symmetry proofs for heq, fixes #286 
The problem was that heq type is
    Pi {A : Type} (a : A) {B : Type} (b : B), Prop

The calc_proof_elaborator was assuming that (a : A) (b : B) were the
last two arguments in any relation supported by calc.

The fix is to remove this assumption.
 2014-11-01 07:30:04 -07:00
Leonardo de Moura
2688ca38bf feat(frontends/lean/inductive_cmd): notation for enumeration types 2014-10-31 19:01:32 -07:00
Leonardo de Moura
57b19b787b feat(frontends/lean/calc_proof_elaborator): when 'elaborator.calc_assistant' is on, generate same info that is generated if ! was used 2014-10-31 09:49:45 -07:00
Leonardo de Moura
dc7ab17d2a feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option 2014-10-31 09:49:45 -07:00
Leonardo de Moura
d7beabe91c fix(frontends/lean/calc_proof_elaborator): improve calc proof assistant 2014-10-31 09:49:45 -07:00
Leonardo de Moura
17df85f592 feat(frontends/lean/calc_proof_elaborator): add '{...}' if needed in calc proof steps 
This is part of #268
 2014-10-31 00:55:19 -07:00
Leonardo de Moura
591e566472 feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator 
This is part of #268
 2014-10-30 23:24:09 -07:00
Leonardo de Moura
c5a62f8abb feat(frontends/lean): insert ! in calculational proofs when needed 
This is part of #268
 2014-10-30 22:22:04 -07:00
Leonardo de Moura
b87764eaf6 test(tests/lean): add unique class instance resolution test 2014-10-30 14:50:32 -07:00
Leonardo de Moura
64c3ba7b74 feat(frontends/lean): display metavariable application arguments in check command 
The idea is to "fix" counter-intuitive output like the ones were
produced in the tests check.lean and check2.lean
 2014-10-30 13:28:25 -07:00
Leonardo de Moura
dcd7e53fa7 feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command 
We don't need it anymore after previous commit 2a16050
 2014-10-30 13:12:45 -07:00
Leonardo de Moura
2a160508c3 feat(frontends/lean): lean --server should display meta-variables using the approach used in check command, closes #280 2014-10-30 12:45:41 -07:00
Leonardo de Moura
a1ea087f8e fix(frontends/lean/info_manager): std::set insert is a noop if set already contains an equivalent element 2014-10-30 10:35:45 -07:00
Leonardo de Moura
84b516994c fix(library/tactic): type check generalization result, fixes #273 2014-10-29 20:34:01 -07:00
Leonardo de Moura
6107da05db fix(frontends/lean): universe variable is treated as parameter inside section, fixes #283 2014-10-29 19:47:14 -07:00
Leonardo de Moura
d7ded15486 fix(tests/lean/interactive): modify to reflect recent changes 2014-10-29 19:44:53 -07:00
Leonardo de Moura
9547e2d077 feat(library/tactic): add rotate_left/rotate_right tactics, closes #278 2014-10-29 19:13:55 -07:00
Leonardo de Moura
a98b12f067 fix(frontends/lean/elaborator): incorrect error position in begin-end block, fixes #276 2014-10-29 16:51:06 -07:00
Leonardo de Moura
88d55bfef0 fix(library/definitional/projection): remove redundant 'error in' 2014-10-29 16:51:06 -07:00
Leonardo de Moura
30571ce418 fix(library/definitional/projection): error messages for projection generation 2014-10-29 13:39:17 -07:00
Leonardo de Moura
fe4ea48381 feat(library/definitional/projection): add projection generator, closes #257 2014-10-29 13:13:05 -07:00
Leonardo de Moura
e22eb3543c feat(library/tactic): add whnf tactic, closes #270 2014-10-28 23:18:49 -07:00
Leonardo de Moura
83e4c0fcec feat(frontends/lean): hide tactic "types" 
it is not very useful to display the type of tactics (e.g., apply,
intros, ...)
 2014-10-28 22:38:10 -07:00
Leonardo de Moura
eeb6c72508 feat(frontends/lean): modify begin-end semantics, closes #258 2014-10-28 22:15:38 -07:00
Leonardo de Moura
1c2bbcfebc feat(frontends/lean/info_manager): add separator -- when displaying PROOF_STATE info 
This feature was implemented to address issue #259
 2014-10-28 16:39:21 -07:00
Leonardo de Moura
186e598bf8 feat(library/tactic/goal): add option pp.compact_goals 2014-10-28 16:30:37 -07:00
Leonardo de Moura
ea739100b3 fix(library/unifier): broken optimization in the unifier 
See new comments and tests for details.
 2014-10-28 16:09:41 -07:00
Leonardo de Moura
777aa63660 fix(kernel/inductive): relax eliminator generation rules for empty types 
This commit also removes the workaround false.rec_type. It is not needed anymore
 2014-10-28 10:31:00 -07:00
Leonardo de Moura
60f32fa709 fix(frontends/lean): begin-end automatic tactic notation bug, fixes #262 2014-10-27 17:12:25 -07:00
Leonardo de Moura
78bc3ef7e4 feat(library/unifier): improve FailLocal/FailCircular failures in the unifier by using normalization 
This improvements was marked as TODO, and was preventing us from
elaborating the example in the new test vector3.lean
 2014-10-27 16:49:29 -07:00
Leonardo de Moura
7516fcad97 feat(kernel/type_checker): add is_stuck method, and improve ensure_pi method, closes #261 2014-10-27 13:16:50 -07:00
Leonardo de Moura
49941ce35b test(tests/lean/run/sigma_no_confusion): define 'no_confusion' for sigma types 2014-10-27 07:26:01 -07:00
Leonardo de Moura
d66e5a6c41 fix(frontends/lean/builtin_cmds): bug (name clashing) in 'check' command new meta-variable naming 2014-10-26 19:19:45 -07:00
Leonardo de Moura
81dc201bab fix(frontends/lean/elaborator): nested begin-end bug 2014-10-26 18:23:30 -07:00
Leonardo de Moura
a544d32fcf fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders 2014-10-26 16:11:58 -07:00
Leonardo de Moura
cc6a96e8ba fix(frontends/lean): improve begin-end construct 2014-10-26 15:47:29 -07:00
Leonardo de Moura
fd60cf6a79 feat(library/tactic/exact_tactic): modify 'exact' tactic semantics, use higher-order unification 
See new node.inj4 theorem, we need the extra power to be able to avoid type information at
    exact (assume e₁ e₂, e₁)
 2014-10-26 10:27:33 -07:00
Leonardo de Moura
8e6de93394 fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant 2014-10-26 09:47:11 -07:00
Leonardo de Moura
c7f6a6b94e feat(library/definitional/cases_on): automatically add 'cases_on' 2014-10-25 17:22:02 -07:00
Leonardo de Moura
cdcde661ef feat(library/definitional/induction_on): automatically add 'induction_on' 2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8 feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes 2014-10-25 13:08:59 -07:00
Leonardo de Moura
7a033ac07e feat(frontends/lean): add 'print axioms' command, close #251 2014-10-24 14:35:03 -07:00
Leonardo de Moura
db25f933b0 feat(frontends/lean): use nice names for meta-variables when executing check c and c is a constant 2014-10-24 08:23:26 -07:00
Leonardo de Moura
79d0347721 feat(library/tactic): add generalize tactic, closes #34 
Remark: the intros tactic has been added in a different commit: 7d0100a340
 2014-10-23 22:40:15 -07:00
Leonardo de Moura
b83b065d00 feat(library/tactic/apply_tactic): modify heuristic for adding arguments to apply tactic. 2014-10-23 22:36:32 -07:00
Leonardo de Moura
f027acb5cb fix(frontends/lean): missing type info in expressions nested in tactics 2014-10-23 18:31:05 -07:00
Leonardo de Moura
212ae0b61c feat(frontends/lean): automatically add 'info' tactic in begin-end blocks 
Actually, the tactic is only added when Lean is in collect-info mode.
 2014-10-23 13:30:04 -07:00
Leonardo de Moura
e750c9b67a feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode 2014-10-23 13:18:30 -07:00
Leonardo de Moura
38a9aa2a98 feat(frontends/lean): automatically open 'tactic' namespace (if it is not already open) in 'by' and 'begin-end' expressions 2014-10-23 10:26:19 -07:00
Leonardo de Moura
00f9a10e82 refactor(library/tactic/unfold_tactic): use new 'tactic.expr' to implement 'unfold' tactic 
This change also enabled us to remove hacks used in the tests modified
by this commit.
 2014-10-23 10:26:19 -07:00
Leonardo de Moura
5a553603d1 fix(library/general_notation): mark \tr as left associative 2014-10-22 22:18:40 -07:00
Leonardo de Moura
c50227ea6e feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included 
This commit also adds the tactic rapply that corresponds to the previous
semantics we have been using.
 2014-10-22 18:11:09 -07:00
Leonardo de Moura
e95c7c5f70 refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-10-22 17:29:50 -07:00
Leonardo de Moura
5e15ac0c92 feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics 2014-10-22 17:29:50 -07:00
Leonardo de Moura
33f18b9454 fix(kernel/converter): remove buggy eta-reduction and rely only on eta-expansion 
The bug is exposed by new unit test
 2014-10-21 16:54:25 -07:00
Leonardo de Moura
6b89080b1a feat(frontends/lean): do not allow user to define notation using tokens ! and @, closes #248 2014-10-21 16:28:36 -07:00
Leonardo de Moura
e24225fabf feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations 2014-10-21 15:39:47 -07:00
Leonardo de Moura
6c7e23ecaa refactor(library): use 'reserve' notation in the standard library 2014-10-21 15:39:47 -07:00
Leonardo de Moura
bb953b80aa feat(frontends/lean): reserve notation, closes #95 2014-10-21 15:39:47 -07:00
Leonardo de Moura
8a44dfc1df fix(frontends/lean/pp): bug in pretty printer notation match procedure 2014-10-20 18:58:27 -07:00
Leonardo de Moura
40fb66bf07 feat(frontends/lean): change default precedence to 1 2014-10-20 18:40:55 -07:00
Leonardo de Moura
e2fa981e89 fix(frontends/lean/pp): avoid parentheses around atomic notation 2014-10-20 18:08:13 -07:00
Leonardo de Moura
e68007a727 fix(frontends/lean/builtin_tactics): adjust tactics precedence 2014-10-20 17:10:16 -07:00
Leonardo de Moura
9b8f60b739 feat(frontends/lean/builtin_exprs): tolerate dangling ',' in begin-end block 
This is useful when debugging proofs.
 2014-10-20 15:59:49 -07:00
Leonardo de Moura
c09bb3cc6f fix(tests/lean/notation): remove 'sorry' warning from expected outputs 2014-10-20 15:34:44 -07:00
Leonardo de Moura
7d0100a340 feat(library/tactic): add 'intros' tactic 2014-10-20 15:26:16 -07:00
Leonardo de Moura
f0cc17af87 fix(frontends/lean/elaborator): missing type information when ! operator (aka consume_args) is used 2014-10-20 08:31:36 -07:00
Leonardo de Moura
a1006073d4 feat(frontends/lean/notation_cmd): do not allow user to define new tokes containing '(', ')', ',' or change their precedence 2014-10-19 13:39:06 -07:00
Leonardo de Moura
4d4bc0551f feat(frontends/lean/pp): minimize number of spaces when pretty printing notation 2014-10-19 13:08:15 -07:00
Leonardo de Moura
ed1afe26bd feat(frontends/lean/pp): support scopedexpr notation in the pretty printer 2014-10-19 12:50:40 -07:00
Leonardo de Moura
f63d47fef3 feat(frontends/lean/pp): support foldl/foldr notation in the pretty printer 2014-10-19 11:16:24 -07:00
Leonardo de Moura
eef1cc4ac2 fix(frontends/lean/pp): implicit arguments in notation 2014-10-19 09:04:43 -07:00
Leonardo de Moura
555d26aa61 feat(frontends/lean/pp): take notation declarations into account when pretty printing 
TODO: support foldl/foldr and binders
 2014-10-19 08:41:29 -07:00
Leonardo de Moura
28128e0330 fix(frontends/lean): EXTRA_TYPE info 2014-10-16 12:25:18 -07:00
Leonardo de Moura
e6606ef2ac feat(library/tactic): add 'rename' hypothesis tactic 2014-10-14 18:19:34 -07:00
Leonardo de Moura
90dba868e3 feat(library/tactic/proof_state): apply substitutions when pretty printing state 2014-10-14 17:37:20 -07:00
Leonardo de Moura
58c9421bab refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44, fixes #70 2014-10-14 17:18:40 -07:00
Leonardo de Moura
d75a9c840c fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244 2014-10-13 21:08:36 -07:00
Leonardo de Moura
b7c1b348d1 feat(frontends/lean/inductive_cmd): don't force user to repeat argument declarations in every datatype in a mutually recursive datatype declaration 2014-10-13 20:53:09 -07:00
Leonardo de Moura
08c0fb3a64 test(tests/lean/run): expand tree example 2014-10-13 07:08:29 -07:00
Leonardo de Moura
5c1d5133dd fix(library/data/prod): make the notation for tuples and product types consistent 2014-10-13 06:48:37 -07:00
Leonardo de Moura
a26618e0f2 feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied 2014-10-12 13:06:00 -07:00
Leonardo de Moura
549f24335e feat(frontends/lean): do not allow coercion definition in sections 2014-10-11 18:41:17 -07:00
Leonardo de Moura
158682219f feat(frontends/lean): allow parameters only in contexts 2014-10-11 17:13:56 -07:00
Leonardo de Moura
f984b51291 feat(frontends/lean/notation_cmd): remove the cleanup notation hack 2014-10-11 16:40:26 -07:00
Leonardo de Moura
ca632cca13 feat(frontends/lean): add 'universe variable' command 
We can declare variables anywhere. So, we must also be able do declare
"universe" variables anywhere. Here is a minimal example that requires
this feature

```
-- We want A and B to be in the same universe
universe variable l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```

The following doesn't work because A and B are in different universes
```
variable A : Type
variable B : Type
definition tst := A = B
```

The following works, but tst is not universe polymorphic, since l is
one *fixed* global universe
```
universe l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```
 2014-10-11 14:22:33 -07:00
Leonardo de Moura
b0f8d86f26 feat(frontends/lean/parser): reject ambiguous parameter declaration, closes #242 2014-10-10 18:08:03 -07:00
Leonardo de Moura
5e6ff3eef3 fix(frontends/lean/elaborator): bug when reporting error position 2014-10-10 17:31:12 -07:00
Leonardo de Moura
f0523a3465 feat(frontends/lean): namespaces also define scope for variables 2014-10-10 16:21:30 -07:00
Leonardo de Moura
0641ee33ce feat(frontends/lean): allow variables anywhere 2014-10-10 16:16:19 -07:00
Leonardo de Moura
3d65b1c25c fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241 2014-10-10 15:41:55 -07:00
Leonardo de Moura
235b8975d2 feat(kernel/inductive): K-like reduction in the kernel 
Given (H_1 : a = a), we have that
      eq.rec H_2 H_1
reduces to H_2

This is not exclusive to equality.
It applies to any inductive datatype in Prop, containing only one
constructor with zero "arguments" (we say they are nullary).

BTW, the restriction to only one constructor is not needed, but it is
does not buy much to support multiple nullary constructors since Prop is
proof irrelevant.
 2014-10-10 14:37:45 -07:00
Leonardo de Moura
402a351937 feat(frontends/lean): add 'universes' command 2014-10-10 08:45:59 -07:00
Leonardo de Moura
9ba59c6b25 feat(library/universe): improve support for universe level constraints in the unifier 2014-10-09 20:28:39 -07:00
Leonardo de Moura
8f1b6178a7 chore(*): minimize the use of parameters 2014-10-09 07:13:06 -07:00
Leonardo de Moura
8c5d3392c7 fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests 2014-10-08 23:44:09 -07:00
Leonardo de Moura
8947bf4347 feat(frontends/lean): display type of binders, closes #238 2014-10-08 22:54:10 -07:00
Leonardo de Moura
25fd370c51 fix(frontends/lean): bug when using nested sections and parameters 
see tests/lean/run/section4.lean
 2014-10-08 22:23:20 -07:00
Leonardo de Moura
57c85221fe fix(frontends/lean): collect used universe levels after elaboration in the check command 2014-10-08 22:23:19 -07:00
Leonardo de Moura
eab9321a3b fix(frontends/lean): make all variables/parameters visible for 'variables' command 2014-10-08 22:23:19 -07:00
Leonardo de Moura
757cb46579 test(tests/lean/run): add no_confusion test 2014-10-08 22:23:19 -07:00
Leonardo de Moura
3b23bec25b feat(frontends/lean): variables/parameters and check commands have access to all section variables/parameters, closes #231 2014-10-08 08:40:55 -07:00
Leonardo de Moura
744cee8dd8 feat(frontends/lean): force 'classes' to be declared before instances are declared, closes #228 2014-10-07 18:02:15 -07:00
Leonardo de Moura
d8572e249d feat(frontends/lean/builtin_cmds): add 'print classes' command 2014-10-07 17:30:57 -07:00
Leonardo de Moura
90ece4dd1b feat(frontends/lean): remove tactic hints for specific classes 
The idea is to separate class-instance resolution and tactic framework
as two independent engines.
 2014-10-07 09:44:01 -07:00
Soonho Kong
e41573afc4 chore(tests/*/test.sh): change working dir; avoid using ls in for-loop 2014-10-06 11:20:13 -07:00
Leonardo de Moura
f7e1b67f6c test(tests/lean/run/print): add tests for 'print' cmd 2014-10-05 19:06:29 -07:00
Leonardo de Moura
a0d4d82f3f refactor(data/nat/order): use new policy for marking implicit arguments and '!' operator 2014-10-05 11:36:39 -07:00
Leonardo de Moura
73aa024c31 refactor(library/logic): remove 'core' subdirectory 2014-10-05 10:50:13 -07:00
Leonardo de Moura
317e910054 refactor(library/data/bool): use new style 2014-10-05 09:50:55 -07:00
Leonardo de Moura
60d8369688 fix(library/unifier): missing justification when updating choice constraints 
The bug was not producing incorrect results, but really bad error
messages.
See: empty.lean.expected.out
 2014-10-04 10:40:53 -07:00
Leonardo de Moura
64f6601fe3 fix(frontends/lean/proof_qed_elaborator): information about synthesized variables in a proof-qed block was being lost 2014-10-04 09:15:42 -07:00
Leonardo de Moura
7073f036d8 test(tests/lean/run): add additional tests for section parameter/variable and strict implicit argument 2014-10-04 08:15:43 -07:00
Leonardo de Moura
bf01cfeec5 fix(frontends/lean): avoid superfluous local references of the form @-1 (@ f), 
This kind of term also confuses the elaborator
 2014-10-04 07:55:32 -07:00
Leonardo de Moura
e71d4548de fix(frontends/lean): universe levels associated with section variables should not be fixed in the section 2014-10-04 07:13:19 -07:00
Leonardo de Moura
938e12baa1 feat(frontends/lean/notation_cmd): allow local numeric notation 2014-10-03 13:55:57 -07:00
Leonardo de Moura
fd013e8d07 chore(tests/lean/run/group3): cleanup test 2014-10-03 13:55:57 -07:00
Leonardo de Moura
c0725d1934 refactor(frontends/lean): remove 'including' expressions 2014-10-03 09:09:27 -07:00
Leonardo de Moura
01d4644026 fix(frontends/lean): bug in include/omit commands: in the end of section/context, the configuration must be restored 2014-10-03 08:52:35 -07:00
Leonardo de Moura
284f300440 feat(frontends/lean): add 'include' and 'omit' commands, closes #184 2014-10-03 07:23:24 -07:00
Leonardo de Moura
6950b4aa9b fix(frontends/lean/decl_cmds): do not allow section parameters/variables to shadow existing parameters/variables 2014-10-02 18:29:41 -07:00
Leonardo de Moura
f006d93794 feat(frontends/lean): section variables occur after section parameters 2014-10-02 17:55:34 -07:00
Leonardo de Moura
0a13e7863a feat(frontends/lean): enforce rule section parameters cannot depend on section variables 2014-10-02 17:55:34 -07:00
Leonardo de Moura
bf081ed431 refactor(kernel): rename var_decl to constant_assumption 
Motivation: it matches the notation used to declare it.
 2014-10-02 17:55:34 -07:00
Leonardo de Moura
4946f55290 refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-10-02 17:55:34 -07:00
Leonardo de Moura
f78d831de3 refactor(frontends/lean): remove hardcoded Type', and define it using notation 2014-10-02 14:29:51 -07:00
Leonardo de Moura
4cb54ac825 feat(frontends/lean/elaborator): more strict test for bad universe solution 2014-10-02 14:29:51 -07:00
Leonardo de Moura
98e66586e9 feat(frontends/lean/elaborator): elaborator rejects 'Type' if the universe is explicit 2014-10-02 14:29:51 -07:00
Leonardo de Moura
153e3927ac feat(frontends/lean/elaborator): modify '!' semantics: it stops consuming arguments as soon it finds an argument that does not occur in the rest of the type. 2014-10-01 18:50:17 -07:00
Leonardo de Moura
e64d5c4a4a refactor(library/data/nat): use new operator '!' 2014-10-01 18:39:47 -07:00
Leonardo de Moura
716cd4d651 refactor(library): rename namespace eq_ops to eq.ops 2014-10-01 17:51:17 -07:00
Leonardo de Moura
ead827d6b7 feat(frontends/lean): add ! operator the "dual" of @, closes #220 2014-10-01 17:13:41 -07:00
Leonardo de Moura
bc6ebf34be feat(library/data/bool): do not use ! as notation for bnot, rename band/bor -> and/or 2014-10-01 17:00:03 -07:00
Leonardo de Moura
c46ec6a548 fix(frontends/lean): missing type information for INFO, fixes #218 2014-10-01 14:29:07 -07:00
Leonardo de Moura
f863d82e69 fix(frontends/lean/pp): pp was not taking into account new namespace name resolution rules, fixes #216 2014-10-01 11:24:45 -07:00
Leonardo de Moura
966366e18e feat(kernel/inductive): relaxed rules for defining datatypes with explicit universes, closes #217 2014-10-01 10:56:05 -07:00
Leonardo de Moura
263b081e69 fix(frontends/lean/inductive_cmd): temporary aliases must take explicit universes into account, fixes #215 2014-10-01 10:24:44 -07:00
Leonardo de Moura
2730e5163e feat(frontends/lean): allow 'sorry' implicit argument to access the whole context, and avoid cryptic error message 
See new test for explanation.
 2014-09-30 18:04:04 -07:00
Leonardo de Moura
113879a7dd feat(frontends/lean/server): sort exact matches by size in FINDP 2014-09-29 16:44:55 -07:00
Leonardo de Moura
a0c37b231f feat(kernel/expr): add hash_bi function that takes binder information into account 2014-09-29 16:44:55 -07:00
Leonardo de Moura
0d6d746d98 feat(frontends/lean): check modification time of imported files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-29 15:17:27 -07:00
Leonardo de Moura
21be308884 feat(frontends/lean/inductive_cmd): infer implicit argument annotation after elaboration, allow user to disable it by using '()' annotation, closes #210 2014-09-29 11:11:17 -07:00
Leonardo de Moura
9c55bbb871 feat(frontends/lean/elaborator): report an error when Type becomes a Prop after elaboration, closes #208 2014-09-29 08:18:10 -07:00
Leonardo de Moura
397395bbc9 feat(frontends/lean): allow user to associate priorities to class-instances, closes #180 2014-09-28 12:20:42 -07:00
Leonardo de Moura
22e47430b5 feat(library/unifier): add 'on-demand' choice constraints, they are processed as soon as their type does not contain meta-variables anymore 2014-09-27 21:50:39 -07:00
Leonardo de Moura
8e7aac1eb4 fix(frontends/lean): add 'eval' command 2014-09-26 20:16:03 -07:00
Leonardo de Moura
69f50adb2e fix(frontends/lean/server): must save the starting environment/options when reprocessing file, fixes #209 2014-09-26 15:36:47 -07:00
Leonardo de Moura
a3e38dc8a0 feat(frontends/lean): allow users to define "numeral notation" 2014-09-26 14:55:23 -07:00
Leonardo de Moura
631ebc6c4b fix(tests/lean/uni_bug1): make sure test does not produce a 'used sorry' warning. 
Thus, the output behavior is the same when we compile lean with/without IGNORE_SORRY=ON
 2014-09-26 09:42:31 -07:00
Leonardo de Moura
c775da16ec feat(frontends/lean/elaborator): discard partial solution during 
class-instance resolution, use only tactic_hints associated with
classes, enforce is_strict
 2014-09-25 19:46:08 -07:00
Leonardo de Moura
10a4148adb fix(tests): make sure tests can be executed on Windows msys2 shell 2014-09-20 15:51:24 -07:00
Leonardo de Moura
8fe7465ade fix(frontends/lean/pp): when formatting a coercion to function-class 
that contains implicit arguments
 2014-09-20 09:56:46 -07:00
Leonardo de Moura
fd5daa8fda feat(frontends/lean): use coercions to function-class and sort-class in 
function arguments, closes #203
 2014-09-20 09:00:10 -07:00
Leonardo de Moura
86f06a54ea refactor(library/data/vector): rename 'vec' to 'vector' 2014-09-19 16:20:50 -07:00
Leonardo de Moura
4e2377ddfc refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
5d8c7fbdf1 refactor(frontends/lean): replace '[private]' modifier with 'private 
definition' and 'private theorem', '[private]' is not a hint.
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
08ccd58eb6 feat(frontends/lean): add 'reducible' modifier for controlling which 
definitions are unfolded during elaboration

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
baf4c01de8 feat(frontends/lean): definitions are opaque by default 2014-09-19 15:54:32 -07:00
Leonardo de Moura
48dbd13eef feat(frontends/lean): allow transient classes/instances, i.e., 
classes/instances that are not saved in .olean files
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
b3e05a2fe9 refactor(frontends/lean/scanner): remove dependency to seekg and unget 
methods

It is not safe to use seekg for textual files. Here is a fragment from a
C++ manual:

seekg() and seekp()

This pair of functions serve respectively to change the position of stream pointers get and put. Both functions are overloaded with two different prototypes:

     seekg ( pos_type position );
     seekp ( pos_type position );

Using this prototype the stream pointer is changed to an absolute position from the beginning of the file. The type required is the same as that returned by functions tellg and tellp.

      seekg ( off_type offset, seekdir direction );
      seekp ( off_type offset, seekdir direction );

Using this prototype, an offset from a concrete point determined by
parameter direction can be specified. It can be:

          ios::beg	offset specified from the beginning of the stream
          ios::cur	offset specified from the current position of the stream pointer
          ios::end	offset specified from the end of the stream

The values of both stream pointers get and put are counted in different
ways for text files than for binary files, since in text mode files some
modifications to the appearance of some special characters can
occur. For that reason it is advisable to use only the first prototype
of seekg and seekp with files opened in text mode and always use
non-modified values returned by tellg or tellp. With binary files, you
can freely use all the implementations for these functions. They should
not have any unexpected behavior.
 2014-09-18 15:24:48 -07:00
Leonardo de Moura
78ad24a697 feat(frontends/lean/server): add SYNC command, closes #199 2014-09-16 18:42:34 -07:00
Leonardo de Moura
e3e2370a38 feat(frontends/lean): split 'opaque_hint' command into 'opaque' and 'transparent' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-16 18:03:40 -07:00
Leonardo de Moura
50f788a427 fix(tests/lean/interactive): adjust test to library reorg 2014-09-16 13:16:46 -07:00
Jeremy Avigad
74cb289d48 refactor(library): rename algebra directory to struc, move categories.lean to algebra 2014-09-16 13:13:01 -07:00
Jeremy Avigad
9988914189 refactor(library/logic): move files in classes directory to core 2014-09-16 13:13:01 -07:00
Leonardo de Moura
dffe9a6f17 fix(frontends/lean/elaborator): more robust support for coercions to 
function-class that contains implicit arguments
 2014-09-16 13:08:34 -07:00
Leonardo de Moura
d0d23eb525 fix(frontends/lean/inductive_cmd): improve name resolution in inductive 
command

The new test demonstrates the problem being fixed by this commit
 2014-09-16 09:48:51 -07:00
Leonardo de Moura
851444b77a test(tests/lean/interactive): test for issue #193 2014-09-15 16:07:23 -07:00
Leonardo de Moura
8e52c478b1 refactor(library/data/num): add 'succ', 'pred' and 'size' (aka number of bits), 
rename is_inhabited theorems
 2014-09-15 16:05:17 -07:00
Leonardo de Moura
af2c3b1815 fix(frontends/lean/info_manager): bug in save_environment_options, 
server was displaying old results
 2014-09-15 16:05:17 -07:00
Leonardo de Moura
edcbe6fe10 feat(frontends/lean): allow multiple coercions from class A to B, closes #187 
See new tests (for examples)
tests/lean/run/coe10.lean
tests/lean/run/coe11.lean
tests/lean/run/coe9.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-14 12:59:43 -07:00
Leonardo de Moura
029acbd1df feat(library/coercion): better support for coercions to function-class. closes #185 2014-09-12 13:17:20 -07:00
Leonardo de Moura
a2e36e97f2 fix(frontends/lean/builtin_cmds): allow coercion command inside section, fixes #186 2014-09-12 12:13:29 -07:00
Leonardo de Moura
010ecebfea 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.
 2014-09-11 18:14:49 -07:00
Leonardo de Moura
7ffe73b8ca fix(frontends/lean): name clash inside section, fixes #181 2014-09-11 16:37:23 -07:00
Leonardo de Moura
5cff53c447 test(tests/lean/run): add section test 2014-09-11 15:33:20 -07:00
Leonardo de Moura
85f7132efe feat(frontends/lean/placeholder_elaborator): perform class-instance resolution in a completely independent unifier object, it also triggers the resolution when expected type does not contain metavariables, closes #175, closes #173, closes #68 2014-09-11 14:49:35 -07:00
Leonardo de Moura
b82092a123 fix(frontends/lean/parser): segmentation fault after REPLACE, fixes #172 2014-09-10 08:39:39 -07:00
Leonardo de Moura
570879b55f feat(frontends/lean): add declaration to namespace without opening it, closes #161 2014-09-09 18:02:14 -07:00
Leonardo de Moura
efb14d906b chore(tests/lean): add untracked tests 2014-09-09 16:21:30 -07:00
Leonardo de Moura
9b9adf8831 refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
Leonardo de Moura
47e02342bb feat(frontends/lean/elaborator): use whnf in class-instance resolution, closes #160 2014-09-09 15:04:44 -07:00
Leonardo de Moura
abdd784729 feat(shell): start 'lean --server' with 'pp.beta = true' 2014-09-09 14:13:35 -07:00
Leonardo de Moura
ee196bbf1a fix(frontends/lean/pp): pretty printing coercions to functions, fixes #151 2014-09-09 12:49:32 -07:00
Leonardo de Moura
d8caa294b5 fix(frontends/lean/parser): configuration options defined in a context are transient, fixes #162 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-09 11:02:54 -07:00
Leonardo de Moura
05c6e1461e fix(tests/lean/interactive): interactive tests expected output, they must include the new '-- BEGINWAIT' messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-09 09:47:19 -07:00
Leonardo de Moura
187661aa6a feat(library/unifier): consider whnf case-split on flex-rigid constraints whenever the rhs contains a local constant that is not in the lhs 2014-09-09 09:27:26 -07:00
Leonardo de Moura
4088cdc139 chore(frontend/lean/pp_options): use consistent name convention for pp option names 2014-09-09 09:27:26 -07:00
Leonardo de Moura
b4793df653 feat(frontends/lean): rename '[fact]' to '[visible]' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-08 07:47:42 -07:00
Leonardo de Moura
559dd586f2 feat(library): add 'decidable_eq' class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-07 22:23:36 -07:00
Leonardo de Moura
cbdfb0dcdc feat(frontends/lean/elaborator): (Pi/forall) intro in class inference, closes #77 2014-09-07 19:59:34 -07:00
Leonardo de Moura
2631979f5c fix(library/scoped_ext): section/context should not affect namespace 2014-09-07 19:59:34 -07:00
Leonardo de Moura
3310eb3dfc feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-07 12:29:32 -07:00
Leonardo de Moura
5549295c47 fix(frontends/lean/inductive_cmd): bug when elaborating inductive tyoe parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-06 11:38:32 -07:00
Leonardo de Moura
bbff564a1c feat(frontends/lean): persistent notation in sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-06 11:14:20 -07:00
Leonardo de Moura
b5f595c432 fix(frontends/lean/inductive_cmd): bugs when declarating inductive datatypes in sections, fixes #141, fixes #142 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-05 19:17:09 -07:00
Leonardo de Moura
9412e604c8 refactor(library/data): cleanup datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 22:31:52 -07:00
Leonardo de Moura
6632a50015 refactor(library): add namespaces 'or', 'and' and 'iff' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 21:25:21 -07:00
Leonardo de Moura
68d9bef860 refactor(library): add 'eq' and 'ne' namespaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 18:41:06 -07:00
Leonardo de Moura
2bc6f92d33 refactor(library): add 'and' namespace 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 17:44:53 -07:00
Leonardo de Moura
364bba2129 feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 17:26:36 -07:00
Leonardo de Moura
8743394627 refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 15:04:57 -07:00
Leonardo de Moura
653141135d chore(tests/lean): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 15:04:57 -07:00
Leonardo de Moura
ffc871ea8c feat(frontends/lean/server): only display 'EXTRA_TYPE' info when the column number is provided to the 'INFO' command, closes #133 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 14:02:53 -07:00
Leonardo de Moura
9d0a4d21d4 chore(tests/lean/interactive): adjust test expected output 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 10:00:42 -07:00
Leonardo de Moura
f9a90b9920 feat(frontends/lean): add 'export' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-03 18:37:01 -07:00
Leonardo de Moura
5e18e6609c feat(frontends/lean): add 'as' clause to 'open' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-03 17:37:02 -07:00
Leonardo de Moura
e51c4ad2e9 feat(frontends/lean): rename 'using' command to 'open' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-03 16:00:38 -07:00
Leonardo de Moura
e14814d4bf feat(frontends/lean): add '[protected]' modifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-03 15:01:13 -07:00
Leonardo de Moura
2ca0a22e2c fix(tests/lean/interactive/in4): adjust test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-03 01:35:46 -07:00
Leonardo de Moura
0f9478d91e feat(frontends/lean): add 'class' command back 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-02 15:04:23 -07:00
Leonardo de Moura
8dec18018c refactor(library/data/list): avoid placeholders '_', make first argument of false_elim implicit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-01 19:44:04 -07:00
Leonardo de Moura
b7d7f12b8e fix(frontends/lean/info_manager): several bugs: invalid flag was not being reset for empty lines, merge with overwrite=false was adding 'poluting' state, --NAY generation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-30 10:35:36 -07:00
Jeremy Avigad
6ffd719c1a refactor(library/logic): move identities from classical to identities 2014-08-29 22:28:22 -07:00
Leonardo de Moura
59d3227eaa fix(tests/lean/interactive): test output 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 18:17:07 -07:00
Leonardo de Moura
9a4472cff5 fix(frontends/lean): wrong displayed type in proof with multiple sorry's, fixes #112 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 14:32:53 -07:00
Leonardo de Moura
b9489ce585 fix(frontends/let): let-expression pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 10:58:27 -07:00
Leonardo de Moura
d8548369e7 feat(frontends/lean/pp): improve let-expr pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-29 07:46:58 -07:00
Leonardo de Moura
be56fcf0bd fix(frontends/lean/pp): pretty print 'let-expressions', closes #87 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 18:20:58 -07:00
Leonardo de Moura
1e80a9dfe9 feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 16:27:52 -07:00
Leonardo de Moura
d536475e49 refactor(library): more implicit_args for: and_assoc, and_comm, or_assoc, or_comm, if_pos, if_neg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 11:10:04 -07:00
Leonardo de Moura
6b7e79b62f feat(library/data/nat): mark more arguments implicit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 10:38:58 -07:00
Leonardo de Moura
8de9cab62d test(tests/lean/interactive): add --server test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 07:41:38 -07:00
Jeremy Avigad
00a049a667 refactor(library/logic): rename connectives -> core, basic -> connectives 2014-08-27 18:43:24 -07:00
Leonardo de Moura
2d78387541 refactor(library/logic/basic): rename absurd_elim to absurd, delete contrapos and trivial_not_true theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 18:34:09 -07:00
Leonardo de Moura
477b7b4811 fix(tests/lean/run/class_coe): adjust test to reflect library changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 17:55:42 -07:00
Leonardo de Moura
8719dff361 fix(frontends/lean): distribute '@' over choice 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 16:31:18 -07:00
Leonardo de Moura
c7e9e238ec fix(frontends/lean/server): ignore output produced by worker thread, fixes #98 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 10:46:49 -07:00
Leonardo de Moura
a8d58fdd33 refactor(library): mark absurd_elim argument as implicit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-26 18:27:39 -07:00
Leonardo de Moura
dd99e60a00 refactor(frontends/lean/info_manager): store environment+options in the info_manager, fixes #96 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-26 18:07:09 -07:00
Leonardo de Moura
4ab0dd4700 fix(tests/lean): adjust test to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-26 09:12:18 -07:00
Leonardo de Moura
c11fd6b0d2 fix(tests/lean/run): adjust tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 21:39:46 -07:00
Leonardo de Moura
04d9eb17d1 feat(kernel/conveter): improve support for proof irrelevant in the converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 11:19:18 -07:00
Leonardo de Moura
42a8fb5965 chore(tests/lean/run/matrix): simplify same_dim_irrel proof 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 09:27:19 -07:00
Leonardo de Moura
60d5e87a66 test(tests/lean/run): add matrix test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 09:04:39 -07:00
Leonardo de Moura
cbc81ea6c5 chore(*): minimize dependencies on tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-24 19:58:48 -07:00
Leonardo de Moura
dbaf81e16d refactor(library): remove unnecessary 'standard' subdirectory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:08:09 -07:00
Jeremy Avigad
47a1c00a6d refactor(library/standard): collect notation in general_notation 2014-08-23 17:53:02 -07:00
Leonardo de Moura
2f699fa53a feat(*): make sections 'permanent', and add 'transient' contexts, closes #88 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 15:45:15 -07:00
Leonardo de Moura
e602c4ba49 feat(frontends/lean): change multicomment to /- ... -/ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 17:55:13 -07:00
Leonardo de Moura
c5a44aca44 fix(frontends/lean/elaborator): do not expose type information produced when synthesizing class instances 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 17:07:12 -07:00
Leonardo de Moura
a5f0593df1 feat(*): change inductive datatype syntax 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 15:46:10 -07:00
Leonardo de Moura
626cd952e7 test(tests/lean/run): add overload test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 15:23:33 -07:00
Leonardo de Moura
01000ff7df feat(library): add typed_expr macro 
We use it to enforce that a let-variable has the expected type

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 11:26:06 -07:00
Leonardo de Moura
937c465685 fix(library/unifier): too much reduction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 21:37:51 -07:00
Leonardo de Moura
07bc0727e2 feat(frontends/lean): 'let [inline]' is the default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 18:24:22 -07:00
Leonardo de Moura
6cf73b51e2 fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 17:56:18 -07:00
Leonardo de Moura
bb6dbe0e6f fix(library/unifier): we should preprocess choice constraints before we start solving any constraint, fixes #85 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 16:58:25 -07:00
Leonardo de Moura
725f5ba0a0 feat(frontends/lean): use 'begin-end' instead of 'proof-qed' for blocks of tactics, closes #81 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 16:58:25 -07:00
Leonardo de Moura
359c72b02f fix(frontends/lean/pp): bug when pretty printing binder information, fixes #73 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 09:28:07 -07:00
Leonardo de Moura
8375626cb6 fix(doc/lean/tutorial): adjust tutorial to library changes, fix test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 18:32:53 -07:00
Jeremy Avigad
6264fb52d6 fix(lean/library/standard): fix tests, more cleanup 2014-08-20 18:04:31 -07:00
Leonardo de Moura
f5987b7bda refactor(library/unifier): make it easier to add new options to the unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 17:30:08 -07:00
Leonardo de Moura
b60c9d9ecc test(tests/lean/run): add test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 16:46:19 -07:00
Leonardo de Moura
f0d50e0d33 feat(frontends/lean): change the name resolution rules: when in a namespace N that defines C, then C always refers to N.C (i.e., it overrides any alias) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-18 18:58:50 -07:00
Leonardo de Moura
08ae17650b feat(frontends/lean): try overloaded notation and declarations in the order they were defined 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-18 18:58:50 -07:00
Leonardo de Moura
919f02983e feat(frontends/lean/elaborator): case-split on coercions that cannot be resolved by postponing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-18 18:58:50 -07:00
Leonardo de Moura
4a96fefd96 fix(library/unifier): bug in unifier priority queue 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-18 18:58:50 -07:00
Leonardo de Moura
1d306c09ee fix(tests/lean/interactive): remove leftover from test output 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-17 17:29:52 -07:00
Leonardo de Moura
05b0f24cb5 fix(frontends/lean/decl_cmds): improve error message for invalid end of theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-17 17:03:54 -07:00
Leonardo de Moura
13af81d554 fix(tests/lean/interactive): adjust test output to reflect new features 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-17 15:23:53 -07:00
Leonardo de Moura
55b0a03e3d refactor(frontends/lean/info_manager): to allow cache to be used when producing info data, fixes #37, closes #45 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-17 12:16:32 -07:00
Leonardo de Moura
1436212a34 fix(library/unifier): use depth-first search strategy for solving class-instance constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-16 13:51:24 -07:00
Leonardo de Moura
670bfe24f5 chore(build): remove hott library directory, and move hott tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-15 13:30:56 -07:00
Leonardo de Moura
094459504b fix(tests/lean/run): adjust test to changes in the library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-15 13:27:18 -07:00
Leonardo de Moura
28b7d87f1f feat(frontends/lean/pp): pretty print numerals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 09:12:22 -07:00
Leonardo de Moura
e778e3faec fix(tests/lean): adjust tests expected output 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-13 12:35:14 -07:00
Leonardo de Moura
60ab6d3bd8 feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
7d0c0818e5 test(tests/lean/slow): add self contained path_groupoids test file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-11 16:44:30 -07:00
Leonardo de Moura
70c0eda9fc feat(frontends/lean): make sure all scopes are closed in the end of the module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 17:08:59 -07:00
Leonardo de Moura
1a67e69678 feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:59:08 -07:00
Leonardo de Moura
2486c483cf chore(kernel/error_msgs): change type mismatch error messages, closes #33 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:18:40 -07:00
Leonardo de Moura
9e6c5695be fix(library/unifier): make sure the imitation step is type correct, fix ensure_sufficient_args 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:09:45 -07:00
Leonardo de Moura
4ad7e709aa feat(frontends/lean): default for inductive types, closes #32 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 07:52:37 -07:00
Leonardo de Moura
8d9ca4c4ea fix(tests/lean): remove obsolete test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 19:40:02 -07:00
Leonardo de Moura
a173b7f6e6 test(tests/lean/interactive): add old 'interactive' tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 14:57:08 -07:00
Leonardo de Moura
069f217215 fix(frontends/lean/elaborator): use full local context for metavariables due to coercions and overloads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 17:21:21 -07:00
Leonardo de Moura
9cc2015caa feat(library/unifier): better error message for invalid local context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 16:25:22 -07:00
Leonardo de Moura
d1924097d5 feat(library/match): add 'local' backtracking 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 10:09:00 -07:00
Leonardo de Moura
e6ffda0c51 feat(library/match): add basic match_plugin that just invokes whnf before failing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-05 08:37:03 -07:00
Leonardo de Moura
56d151ef7f feat(frontends/lean): 'partial' aliases. closes #24 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 22:08:10 -07:00
Leonardo de Moura
50b0c17092 feat(library/unifier): add more information in error messages due to type errors when assigning metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 09:49:30 -07:00
Leonardo de Moura
938b4e8421 test(tests/lean/run): add unicode in identifiers test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 20:05:46 -07:00
Leonardo de Moura
fbc4a7af3b feat(library/unifier): when unifier.expensive == true, then use only restrict higher-order unification (a fragment slightly more general than higher-order pattern matching) for solving class-instance constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 14:30:25 -07:00
Leonardo de Moura
5e2185cfbe feat(library/unifier): postpone as much as possible universe constraints of the form ?m1 =?= max(l1, l2) and ?m1 =?= imax(l1, l2) where ?m1 occurs in the right hand side. When there is nothing else to be done, try to solve them by reducing to ?m1 = l1 and ?m1 = l2. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 09:14:35 -07:00
Leonardo de Moura
3795d466c1 fix(frontends/lean/elaborator): provide type information for expressions using '@' operator, and strict function applications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 20:57:24 -07:00
Leonardo de Moura
4cb8fb20fe fix(frontends/lean/elaborator): bug when mixing string and non-strict implict arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 10:58:20 -07:00
Leonardo de Moura
01908c4dac chore(tests/lean): add 'expensive' file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 10:35:32 -07:00
Leonardo de Moura
8e6324185a fix(tests/lean): adjust tests to new library structure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 09:37:23 -07:00
Leonardo de Moura
6ca80b5000 feat(frontends/lean): add 'sorry' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 18:35:57 -07:00
Leonardo de Moura
de05c041c7 feat(library/unifier): add flag for enabling/disabling expensive extensions in the unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 16:46:16 -07:00
Leonardo de Moura
f57fc33442 fix(library/unifier): bug that was making unifier miss solutions, and add a new case-split that tries to solve flex_rigid constraints by putting the rhs into whnf 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 16:46:16 -07:00
Leonardo de Moura
9637ceb86e feat(frontends/lean): allow user to provide a terminator for 'foldr' and 'foldl' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-30 15:04:44 -07:00
Leonardo de Moura
450131692a fix(library/converter): missing constraint on eta expansion 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-30 10:43:47 -07:00
Leonardo de Moura
936bb2744b fix(library/unifier): add a flag to sign that a choice constraint owns a metavariable ?m, that is, it has the right to assign ?m, and the unifier should postpone any other constraint that tries to assign ?m 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-29 17:32:55 -07:00
Leonardo de Moura
320bc55e85 fix(frontends/lean/elaborator): use preprocessed expression when displaying errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-29 14:25:50 -07:00
Leonardo de Moura
b15f1bb8c7 fix(frontends/lean/elaborator): apply coercions in definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-29 13:55:39 -07:00
Leonardo de Moura
501cae37e5 fix(frontends/lean/parser): bug in check_constant_next (when invoked inside of a section) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-29 13:04:58 -07:00
Leonardo de Moura
105c29b51e refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-28 19:59:38 -07:00
Leonardo de Moura
5f360cd8ec feat(kernel/error_msgs): improve application type mismatch error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-28 07:08:12 -07:00
Leonardo de Moura
4b2e403023 test(tests/lean/run): add more tests sent by Cody 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 12:17:38 -07:00
Leonardo de Moura
faee08591f fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 12:12:54 -07:00
Leonardo de Moura
6ca120bf77 test(tests/lean/run): add Cody's file to test suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 08:17:46 -07:00
Leonardo de Moura
0cdd4a267c feat(frontends/lean/pp): pretty print 'show' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 21:56:35 -07:00
Leonardo de Moura
60cc9ac8e2 feat(frontends/lean/pp): pretty print 'have' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 21:35:26 -07:00
Leonardo de Moura
cf35c07786 fix(frontends/lean): fix 'let' annotation placement and pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 21:00:22 -07:00
Leonardo de Moura
206206060f test(tests/lean/hott): add some of Vladimir's definitions as tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 20:50:37 -07:00
Leonardo de Moura
70ef92cd5e feat(build): add tests/lean/slow test directory, and add nat_wo_hints.lean file that elaborates nat.lean without using any hint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 10:53:44 -07:00
Leonardo de Moura
23af5ab217 fix(library/unifier): eager whnf application 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 10:37:02 -07:00
Leonardo de Moura
709b5ce90f fix(kernel/justification): duplicate position 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 21:16:49 -07:00
Leonardo de Moura
70c887a0bd fix(library/unifier): fix cryptic error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 21:10:32 -07:00
Leonardo de Moura
e79b0b11cf test(tests/lean/run): another test for the unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 20:55:05 -07:00
Leonardo de Moura
cf44c80ffb fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 16:00:38 -07:00
Leonardo de Moura
7b84503133 fix(library/unifier): do not let a unification plugin to 'prioritize' a flex-flex constraint, and add missing case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 15:03:57 -07:00
Leonardo de Moura
0f12e5a35b fix(library/inductive_unifier_plugin): unification problem failure on problems with inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 13:49:45 -07:00
Leonardo de Moura
a59eec39b8 feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 09:44:40 -07:00
Leonardo de Moura
21176c61fe fix(tests/lean): move crash.lean to different directory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 08:48:35 -07:00
Leonardo de Moura
e7c7d5718a fix(frontends/lean/pp): fix bug in the pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 08:30:30 -07:00
Leonardo de Moura
15c1e39f88 feat(frontends/lean/elaborator): distribute application over choice, this feature improves the support for overloaded aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 23:43:40 -07:00
Leonardo de Moura
905a1095f9 fix(tests/lean/run/tactic14): remove not_intro, it is not needed anymore 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 23:41:23 -07:00
Leonardo de Moura
5529ef1056 feat(library/standard): add function 'helper' module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 16:29:39 -07:00
Leonardo de Moura
d998bf9300 test(tests/lean/run): add some 'lost' tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-23 08:22:53 -07:00
Leonardo de Moura
b522ea6f2d refactor(library/standard): rename bit to bool 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 09:49:54 -07:00
Leonardo de Moura
5eaf04518b refactor(*): rename Bool to Prop 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 09:43:18 -07:00
Leonardo de Moura
a9f7d87aae test(tests/lean/run/decidable): show implicit argument that is computed automatically 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 05:58:36 -07:00
Leonardo de Moura
5e8c128b00 feat(library/standard): add more decidable instances 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-20 01:10:49 +01:00
Leonardo de Moura
6b60db7b93 fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-19 09:55:34 +01:00
Leonardo de Moura
0f44e3c9f4 fix(frontends/lean): calc configuration commands, add check_constant_next auxiliary method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-15 01:19:47 +01:00
Leonardo de Moura
2e6184a721 fix(frontends/lean): more bugs in section management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 06:27:36 +01:00
Leonardo de Moura
8167ad329f fix(frontends/lean): bug in section management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 05:04:01 +01:00
Leonardo de Moura
fab7934265 refactor(frontends/lean/elaborator): modify when tactic_hints are invoked, add the notion of strict placeholder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-14 02:53:02 +01:00
Leonardo de Moura
e432e23115 test(tests/lean/run/class5): improve test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-13 22:39:16 +01:00
Leonardo de Moura
1d273fcfdd chore(frontends/lean): rename 'obtains' to 'obtain' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-12 06:35:24 +01:00
Leonardo de Moura
1230e942aa feat(library/unifier): handle 'first-order' flex-flex constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-11 04:51:28 +01:00
Leonardo de Moura
cf34f75ab5 feat(frontends/lean): add 'obtains' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-11 04:08:51 +01:00
Leonardo de Moura
6000270d35 chore(tests/lean): reactivate config.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 23:32:23 +01:00
Leonardo de Moura
e9c17b154c fix(tests/lean): define LEAN_PATH in tests scripts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 23:26:55 +01:00
Leonardo de Moura
92bb046854 test(tests/lean/run): add nested let-expr test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 15:56:15 +01:00
Leonardo de Moura
c13c75b93e feat(frontends/lean/pp): add option for displaying fully qualified names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 15:55:19 +01:00
Leonardo de Moura
06beff327f test(tests/lean/run): add more universe tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 14:43:55 +01:00
Leonardo de Moura
49bc3fffbd fix(frontends/lean/pp): purify procedure for local names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 14:13:51 +01:00
Leonardo de Moura
fc8ddcb0ce feat(frontends/lean): improve 'check' command when used inside sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 14:07:41 +01:00
Leonardo de Moura
1a6d0784f2 feat(kernel/level): improve universe level normalization procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 13:49:41 +01:00
Leonardo de Moura
d9b2801eeb feat(frontends/lean): use the same universe in declarations such as (A B : Type) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 13:18:52 +01:00
Leonardo de Moura
12d89ea0b9 fix(kernel/level): is_geq predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-10 13:18:41 +01:00
Leonardo de Moura
aff766430d fix(frontends/lean/pp): universe pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 19:17:28 -07:00
Leonardo de Moura
43eba857cb feat(frontends/lean): add let-expr pretty printer, reduce default indentation to 2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 18:47:10 -07:00
Leonardo de Moura
2ef7b9be2f feat(frontends/lean): add basic pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-09 01:12:36 -07:00
Leonardo de Moura
2ad1a93657 test(tests/lean/run): add append tactic test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 18:21:22 -07:00
Leonardo de Moura
a1601e7a5f feat(library/tactic/apply_tactic): add option for 'refreshing' universe metavariables in the 'apply' tactic 
The new test ../../tests/lean/run/tactic27.lean demonstrates why we need this feature. The tactic 'apply @refl' is actually 'apply @refl.{?l}'. It is used inside of a repeat tactical. Each iteration of the 'repeat' may need to use a different value for ?l. Before this commit, there was not way to say we want a fresh ?l each iteration.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 16:55:23 -07:00
Leonardo de Moura
4505016154 feat(frontends/lean): allow tactic_hints to be applied when class-instance mechanism fails 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 15:08:13 -07:00
Leonardo de Moura
5e836092cc feat(frontends/lean): allow user to suppress proofs in theorems, and let them be inferred automatically using tactic_hints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 15:08:13 -07:00
Leonardo de Moura
a3be63af73 feat(frontends/lean): add tactic_hint command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-08 15:08:13 -07:00
Leonardo de Moura
da4c1922e3 feat(frontends/lean): add '_root_' prefix for referencing names in the root namespace 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 19:15:46 -07:00
Leonardo de Moura
b43fb7448c feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 19:00:06 -07:00
Leonardo de Moura
e6d4c01b88 feat(frontends/lean): check whether namespace exists or not in the 'using' command, add to_valid_namespace_name helper function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 18:17:10 -07:00
Leonardo de Moura
bd1873f6b1 feat(frontends/lean): add coercion modifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 17:48:20 -07:00
Leonardo de Moura
08465f049a feat(frontends/lean): remove [class] annotation and 'class' command, they are redundant, we only need [instance] and 'instance' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 16:09:30 -07:00
Leonardo de Moura
112353861c feat(frontends/lean): rename command 'reset_proof_qed' to 'set_proof_qed' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 15:48:16 -07:00
Leonardo de Moura
c16951aba6 fix(library/aliases): aliasing behavior 
The new test '../../tests/lean/run/alias3.lean' demonstrates the issue being fixed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 15:40:55 -07:00
Leonardo de Moura
b9d08ff28c feat(frontends/lean/builtin_cmds): allow many namespaces in the same 'using' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 14:53:06 -07:00
Leonardo de Moura
d30f387e72 feat(library/standard): add namespace 'pair' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 14:48:19 -07:00
Leonardo de Moura
10b0dfeb37 feat(frontends/lean/class): allow many instances to provided with a single 'instance' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 14:41:14 -07:00
Leonardo de Moura
6ceecf6a15 feat(library/aliases): remove duplicates from aliasing tables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 12:59:57 -07:00
Leonardo de Moura
b956ce68d2 feat(frontends/lean/elaborator): keep postponing delayed coercions until the type can be inferred 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 12:50:43 -07:00
Leonardo de Moura
831de22bcd fix(frontends/lean): bugs in notation management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-07 09:31:42 -07:00
Leonardo de Moura
e8bd267a00 fet(frontends/lean): allow coercions to sort-class in the types of variable and definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-06 21:54:16 -07:00
Leonardo de Moura
48b28ad75c fix(library/unifier): missing test in flex_rigid 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-06 21:36:23 -07:00
Leonardo de Moura
dcf7cf00ff fix(*): bugs in the type checker, inductive datatypes, and unifier 
The bugs were indentified when performing the tiny change in the file
tests/lean/run/group.lean
 2014-07-06 18:44:56 -07:00
Leonardo de Moura
9a13bef4f3 fix(frontends/lean): fix (and simplify) parameter universe inference 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-06 16:56:54 -07:00
Leonardo de Moura
8e5ac54ae1 test(tests/lean/run): group experiments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 22:31:57 -07:00
Leonardo de Moura
55894f01e3 feat(frontends/lean): add 'opaque_hint' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 18:58:20 -07:00
Leonardo de Moura
e68a3e5251 test(tests/lean/run): add another class-instance example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 17:41:08 -07:00
Leonardo de Moura
59755289e4 feat(library/unifier): case split on constraints of the form (f ...) =?= (f ...), where f can be unfolded, and there are metavariables in the arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 15:52:40 -07:00
Leonardo de Moura
a52c9f4e2b feat(library/unifier): add option 'unifier.unfold_opaque', remove option 'unifier.use_exceptions' (the user should not be able to change this) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 09:43:16 -07:00
Leonardo de Moura
efabd2280c feat(library/unifier): allow unifier to unfold opaque definitions of the current module 
It is not clear whether this is a good idea or not. In some cases, it seems to do more harm than good.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 00:46:03 -07:00
Leonardo de Moura
99fb6431a6 fix(frontends/lean/elaborator): support for local instances 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 18:38:08 -07:00
Leonardo de Moura
8ab0b5bee3 feat(frontends/lean/elaborator): use local declarations as class instances 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 18:18:25 -07:00
Leonardo de Moura
00e1a7db23 feat(frontends/lean/elaborator): add class instance elaboration 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 15:45:50 -07:00
Leonardo de Moura
b94ce412ae fix(library/unifier): non-termination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 10:32:01 -07:00
Leonardo de Moura
a97f82be1a fix(library/standard): orelse notation, avoid conflict with inductive datatype declaration 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 10:10:05 -07:00
Leonardo de Moura
e0501104e2 feat(library/tactic): add 'fixpoint' tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-04 01:30:28 -07:00
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
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
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
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
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
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
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
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
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
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
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
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
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
33cb9382aa feat(frontends/lean): add beta-reduction tactic command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 19:41:54 -07:00
Leonardo de Moura
360e9b9486 feat(library/tactic): add apply tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 18:33:53 -07:00
Leonardo de Moura
6645fdeae0 feat(frontends/lean): add repeat tactic command, refactor tactic sequence notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 12:24:13 -07:00
Leonardo de Moura
2510d5722a feat(frontends/lean): add unfold tactic command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 12:05:45 -07:00
Leonardo de Moura
6d09d82a7c feat(frontends/lean): add notation for orelse tactic, add show and now tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 11:39:18 -07:00
Leonardo de Moura
a1bbb09de4 feat(frontends/lean): add notation for then tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 11:24:56 -07:00
Leonardo de Moura
ffa175009b feat(frontends/lean): use tactics for solving unassigned metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 09:50:16 -07:00
Leonardo de Moura
1e39a21823 feat(frontends/lean): add basic tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 09:03:51 -07:00
Leonardo de Moura
7d5522e36a chore(tests): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 09:03:51 -07:00
Leonardo de Moura
f5f3816596 chore(tests): cleanup test scripts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 09:03:39 -07:00
Leonardo de Moura
cf28981f45 feat(tests/lean/run): add test_single script that sets the LEAN_PATH 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 07:47:46 -07:00
Leonardo de Moura
193ce35419 refactor(frontends/lean/inductive_cmd): redesign inductive datatype elaboration, use the new elaborator, and use simpler algorithm to infer the resulting universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-28 15:33:56 -07:00
Leonardo de Moura
0adacb5191 feat(kernel): add infer implicit, and use it to infer implicit arguments of inductive datatype eliminators, and tag whether parameters should be implicit or not in introduction rules in the module inductive_cmd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-28 13:57:36 -07:00
Leonardo de Moura
47ff300d1a fix(frontends/lean): '@' explicit mark 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-28 07:30:36 -07:00
Leonardo de Moura
ccce9d90a4 feat(frontends/lean/elaborator): add 'delayed coercions', add example demonstrating why the new feature is useful 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 18:39:23 -07:00
Leonardo de Moura
340dc622c6 fix(kernel/formatter): make sure simple formatter output is not sensitive to internal names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 14:58:59 -07:00
Leonardo de Moura
150d285b39 fix (library/unifier): occurs_context_check 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 14:45:36 -07:00
Leonardo de Moura
16bdc51fc4 refactor(kernel/type_checker): simplify type checker API, and remove add_cnstr_fn 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 13:36:31 -07:00
Leonardo de Moura
a70f8dd98e feat(kernel/inductive): mark parameters, type formers and indices as implicit parameters in the elimination rule 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 11:05:14 -07:00
Leonardo de Moura
5e0e737213 feat(library/scoped_ext): do not import 'children' namespace objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 10:32:34 -07:00
Leonardo de Moura
a7623845f9 test(tests/lean/run): add another example on how to deal with ambiguity 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 10:18:35 -07:00
Leonardo de Moura
930960c54d fix(frontends/lean/builtin_cmds): abstract section parameters in the 'check' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 10:06:50 -07:00
Leonardo de Moura
cc21bfd01d test(tests/lean/run): more tests on how to deal with ambiguity 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 09:32:26 -07:00
Leonardo de Moura
dc5553ea5c test(tests/lean/run): add test demonstrating how to control ambiguity 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 09:32:19 -07:00
Leonardo de Moura
da6e92787a test(tests/lean/run): add simple overloading test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 09:32:12 -07:00
Leonardo de Moura
acf8c13619 feat(kernel): add strict implicit arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 17:50:49 -07:00
Leonardo de Moura
4bc1f3cf81 test(lean/run): add elaborator tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 16:15:01 -07:00
Leonardo de Moura
49a6048060 test(lean/run): add another test for new elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 13:18:32 -07:00
Leonardo de Moura
3e7dfa6212 fix(frontends/lean): infer type of definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 08:39:14 -07:00
Leonardo de Moura
d055c4880f feat(frontends/lean): connect new elaborator to frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 08:31:00 -07:00
Leonardo de Moura
603dafbaf7 refactor(kernel): remove 'let'-expressions 
We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
      ((fun (x : t), b) v)
   We also use a macro (let-macro) to mark this pattern.
   Thus, the pretty-printer knows how to display it correctly.

2- Transparent 'let'-expressions are eagerly expanded by the parser.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 16:27:27 -07:00
Leonardo de Moura
aa8b5655dd feat(frontends/lean): add notation overwrite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 16:10:36 -07:00
Leonardo de Moura
5bd86754af feat(frontends/lean/builtin_cmds): change notation for marking implicit/cast parameter in sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 17:51:00 -07:00
Leonardo de Moura
2589d60bfd feat(frontends/lean): add nameless 'have' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 17:18:18 -07:00
Leonardo de Moura
4b227409bf feat(frontends/lean): add 'then have' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 14:27:21 -07:00
Leonardo de Moura
4560413a92 feat(frontends/lean): add '[fact]' modifier for 'have' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 11:58:05 -07:00
Leonardo de Moura
39177ec10a feat(frontends/lean): flip definition modifiers position, now they must occur after the identifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 11:58:05 -07:00
Leonardo de Moura
bdab979e09 feat(frontends/lean): add inductive_cmd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 16:00:59 -07:00
Leonardo de Moura
3bb53810c5 test(lean/run): add notation test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 09:48:47 -07:00
Leonardo de Moura
08845be2fc feat(frontends/lean/notation_cmd): improve 'notation' cmd 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 09:28:01 -07:00
Leonardo de Moura
3e3c4ee5ed feat(frontends/lean/parser): add local_scope object to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 08:38:23 -07:00
Leonardo de Moura
6259d20218 feat(frontends/lean/parser): expand Lua parser API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 08:03:17 -07:00
Leonardo de Moura
813e033f54 test(lean): add simple example of notation implemented using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 22:37:22 -07:00
Leonardo de Moura
4cbc429192 feat(frontends/lean/calc): add parse_calc function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 17:16:15 -07:00
Leonardo de Moura
e178979061 feat(frontends/lean): add calc_subst, calc_refl, calc_trans commands for configuring calc-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 13:35:31 -07:00
Leonardo de Moura
819c8276f2 feat(frontends/lean/builtin_cmds): add 'variables' command family 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-17 08:25:00 -07:00
Leonardo de Moura
ea49176043 feat(frontends/lean/builtin_cmds): add 'using' command, and 'hiding/renaming' directives 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 18:42:39 -07:00
Leonardo de Moura
639d58f4c7 feat(frontends/lean/builtin_cmds): add 'print options' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 17:31:28 -07:00
Leonardo de Moura
3e377a9732 feat(frontends/lean/builtin_cmds): add 'set_option' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 17:27:43 -07:00
Leonardo de Moura
4f3da90443 feat(frontends/lean/builtin_exprs): add 'have' and 'show' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 15:04:29 -07:00
Leonardo de Moura
873a5c8605 test(lean): add 'let' expression test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:11:26 -07:00
Leonardo de Moura
21c54755a9 fix(kernel/converter): bug in is_def_eq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:09:12 -07:00
Leonardo de Moura
f70b1b028a feat(frontends/lean): provide position to parse_fn external function, add 'by' expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 12:28:58 -07:00
Leonardo de Moura
34dfacc10e refactor(frontends/lean): Bool does not need to be a reserved keyword 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 10:52:12 -07:00
Leonardo de Moura
6db265e7ab feat(frontends/lean/builtin_exprs): parse '_' placeholder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 10:41:08 -07:00
Leonardo de Moura
5ce0502a36 feat(frontends/lean/builtin_exprs): add parser for 'let' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 09:50:34 -07:00
Leonardo de Moura
27130c9499 feat(frontends/lean): local notation 'shadows' global one 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 11:50:41 -07:00
Leonardo de Moura
28047a33ae feat(frontends/lean): add local notation support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 11:30:52 -07:00
Leonardo de Moura
64cafd6875 feat(frontends/lean/notation_cmd): add 'notation' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 10:49:05 -07:00
Leonardo de Moura
9b389a96d5 feat(frontends/lean/notation_cmd): modify infixl/infixr/postfix command syntax 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 08:28:49 -07:00
Leonardo de Moura
e7019ec840 feat(frontends/lean): add infixl/infixr/postfix/precedence commands, add support for storing notation in .olean files, add support for organizing notation into namespaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 22:13:25 -07:00
Leonardo de Moura
891a3fb48b feat(frontends/lean): add command block reader with snapshot and resume 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 14:13:32 -07:00
Leonardo de Moura
5fee6fd140 feat(shell/lean): add '-o' command line option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 08:10:43 -07:00
Leonardo de Moura
282a35bd1b feat(frontends/lean): add '#setline' directive 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 07:28:56 -07:00
Leonardo de Moura
fad4780d72 test(lean/run): add overload test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 18:06:44 -07:00
Leonardo de Moura
48c58af9b5 feat(frontends/lean/parser): allow explicit universe level to be provided to aliases and locals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 18:00:52 -07:00
Leonardo de Moura
a65c43c0db feat(frontends/lean/builtin_cmds): add definition command family 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 17:30:35 -07:00
Leonardo de Moura
01cecb76db feat(frontends/lean/builtin_cmds): add 'variable' command family 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 15:13:50 -07:00
Leonardo de Moura
ce259e6265 feat(frontends/lean/parser): add namespace/section/end commands, add support for explicit universe levels, fix Type notation' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 11:34:43 -07:00
Leonardo de Moura
3bde699fbe feat(frontends/lean/parser): add parse_level 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-12 12:34:55 -07:00
Leonardo de Moura
cffbae3667 test(tests/lean/run): add new test group, where we just execute Lean (and don't check output) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 21:07:23 -07:00
Leonardo de Moura
05edbe00ad chore(shell): re-activate .lean tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 14:36:42 -07:00
Leonardo de Moura
1972a09021 feat(frontends/lean/builtin_cmds): add simple 'print' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 14:35:34 -07:00
Leonardo de Moura
2e8ebb6d9e feat(frontends/lean/parser): add 'parse_commands' and 'parse_script' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 14:32:07 -07:00
Leonardo de Moura
3a0861bca7 test(lean): remove old test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 10:42:10 -07:00
Leonardo de Moura
9f06cd553e test(lean): remove tests using Lean old syntax and kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 10:38:53 -07:00
Leonardo de Moura
e9dada5e14 refactor(builtin/kernel): use standard definition for 'or' and 'and' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-17 12:05:34 -08:00
Leonardo de Moura
1739b5c153 fix(kernel/type_checker): caching bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 10:43:01 -08:00
Leonardo de Moura
368fcb5ff9 refactor(builtin/kernel): rename refute to by_contradiction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-12 08:49:19 -08:00
Leonardo de Moura
b7b868de85 fix(library/elaborator): bug reported by Jeremy Avigad 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-10 14:01:22 -08:00
Leonardo de Moura
a2d2e36f04 refactor(frontends/lean): remove notation for creating tuples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-10 09:03:42 -08:00
Leonardo de Moura
4317f67bd2 fix(builtin/tactic): more meaningful error message when skip tactic is used in a full proof 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 18:57:33 -08:00
Leonardo de Moura
c45c1748d8 refactor(builtin/kernel): reorder congr1 arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 16:15:44 -08:00
Leonardo de Moura
8df7c7b02d feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker 
We should not rely on this feature. It can be quite expensive.
We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as

   is_convertible(num, Nat)

If is_convertible starts unfolding opaque definitions, we would keep expanding num.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 11:31:24 -08:00
Leonardo de Moura
1ec01f5757 refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 16:04:44 -08:00
Leonardo de Moura
ad7b13104f feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 15:03:16 -08:00
Leonardo de Moura
d4b08fcf96 feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator 
Unification constraints of the form

         ctx |- ?m[inst:i v] == T

         and

         ctx |- (?m a1 ... an) == T

are delayed by elaborator because the produce case-splits.
On the other hand, the step that puts terms is head-normal form is eagerly applied.
This is a bad idea for constraints like the two above. The elaborator will put T in head normal form
before executing process_meta_app and process_meta_inst. This is just wasted work, and creates
fully unfolded terms for solvers and provers.

The new test demonstrates the problem. In this test, we mark several terms as non-opaque.
Without this commit, the produced goal is a huge term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 21:08:00 -08:00
Leonardo de Moura
593f1f2ebd fix(frontends/lean): allow user set constants defined in other namespaces as opaque 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 20:56:31 -08:00
Leonardo de Moura
363c4dc5c2 feat(library/elaborator): improve support for dependent pairs in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 20:56:31 -08:00
Leonardo de Moura
ea06bb2885 feat(frontends/lean/pp): change how lift local entries are pretty printed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 17:26:38 -08:00
Leonardo de Moura
a51139e63b feat(frontends/lean): position information in error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 17:26:38 -08:00
Leonardo de Moura
e4579b93e4 fix(library/elaborator): try first projection before imitation in the higher-order unifier 
Projections build more general solutions. This commit also adds a test that demonstrates the issue. Before this commit, the elaborator would produce the "constant" predicate (fun x, a + b = b + a).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 13:35:05 -08:00
Leonardo de Moura
ef321e730f feat(builtin/tactic): add the 'skip' (bogus) tactic for ignoring a proof hole in a big proof 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 12:47:23 -08:00
Leonardo de Moura
eab0456b27 test(tests/lean): test super opaque style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 11:33:27 -08:00
Leonardo de Moura
fdc4c9b53c test(tests/lean): add nested 'have' expression test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 08:13:04 -08:00
Leonardo de Moura
1d23d93e60 feat(frontends/lean): new 'have' expression 
Add 'have' notation suggested by Jeremy Avigad.
Add his example to the test suite.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 08:03:59 -08:00
Leonardo de Moura
ba9a8f9d98 feat(frontends/lean): add 'show' expression syntax sugar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 07:50:22 -08:00
Leonardo de Moura
419fb7464e fix(tests/lean): adjust tests to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-05 21:04:06 -08:00
Leonardo de Moura
aec9c84d0d fix(util/lua): deadlock 
Errors in the Lua library produce longjmps.
The longjmp will not unwind the C++ stack.
In the new test, the lock was not being released, and the system was deadlocking in the next call that tried to lock the environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 15:16:29 -08:00
Leonardo de Moura
f4ec874c6e refactor(builtin): remove dead module heq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 14:42:28 -08:00
Leonardo de Moura
0283887ee9 refactor(builtin/kernel): move the heq axioms into kernel.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 14:17:34 -08:00
Leonardo de Moura
f03c09c10b feat(library/elaborator): add support for proj/pair/sigma in the the higher-order unification procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 13:53:30 -08:00
Leonardo de Moura
413391b2b4 chore(tests/lean/sig2): remove unnecessary parenthesis from test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 11:37:08 -08:00
Leonardo de Moura
c9b72df34b fix(frontends/lean/parser): bug when applying tactics to synthesize remaining meta-variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 11:36:26 -08:00
Leonardo de Moura
96c9c7505a test(tests/lean): add another sigma-type test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 10:12:39 -08:00
Leonardo de Moura
9dc86e3cf5 fix(builtin/kernel): rename generalized proof_irrel axiom to hproof_irrel, and derive the restricted one 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 10:06:29 -08:00
Leonardo de Moura
4fcc292332 feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 22:10:01 -08:00
Leonardo de Moura
cc96b50644 feat(frontends/lean): support for nary-tuples, improve notation for non-dependent tuples, add support in the elaborator for sigma types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 20:53:11 -08:00
Leonardo de Moura
5c991f8fbf feat(frontends/lean): parse and pretty print tuples/pairs 
This commit also fixes a bug in the type checker when processing dependent pairs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 20:10:30 -08:00
Leonardo de Moura
640ebcc040 test(tests/lean/exp): add example for Steve 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 11:35:40 -08:00
Leonardo de Moura
e4afa3dc43 fix(tests/lean/map): incorrect output 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 00:05:19 -08:00
Leonardo de Moura
87f9c9b27e fix(tests/lean/map): make sure the unit test produce the same result in different platforms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 20:29:34 -08:00
Leonardo de Moura
e2add5c9f2 test(tests/lean): add heterogeneous equality simplification example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 20:27:39 -08:00
Leonardo de Moura
6be50f0133 refactor(builtin/heq): merge cast and heq modules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 15:01:48 -08:00
Leonardo de Moura
c56df132b8 refactor(kernel): remove semantic attachments from the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 14:48:27 -08:00
Leonardo de Moura
2b7bc7b673 test(tests/lean/exp): simulating HOL constructions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 17:59:57 -08:00
Leonardo de Moura
e3dc552c39 fix(library/simplifier): nontermination 
The example tests/lua/simp1.lua demonstrates the issue.
The higher-order matcher matches closed terms that are definitionally equal.
So, given a definition

    definition a := 1

it will match 'a' with '1' since they are definitionally equal.

Then, if we have a theorem

    theorem a_eq_1 : a = 1

as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a"

   a --> 1 --> 1 --> 1 ...

The first simplification is expected. The other ones are not.
The problem is that "1" is definitionally equal to "a", and they match.
The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side.

To avoid this loop, we test if the new expression is not equal to the previous one.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 15:55:21 -08:00
Leonardo de Moura
1d85267d26 fix(library/simplifier): assumptions/context may contain equations where the left-hand-side is a metavariable or semantic attachment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 15:38:22 -08:00
Leonardo de Moura
110ca84984 feat(library/simplifier): allow the user to associate a simplifier monitor with the lua_State object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 13:49:24 -08:00
Leonardo de Moura
759aa61f70 refactor(builtin/kernel): define if-then-else using Hilbert's operator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 19:28:42 -08:00
Leonardo de Moura
b45ab9dc30 feat(library/elaborator): use equality constraints instead of convertability constraints on definitions 
Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 14:13:21 -08:00
Leonardo de Moura
8c1f6b9055 fix(kernel/typechecker): allow elaborator to infer (Type U+1) 
In the new test elab8.lean, the parameter B is in (Type U+1).
Before, this commit, the type checker was forcing all metavariables that must be types to be <= (Type U). This restriction was preventing the elaborator from succeeding in reasonable cases.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 14:00:01 -08:00
Leonardo de Moura
41f5e2a067 feat(library/simplifier): statically check (conditional) equations (aka rewrite rules) to verify whether we can skip type checking when using them in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 18:32:40 -08:00
Leonardo de Moura
01259b1e84 feat(kernel): make sure U is the maximal universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 16:31:00 -08:00
Leonardo de Moura
ea6bf224e5 feat(frontends/lean): make the parser accept (Type -> ...) 
Before this commit, the parser would accept only a universe level or a ')' after '(' 'Type'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 15:23:20 -08:00
Leonardo de Moura
4f3127d3d5 fix(library/simplifier): check if the given types are convertible to ceq expected types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 15:15:55 -08:00
Leonardo de Moura
0bb8fe75b3 test(tests/lean): new simplifier test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 14:21:18 -08:00
Leonardo de Moura
a19f9d4846 feat(library/simplifier): discard conditional equations that are clearly non-terminating 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 13:56:45 -08:00
Leonardo de Moura
4dc3aa46c3 feat(frontends/lean): allow tactics to be used in axiom/variable declarations and in the type of definitions/theorems; add a new test showing the need for this feature 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 12:02:12 -08:00
Leonardo de Moura
069e5edf6b fix(library/simplifier): include flag indicating if the proof generated by simplifier is a homogenous or heterogenous equality, use flag to fix bug in the simp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 12:01:01 -08:00
Leonardo de Moura
62408a6adc test(tests/lean): move simp_loop test to slow subdirectory 
This example produces a stackoverflow on Valgrind.
We don't execute Valgrind on tests in the slow subdirectory.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 10:32:48 -08:00
Leonardo de Moura
ee4344076e feat(library/simplifier): improve error message when simplifier is looping 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 19:36:31 -08:00
Leonardo de Moura
72c607846a test(tests/lean): add Jeremy's proof to test suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 16:05:46 -08:00
Leonardo de Moura
7f53cb9601 feat(frontends/lean/parser): add_rewrite take the 'using' command into account 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 01:15:28 -08:00
Leonardo de Moura
b31ef34787 feat(library/simplifier): preserve binder names when applying higher-order rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:50:27 -08:00
Leonardo de Moura
6da1b447f0 fix(library/hop_match): do not match iff with = 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:21:05 -08:00
Leonardo de Moura
db45d02078 fix(tests/lean): test discrepancy on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 23:31:35 -08:00
Leonardo de Moura
7b88d68afb test(tests/lean): add test using simplifier monitor for tracking failures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 15:11:16 -08:00
Leonardo de Moura
8bccfb947a feat(library/simplifier): expose simplier and simplifier_monitor objects in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 15:02:05 -08:00
Leonardo de Moura
b26035fcf6 feat(kernel/type_checker): improve application type mismatch error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 09:45:17 -08:00
Leonardo de Moura
4d25cb7f47 feat(library/tactic): add simplify_tactic based on the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 18:53:18 -08:00
Leonardo de Moura
844572c382 feat(library/simplifier): support for dependent simplification in Pi/forall expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 00:32:05 -08:00
Leonardo de Moura
e8bba1ebf3 fix(frontends/lean/frontend): the definition of the explicit version @f must be definitionally equal to f 
Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f.

For example, if we had

variable f {A : Type} : A -> Bool

Then, the definition of @f was

definition @f (A : Type) (a : A) : Bool := f A a

This definition is equivalent to
     fun A a, f A a
which is not definitionally equal to
     f
since definitionally equality in Lean ignores Eta conversion.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 20:34:28 -08:00
Leonardo de Moura
9fb3ccb4c0 feat(library/simplifier): support for dependent simplification in lambda expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 16:54:42 -08:00
Leonardo de Moura
5b13ef1b90 test(tests/lean): new simplifier test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 10:56:49 -08:00
Leonardo de Moura
7015089734 fix(library/simplifier): move to locally nameless approach in the simplifier. Contextual simplification may add rewriting rules with free variables, and it is a mess to manage them when using de Bruijn indices 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 10:49:44 -08:00
Leonardo de Moura
7a4eb4b8ed feat(library/simplifier): contextual simplification for A -> B 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 22:32:55 -08:00
Leonardo de Moura
c2381e43f1 fix(library/simplifier): bug in cast elimination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 21:25:09 -08:00
Leonardo de Moura
35ad156a46 fix(tests/lean): make sure pretty print and parse test passes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:23:55 -08:00
Leonardo de Moura
8f455f5965 fix(frontends/lean): bug in scope construct 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:23:29 -08:00
Leonardo de Moura
7f3e2b3ef4 fix(frontends/lean/parser): bug in 'using' construct 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
8e0888828d fix(library/simplifier): missing check in mk_hcongr_th 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
1a3660180e test(tests/lean): add new simplifier test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
26bea77721 fix(library/simplifier): bug in heterogeneous equality support, and universe commutativity support in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:46 -08:00
Leonardo de Moura
dbc100cc2e feat(library/simplifier): cast elimination in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 17:28:14 -08:00
Leonardo de Moura
cd87cb3de4 test(tests/lean): add test for congruence theorem that uses an argument before simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 13:26:09 -08:00
Leonardo de Moura
180be5c4a2 feat(library/simplifier): improve contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 13:11:58 -08:00
Leonardo de Moura
5ba2525eab test(tests/lean): add test disabling contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 12:57:05 -08:00
Leonardo de Moura
33193e1ab3 feat(library/simplifier): improve contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 12:54:29 -08:00
Leonardo de Moura
d6692264e8 feat(library/simplifier): contextual simplifications 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-23 12:23:22 -08:00
Leonardo de Moura
1638a7bb02 fix(frontends/lean/pp): compute local shared nodes, and avoid unnecessary let's 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-22 21:44:24 -08:00
Leonardo de Moura
17cce340f6 fix(library/elaborator): in optimization for metavariable free terms 
The optimization was incorrect if the term indirectly contained a metavariable.
It could happen if the term contained a free variable that was assigned in the context to a term containing a metavariable.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-22 18:06:00 -08:00
Leonardo de Moura
8214c7add4 feat(library/elaborator): compensate the lack of eta-reduction (and eta-expanded normal forms) in the kernel normalizer 
Before this commit, the elaborator was solving constraints of the form

       ctx |- (?m x) == (f x)
as
       ?m <- (fun x : A, f x)    where A is the domain of f.

In our kernel, the terms f and (fun x, f x) are not definitionally equal.
So, the solution above is not the only one. Another possible solution is

       ?m  <- f

Depending of the circumstances we want  ?m <- (fun x : A, f x) OR ?m <- f.
For example, when Lean is elaborating the eta-theorem in kernel.lean, the first solution should be used:
       ?m <- (fun x : A, f x)

When we are elaborating the axiom_of_choice theorem, we need to use the second one:
       ?m <- f

Of course, we can always provide the parameters explicitly and bypass the elaborator.
However, this goes against the idea that the elaborator can do mechanical steps for us.

This commit addresses this issue by creating a case-split
       ?m <- (fun x : A, f x)
       OR
       ?m <- f

Another solution is to implement eta-expanded normal forms in the Kernel.

With this change, we were able to cleanup the following "hacks" in kernel.lean:
     @eps_ax A (nonempty_ex_intro H) P w Hw
     @axiom_of_choice A B P H
where we had to explicitly provided the implicit arguments

This commit also improves the imitation step for Pi-terms that are actually arrows.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-22 13:28:54 -08:00
Leonardo de Moura
331b5846c6 test(library/simplifier): add test for the single_pass option in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-21 13:47:54 -08:00
Leonardo de Moura
ead54bbf57 feat(library/simplifier): enforce max_steps option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-21 12:12:17 -08:00
Leonardo de Moura
1ccfac5873 feat(library/simplifier): conditional rewriting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 21:15:46 -08:00
Leonardo de Moura
cd19d4da01 feat(library/simplifier): memoize intermediate results 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 17:03:44 -08:00
Leonardo de Moura
97ead50a3e feat(builtin/Nat): flip orientation of associativity axioms for + and * 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 15:38:00 -08:00
Leonardo de Moura
d1bd56b3d3 fix(tests/lean): adjust test to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 14:47:03 -08:00
Leonardo de Moura
ad219d43d9 refactor(*): semantic attachment parsing and simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 14:44:45 -08:00
Leonardo de Moura
5224df56a3 test(tests/lean): add example showing how to 'sort' argumentes of AC operators using the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 08:36:48 -08:00
Leonardo de Moura
913d893204 feat(library/simplifier): add support for 'permutation' rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-20 08:29:31 -08:00
Leonardo de Moura
69d7ee316f feat(library/simplifier): improve simplification by evaluation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 23:26:34 -08:00
Leonardo de Moura
bcede6925f fix(tests/lean): add expected result file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-19 16:31:35 -08:00