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

396 commits

Author SHA1 Message Date
Leonardo de Moura
df51ba8b7c feat(library/definitional/projection): use strict implicit inference, closes #344 2014-11-25 18:04:06 -08:00
Leonardo de Moura
edc9e4908c test(tests/lean/run): add another subterm example 2014-11-25 16:53:09 -08:00
Leonardo de Moura
f737a140c1 test(tests/lean/run): direct subterm for non-reflexive datatype 2014-11-25 16:22:11 -08:00
Leonardo de Moura
ef75cac1c0 feat(kernel/expr): change the rules for inferring implicit arguments, closes #344 2014-11-25 12:54:07 -08:00
Leonardo de Moura
24a15b6c46 fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343 2014-11-24 21:33:52 -08:00
Leonardo de Moura
f729762c23 test(tests/lean/run): add test for well_founded relation for mutually recursive datatypes 2014-11-24 14:58:30 -08:00
Leonardo de Moura
d81a6259e8 feat(frontends/lean/find_cmd): add options for controlling find_decl 2014-11-24 00:16:10 -08:00
Leonardo de Moura
f1e915a188 feat(frontends/lean): add 'find_decl' command 2014-11-23 23:00:59 -08:00
Leonardo de Moura
44a2ef8f6f fix(frontends/lean/parser_config): binder(s) rbp was not being saved in .olean file 2014-11-23 17:49:14 -08:00
Leonardo de Moura
64686c1278 feat(frontends/lean): allow user to associate precedence to binders, closes #323 2014-11-23 17:30:46 -08:00
Leonardo de Moura
cf3b0e1087 feat(frontends/lean/placeholder_elaborator): apply substitution before collecting local instances, closes #333 2014-11-23 17:30:46 -08:00
Leonardo de Moura
13fba433b0 feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327 2014-11-23 17:30:22 -08:00
Leonardo de Moura
919007612a fix(tests/lean): adjust tests since module 'logic' depends on nat 
We need that because of the definitional package
 2014-11-22 17:34:05 -08:00
Leonardo de Moura
5db13da95f test(tests/lean/run/div_wf): cleanup div based on well founded recursion 2014-11-22 09:56:47 -08:00
Leonardo de Moura
064ecd3e3d refactor(library/data/nat): declare lt and le asap using inductive definitions, and make key theorems transparent for definitional package 
We also define key theorems that will be used to generate the
automatically generated a well-founded subterm relation for inductive
datatypes.
We also prove decidability and wf theorems asap.
 2014-11-22 00:19:39 -08:00
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
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
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
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
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
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
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
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