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

1757 commits

Author SHA1 Message Date
Leonardo de Moura
b5444c1314 refactor(frontends/lean/builtin_cmds): allow "constant" edges in the instance transitive closure graph 2015-06-29 18:57:05 -07:00
Leonardo de Moura
0fc2efe88e fix(library/tactic/rewrite_tactic): fixes #702 2015-06-28 20:37:17 -07:00
Leonardo de Moura
1b864a838f fix(library/tactic/induction_tactic.cpp): condition for checking whether 'induction' tatic is applicable or not 
fixes #690
 2015-06-28 13:07:02 -07:00
Leonardo de Moura
88844f6261 chore(src/library/user_recursors): add missing include 2015-06-28 12:53:48 -07:00
Leonardo de Moura
2f75768243 feat(library/tactic/rewrite_tactic): fail when nothing is rewritten 
fixes #686
 2015-06-28 12:05:00 -07:00
Leonardo de Moura
8616ed096e fix(library/composition_manager): typo 2015-06-27 14:12:26 -07:00
Leonardo de Moura
ca0aa4eb47 feat(library/composition_manager): simplify compositions of the form (mk ... (proj (mk ...)) ...) 
closes #666
 2015-06-27 14:07:32 -07:00
Leonardo de Moura
430dc21a28 feat(library/composition_manager): disable conversion optimization for automatically generated compositions 
see issue #666
 2015-06-27 14:07:22 -07:00
Leonardo de Moura
bd0e9d958d feat(library/tc_multigraph): shorter names for transitive edges 
see issue #666
 2015-06-27 14:07:15 -07:00
Leonardo de Moura
859ef441a0 feat(library/class): transitive instances 
see issue #666
 2015-06-27 14:06:56 -07:00
Leonardo de Moura
68785b8bed fix(library/tactic/generalize_tactic): fixes #711 2015-06-26 19:35:30 -07:00
Leonardo de Moura
1886b71c17 fix(library/unifier): fixes #705 2015-06-26 19:10:46 -07:00
Leonardo de Moura
e3e9220ab9 fix(library/tactic/rewrite_tactic): fixes #708 2015-06-26 18:41:08 -07:00
Leonardo de Moura
c61e6f6595 feat(library/unifier): add new rule for constraints of the form (pr ...) =?= t, where (pr ...) is a "stuck" projection application 2015-06-26 17:18:29 -07:00
Leonardo de Moura
0b7859f387 feat(library,frontends/lean): add support for projections in the elaborator 
The idea is to simulate the computation rules such as

    pr1 (mk a b) ==> a

in the elaborator
 2015-06-26 17:18:29 -07:00
Leonardo de Moura
31a4ee2ac3 fix(library/inductive_unifier_plugin): avoid potential assertion violation 2015-06-26 17:18:29 -07:00
Leonardo de Moura
a680114fd8 fix(library/tactic/rewrite_tactic): potential crash in the rewrite tactic 2015-06-26 17:18:29 -07:00
Leonardo de Moura
5581b735f4 feat(library/constants.txt): add poly_unit and poly_unit.star 2015-06-25 17:36:34 -07:00
Floris van Doorn
fa1979c128 feat(datatypes): let the type of unit be the lowest non-Prop universe 
The definitional package (brec_on and cases_on) now use poly_unit instead of unit

closes #698
 2015-06-25 17:33:46 -07:00
Leonardo de Moura
5687c24944 refactor(library/tactic/induction_tactic): cleanup 2015-06-22 10:23:54 -07:00
Leonardo de Moura
aeea8f83c4 feat(library/composition_manager): check if existing definition is definitionally equal 2015-06-21 16:53:08 -07:00
Leonardo de Moura
b8243934de feat(library/tc_multigraph): finish transitive closed multigraph 2015-06-20 20:25:20 -07:00
Leonardo de Moura
c6ad37a651 chore(src/library/tc_multigraph): fix typo 2015-06-19 21:12:11 -07:00
Leonardo de Moura
6872761c67 fix(library/tc_multigraph): typos 2015-06-19 20:11:31 -07:00
Leonardo de Moura
1f753aeccb feat(library): add tc_multigraph skeleton 2015-06-19 20:05:05 -07:00
Leonardo de Moura
70fc05294b refactor(library/local_context): avoid hack in local_context 2015-06-18 15:41:00 -07:00
Leonardo de Moura
694eef7f6a fix(util/sexpr/format): retract change that may be creating problems for emscripten 2015-06-18 10:49:13 -07:00
Leonardo de Moura
a4c0699e81 feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic 
See issue #676

