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

734 commits

Author SHA1 Message Date
Rob Lewis
10f1232296 feat(library/algebra/field): fix broken theorems 2015-02-28 08:49:28 -08:00
Rob Lewis
8ef2849b67 feat(library/algebra/fields): prove more theorems about division rings 2015-02-28 08:49:28 -08:00
Jeremy Avigad
a8cf58d97c feat(library/algebra/field): define discrete field 2015-02-28 08:49:28 -08:00
Rob Lewis
eef2e99a1c feat(library/algebra/field): add theorems about division rings 2015-02-28 08:49:05 -08:00
Rob Lewis
b8f0341119 feat(library/algebra): add field.lean 2015-02-28 08:48:48 -08:00
Floris van Doorn
23a248ab28 style(hott): let inverse notation have higher binding power than application 2015-02-28 01:16:23 -05:00
Floris van Doorn
9201bd7ca6 feat (hott/init): move nat.of_num to init.num and make it reducible outside namespace nat 
This is so that init.trunc can already use nat.of_num.
Also make nat.of_num reducible in the standard library
Also make gt and ge abbreviations
 2015-02-26 12:28:57 -05:00
Leonardo de Moura
68110faa4d feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations 2015-02-25 17:00:10 -08:00
Leonardo de Moura
5ca52d81ec feat(frontends/lean): ML-like notation for match and recursive equations 2015-02-25 16:20:44 -08:00
Leonardo de Moura
3c24461e51 refactor(*): modify '|' binding power, use 'abs a' instead of '|a|', and '(a | b)' instead of 'a | b' 2015-02-25 15:18:21 -08:00
Leonardo de Moura
c04c610b7b feat(frontends/lean): add 'assert H : A, ...' as notation for 'have H [visible] : A, ...' 2015-02-25 14:30:42 -08:00
Jeremy Avigad
e513b0ead4 refactor(library,hott): rename theorems for decidable and inhabited 
The convention is this: we use e.g. nat.is_inhabited and nat.has_decidable_eq
for these two purposes only, to avoid clashing with "inhabited" and "decidable_eq"
in a namespace. Otherwise, we use "decidable_foo" and "inhabited_foo".
 2015-02-25 14:05:07 -08:00
Jeremy Avigad
e555531eb6 feat(library/data/int/div): start on div for integers 2015-02-25 14:05:07 -08:00
Jeremy Avigad
7a57908d62 feat/refactor(library/data/int): revise and add theorems 2015-02-25 14:05:07 -08:00
Jeremy Avigad
cfdaffb6f5 feat/refactor(library/data/nat): do some housecleaning, add facts to div 2015-02-25 14:05:07 -08:00
Jeremy Avigad
a607e7dd57 feat(library/algebra/group): add rules for sub equalities 2015-02-25 14:05:06 -08:00
Leonardo de Moura
577a6da119 refactor(library/algebra/category/morphism): reduce compilation time using rewrite tactic 2015-02-25 14:04:17 -08:00
Leonardo de Moura
4f79d12da7 refactor(library/algebra/category/morphism): improve performance using rewrite tactic 2015-02-24 18:28:49 -08:00
Leonardo de Moura
909ebfc5f1 feat(frontends/lean/elaborator): try coercions after each overload 
We try only the easy cases since the more general case is too expensive.

closes #444
 2015-02-24 17:41:20 -08:00
Leonardo de Moura
3ede8e9150 refactor(library): use [] binder annotation when declaring instances 2015-02-24 16:12:39 -08:00
Leonardo de Moura
1cd44e894b feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible 
closes #442
 2015-02-24 16:12:35 -08:00
Leonardo de Moura
3197e6d403 feat(frontends/lean/parse_rewrite_tactic): improve rewrite tactic parser 2015-02-23 19:40:03 -08:00
Leonardo de Moura
74b8499fa9 refactor(library/data/nat/div): simplify proof of dvd_of_dvd_add_left 2015-02-17 18:55:44 -08:00
Leonardo de Moura
421a30d75c feat(library): export [reducible] annotations from function namespace to top-level 
see issue #433
 2015-02-16 18:52:41 -08:00
Leonardo de Moura
a35cce38b3 feat(frontends/lean): new semantics for "protected" declarations 
closes #426
 2015-02-11 14:09:25 -08:00
