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

1528 commits

Author SHA1 Message Date
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