Add new test demonstrating why it is useful to have the old semantics
for 'constructor'
 2015-06-17 23:48:54 -07:00
Leonardo de Moura
bf71d9f342 fix(library/tactic/rewrite_tactic): fixes #682 2015-06-17 18:49:02 -07:00
Leonardo de Moura
ce8f2a1674 feat(library/class): allow any constant to be marked as a class 
closes #679
 2015-06-17 16:26:45 -07:00
Leonardo de Moura
c59e1f49db feat(library): add composition manager 2015-06-17 14:41:50 -07:00
Leonardo de Moura
14c33c4e01 feat(kernel/error_msgs): add workaround for issue #669 
This issue should fix the new problem reported at #669.
It only disables beta-reduction in the pretty printer for application
type mismatch at (f n) when f is a lambda expression.
 2015-06-17 12:00:25 -07:00
Leonardo de Moura
f60cdee14b fix(library/tactic/rewrite_tactic): memory leak 2015-06-16 15:47:21 -07:00
Leonardo de Moura
0ae24faae3 feat(library/tactic/constructor_tactic): use 'fapply' in 'constructor' tactic 
closes #676
 2015-06-16 12:03:31 -07:00
Leonardo de Moura
2277b170f6 feat(library/tactic/exact_tactic): use 'append' instead of 'orelse' at eassumption 'tactic' 2015-06-16 11:58:10 -07:00
Leonardo de Moura
169f956143 fix(library/tactic): remove dead code 2015-06-16 11:57:37 -07:00
Leonardo de Moura
d8620ef4c9 fix(kernel,library,frontends/lean): improve error messages 
see #669
 2015-06-14 19:44:00 -07:00
Leonardo de Moura
8699d2dfb7 feat(library/tactic/rewrite_tactic): display list of overloads occurring in a failed rewrite step 2015-06-14 16:30:18 -07:00
Leonardo de Moura
9fbf267a3f feat(library/tactic/rewrite_tactic): when 'rewrite' step fails apply esimp and try again 
closes #670
 2015-06-12 19:48:58 -07:00
Leonardo de Moura
7bad9fe554 feat(library/error_handling/error_handling): set 'pp.beta' to false when displaying errors 
see issue #669
 2015-06-12 14:46:51 -07:00
Leonardo de Moura
69be4c720c fix(library/tactic/subst_tactic): bug in 'subst' tactic 2015-06-12 12:11:44 -07:00
Leonardo de Moura
25cbc5c154 fix(kernel/expr): remove 'cast_binder_info' 
We should put it back when we decide to implement it.
We also fix the bogus comment at src/frontends/lean/parser.cpp.

see issue #667
 2015-06-11 18:11:22 -07:00
Leonardo de Moura
8b7dc4e03a feat(frontends/lean): apply eta-reduction in postprocessing step 
Perhaps, we should add an option to disable this new feature.

Remark: this commit makes commit 46d418a redundant.
I'm keeping 46d418a because we may retract this commit in the future.
 2015-06-10 16:29:30 -07:00
Leonardo de Moura
46d418af3d feat(library/abbreviation): apply eta-reduction when expanding abbreviations 2015-06-10 14:52:59 -07:00
Leonardo de Moura
f3d50963ce fix(library/idx_metavar): compilation problem in debug mode 2015-06-09 14:37:17 -07:00
Leonardo de Moura
e3a0e62859 fix(library/unifier): try to generate approximate solution for flex-flex constraints before discarding them 
fixes #662
 2015-06-09 14:36:31 -07:00
Leonardo de Moura
f7dd85a935 chore(*): fix 'breif' typos 2015-06-08 16:54:55 -07:00
Leonardo de Moura
627e05c9e6 fix(library/tactic/rewrite_tactic): improve krewrite 2015-06-08 16:46:28 -07:00
Leonardo de Moura
d6a483fe84 feat(library): add idx_metavar module 2015-06-08 16:02:37 -07:00
Leonardo de Moura
496189feed feat(kernel/default_converter): cache failures for (f t =?= f s) heuristic 
See item 4 at
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/oJXwW5wT2Ds/d1Dgr8B-pE0J