Leonardo de Moura
c7ee831c69 refactor(library/algebra/ordered_group): use rewrite tactic at ordered_group 2015-02-08 17:35:28 -08:00
Leonardo de Moura
f9ff4ee6bd refactor(library/algebra/ring): use rewrite tactic at ring module 2015-02-08 17:35:01 -08:00
Leonardo de Moura
d143b525f7 feat(library/algebra/ordered_group): reduce compilation time 2015-02-06 18:34:41 -08:00
Leonardo de Moura
96c161a659 feat(library/algebra/ring): simplify ring theorems using rewrite tactic 2015-02-05 18:48:02 -08:00
Leonardo de Moura
0ae6e2b3e4 feat(library/algebra/group): use rewrite tactic in the algebraic hierarchy 2015-02-05 18:03:02 -08:00
Leonardo de Moura
2ffdbba8b0 feat(library): replace same 'calc' proofs with 'rewrite' 2015-02-05 10:39:25 -08:00
Leonardo de Moura
b4dd2cc729 refactor(library/tactic/rewrite_tactic): more general rewrite step 
The rule can be an arbitrary expression.
Allow user to provide a pattern that restricts the application of the rule.
 2015-02-04 11:51:39 -08:00
Leonardo de Moura
c845e44777 feat(frontends/lean): parse rewrite tactic 2015-02-04 11:51:39 -08:00
Jeremy Avigad
77e8439012 feat(library/data/nat/div): add theorems for coprime, etc. 2015-02-03 13:50:59 -08:00
Leonardo de Moura
7e5fb3e493 fix(library/algebra/function): remove notation that conflicts with top-level notation for dependent pairs 2015-02-01 11:35:01 -08:00
Jeremy Avigad
90da0290f4 fix(library/init/{prod,sigma},library/data/sum): move notation in/out of namespaces 2015-02-01 11:17:45 -08:00
Jeremy Avigad
d48a332876 refactor(library/data/prod): move specialized theorems to quotient 2015-02-01 11:17:45 -08:00
Jeremy Avigad
3e92cd4922 feat(library/data,init/prod,sigma,sum): make more notation available at top level 2015-02-01 11:17:45 -08:00
Jeremy Avigad
5ef510f290 feat(library/logic/axioms/prop_complete): add by_cases, by_contradiction 2015-02-01 11:17:45 -08:00
Jeremy Avigad
003a2c1e2c refactor(library/logic/axioms): rename files, import logic.axioms.classical now imports all classical axioms 2015-02-01 11:17:45 -08:00
Jeremy Avigad
e5c25ff7a3 refactor(library/data/nat,int): use nicer definitions of structure instances 2015-02-01 11:17:45 -08:00
Jeremy Avigad
95d79e7bda refactor(library/data/nat): merge comm_semiring, make minor fixes 2015-02-01 11:17:44 -08:00
Jeremy Avigad
8d5a7a96b6 feat(library/data/nat/div): revise theorems, add lcm 2015-01-31 21:52:35 -08:00
Jeremy Avigad
928fc3ab81 feat(library/algebra/order,library/data/{nat,int}/order): make gt, ge reducible, add transitivity rules 2015-01-26 20:38:21 -05:00
Jeremy Avigad
0c04c7b0d2 fix(library/data/nat,int): make structure instances reducible 2015-01-26 20:38:21 -05:00
Jeremy Avigad
85ef7c5151 refactor(library/algebra/group): rename neg_add_distrib to neg_add, etc. 2015-01-26 20:38:21 -05:00
Jeremy Avigad
ba15da8d83 refactor(library/init/reserved_notation): increase binding strength of ^-1 to max+10 2015-01-26 20:38:21 -05:00
Leonardo de Moura
e2c41fca75 feat(frontends/lean): modify syntax for local notation 
The idea is to make it uniform with the syntax for defining local
attributes.
 2015-01-26 11:51:17 -08:00
Leonardo de Moura
b4d6f6e3ed feat(frontends/lean): 'attribute' command is persistent by default 2015-01-26 11:51:17 -08:00
Leonardo de Moura
4f2e0c6d7f refactor(frontends/lean): add 'attribute' command 
The new command provides a uniform way to set declaration attributes.
It replaces the commands: class, instance, coercion, multiple_instances,
reducible, irreducible
 2015-01-24 20:23:21 -08:00
