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

231 commits

Author SHA1 Message Date
Leonardo de Moura
9715d06f4a feat(library): minor cleanup, replace 'refl _' with 'rfl', define equivalence relation for sets 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 22:54:44 -07:00
Leonardo de Moura
3903be34a4 feat(frontends/lean): process theorem statement independently of proof, thus we have the same behavior in sequential and parallel compilation modes, closes #84 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 21:26:17 -07:00
Leonardo de Moura
7cb2ca62f4 refactor(Makefile): do not use full path on makefile rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:28:34 -07:00
Leonardo de Moura
06da0ebaaf refactor(library): rename Makefile.common to Makefile 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:10:39 -07:00
Leonardo de Moura
dbaf81e16d refactor(library): remove unnecessary 'standard' subdirectory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:08:09 -07:00
Jeremy Avigad
505b93b7cb refactor(lean/examples/constable.lean): move to library/standard/logic/examples/nuprl_examples.lean 2014-08-23 17:55:00 -07:00
Jeremy Avigad
d0f0e58a85 refactor(library/standard/data/int): split basic.lean into basic.lean and order.lean 2014-08-23 17:53:02 -07:00
Jeremy Avigad
47a1c00a6d refactor(library/standard): collect notation in general_notation 2014-08-23 17:53:02 -07:00
Jeremy Avigad
ad969b4695 feat(library/standard/logic): add identities 2014-08-23 17:53:02 -07:00
Leonardo de Moura
df60ab4ada fix(frontends/lean/calc): allow calc_subst to be defined for multiple operators, allow calc cmds to be organized into namespaces, fixes #65 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 16:45:04 -07:00
Leonardo de Moura
e602c4ba49 feat(frontends/lean): change multicomment to /- ... -/ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 17:55:13 -07:00
Leonardo de Moura
a5f0593df1 feat(*): change inductive datatype syntax 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 15:46:10 -07:00
Leonardo de Moura
fdd37fb1f3 chore(library/standard/data/sum): remove hints, they are not needed after the fix 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 21:44:02 -07:00
Jeremy Avigad
1fdc483ab9 fix(library/standard/data/int): remove misnamed file 2014-08-21 21:41:28 -07:00
Jeremy Avigad
02fba6e949 feat(library/standard/hott/fibrant.lean): add fibrant to library 2014-08-21 21:41:28 -07:00
Jeremy Avigad
05d0089381 feat(library/standard/sum.lean): add properties of sum 2014-08-21 21:41:28 -07:00
Jeremy Avigad
3afad10a72 feat(library/standard): add decidability of le for int 2014-08-21 21:41:28 -07:00
Leonardo de Moura
c4cc837e34 refactor(library/standard): define abbreviations using '@' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 18:39:38 -07:00
Leonardo de Moura
07bc0727e2 feat(frontends/lean): 'let [inline]' is the default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 18:24:22 -07:00
Leonardo de Moura
0df87bae24 chore(library/standard/data/nat/div): remove TODO 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 17:58:03 -07:00
Leonardo de Moura
ab404beb01 chore(library/standard/data/nat/order): remove unnecessary 'proofs' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 21:51:41 -07:00
Leonardo de Moura
38f46b1290 feat(library/standard/data/nat/order): add le_decidable, lt_decidable, ge_decidable, gt_decidable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 21:47:37 -07:00
Leonardo de Moura
129bb5fa09 chore(library/standard/data/int/basic): remove TODO's that were addressed by recent improvements 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 19:04:48 -07:00
Jeremy Avigad
d78c26977b feat(library/standard/data/nat/div): port div 2014-08-20 18:04:31 -07:00
Jeremy Avigad
6264fb52d6 fix(lean/library/standard): fix tests, more cleanup 2014-08-20 18:04:31 -07:00
Jeremy Avigad
148d475421 feat(library/standard): port int, and reorganize a lot 2014-08-20 18:03:24 -07:00
Jeremy Avigad
ad26c7c93c feat(library/standard/data/quotient): import quotient from lean 0.1 2014-08-20 18:03:24 -07:00
Leonardo de Moura
be5d034b6e chore(library/standard): remove workarounds 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 16:46:19 -07:00
Leonardo de Moura
9588336c15 refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 16:46:19 -07:00
Soonho Kong
76d310da8b chore(library/.gitignore): add TAGS 2014-08-15 20:55:38 -07:00
Soonho Kong
009e9fb3e6 feat(library/Makefile.common): add tags target 2014-08-15 20:52:29 -07:00
Leonardo de Moura
670bfe24f5 chore(build): remove hott library directory, and move hott tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-15 13:30:56 -07:00
Jeremy Avigad
5b7fb1f61a feat(library/standard/classes): add nonempty 2014-08-15 13:06:27 -07:00
Jeremy Avigad
39c1683546 feat(library/standard/logic): add class nonempty 2014-08-15 12:58:58 -07:00
Jeremy Avigad
2d69303344 feat(library/standard): add sigma types and subtypes, make inhabited constructive 2014-08-15 12:58:58 -07:00
Jeremy Avigad
a1645c5ce5 feat(library/standard/hott/path.lean): add theorems and clean up file 2014-08-15 12:58:58 -07:00
Jeremy Avigad
7d7655c3f1 refactor(library/standard): integrate hott with standard library 2014-08-15 12:58:58 -07:00
Jeremy Avigad
218c9dfc81 feat(library/hott): begin porting Coq HoTT 2014-08-15 12:58:58 -07:00
Jeremy Avigad
0ea2d287e1 feat(library/standard): add classes for relations 2014-08-15 12:58:58 -07:00
Soonho Kong
caa47b9a70 fix(library): add LEAN_VERSION_FILE to Makefile.common 2014-08-14 18:21:58 -07:00
Leonardo de Moura
2225a2acc5 feat(library/Makefile.common): generate .ilean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 18:05:48 -07:00
Leonardo de Moura
e1c97d1fc4 fix(library): remove LEAN_VERSION_FILE from Makefile.common, it breaks the build on Linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-14 18:05:48 -07:00
Soonho Kong
6f2c14be23 feat(library/Makefile.common): add dependency on bin/version 
This is related with issue #43.