See also
https://github.com/leanprover/lean/pull/659
 2015-06-08 10:41:30 -07:00
Leonardo de Moura
0e099b5fd8 feat(library/tactic/rewrite_tactic): apply beta&eta reduction before rewriting steps, add option 'rewrite.beta_eta' (default true) to control new feature. 2015-06-06 20:43:52 -07:00
Leonardo de Moura
1cbace9df6 feat(library/tactic/congruence_tactic): add congruence lemma generator 
The generated congruence theorems ignore arguments that are subsingleton types.
 2015-06-05 22:00:10 -07:00
Leonardo de Moura
d0d3f9bb41 refactor(kernel,library,frontends/lean): add helper functions, and cleanup collect_locals 2015-06-05 17:29:36 -07:00
Leonardo de Moura
c76d92284f feat(library/pp_options): add 'pp.all' option 2015-06-05 08:41:46 -07:00
Leonardo de Moura
c8ad1874a2 fix(library/util): compilation error in debug mode 2015-06-03 17:39:03 -07:00
Leonardo de Moura
68688ecdf6 fix(library/tactic/subst_tactic): in the standard mode, use dependent elimination in the subst tactic (when needed) 
Before this commit, the subst tactic was producing an type incorrect
result when dependent elimination was needed (see new test for an example).
 2015-06-03 17:36:04 -07:00
Leonardo de Moura
dce86b3a84 feat(library/init/logic): add 'eq.drec' (in standard Lean) with a signature very similar to eq.rec in the HoTT library 2015-06-03 17:29:26 -07:00
Leonardo de Moura
b2f8d2000c fix(library/simplifier/rewrite_rule_set): avoid compiler specific behavior 2015-06-01 22:23:34 -07:00
Leonardo de Moura
d6997300f1 fix(library/private): use environment fingerprint to compute private decls "unique" identifier 
fixes #648
 2015-06-01 22:21:31 -07:00
Leonardo de Moura
4ace996057 fix(library/simplifier): bug in is_permutation_ceqv 2015-06-01 18:07:31 -07:00
Leonardo de Moura
0fbc944cdd feat(frontends/lean): add '[rewrite]' attribute 2015-06-01 17:58:24 -07:00
Leonardo de Moura
d547698a56 refactor(library,library/tactic): move class_instance_synth to library 
This module will be needed by the simplifier
 2015-06-01 16:30:40 -07:00
Leonardo de Moura
8a89588079 refactor(library,library/tactic): move auxiliary procedures from tactic to library 2015-06-01 16:19:55 -07:00
Leonardo de Moura
b62e6bb133 feat(library/simplifier): add rewrite rule sets 2015-06-01 15:15:57 -07:00
Leonardo de Moura
780d313686 fix(library/annotation): add missing == and hash methods for annotation class 
We have multiple annotations. The default == and hash methods were
ignoring that.
 2015-06-01 11:27:46 -07:00
Leonardo de Moura
ca110012d8 feat(library/tactic): automate "generalize-intro-induction/cases" idiom 
closes #645
 2015-05-30 21:57:28 -07:00
Leonardo de Moura
6d2f37857d feat(frontends/lean/builtin_cmds): add 'print [reducible]', 'print [irreducible]' and 'print [quasireducible]' commands 2015-05-29 16:47:29 -07:00
Leonardo de Moura
c07d14e94a fix(library/tactic/rewrite_tactic): incorrect assertion 2015-05-29 15:59:03 -07:00
Leonardo de Moura
0ceedbe69e fix(library/normalize): fixes #640 2015-05-29 15:58:59 -07:00
Leonardo de Moura
f48cdccd20 fix(frontends/lean/pp): abbreviation with parameters 
closes #639
 2015-05-29 15:13:31 -07:00
Leonardo de Moura
a071012346 fix(frontends/lean/pp,library/head_map): handle 'as_atomic' annotation 
This commit fixes local notation that contains parameters

