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

1684 commits

Author SHA1 Message Date
Leonardo de Moura
750f6d5a43 feat(library,frontends/lean): validate user defined recursors and add attribute to mark them 
see issue #492

The user-defined recursors will also be used to implement the blast tactic
 2015-05-12 15:48:01 -07:00
Leonardo de Moura
fa70930ef4 feat(library/blast): add union-find datastructure 2015-05-11 16:19:51 -07:00
Leonardo de Moura
9649d540c0 fix(library/tactic/rewrite_tactic.cpp): memory leak 2015-05-11 16:19:17 -07:00
Leonardo de Moura
c5fb3ec6d0 fix(library/definitional/equations): fixes #541 
This commit allows recursive applications to have less or more arguments
than the equation left-hand-side.
We add two tests
   - 541a.lean  recursive call with more arguments
   - 542b.lean  recursive call with less arguments
 2015-05-10 20:37:44 -07:00
Leonardo de Moura
207e8e86da fix(library/definitional/equations): do not clear eliminated hypotheses when invoking 'cases' tactic from definitional package 2015-05-10 11:08:02 -07:00
Leonardo de Moura
bd28396be0 feat(kernel): transparent theorems 
closes #576
 2015-05-09 11:42:29 -07:00
Leonardo de Moura
f8e2f68ce0 feat(frontends/lean): add 'wait' command 
This commit also fixes several problems with -j option (parallel
compilation). The .olean files were not missing data when -j was used

see issue #576
 2015-05-08 20:05:21 -07:00
Leonardo de Moura
cf7e60e5a6 refactor(kernel): remove "opaque" field from kernel declarations 
see issue #576
 2015-05-08 16:06:16 -07:00
Leonardo de Moura
6c958a25e7 refactor(library/tactic/expr_to_tactic): make sure builtin tactics don't need to be marked opaque 
This modification is needed since we will remove opaque definitions from
the kernel.

see issue #576
 2015-05-08 16:06:16 -07:00
Leonardo de Moura
57ea660963 refactor(*): start process for eliminating of opaque definitions from the kernel 
see issue #576
 2015-05-08 16:06:04 -07:00
Leonardo de Moura
061e26157e fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking 2015-05-08 12:41:23 -07:00
Leonardo de Moura
72663e8a06 feat(library/tactic/rewrite_tactic): take hypotheses into account when checking rewrite step 2015-05-08 11:34:50 -07:00
Leonardo de Moura
12bad8794b feat(frontends/lean/pp): use 'assert' instead of 'have ... [visible]' 2015-05-08 10:02:15 -07:00
Leonardo de Moura
0b57f7d00a refactor(library/tactic): refine interface between tactic and proof-term modes 
Some constraints were being lost with the previous interface.
This is why we had a workaround in fintype.lean.

We can also remove some hacks we have used in the past.
 2015-05-07 18:02:51 -07:00
Leonardo de Moura
12b818b7d3 fix(library/util): "empty" is not universe polymorphic anymore 2015-05-07 16:43:58 -07:00
Leonardo de Moura
eb3a236119 fix(library/unifier): typo 
fixes #588
 2015-05-07 16:30:02 -07:00
Leonardo de Moura
88cd6e9a63 chore(library/unifier): remove dead code 2015-05-07 15:49:33 -07:00
Leonardo de Moura
aff9257c72 feat(frontends/lean): allow → to be used in calc proofs 
see issue #586
 2015-05-07 12:28:47 -07:00
Leonardo de Moura
b03266be70 feat(library/normalize,frontends/lean): rename '[unfold-m]' hint to '[constructor]', and allow it to be attached to constants 
closes #587
 2015-05-07 12:00:34 -07:00
Leonardo de Moura
ac24f19210 fix(library/tactic/rewrite_tactic): use relaxed type checker when processing rewrite "proof step" 
That is, the restricted type checker should only be used in the
matching/unification step.

fixes #583
 2015-05-07 09:57:23 -07:00
Leonardo de Moura
e0b7017435 feat(frontends/lean): make sure the proof state bit "report errors" is 
set in the beginning of each begin-end element

see discussion at #583
 2015-05-07 09:43:39 -07:00
Leonardo de Moura
e841852be4 feat(library/max_sharing): maximize sharing in universe level expressions 2015-05-06 14:26:12 -07:00
Leonardo de Moura
210cae7d6c fix(library/tactic): we must unfold untrusted macros when type checking intermediate results 
Example: before this commit, the file librata/data/list/perm.lean would
not type check if the option -t 0 (trust level zero) was provided.
Reason: the intermediate term contained a macro, and macros are not
allowed at trust level zero.
 2015-05-06 14:23:58 -07:00
Leonardo de Moura
b5619c2109 fix(library/export): remove workaround from 'export' procedure 
The workaround was needed due to a bug in the max_sharing procedure
 2015-05-06 14:00:57 -07:00
Leonardo de Moura
2ca16a099b fix(library/max_sharing): conflict with the kernel approximate caching 2015-05-06 13:57:36 -07:00
Leonardo de Moura
84deddcca9 feat(library/tactic/rewrite_tactic): apply 'reflexivity' tactic after 'rewrite' instead of hard coded solution 2015-05-05 20:23:49 -07:00
Leonardo de Moura
c7a20644c0 fix(library/tactic/rewrite_tactic): bug in rewrite tactic (HoTT mode) 
closes #580
 2015-05-05 19:25:15 -07:00