[skip ci]
 2014-08-14 15:46:13 -07:00
Soonho Kong
87632622ee chore(library): add .gitignore 
[skip ci]
 2014-08-14 15:31:57 -07:00
Leonardo de Moura
60ab6d3bd8 feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
f319d084d4 feat(library/Makefile.common): use new --cache/-c option at Makefile.common 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-10 11:20:08 -07:00
Leonardo de Moura
f6ba6da4b5 fix(library/standard): add missing 'end' of namespace 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 17:52:51 -07:00
Leonardo de Moura
1a67e69678 feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-07 16:59:08 -07:00
Soonho Kong
e0bc5915fb fix(library/standard): remove long comments introduced by b2c2d1d 2014-08-07 11:59:59 -07:00
Soonho Kong
8d4c7b4b2c fix(library/hott/Makefile): specify LEAN_OPTIONS "--hott" 2014-08-07 09:59:15 -07:00
Leonardo de Moura
59f6cb5962 fix(build): delete incorrect/old .d and .olean files, detect errors when generating .d files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:48 -07:00
Leonardo de Moura
d5bb7d45ec fix(library/unifier): constraint priority in the unifier, and remove hack from if.lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:47 -07:00
Leonardo de Moura
47d49643b0 feat(library/standard/logic/connectives/if): add more general if_congr theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-04 13:58:47 -07:00
Soonho Kong
d8ae285f93 fix(library/Makefile.common): clean remove olean/d files recursively 
[skip ci]
 2014-08-04 11:47:24 -07:00