see issue #639
 2015-05-29 14:51:28 -07:00
Leonardo de Moura
ae0bdaa836 chore(library,util): fix style 2015-05-27 16:46:58 -07:00
Leonardo de Moura
d95c064a29 feat(library/simplifier/ceqv): add to_ceqv procedure 2015-05-27 16:35:56 -07:00
Leonardo de Moura
85409a59d3 feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants 
closes #511
 2015-05-27 16:32:43 -07:00
Leonardo de Moura
7d73f4f091 refactor(library,frontends/lean): simplify the creation of custom normalizers 2015-05-27 15:33:20 -07:00
Leonardo de Moura
dc6411b903 feat(library/inductive_unifier_plugin): restrict rule that was generating non-terminating behavior 
see issue #632
 2015-05-27 14:41:12 -07:00
Leonardo de Moura
47e5633498 feat(frontends/lean/calc_proof_elaborator): avoid unnecessary unfolding in the calc tactic 2015-05-27 12:07:39 -07:00
Leonardo de Moura
77f742ae8e feat(library/relation_manager): add auxiliary functions 2015-05-27 12:07:06 -07:00
Leonardo de Moura
ea43f3ea80 fix(frontends/lean/builtin_cmds): fixes #630 2015-05-26 22:19:42 -07:00
Leonardo de Moura
ed01242bc1 chore(library/tactic/apply_tactic): remove dead code 2015-05-26 12:18:50 -07:00
Leonardo de Moura
7f0951b8e7 feat(library/tactic): improve assumption tactic performance 2015-05-25 20:22:37 -07:00
Leonardo de Moura
d0987eb3ac feat(library/tactic): add 'subtvars' tactic 2015-05-25 16:36:44 -07:00
Leonardo de Moura
a3f23d5233 feat(library/tactic): add improved 'subst' tactic 2015-05-25 15:03:59 -07:00
Leonardo de Moura
f13ca3cd9a feat(library/tactic/contradiction_tactic): handle (h1 : p) and (h2 : not p) hypotheses in the contradiction tactic 2015-05-25 10:29:51 -07:00
Leonardo de Moura
88975927e6 fix(library/tactic/relation_tactics): beta-reduce goal before trying to extract head symbol 2015-05-24 18:56:35 -07:00
Leonardo de Moura
004ea80e65 fix(library/tactic/rewrite_tactic): apply beta reduction when selecting patterns 2015-05-24 18:44:30 -07:00
Leonardo de Moura
b83b0c0017 fix(library/tactic/induction_tactic): fixes #619 2015-05-21 18:22:07 -07:00
Leonardo de Moura
f830bf54c2 refactor(*): clarify name_generator ownership 2015-05-21 14:32:36 -07:00
Leonardo de Moura
a7ead5fc14 fix(library/relation_manager): typo 2015-05-21 14:12:28 -07:00
Leonardo de Moura
e3250f0ffd feat(library/simplifier): add conditional equivalence detection 2015-05-21 13:55:23 -07:00
Leonardo de Moura
907d017cbf feat(library/relation_manager): cache information about binary relations 2015-05-21 13:04:33 -07:00
Leonardo de Moura
c2faa0fe98 refactor(library): rename equivalence_manager to relation_manager 2015-05-21 12:25:02 -07:00
Leonardo de Moura
2b4233ee8e fix(library/tactic/induction_tactic): exception handling 2015-05-21 10:15:49 -07:00
Leonardo de Moura
d6b72ef4d7 feat(library/tactic/induction_tactic): try available recursors until one works 
closes #615
 2015-05-20 23:23:05 -07:00
Leonardo de Moura
2164ba6f20 fix(library/tactic/induction_tactic): fixes #614 2015-05-20 23:14:11 -07:00
Leonardo de Moura
51d4644832 fix(library/tactic/induction_tactic): fixes #613 2015-05-20 22:26:50 -07:00
Leonardo de Moura
5508e4b132 feat(library/tactic/induction_tactic): type class inference for minor premises 
closes #611
 2015-05-20 20:48:33 -07:00