Leonardo de Moura
a4efefb6ff feat(library/tactic/rewrite_tactic): display type error message when 
rewrite tactic fails
 2015-05-05 19:23:41 -07:00
Leonardo de Moura
616f49c2e4 feat(frontends/lean): improved 'obtains' expression 2015-05-05 18:30:16 -07:00
Leonardo de Moura
c0c0490db3 feat(library/export): simplify format 2015-05-04 18:22:12 -07:00
Leonardo de Moura
701b0ae66f feat(library): export environment in textual format 
closes #577
 2015-05-04 18:05:00 -07:00
Leonardo de Moura
6571c47353 feat(library/normalize): add '[unfold-m]' hint 
See issue #496
 2015-05-04 14:23:04 -07:00
Leonardo de Moura
3c8c75470f fix(library/tactic/exact_tactic): do not report unassigned metavariables in the 'refine' tactic 2015-05-03 21:08:09 -07:00
Leonardo de Moura
326048df54 feat(library/tactic/inversion_tactic): clear variables that have been eliminated by cases tactic 
see discussion at:
https://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc
 2015-05-02 19:33:59 -07:00
Leonardo de Moura
e1dc18f6b6 fix(library/tactic/inversion_tactic): check whether eliminator can only eliminate to Prop 
fixes #571
 2015-05-02 17:48:08 -07:00
Leonardo de Moura
e379034b95 feat(library/tactic): improve 'assumption' tactic 
- It uses the unifier in "conservative" mode
- It only affects the current goal

closes #570
 2015-05-02 17:33:54 -07:00
Leonardo de Moura
b39fe17dee feat(library/tactic): add 'transitiviy', 'reflexivity' and 'symmetry' tactics 
closes #500
 2015-05-02 15:48:25 -07:00
Leonardo de Moura
cd17618f4a refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]' 
These attributes are used by the calc command.
They will also be used by tactics such as 'reflexivity', 'symmetry' and
'transitivity'.

See issue #500
 2015-05-02 15:15:35 -07:00
Leonardo de Moura
415ca2b93f feat(library/tactic): add 'congruence' tactic 
It is the f_equal described at issue #500.
 2015-05-02 12:58:46 -07:00
Leonardo de Moura
2054d67483 chore(library/tactic/rewrite_tactic): fix style 2015-05-01 19:49:48 -07:00
Leonardo de Moura
9dc0388022 fix(library/tactic/rewrite_tactic): bug when rewriting hypotheses 2015-05-01 19:45:23 -07:00
Leonardo de Moura
ac8ba6a3cf feat(library/tactic): add 'subst' tactic 
see issue #500
 2015-05-01 19:31:24 -07:00
Leonardo de Moura
b0759f3986 fix(library/tactic/rewrite_tactic): bug when rewriting multiple hypotheses 2015-05-01 19:03:43 -07:00
Leonardo de Moura
de369a0a0a feat(library/tactic/injection_tactic): improve 'injection' tactic 
see issue #500
 2015-05-01 15:49:56 -07:00
Leonardo de Moura
9ba8b284a1 fix(library/tactic/apply_tactic): add eapply, and fix issue #361 2015-05-01 15:08:00 -07:00
Leonardo de Moura
63eb155c7e feat(library/tactic): add 'injection' tactic 
see issue #500
 2015-05-01 12:45:21 -07:00
Leonardo de Moura
7e9f574ef3 fix(library/tactic/apply_tactic): use internally 'apply' instead of 'fapply' as the default "apply" tactic 
This changes improves the 'constructor' tactic
 2015-04-30 21:58:35 -07:00
Leonardo de Moura
2d9c950144 feat(library/tactic/constructor_tactic): allow 'constructor' tactic without index 
see issue #500
 2015-04-30 21:15:07 -07:00
Leonardo de Moura
15e52b06df fix(library/tactic/constructor_tactic): bug in constructor tactic 
see example (constr_tac2.lean) in comment at issue #500
 2015-04-30 20:18:24 -07:00
Leonardo de Moura
d18f9c7607 fix(library/tactic/constructor_tactic): use 1 (instead of 0) to reference the first constructor 
see comment at issue #500
 2015-04-30 20:08:00 -07:00
Leonardo de Moura
0b995c4fe3 fix(library/tactic/rewrite_tactic): relax reducibility constraints in some parts of the rewrite tactic 
fixes #567
 2015-04-30 18:22:58 -07:00
Leonardo de Moura
d152f38518 feat(library/tactic): add 'constructor', 'split', 'left', 'right' and 'existsi' tactics 
see issue #500
 2015-04-30 17:52:29 -07:00
Leonardo de Moura
1c6067bac2 feat(library/tactic): add 'exfalso' tactic 
see issue #500
 2015-04-30 15:43:07 -07:00
Leonardo de Moura
d546b019fb fix(library/tactic/rewrite_tactic): assertion violation when checking 
dependencies at rewrite tactic
 2015-04-30 15:41:57 -07:00
Leonardo de Moura
936e024128 fix(library/tactic/rewrite_tactic): bug in rewrite hypothesis in HoTT mode 2015-04-30 15:30:25 -07:00
Leonardo de Moura
9c8a63caec feat(library/tactic): add 'contradiction' tactic 
see issue #500

Remark: this tactic also applies no_confusion to take care of a contradiction
 2015-04-30 13:47:40 -07:00
Leonardo de Moura
3233008039 feat(library/tactic): allow user to name generalized term in the 'generalize' tactic 
closes #421
 2015-04-30 11:57:40 -07:00
