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

994 commits

Author SHA1 Message Date
Leonardo de Moura
5d5fd2da50 fix(frontends/lean): tactic + section variables, fixes #332 2014-11-21 10:07:16 -08:00
Leonardo de Moura
7e7e7c241c test(tests/lean/run/gcd): gcd compiled by hand into wf recursion 2014-11-18 19:34:01 -08:00
Leonardo de Moura
4fbb5cfcca test(tests/lean/run/div_wf): cleanup 2014-11-18 17:59:14 -08:00
Leonardo de Moura
a065c7bf96 test(tests/lean/run/tree_height): experiment with wf relation based on the height 
This is easier to generate than the subterm relation
 2014-11-18 17:57:17 -08:00
Leonardo de Moura
5fbe990c7a test(tests/lean/run): define div using wf package 2014-11-18 13:55:58 -08:00
Leonardo de Moura
5daff18017 test(tests/lean/run): pre-quotient experiment 2014-11-17 18:30:11 -08:00
Leonardo de Moura
28c63e685b feat(frontends/lean): add '[local]' notation, closes #322 2014-11-16 21:15:04 -08:00
Leonardo de Moura
bf5f48730c refactor(library/data/subtype): define subtype using 'structure' command 2014-11-16 15:01:14 -08:00
Leonardo de Moura
a171f8fbc3 test(tests/lean/run): simple diag for square matrices 2014-11-15 18:49:17 -08:00
Leonardo de Moura
1b95b69251 test(tests/lean/run): define subterm relation for vectors 2014-11-15 16:17:51 -08:00
Leonardo de Moura
ea640257bf feat(frontends/lean/structure_cmd): generate no_confusion for structures too 2014-11-15 16:00:09 -08:00
Leonardo de Moura
b87559dac5 test(tests/lean/run): define subterm relation for trees by hand 2014-11-15 13:29:23 -08:00
Leonardo de Moura
7685516d1e feat(frontends/lean): better default for atomic notation 2014-11-14 16:25:13 -08:00
Leonardo de Moura
67de3b06f3 feat(kernel/level): improve universe level pretty printer 
Example: produce `l+2` instead of `succ (succ l)`.
 2014-11-14 14:51:03 -08:00
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