Leonardo de Moura
ae7b5a9bc9 fix(library/algebra): add missing [reducible] 
It addresses issues raised at #403
 2015-01-21 15:53:56 -08:00
Jeremy Avigad
44642a4285 feat(library/algebra/ordered_ring,library/data/int/): add sign and theorems about abs, make int an instance, port theorems 2015-01-21 15:46:17 -08:00
Jeremy Avigad
58057c5d99 feat(library/algebra/ordered_group): add abs 2015-01-21 15:46:17 -08:00
Leonardo de Moura
abc64fbab8 refactor(library/algebra/group): remove unnecessary symm 2015-01-20 16:20:47 -08:00
Leonardo de Moura
8323d580b1 refactor(library/algebra/order): factor out proofs 2015-01-20 15:28:46 -08:00
Leonardo de Moura
21a3d918ff refactor(library/algebra/ordered_ring): use cleaner hack for improving performance 2015-01-19 17:41:11 -08:00
Leonardo de Moura
2e13e81fe0 refactor(library/data/nat/order): use record/structure instance expression 
Motivation: do not rely on a specific argument ordering
 2015-01-19 17:39:59 -08:00
Leonardo de Moura
2717adde94 feat(library/unifier): add option 'unifier.conservative', use option by default in the calc_assistant 2015-01-19 16:23:29 -08:00
Leonardo de Moura
7149c49553 refactor(library/algebra): factor out proofs from coercions 
Coercions/instances should be simple definitions
 2015-01-19 13:00:24 -08:00
Leonardo de Moura
edcc92d9c7 feat(frontends/lean): remove 'using' from structure instance command 2015-01-17 09:38:10 -08:00
Leonardo de Moura
50fe085374 refactor(library/algebra/ordered_ring): using new structure instance syntax sugar to define instances 2015-01-16 18:01:08 -08:00
Leonardo de Moura
3d63c0b5dc refactor(library/algebra/ring): using new structure instance syntax sugar to define instance 2015-01-16 17:42:30 -08:00
Leonardo de Moura
a86661f42c refactor(library/algebra/ordered_group): using new structure instance syntax sugar to define instances 2015-01-16 17:37:08 -08:00
Leonardo de Moura
ebc1878028 refactor(library/algebra/group): using new structure instance syntax sugar to define instances 2015-01-16 17:23:41 -08:00
Leonardo de Moura
8246feff67 refactor(library/logic/eq): cleanup proof 2015-01-13 17:12:21 -08:00
Leonardo de Moura
e4b9a89f5f refactor(library/data/fin): remove unnecessary import 2015-01-13 16:35:59 -08:00
Jeremy Avigad
b68ce77650 refactor/feat(library/data/nat): fix up sub and div, rename theorems, add theorems 2015-01-13 11:56:25 -05:00
Jeremy Avigad
0dcf06000b refactor(library/data/int/sub): rename theorems, add theorems, clean up 2015-01-12 16:28:42 -05:00
Leonardo de Moura
08a7997a97 refactor(library/data/string): put is_inhabited theorems on the toplevel 2015-01-10 14:07:20 -08:00
Leonardo de Moura
f053330755 refactor(library/data/sum): simplify has_decidable_eq proof using recursive equations and match expressions 2015-01-10 12:45:05 -08:00
Leonardo de Moura
2e4a2451e6 refactor(library/reducible): simplify reducible/irreducible semantics 2015-01-08 18:52:18 -08:00
Leonardo de Moura
a23f3e9102 refactor(library/init/nat): use recursive equations to prove nat.has_decidable_eq 2015-01-08 12:38:44 -08:00
Leonardo de Moura
7a3a73d931 refactor(library/data/nat): move nat.comm_semiring to separate file 2015-01-08 12:12:30 -08:00
Leonardo de Moura
05e1fc21f6 refactor(library/data/vector): define vector functions using recursive equations 2015-01-08 11:22:56 -08:00
Leonardo de Moura
4e49e73585 refactor(library/init/logic): add inhabited related functions, rename inhabited.default to default 2015-01-07 18:45:58 -08:00
Leonardo de Moura
1fab144aa7 refactor(library/init/nat): rename constants 
closes #387
 2015-01-07 18:26:51 -08:00