Leonardo de Moura
3912bc24c8 feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears' 2015-04-30 11:00:39 -07:00
Leonardo de Moura
dce7177382 feat(library/tactic/change_tactic): improve 'change' tactic 
- Better error messages
- Try to solve unification constraints produced during is_def_eq test

addresses comment on issue #531
 2015-04-29 13:31:09 -07:00
Leonardo de Moura
d055947243 feat(library/tactic/rewrite_tactic): ignore implicit argument when matching at rewrite tactic 2015-04-29 12:51:33 -07:00
Leonardo de Moura
182a8a542e feat(library/tactic/rewrite_tactic): store exception "what" message in rewrite trace 2015-04-29 12:46:41 -07:00
Leonardo de Moura
b790ca9806 fix(library/tactic/rewrite_tactic): type check rewriting steps 
closes #550
 2015-04-29 12:16:37 -07:00
Leonardo de Moura
91abba3c3d refactor(kernel): rename method 2015-04-29 11:46:27 -07:00
Leonardo de Moura
d2c7b5c319 feat(library/tactic): add 'let' tactic 
closes #555
 2015-04-28 17:24:43 -07:00
Leonardo de Moura
ca8943f45b feat(library,hott): remove rapply tactic 2015-04-27 15:06:16 -07:00
Leonardo de Moura
9d01868361 feat(frontends/lean): use rewrite tactic to implement unfold (it has a unfold step) 
closes #502
 2015-04-24 17:23:12 -07:00
Leonardo de Moura
28404fe16d fix(library/tactic/rewrite_tactic): second problem reported at issue #548 
closes #548
 2015-04-24 16:49:32 -07:00
Leonardo de Moura
4148d6b8cc fix(library/tactic/rewrite_tactic): first two problems at issue #548 2015-04-24 16:07:00 -07:00
Leonardo de Moura
8241863abe feat(kernel/hits): add two builtin HITs: type_quotient and trunc 2015-04-23 15:32:31 -07:00
Leonardo de Moura
2613e7c444 fix(frontends/lean): bug when handling identifiers in tactics 
This bug was reported by Jeremy in the Lean Google group:
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/ZKJ8WPPEVJA/n05x6rPRzvMJ
 2015-04-22 16:03:22 -07:00
Leonardo de Moura
91f21c007a feat(frontends/lean): remove 'context' command 2015-04-22 11:32:02 -07:00
Leonardo de Moura
bf8a7eb9b4 fix(library/scoped_ext): bug in local metadata in sections 
The problem is described in issue #554
 2015-04-21 18:56:28 -07:00
Leonardo de Moura
697a536d9e fix(library/tactic/inversion_tactic): type incorrect term being built by 'cases' tactic 
fixes #545
 2015-04-20 19:24:52 -07:00
Leonardo de Moura
eb23a30626 feat(library/unifier): additional memory checks 2015-04-20 17:41:08 -07:00
Leonardo de Moura
28dad944c5 fix(library/unifier): cyclic assignment (?M <- ?M) 
This was producing nonterminating behavior on example described at issue #489
 2015-04-20 17:35:37 -07:00
Leonardo de Moura
431eade894 fix(library/tactic/inversion_tactic): incorrect use of optimization 2015-04-20 16:21:44 -07:00
Leonardo de Moura
6f6d106a10 feat(library/tactic): add "check_expr" tactic 
closes #486
 2015-04-19 19:00:05 -07:00
Leonardo de Moura
b7ca2a0ec9 fix(library/tactic/exact_tactic): exact and or_else 
fixes #543
 2015-04-19 17:23:09 -07:00
Leonardo de Moura
5d95cb0979 feat(library/tactic): add 'refine' tactic 
closes #482
 2015-04-06 18:36:56 -07:00
Leonardo de Moura
412f03b08b feat(library/tactic/exact_tactic): generate error if 'exact' tactic produces a term containing metavariables 2015-04-06 13:38:53 -07:00
Leonardo de Moura
2bc13f6bfd feat(library/tactic/exact): enforce goal type during elaboration when executing 'exact' tactic 
Remark: this was the behavior of the 'sexact' tactic.

This commit also adds the 'rexact' (relaxed exact) tactic which does not
enforce the goal type.

closes #495
 2015-04-06 13:23:38 -07:00
Leonardo de Moura
969d17fd12 fix(frontends/lean/elaborator): class inference in tactic mode with trunc 
closes #477
 2015-04-05 17:47:14 -07:00
Leonardo de Moura
d731a4ab13 feat(library/normalize): add '[unfold-f]' hint 
closes #497
 2015-04-05 03:00:13 -07:00
Leonardo de Moura
4ec0e1b07c feat(frontends/lean): improve calc mode 
Now, it automatically supports transitivity of the form
    (R a b) -> (b = c) -> R a c
    (a = b) -> (R b c) -> R a c

closes #507
 2015-04-04 08:58:35 -07:00
Leonardo de Moura
b960e123b1 feat(kernel): add experimental support for quotient types 2015-03-31 22:04:16 -07:00
Leonardo de Moura
26c914173c feat(frontends/lean): add --profile option 2015-03-31 11:53:55 -07:00
Leonardo de Moura
ea3407d06d fix(library/tactic): valgrind warnings for still reachable memory 2015-03-28 12:32:57 -07:00
Leonardo de Moura
1b15036dba feat(library/definitional): automatically add attribute [unfold-c] to cases_on, brec_on and rec_on 
see #496
 2015-03-27 19:12:17 -07:00