Leonardo de Moura
029f374a69 fix(library/tactic/induction_tactic): fixes #610 2015-05-20 20:28:02 -07:00
Leonardo de Moura
2d22bb8ea2 feat(frontends/lean/builtin_cmds): do not unfold proofs in the eval command 
In the future, we should probably add an option for unfolding proofs.
 2015-05-20 19:14:57 -07:00
Leonardo de Moura
3e87f09d78 feat(library/tactic/induction_tactic): add support for user-defined recursors that contain parameters that should be synthesized by type class resolution 2015-05-19 15:33:46 -07:00
Leonardo de Moura
78ee055de8 feat(library/tactic): add induction tactic with support for user defined recursors 
closes #483
closes #492
 2015-05-19 13:27:17 -07:00
Leonardo de Moura
5b1491bdbd feat(library/user_recursors): store number of arguments expected by recursor 2015-05-19 12:24:46 -07:00
Leonardo de Moura
1e4285cf41 fix(library/user_recursors): invalid recursor_info for builtin indexed families 2015-05-19 12:19:46 -07:00
Leonardo de Moura
6da2ba331f fix(library/user_recursors): memory access violation 2015-05-19 11:07:31 -07:00
Leonardo de Moura
4f12409c63 fix(library/unifier): assertion violation 
This assertion violation was introduced when we added "projection
macros" to speedup the elaboration process.
 2015-05-19 10:07:31 -07:00
Leonardo de Moura
937d6ac7b6 fix(frontends/lean/pp): print notation produces incorrect output 
fixes #604
 2015-05-19 09:57:13 -07:00
Leonardo de Moura
e1c2340db2 fix(frontends/lean): consistent behavior for protected declarations 
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608

closes #609
 2015-05-18 22:35:18 -07:00
Leonardo de Moura
19361f0196 feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables 
see discussion at #604
 2015-05-18 15:45:23 -07:00
Leonardo de Moura
c61c049152 feat(library/user_recursors): generalize acceptable use-defined recursors 
see issue #492
 2015-05-18 14:21:10 -07:00
Leonardo de Moura
62082c72a8 fix(library/user_recursors): remove unnecessary restriction on minor premises of user-defined recursors 
see issue #492
 2015-05-18 10:09:11 -07:00
Leonardo de Moura
830d0ce1a7 fix(library/user_recursors): make sure homotopy.rec_on is recognized as a valid user-defined recursor 
see issue #492
 2015-05-18 09:57:50 -07:00
Leonardo de Moura
b1ece388a6 feat(frontends/lean,library/tactic/induction_tactic): improve induction tactic notation, expand induction tactic implementation 2015-05-18 09:25:07 -07:00
Leonardo de Moura
4256984803 fix(library/tactic/inversion_tactic): incorrect check 2015-05-18 09:16:07 -07:00
Leonardo de Moura
d41bff8c43 feat(library): add helper function 2015-05-18 09:16:07 -07:00
Leonardo de Moura
84faef5d5d feat(library/tactic/rewrite_tactic): rewrite tactic with 'iff' lemmas 2015-05-14 18:27:13 -07:00
Leonardo de Moura
1dedd2829c fix(library/match): bug in higher-order matcher 2015-05-14 18:27:10 -07:00
Sebastian Ullrich
77c20e99ff feat(library/tactic/inversion_tactic): consistent orientation of generated equalities 
Generated equalities in proof irrelevant environments were inverted
compared with the documentation and the proof relevant case, which
resulted in newly generated local vars replacing equivalent old ones
instead of the other way around.
 2015-05-14 23:32:54 +02:00
Leonardo de Moura
163577c23a fix(library/normalize): fixes #599 2015-05-13 18:36:16 -07:00
Leonardo de Moura
d0582b2537 fix(library/user_recursors): warning 2015-05-13 10:04:38 -07:00
Leonardo de Moura
dd5b221d32 fix(library/user_recursors): warning message 2015-05-13 09:42:32 -07:00
Leonardo de Moura
065a1f7501 feat(library/tactic): add 'induction' tactic skeleton 2015-05-12 20:21:25 -07:00
Leonardo de Moura
99084dce1c chore(library/user_recursors): fix style 2015-05-12 15:48:24 -07:00
Leonardo de Moura
f403ea984b feat(frontends/lean): add 'print [recursor]' command for debugging purposes 2015-05-12 15:48:24 -07:00
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