Leonardo de Moura
94efd51fc5 chore(library/standard/logic/connectives/if): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 23:11:52 -07:00
Leonardo de Moura
c3f57cdb1c feat(library/standard/logic/classes): add 'by_contradiction' theorem for decidable propositions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 22:58:12 -07:00
Leonardo de Moura
ae2e0fd3dc feat(library/standard/logic/connectives/if): add 'if-then-else' congruence theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 21:41:01 -07:00
Leonardo de Moura
f3cb5f2f84 feat(library/standard/logic/connectives/quantifiers): add some theorems for simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-03 20:03:49 -07:00
Leonardo de Moura
aeebd942f2 refactor(library/standard): use relative paths in some files in the standard library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 20:04:27 -07:00
Leonardo de Moura
4b030c5d5f feat(library/module): relative module path 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 19:47:55 -07:00
Leonardo de Moura
700c911cf7 chore(library/standard/logic/class/decidable): add missing 'end' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 17:00:01 -07:00
Leonardo de Moura
148836d14b feat(library/standard/data/option): add basic theorems for option types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 16:59:01 -07:00
Jeremy Avigad
b832b2e33e refactor(library/standard/data/nat): stylistic changes 2014-08-01 21:22:54 -07:00
Jeremy Avigad
b5db9a4797 feat(library/standard/data/nat): port most recent nat to lean 0.2 2014-08-01 21:22:53 -07:00
Jeremy Avigad
4b05e70762 feat(library/standard/logic/axioms): add import default 2014-08-01 21:22:53 -07:00
Jeremy Avigad
77931f2af8 feat(library/standard): add markdown documentation 2014-08-01 21:22:53 -07:00
Soonho Kong
3cb9b4c265 fix(library/Makefile.common): make OSX-compatible 2014-08-01 10:21:40 -07:00
Leonardo de Moura
d27c85e30c fix(library/Makefile.common): avoid error message when .d files do not exist 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 10:11:01 -07:00
Leonardo de Moura
f75beb8087 fix(library/standard/data/list/basic): remove 'sorry' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 09:15:30 -07:00
Jeremy Avigad
b2c2d1dd44 refactor(library/standard): organize files into a hierarchy 2014-08-01 09:11:51 -07:00
Jeremy Avigad
fbaf8b7e77 refactor(library/standard): begin reorganization into hierarchy 2014-08-01 09:11:51 -07:00
Jeremy Avigad
df84c4c2ca refactor(library/standard): clean up logic, reorder arguments to elim rules 2014-08-01 09:11:51 -07:00
Jeremy Avigad
c89c96b913 feat(library/standard/list.lean): add facts about lists 2014-08-01 09:11:51 -07:00
Jeremy Avigad
e846c8c76b index on master: 9dc1baa feat(library/standard/congruence.lean): finish congruence classes for propositional logic 2014-08-01 09:11:51 -07:00
Jeremy Avigad
5847743573 feat(library/standard/congruence.lean): finish congruence classes for propositional logic 2014-08-01 09:11:51 -07:00
Jeremy Avigad
8ea5dad4c0 feat(library/standard/congruence.lean): add class to infer that a function is a congruence with respect to two relations 2014-08-01 09:11:51 -07:00
Jeremy Avigad
09d5d074ec feat(library/standard/list.lean): begin to port lists from lean 0.1 2014-08-01 09:11:51 -07:00
Leonardo de Moura
b279c94037 feat(build): cread .d (dependency) files for .lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 09:08:16 -07:00
Leonardo de Moura
105c29b51e refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-28 19:59:38 -07:00
Leonardo de Moura
8ad6d7a98b doc(doc/lean): update Lean tutorial to Lean 0.2, and use org-mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-28 10:52:09 -07:00
Leonardo de Moura
864fdd37da refactor(library/aliases): aliases are from name to names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 21:01:59 -07:00
Leonardo de Moura
5555d620cf feat(library/standard): add or_inl and or_inr as short-hands for the commonly used 'or_intro_left _' and 'or_intro_right _' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 17:25:57 -07:00
Leonardo de Moura
99a1966fd6 refactor(library/standard/set): use the same style for mem_inter and mem_union 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 13:32:59 -07:00
Leonardo de Moura
88130f339e feat(library/standard): add basic set theory that does not rely on classical axioms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 13:18:33 -07:00
Leonardo de Moura
3a77226b92 feat(library/standard/bool): add bor_to_or theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 13:17:55 -07:00
Leonardo de Moura
25f7929ea3 feat(library/standard/bool): add band_assoc and bor_assoc theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 12:50:57 -07:00
Leonardo de Moura
d9ee994281 feat(library/hott): copy basic files to hott library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-26 19:13:04 -07:00
Leonardo de Moura
abe1dbd7e0 refactor(library/standard): cleanup notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:36:28 -07:00
Leonardo de Moura
a450ad5a95 feat(frontends/lean/inductive_cmd): improve notation for declaring 'empty' inductive datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:24:01 -07:00
Leonardo de Moura
a5b9a7b296 fix(frontends/lean/decl_cmds): support for section declarations with implicit parameters, they must be tagged with '@' when creating aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-25 11:10:45 -07:00
Leonardo de Moura
62483b793f feat(library/standard): add notation for symm, trans and subst 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 22:49:12 -07:00
Leonardo de Moura
ebf34f2fe9 refactor(library/standard): mark 'not' as transparent 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 22:14:15 -07:00
Leonardo de Moura
d84a4bea5f chore(library/standard): port (an older version of) Floris's nat library to Lean 0.2 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 20:31:28 -07:00
Leonardo de Moura
fd0deb4555 feat(library/standard): add basic properties of binary functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 17:48:30 -07:00
Leonardo de Moura
bfdf187ce7 refactor(library/standard): rename rec to rec_on 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 17:01:51 -07:00
Leonardo de Moura
5529ef1056 feat(library/standard): add function 'helper' module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 16:29:39 -07:00
Leonardo de Moura
5296275c41 feat(library/standard/logic): add imp_or theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 12:29:23 -07:00
Leonardo de Moura
08174f904b feat(library/standard/logic): mark 'not equal' as an abbreviation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-24 12:01:09 -07:00
Leonardo de Moura
8adf6e25ef refactor(library/standard/unit): make unit type similar to the one in the hott library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 09:56:05 -07:00
Leonardo de Moura
c5cbe1cc2c refactor(library/standard): rename bool_decidable to prop_decidable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 09:53:05 -07:00