Leonardo de Moura
b9e3c474c9 feat(library/tactic): add all_goals tactic 
closes #501
 2015-03-25 17:42:34 -07:00
Leonardo de Moura
49bc56ec07 feat(frontends/lean/pp): improve pretty printer for prefix and postfix notation 
closes #491
 2015-03-25 16:45:58 -07:00
Leonardo de Moura
38a63a8a58 fix(library/tactic/exact_tactic): segfault when accessing head of empty list 
closes #485
 2015-03-23 19:00:01 -07:00
Leonardo de Moura
ac30052a29 fix(library/tactic/rewrite_tactic): apply substitution before trying to rewrite 
closes #487
 2015-03-23 18:32:52 -07:00
Leonardo de Moura
5bf46d1226 fix(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT mode 
closes #481
 2015-03-23 18:06:11 -07:00
Leonardo de Moura
98cc325695 refactor(library/tactic/inversion_tactic): cleanup 2015-03-23 17:15:47 -07:00
Leonardo de Moura
0814e76298 fix(library/tactic/clear_tactic): unexpected failure 
This commit also improves the error message produced by the 'clear' tactic.

fixes #488
 2015-03-23 12:08:15 -07:00
Leonardo de Moura
f6f2c499ae fix(library/tactic/rewrite_tactic): rewrite macros did not implement operator== 
This problem was affecting the cache
 2015-03-13 19:24:09 -07:00
Leonardo de Moura
cfeb426cd7 fix(frontends/lean): pretty print numeral notation from algebra 2015-03-13 18:58:34 -07:00
Leonardo de Moura
aba158dbd4 feat(library/tactic/inversion_tactic): improve error message for unknown hypothesis 2015-03-13 15:19:19 -07:00
Leonardo de Moura
cda19f5aa6 feat(library/tactic/rewrite_tactic): improve rewrite tactic error messages 
closes #471
 2015-03-12 20:49:53 -07:00
Leonardo de Moura
7accd0f1e6 feat(library/tactic/rewrite_tactic): allow rewrite with terms that contains binders 
see discussion at #470
 2015-03-12 18:07:55 -07:00
Leonardo de Moura
9fe2d5c74c refactor(library/unifier): use new assign method in the unifier 2015-03-12 15:01:40 -07:00
Leonardo de Moura
4ea323a2b2 refactor(library/tactic): cleanup common pattern 2015-03-12 14:52:41 -07:00
Leonardo de Moura
8f004671a2 fix(library/unifier): typo 2015-03-12 13:15:23 -07:00
Leonardo de Moura
3e4d849a4a refactor(kernel/metavar.h): simplify API 2015-03-12 12:50:53 -07:00
Leonardo de Moura
6a78ae7b46 fix(library/tactic/class_instance_synth): enforce consistent behavior in type class resolution 
Auxiliary procedure mk_class_instance was not discarding partial solutions.
This procedure is used by the apply and inversion (aka cases) tactics
 2015-03-12 10:27:05 -07:00
Leonardo de Moura
b38c943086 fix(library/tactic/class_instance_synth): discard partial solutions even when option class.unique_instances = true is used 2015-03-12 10:13:16 -07:00
Leonardo de Moura
47a350d888 fix(library/tactic/inversion_tactic): missing condition for applying optimization 2015-03-12 09:11:36 -07:00
Leonardo de Moura
7de3d5771d feat(library/tactic/rewrite_tactic): add eta-reduction support at esimp 
closes #469
 2015-03-12 00:32:31 -07:00
Leonardo de Moura
a9fa0fead9 feat(library/match): match modulo eta 2015-03-12 00:30:44 -07:00
Leonardo de Moura
a7af8e7c71 feat(library/tactic/inversion_tactic): remove dummy hypotheses of the form (H : a = a) 
closes #468
 2015-03-11 20:50:06 -07:00
Leonardo de Moura
b5fb7c734e feat(library/tactic/inversion_tactic): remove hypothesis being destructed 
addresses second issue in #468
 2015-03-11 20:42:50 -07:00
Leonardo de Moura
0a5340aa22 feat(library/tactic/goal): add auxiliary method 2015-03-11 20:39:41 -07:00
Leonardo de Moura
ebdda67812 fix(library/tactic/inversion_tactic.cpp): remove unnecessary hypothesis in HoTT mode 
partial solution for #468
 2015-03-11 19:30:34 -07:00
Leonardo de Moura
737faecc65 feat(library/tactic/inversion_tactic): fail if is_hset type class synthesis produced term containing meta-variables, improve error messages 
fixes #467
 2015-03-11 15:54:50 -07:00
Leonardo de Moura
4c6b0dc0e5 fix(library/tactic/expr_to_tactic): tactic_expr_to_id did not take as_atomic annotation into account 
fixes #466
 2015-03-11 08:49:59 -07:00
Leonardo de Moura
1244f01518 chore(library/unifier): remove dead code 2015-03-09 14:07:14 -07:00
Leonardo de Moura
9a6c675908 feat(library/unifier): add option to disable nonchronological backtracking 2015-03-09 12:08:58 -07:00
Leonardo de Moura
1490bdad49 feat(frontends/lean): add version of 'exact' tactic (sexact) that enforces goal type during term elaboration 2015-03-06 17:34:45 -08:00
Leonardo de Moura
4edd7b9099 fix(library/definitional/equations): allow a function to be the result of a match-with term or recursive definition 2015-03-06 15:08:52 -08:00
Leonardo de Moura
368f9d347e refactor(frontends/lean): approach used to parse tactics 
The previous approach was too fragile

TODO: we should add separate parsing tables for tactics
 2015-03-05 18:11:21 -08:00
Leonardo de Moura
039afb4578 feat(frontends/lean): treat "proof t qed" as alias for "by exact t" 2015-03-05 11:12:39 -08:00
Leonardo de Moura
bd0f209659 feat(library/tactic/exact_tactic): do not force 'exact' tactic expression to be fully elaborated (i.e., metavariable free) 2015-03-05 11:12:39 -08:00
Leonardo de Moura
8295ef4e57 fix(library/tactic/class_instance_synth): constraint execution order at type class resolution 
We could not fix this problem before because we did not have the
[quasireducible] annotation.

Without this annotation, the fixed TC would loop in some HoTT files.
 2015-03-04 22:20:20 -08:00
Leonardo de Moura
abd238aef0 feat(*): add [quasireducible] attribute 2015-03-04 22:12:49 -08:00
Leonardo de Moura
51504a1872 feat(library/tactic/class_instance_synth): restrict higher-order unification even more during type class resolution 2015-03-03 20:26:49 -08:00
Leonardo de Moura
7db6ed7c14 refactor(library/unifier): move m_pattern configuration option to unifier_config 2015-03-03 20:24:18 -08:00
Leonardo de Moura
341a9a2010 refactor(library/unifier): remove dead code 2015-03-03 20:14:17 -08:00
Leonardo de Moura
fa79b214b8 fix(frontends/lean): allow 'attribute <id> [priority ...]' 2015-03-03 16:17:32 -08:00
Leonardo de Moura
11aad4449b feat(frontends/lean): add '[semireducible]' attribute 
This commit also renames the elements of reducible_status.
The idea is to use in the C++ implementation the same names used in the
Lean front-end.
 2015-03-03 10:48:36 -08:00
Leonardo de Moura
7e2f0f9a36 fix(library/unifier): in the context_check, we should not consider local constants that occur in the type of other constants 
This was a performance bug.
We were missing higher-order pattern constraints due to this bug.
 2015-03-02 17:28:56 -08:00
Leonardo de Moura
fdb169b8f3 feat(library/tactic): improve error localization when compiling tactics 2015-03-02 12:21:02 -08:00
Leonardo de Moura
ededf4fc6c feat(frontends/lean): remove unnecessary instantiate_all's that were messing with error localization 2015-03-01 14:51:44 -08:00
Leonardo de Moura
ca57b43698 feat(library/tactic): add 'change' tactic 2015-03-01 14:15:39 -08:00
Leonardo de Moura
e07c6675b3 feat(library/tactic/elaborate): better error message for tactics using elaborate_with_respect_to 2015-03-01 13:42:53 -08:00
Leonardo de Moura
cf56935b01 feat(frontends/lean): improve support for user defined tactics 2015-02-27 16:58:25 -08:00
Leonardo de Moura
7d827a14c9 feat(library/module): expand 'failed to import' error message 
see issue #448
 2015-02-27 08:00:30 -08:00
Leonardo de Moura
5b736a2268 feat(frontends/lean): add support for empty match-with expressions 2015-02-26 16:36:15 -08:00
Leonardo de Moura
72eed42ac8 feat(library/unifier): ignore irrelevant branches when solving flex-rigid constraints 2015-02-26 13:43:54 -08:00
Leonardo de Moura
96b54a8007 feat(frontends/lean/builtin_exprs): add 'have' notation in 'begin-end' blocks 
It is notation for the assert tactic.
 2015-02-25 14:04:17 -08:00
Leonardo de Moura
425aba9aa9 feat(library/pp_options): reduce default limits in the pretty printer 
The goal is to avoid problems like the one described in issue #428
 2015-02-25 14:04:17 -08:00
Leonardo de Moura
42289d4334 feat(library/tactic/class_instance_synth): create class instance synthesis subproblems only for arguments marked with the [] binder annotation 2015-02-24 16:12:39 -08:00
Leonardo de Moura
1cd44e894b feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible 
closes #442
 2015-02-24 16:12:35 -08:00
Leonardo de Moura
4364b7f926 feat(frontends/lean): pp.beta is true by default 
Remark: there is one exception (command: print definition). For this
command pp.beta is still false.
 2015-02-24 12:27:53 -08:00
Leonardo de Moura
dc2ac92846 fix(library/definitional/equations): use whnf on recursive definition arguments 
The idea is to expose "hidden" datatypes.
 2015-02-23 22:27:30 -08:00
Leonardo de Moura
787fed95aa fix(library/tactic/inversion_tactic): bug in simpler case (hypotheses were being lost) 2015-02-23 16:10:49 -08:00
Leonardo de Moura
7d35d18cad fix(library/tactic/rewrite_tactic): bug when matching terms that expanded into projections 2015-02-22 18:23:10 -08:00
Leonardo de Moura
af787d9b7f fix(library/constants): regenerate constants.cpp and fix affected files 2015-02-22 09:22:51 -08:00
Floris van Doorn
61901cff81 feat(hott): rename definition and cleanup in HoTT library 
also add more definitions in types.pi, types.path, algebra.precategory

the (pre)category library still needs cleanup
authors of this commit: @avigad, @javra, @fpvandoorn
 2015-02-20 21:40:42 -05:00
Leonardo de Moura
7fc216183e feat(library/tactic): produce better error message when a tactic fails 
closes #348
 2015-02-16 18:42:15 -08:00
Leonardo de Moura
3a67ddb7c5 feat(library/locals): use optional<expr> instead of bool at depends_on (for arrays) 2015-02-16 18:42:05 -08:00
Leonardo de Moura
5cbdd77ad0 feat(library/tactic/rewrite_tactic): improve matcher in rewrite_tactic 
closes #433
 2015-02-13 12:40:55 -08:00
Leonardo de Moura
98960cbeda fix(library/tactic/rewrite_tactic): bug in HoTT mode 2015-02-13 10:09:18 -08:00
Leonardo de Moura
eceed03044 feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command 2015-02-11 11:02:59 -08:00
Leonardo de Moura
1832fb6f54 feat(*): uniform metaclass names, metaclass validation at 'open' command 2015-02-11 10:35:04 -08:00
Leonardo de Moura
2cbaf1bbe3 feat(library/scoped_ext): add get_metaclasses API 2015-02-11 10:12:28 -08:00
Leonardo de Moura
9398b887cc fix(library/abbreviation): missing condition 2015-02-10 18:34:45 -08:00
Leonardo de Moura
bd304e1911 chore(*): style 2015-02-10 18:31:17 -08:00
Leonardo de Moura
43f849bf95 feat(frontends/lean/pp): add support for abbreviations in the pretty printer 
closes #365
 2015-02-10 18:27:02 -08:00
Leonardo de Moura
13748b9347 feat(library/abbreviation): simplify expand_abbreviations 2015-02-10 18:26:39 -08:00
Leonardo de Moura
f47e1bed01 feat(library/abbreviation): store inverse map ignoring universe level parameters 2015-02-10 18:21:32 -08:00
Leonardo de Moura
0d96b6b4cb feat(library/expr_lt): add expression comparison operator that ignores treat level parameters as wildcards 2015-02-10 18:20:10 -08:00
Leonardo de Moura
64ac3fa4ee feat(library): add 'abbreviation' management module 2015-02-10 17:25:11 -08:00
Leonardo de Moura
058377c8c6 feat(library/tactic/rewrite_tactic): treat iff.refl as trivial step in the rewrite tactic 2015-02-08 17:27:59 -08:00
Leonardo de Moura
fcd67649ed refactor(kernel): expose may_reduce_later method 2015-02-07 20:36:26 -08:00
Leonardo de Moura
b57f93bad5 refactor(kernel): remove unnecessary procedures 2015-02-07 20:14:19 -08:00
Leonardo de Moura
f018fdabb9 refactor(library/kernel_bindings): remove unnecessary procedure 2015-02-07 18:57:46 -08:00
Leonardo de Moura
1640568f6a refactor(library/reducible): use default_converter in reducible, and converters based on reducible hints 2015-02-07 17:31:53 -08:00
Leonardo de Moura
b4f1029318 refactor(library/reducible): define opaque_type_checker using default_converter 2015-02-07 17:05:29 -08:00
Leonardo de Moura
e04250f0d8 refactor(library/tactic/rewrite_tactic): use default_converter 2015-02-07 16:44:51 -08:00
Leonardo de Moura
c04c0e8381 refactor(*): remove transparent_scope hack, replace [strict] with [all-transparent] annotation 2015-02-07 15:19:41 -08:00
Leonardo de Moura
7945b8adab refactor(kernel/type_checker): remove useless procedures 2015-02-07 14:55:36 -08:00
Leonardo de Moura
c2a296b1de feat(library/tactic/apply_tactic): add flag for disabling class instance resolution in the apply tactic 2015-02-06 17:27:24 -08:00
Leonardo de Moura
1557a579ed feat(library/tactic/proof_state): add report_failure flag to proof state 
tactic can use the flag to produce nice error messages
 2015-02-06 16:29:04 -08:00
Leonardo de Moura
2126b8ec9a feat(library/tactic/apply_tactic): perform class-instance resolution in the apply tactic 
closes #360
 2015-02-06 16:14:03 -08:00
Leonardo de Moura
18808d133e refactor(library/tactic/goal): move goal => local_context conversion to goal class 2015-02-06 16:09:59 -08:00
Leonardo de Moura
f10424d729 fix(library/tactic/rewrite_tactic): memory leak 2015-02-06 15:24:09 -08:00
Leonardo de Moura
aa70334f8d feat(library/tactic/rewrite_tactic): add "fold" step 2015-02-06 15:21:49 -08:00
Leonardo de Moura
47bd5e53e2 fix(library/tactic/rewrite_tactic): memory leak 2015-02-06 14:24:10 -08:00
Leonardo de Moura
7aac9f1fdb feat(library/tactic/rewrite_tactic): use expensive convertability checker at reduce_to steps and trivial goal 2015-02-06 13:53:03 -08:00
Leonardo de Moura
5b2a9dacc2 fix(library/tactic/rewrite_tactic): matcher should unfold only reducible constants 2015-02-06 13:44:04 -08:00
Leonardo de Moura
b4139627e5 feat(library/tactic/rewrite_tactic): add option to prevent any kind of constant unfolding when perfoming pattern matching in the rewrite tactic 2015-02-06 13:27:33 -08:00
Leonardo de Moura
62daf73dd0 chore(library/normalize): fix style 2015-02-06 13:27:10 -08:00
Leonardo de Moura
ba9557bb94 fix(library/tactic/rewrite_tactic): incorrect assertion 2015-02-06 13:02:50 -08:00
Leonardo de Moura
ba641d7c58 feat(library/normalize): validate unfold-c hints 2015-02-06 12:42:53 -08:00
Leonardo de Moura
7205382f8c feat(library/definitional/projection): add "unfold-c" hint to projections 2015-02-06 12:39:57 -08:00
Leonardo de Moura
1bd1f94542 feat(library/normalize): add "unfold-c" hint to normalizer 
This hint will also be used in the simplifier
 2015-02-06 12:39:49 -08:00
Leonardo de Moura
39446a7215 refactor(library/projection): move is_constructor_app to util 2015-02-06 12:12:25 -08:00
Leonardo de Moura
2e626b29fb feat(library/tactic/rewrite_tactic): allow many constants to be provided in a single rewrite unfold step 2015-02-06 11:03:36 -08:00
Leonardo de Moura
264cedb3a6 fix(frontends/lean/rewrite_tactic): incorrect assertion 2015-02-05 20:02:49 -08:00
Leonardo de Moura
e17ba27596 fix(library/tactic/rewrite_tactic): adjust the behavior of class resolution in rewriter 
The solution is not very satisfactory. I should investigate it more.
 2015-02-05 19:08:47 -08:00
Leonardo de Moura
ffe0d1186e feat(library/tactic/rewrite_tactic): add "reduce_to" step at rewrite tactic 2015-02-05 13:59:55 -08:00
Leonardo de Moura
116c65bff5 feat(library/tactic/rewrite_tactic): add reduction step to rewrite tactic 2015-02-05 13:42:50 -08:00
Leonardo de Moura
7cdc88701d feat(library/tactic/rewrite_tactic): add "reduction" step to rewrite tactic 2015-02-05 13:16:05 -08:00
Leonardo de Moura
808521223b feat(library/tactic/rewrite_tactic): support constant unfolding in rewrite tactic 2015-02-05 12:58:30 -08:00
Leonardo de Moura
d6958be7e7 fix(library/tactic/location): replace cache must not be used when only a subset of all occurrences should be replaced at replace_occurrences 2015-02-05 10:50:40 -08:00
Leonardo de Moura
941b493835 chore(library/tactic/rewrite_tactic): modify param name 2015-02-05 10:04:03 -08:00
Leonardo de Moura
0abfa30ead fix(library/tactic/rewrite_tactic): elaboration bug in the rewrite tactic steps/elements 2015-02-05 10:01:18 -08:00
Leonardo de Moura
14c72e82f6 feat(library/tactic/rewrite_tactic): add support for rewriting hypotheses 2015-02-04 20:04:19 -08:00
Leonardo de Moura
55fb678db2 fix(library/tactic/location): clang++ 3.3 compilation problem 2015-02-04 18:48:23 -08:00
Leonardo de Moura
42c2f7eb11 fix(library/tactic/rewrite_tactic): memory leak 2015-02-04 18:40:11 -08:00
Leonardo de Moura
89fde9d829 feat(library/tactic/rewrite_tactic): add maximum number of iterations threshold to rewrite tactic 
The idea is to avoid nontermination.
 2015-02-04 16:13:15 -08:00
Leonardo de Moura
dc297865d4 chore(library/tactic/rewrite_tactic): fix compilation warnings 2015-02-04 15:34:02 -08:00
Leonardo de Moura
ee079d12f4 feat(library/tactic/rewrite_tactic): remove trivial goal in rewrite_tactic 2015-02-04 15:29:52 -08:00
Leonardo de Moura
f0fac1ae0e feat(library/constants): add eq.intro 2015-02-04 15:27:18 -08:00
Leonardo de Moura
e5381679d6 feat(library/tactic/rewrite_tactic): rewrite goal 2015-02-04 15:17:58 -08:00
Leonardo de Moura
09818adf90 feat(library/tactic/rewrite_tactic): elaborate rewrite rule using unifier 2015-02-04 13:51:32 -08:00
Leonardo de Moura
49323ab598 feat(library/util): add mk_symm 2015-02-04 13:44:55 -08:00
Leonardo de Moura
ccae014ef9 feat(library/tactic/rewrite_tactic): ignore inst_implicit arguments when matching applications of declarations which contain them 2015-02-04 12:14:47 -08:00
Leonardo de Moura
0e05c239a5 feat(library/tactic/rewrite_tactic): add custom matcher pluging for rewriter 2015-02-04 11:51:39 -08:00
Leonardo de Moura
d6a7ec4621 chore(library/tactic/rewrite_tactic): fix style 2015-02-04 11:51:39 -08:00
Leonardo de Moura
b4dd2cc729 refactor(library/tactic/rewrite_tactic): more general rewrite step 
The rule can be an arbitrary expression.
Allow user to provide a pattern that restricts the application of the rule.
 2015-02-04 11:51:39 -08:00
Leonardo de Moura
461fd45efc feat(frontends/lean): allow a different location for each rewrite element 2015-02-04 11:51:39 -08:00
Leonardo de Moura
c845e44777 feat(frontends/lean): parse rewrite tactic 2015-02-04 11:51:39 -08:00
Leonardo de Moura
180cda304e feat(library/tactic): add rewrite tactic skeleton 
The tactic has not been implemented yet, but this commit adds all the
support for storing arguments, serializing and deserializing them.
 2015-02-04 11:51:39 -08:00
Leonardo de Moura
8a78adc9af feat(library/tactic): add auxiliary object "location" 
This object will used to specify the scope of application of tactics
 2015-02-04 11:51:39 -08:00
Leonardo de Moura
420da8fd3f feat(library/projection): store bit saying whether a projection is for a class or not. 2015-02-04 08:54:20 -08:00
Leonardo de Moura
c92f3bec65 refactor(library/definitional/projection): move projection "database" to library/projection 2015-02-04 07:18:43 -08:00
Leonardo de Moura
0e06f4aedc feat(library/match): extend match_plugin interface 2015-02-03 18:10:38 -08:00
Leonardo de Moura
44e575c895 feat(library/match): improve match_app_core 2015-02-03 17:37:22 -08:00
Leonardo de Moura
790fd9c24b chore(library/match): remove unused procedure 2015-02-03 15:20:26 -08:00
Leonardo de Moura
f79f43c702 refactor(library/match): use "special" meta-variables instead of free variables to represent placholders in the higher-order matcher 2015-02-03 15:15:04 -08:00
Leonardo de Moura
45e62031e2 fix(library/match): bug in matcher 2015-02-03 13:46:19 -08:00
Leonardo de Moura
4c7a17cc4a refactor(library/tactic/class_instance_synth): move has_expr_metavar_relaxed to util 2015-02-01 10:59:27 -08:00
Leonardo de Moura
c311e0aba6 chore(library/tactic/inversion_tactic): cleanup 2015-02-01 10:47:32 -08:00
Leonardo de Moura
143143e94c fix(library/tactic/inversion_tactic): missing normalization step in the inversion_tactic 2015-02-01 10:38:30 -08:00
Leonardo de Moura
e9e1f86b7f fix(library/app_builder): many bugs, add use_cache option, add tests 2015-01-29 15:30:31 -08:00
Leonardo de Moura
e6f022e3f2 fix(library/match): index out of bounds 2015-01-29 14:41:38 -08:00
Leonardo de Moura
b5d1f4e54c feat(library/match): add low-level match API 2015-01-29 14:09:09 -08:00
Leonardo de Moura
f587cc3e1d feat(library/app_builder): expose app_builder API in Lua 2015-01-29 11:38:56 -08:00
Leonardo de Moura
5efd91e435 fix(library/app_builder): missing initialization 2015-01-29 11:38:28 -08:00
Leonardo de Moura
5bb2a41c64 feat(library/reducible): expose Lua API for reducible hints 2015-01-29 10:37:15 -08:00
Leonardo de Moura
4cf2dcaa7e feat(library/app_builder): add helper class for creating applications efficiently using type inference 
The idea is to use this class in the simplifier.
For example, we will use to create: symmetry, reflexivity, transitivity
and congruence proof steps.
 2015-01-28 18:40:21 -08:00
Leonardo de Moura
4e08cc0659 feat(library/match): add flag for tracking whether matcher assigned anything 2015-01-28 18:39:50 -08:00
Leonardo de Moura
dbc8e9e13a refactor(*): add method get_num_univ_params 2015-01-28 17:22:18 -08:00
Leonardo de Moura
5aaade47d8 feat(library/match): add new API 2015-01-28 16:42:42 -08:00
Leonardo de Moura
a1eeb0a6a1 fix(library/print): typo in is_used_name 
closes #408
 2015-01-25 08:58:08 -08:00
Leonardo de Moura
27f6bfd3f0 refactor(*): add file constants.txt with all constants used by the Lean binary 2015-01-23 16:50:32 -08:00
Leonardo de Moura
880faf89e0 feat(frontends/lean/structure_cmd): add implicit_infer_kind annotation to structure command 
closes #354
 2015-01-21 18:12:29 -08:00
Leonardo de Moura
a53098385c refactor(frontends/lean/type_util): move infer_implicit_params to library 2015-01-21 17:22:41 -08:00
Leonardo de Moura
1d6ff5f761 feat(library/definitional/projection): throw exception if unsupported case occurs 
The user can workaround it by using trust-level 0 (i.e., no option -t num or -T)
 2015-01-20 17:42:34 -08:00
Leonardo de Moura
01ce57e52e feat(library/definitional/projection): add projection macro 2015-01-20 16:21:50 -08:00
Leonardo de Moura
b6750e9d29 feat(library/util): add auxiliary functions 2015-01-20 15:44:58 -08:00
Leonardo de Moura
8355ed55d7 refactor(library/definitional/projection): remove dead code 2015-01-20 13:40:09 -08:00
Leonardo de Moura
752b54085b refactor(kernel/type_checker): type checker should not unfold macros, but sign an error if a untrusted macro is used 
Now, we unfold untrusted macros outside of the Lean kernel.
 2015-01-20 12:36:56 -08:00
Leonardo de Moura
2717adde94 feat(library/unifier): add option 'unifier.conservative', use option by default in the calc_assistant 2015-01-19 16:23:29 -08:00
Leonardo de Moura
d0e9e0e21c feat(library/definitional/projection): add auxiliary function for simplifying expressions containing projections and constructors 2015-01-18 20:58:40 -08:00
Leonardo de Moura
858d21f20b feat(library/definitional/projection): store projection information 2015-01-18 16:26:56 -08:00
Leonardo de Moura
6c07ca5d41 perf(library/print): improve is_used_name 2015-01-15 19:01:13 -08:00
Leonardo de Moura
8ab775bd6f feat(*): distinguish between logical and runtime exceptions. 
Now, we use throwable as the new base class for all Lean exceptions, and
exception is the subclass for "logical" exceptions.
 2015-01-15 16:54:55 -08:00
Leonardo de Moura
ef529c660f fix(library/definitional/no_confusion): mark no_confusion as reducible 
Auxiliary definitions should be marked as reducible
 2015-01-13 18:44:47 -08:00