Jeremy Avigad
42c328e781 refactor(library/data/nat/basic): rename pred.zero and pred.succ 2015-01-07 18:18:28 -08:00
Jeremy Avigad
50f03c5a09 refactor(library/data/nat/order): make nat order an instance of linear_ordered_semigroup, rename various theorems 2015-01-07 18:18:28 -08:00
Leonardo de Moura
7b9758ac14 feat(library/data/fin): add of_nat_to_nat theorem 2015-01-07 17:46:47 -08:00
Leonardo de Moura
98412ee942 refactor(library/data/fin): redo fin using recursive equations 2015-01-07 17:38:00 -08:00
Leonardo de Moura
597f7385e8 fix(library/unifier): incorrect fix 2015-01-07 16:57:02 -08:00
Leonardo de Moura
4b47d22d05 refactor(library/data/list): use recursive equations 2015-01-07 13:38:11 -08:00
Leonardo de Moura
d8f3bcec67 feat(library/init/logic): add 'arbitrary' 
It is identical to default, but it is opaque.
That is, when we use 'arbitrary A', we cannot rely on the particular
value selected.
 2015-01-05 13:27:09 -08:00
Leonardo de Moura
23fa16a23d refactor(library/init): move num.succ to init.datatypes 2015-01-05 10:29:06 -08:00
Jeremy Avigad
b11064a90e fix(library/data/nat,int): fix instance declarations for nat and int 2015-01-03 22:27:21 -08:00
Leonardo de Moura
4781fc8365 fix(library/init/logic): eq.symm should not use eq.subst 
Reason: eq.symm is used by definitional package, and eq.subst is opaque.
Thus, computation will get stuck if it depends on eq.subst.
 2015-01-02 22:20:08 -08:00
Jeremy Avigad
53f486835e fix(library/data/nat/order): delete unused material at end of file 2014-12-26 16:57:10 -05:00
Jeremy Avigad
1eea75b6fc fix(library/data/nat/div,tests/lean/run/ppbeta): make decidable for dvd transparent, name change in ppbeta 2014-12-26 16:44:43 -05:00
Jeremy Avigad
cecabbb401 refactor(library/data/int,library/algebra): make int an instnance of ordered ring, rename theorems 2014-12-26 16:25:05 -05:00
Jeremy Avigad
25394dddb7 refactor(library): change mul.left_id to mul_one, and similarly for mul.right_id, add.left_id, add.right_id 2014-12-23 21:14:36 -05:00
Jeremy Avigad
5bc6dd84cf feat(library/data/nat): make nat an instance of comm_semiring 2014-12-23 21:14:35 -05:00
Jeremy Avigad
486bc321ff refactor(library/data/nat): rename theorems 2014-12-23 21:14:35 -05:00
Jeremy Avigad
e587449a6d refactor(library/data): remove folders with a single file 2014-12-23 21:14:35 -05:00
Jeremy Avigad
6ad091d7bf refactor(library): clean up headers and markdown files 2014-12-22 15:33:42 -05:00
Jeremy Avigad
fe424add26 refactor(library/logic/axioms): rename theorems 2014-12-22 15:33:42 -05:00
Jeremy Avigad
0f0da64264 refactor(library/data/int): make int instance of integral domain 2014-12-22 15:33:42 -05:00
Jeremy Avigad
da7a403b6c refactor(library/algebra/ring): make dvd a definition 2014-12-22 15:33:41 -05:00
Leonardo de Moura
d2958044fd feat(frontends/lean): add multiple_instances command 
After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command

          multiple_instances <class-name>

closes #370
 2014-12-21 17:28:44 -08:00
Leonardo de Moura
1e2fc54f2f refactor(library/init/sigma): rename sigma.dpair->sigma.mk, sigma.dpr1->sigma.pr1, sigma.dpr2->sigma.pr2 2014-12-19 18:23:08 -08:00
Leonardo de Moura
9eea32b076 refactor(library/init/datatypes): change implicit arguments of sum.inl and sum.inr 2014-12-19 18:07:13 -08:00