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

747 commits

Author SHA1 Message Date
Leonardo de Moura
cc2d988aea feat(library/data/num): prove many theorems for pos_num.lt and pos_num.le 2015-03-04 18:30:31 -08:00
Leonardo de Moura
f60fc5183a feat(library/data/bool): add auxiliary theorems 2015-03-04 18:30:31 -08:00
Leonardo de Moura
02d3f7c37c refactor(library/data/list): use 'change' tactic 2015-03-01 14:27:22 -08:00
Leonardo de Moura
df13588b93 chore(library/data): remove unnecessary parentheses 2015-03-01 14:18:36 -08:00
Leonardo de Moura
e8ef1f97b6 feat(library/data/set): use Prop instead of bool when defining set 2015-03-01 08:23:39 -08: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
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
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
a35cce38b3 feat(frontends/lean): new semantics for "protected" declarations 
closes #426
 2015-02-11 14:09:25 -08:00
Leonardo de Moura
2ffdbba8b0 feat(library): replace same 'calc' proofs with 'rewrite' 2015-02-05 10:39:25 -08:00
Jeremy Avigad
77e8439012 feat(library/data/nat/div): add theorems for coprime, etc. 2015-02-03 13:50:59 -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
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
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
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
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
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
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
Jeremy Avigad
b11064a90e fix(library/data/nat,int): fix instance declarations for nat and int 2015-01-03 22:27:21 -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
0f0da64264 refactor(library/data/int): make int instance of integral domain 2014-12-22 15:33:42 -05: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
Leonardo de Moura
235894cec5 fix(data/int/basic): move decidable theorems 2014-12-17 18:27:39 -08:00
Jeremy Avigad
5a2f81e962 fix(library/data/int): define sub from algebra.sub 2014-12-17 18:02:55 -08:00
Jeremy Avigad
9d2587c79b refactor(library/data/int/basic): make the integers an instance of ring 2014-12-17 13:32:38 -05:00
Leonardo de Moura
abe129aa4f refactor(library): rename theorems "iff.flip_sign -> not_iff_not_of_iff" and "decidable_iff_equiv -> decidable_of_decidable_of_iff" 2014-12-15 19:17:51 -08:00
Leonardo de Moura
5cf8064269 refactor(library): rename exists_elim and exists_intro to exists.elim 
and exists.intro
 2014-12-15 19:07:38 -08:00
Jeremy Avigad
3e9a484851 refactor(library/logic/connectives): rename theorems 2014-12-15 15:05:44 -05:00
Leonardo de Moura
c6ebe9456e feat(library/data/nat): add "bounded" quantifiers 
Later, we will add support for arbitrary well-founded relations
 2014-12-13 15:42:38 -08:00
Leonardo de Moura
477d79ae47 refactor(library/init): move more theorems to logic 2014-12-12 13:50:53 -08:00
Leonardo de Moura
d6c8e23b03 refactor(library/init/logic): move theorems to library/logic 2014-12-12 13:24:17 -08:00
Leonardo de Moura
97552a8cfe refactor(library/sigma): fix/use sigma notation 2014-12-11 15:50:44 -08:00
Leonardo de Moura
05f27b8f0e feat(frontends/lean/structure): add option for controlling whether we automatically generate eta and projection-over-intro theorems for structures 
It seems most of the time these theorems are not used at all.
They are just polluting the namespace.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-12-09 12:40:09 -08:00
Jeremy Avigad
057615532e feat(library/data/int): replace int definition with structure and better computational behavior 2014-12-05 22:24:42 -08:00
Leonardo de Moura
e72c4977f0 feat(frontends/lean): nicer notation for dependent if-then-else 2014-12-04 11:13:09 -08:00
Leonardo de Moura
7d19b5b743 refactor(library/data/vector): cleanup 2014-12-03 21:06:17 -08:00
Leonardo de Moura
af978e40e8 refactor(library/data/option): move 'option' declaration to init.datatypes 2014-12-03 18:53:23 -08:00
Leonardo de Moura
b094c1cf43 refactor(library/init): move num->nat coercion to init 2014-12-01 08:23:31 -08:00
Leonardo de Moura
697d4359e3 refactor(library): add 'init' folder 2014-11-30 20:34:12 -08:00
Leonardo de Moura
7dc055cfc9 chore(library/data/nat/decl): remove leftover 2014-11-30 15:10:10 -08:00
Leonardo de Moura
dad94eafbe refactor(data/nat/decl): use new naming convention at data/nat/decl.lean 2014-11-30 15:07:09 -08:00
Leonardo de Moura
2281fb30c8 refactor(library): use "symbolic" precedences in the standard library 2014-11-29 19:08:37 -08:00
Leonardo de Moura
2c0472252e feat(frontends/lean): allow expressions to be used to define precedence, closes #335 2014-11-29 18:29:48 -08:00
Leonardo de Moura
d7042c4618 fix(library/logic/heq): heq.to_eq must be transparent because it is needed in the 'inversion' tactic used by definitional package 2014-11-28 23:49:17 -08:00
Leonardo de Moura
cab99e2e22 refactor(library/data/vector): simplify 'vector' using new 'inversion' tactic 2014-11-28 23:19:53 -08:00
Leonardo de Moura
ae0daf9639 fix(library/data/prod/decl): give preference to unicode version when pretty printing 2014-11-28 23:02:19 -08:00
Jeremy Avigad
bb8d436e75 refactor(library/algebra/relation, library/logic/instances): revise equivalence relations and congruences to use structure command 2014-11-28 22:54:15 -08:00
Jeremy Avigad
89380f088e feat(library): reorganize and declare some notation 2014-11-28 22:54:15 -08:00
Jeremy Avigad
f923d6a24c feat(library/data/sum): use + notation for sum 2014-11-28 22:54:15 -08:00
Leonardo de Moura
011e955fed refactor(library/data/fin): simplify 'fin' module using new inversion tactic 2014-11-28 22:46:06 -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
7231a36ec7 refactor(library/data/nat/div): remove unnecessary annotations 2014-11-23 17:30:46 -08:00
Floris van Doorn
25f5c56bb2 refactor(data/sigma): move notation from sigma.thms to sigma.decl 2014-11-22 17:44:12 -08:00
Floris van Doorn
7bfbe039d9 refactor(data.prod): move theorems about products from data.quotient.util to data.prod.thms 2014-11-22 17:44:12 -08:00
Floris van Doorn
e8b076e460 feat(hott/types/sigma): port large part of the sigma library from the hott library 
most importantly, prove the characterization of paths in sigma types
 2014-11-22 17:44:12 -08:00
Leonardo de Moura
616f2d9b82 fix(library/data/nat/div): notation should be local 2014-11-22 17:33:42 -08:00
Leonardo de Moura
ab9c51bd4b refactor(library/data/nat/div): simplify 'gcd' definition 2014-11-22 17:19:24 -08:00
Leonardo de Moura
2af5ce364d feat(library/data/nat/decl): add 'measure' 2014-11-22 17:19:03 -08:00
Leonardo de Moura
d07481f60f feat(library/data/nat/div): remove some 'sorry's 2014-11-22 14:59:35 -08:00
Leonardo de Moura
9368b879bf refactor(library/data/nat/div): use well-founded library for defining div, mod and gcd 2014-11-22 13:26:55 -08:00
Leonardo de Moura
21b16fd97c feat(library/data/nat): add more basic theorems for definitional package 2014-11-22 13:25:46 -08:00
Leonardo de Moura
9c9f5bba1a refactor(library/data/nat): prove auxiliary theorems about < and sub asap for the definitional package 2014-11-22 09:36:33 -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
dbb3b7c72a refactor(library/data/nat/sub): cleanup 'max' theorems 2014-11-18 17:56:42 -08:00
Leonardo de Moura
e77cd59368 refactor(library/logic): add basic definitions for relations at logic/relation.lean 
We need them for wf and definitional package
 2014-11-18 17:32:22 -08:00
Leonardo de Moura
99c30db805 feat(library/data/fin): add fin type 2014-11-17 23:44:57 -08:00
Leonardo de Moura
e2ceb86884 feat(library/data/nat/order): add calc_trans commands for lt and le 2014-11-17 23:44:27 -08:00
Leonardo de Moura
5dc42762de feat(library/data): define 'nat.addl' addition using recursion on the first argument, prove it to be equivalent to 'add', and use it to define vector.append 2014-11-17 22:03:39 -08:00
Leonardo de Moura
3cd3da5a84 refactor(library/data/prod/wf): remove duplication, and import wf's for sigma and prod 2014-11-16 21:19:10 -08:00
Leonardo de Moura
b7725c2949 feat(library/data/sigma/wf): define 'lex' for 'sigma' types and prove wf theorem 2014-11-16 20:08:52 -08:00
Leonardo de Moura
dd0b1ecdbf refactor(library/data/sigma): break file into smaller pieces to reduce dependencies 2014-11-16 18:22:03 -08:00
Leonardo de Moura
53ac754328 refactor(library/data/option): cleanup using 'no_confusion' 2014-11-16 17:56:51 -08:00
Leonardo de Moura
de209f929e feat(library/data/prod/wf): define relational product and prove wf theorem for it 2014-11-16 17:47:07 -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
b5404cd979 refactor(library/data/vector): cleanup, use variables, add concat 2014-11-15 22:36:52 -08:00
Leonardo de Moura
85f24e4c80 feat(library/data/vector): add 'zip' and 'unzip' functions 2014-11-15 22:19:23 -08:00
Leonardo de Moura
a7adfde84f feat(library/data/vector): use 'mechanical' definitions, and add 'last' function 
The 'mechanical' definitions are "mimicking" what the definitional
package will do.
 2014-11-15 20:21:18 -08:00
Leonardo de Moura
e7a7458922 feat(library/general_notation): reserve unary minus 2014-11-13 22:08:20 -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
ef5a3e83ad feat(library/data/vector): expand 'vector' module 2014-11-11 22:33:47 -08:00
Leonardo de Moura
21b93bd2e5 chore(library/data/prod/wf): remove dependency on opaque theorem 2014-11-11 00:39:53 -08:00
Leonardo de Moura
54213b48dc feat(library/data/prod/wf): lex of well-founded relations is well-founded 2014-11-11 00:29:21 -08:00
Leonardo de Moura
76711d00c1 feat(library/data/nat/wf): define measure using inverse image 2014-11-11 00:28:46 -08:00
Leonardo de Moura
4623a62ec3 feat(library/data/nat/wf): predecessor relation is well-founded 2014-11-10 22:15:15 -08:00
Leonardo de Moura
189e5e6b48 refactor(library/data/nat/wf): mark theorem as transparent 
It doesn't really help since
        le_imp_lt_or_eq, succ_le_cancel, lt_imp_le_succ and or.elim
are still opaque
 2014-11-10 12:52:02 -08:00
Floris van Doorn
780e949992 feat(empty): define negation of types 2014-11-08 19:12:54 -08:00
Leonardo de Moura
b97d437011 refactor(library/data/nat/basic): use no_confusion construction to simplify proofs 2014-11-08 19:00:40 -08:00
Leonardo de Moura
ac5a963db3 refactor(library/data/sum): use no_confusion construction to simplify proofs 2014-11-08 18:58:56 -08:00
Leonardo de Moura
46149d0d50 refactor(library/data/prod): break into pieces to reduce dependencies 
prod is needed for some automatically generated constructions.
So, it is important it is loaded in the environment as early as possible.
 2014-11-08 10:19:29 -08:00
Leonardo de Moura
64d2cc60c2 feat(library/data/nat/wf): add nat.lt is well founded theorem 2014-11-07 10:48:31 -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
fd34fd17de refactor(library/data/bool): break into pieces to reduce dependencies 2014-11-07 08:41: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
60eac0195d feat(frontends/lean/structure_cmd): generate projection over constructor theorems for structures 2014-11-04 09:10:25 -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
d2b5af237e refactor(library): use new 'structure' command to define prod and sigma 2014-11-03 18:57:55 -08:00
Floris van Doorn
d8a616fa70 refactor(library): major changes in the library 
I made some major changes in the library. I wanted to wait with pushing
until I had finished the formalization of the slice functor, but for
some reason that is very hard to formalize, requiring a lot of casts and
manipulation of casts. So I've not finished that yet.

Changes:

- in multiple files make more use of variables

- move dependent congr_arg theorems to logic.cast and proof them using heq (which doesn't involve nested inductions and fewer casts).

- prove some more theorems involving heq, e.g. hcongr_arg3 (which do not
  require piext)

- in theorems where casts are used in the statement use eq.rec_on
  instead of eq.drec_on

- in category split basic into basic, functor and natural_transformation

- change the definition of functor to use fully bundled
categories. @avigad: this means that the file semisimplicial.lean will
also need changes (but I'm quite sure nothing major).  You want to
define the fully bundled category Delta, and use only fully bundled
categories (type and ᵒᵖ are notations for the fully bundled
Type_category and Opposite if you open namespace category.ops). If you
want I can make the changes.

- lots of minor changes
 2014-11-03 18:45:12 -08:00
Leonardo de Moura
ae9d11c9c4 refactor(library/data): rename prod_ext and dpair_ext to prod.eta and sigma.eta 
Reason: they will be generated automatically by definitional package.
 2014-11-03 08:29:05 -08:00
Leonardo de Moura
8d3e9fdc20 refactor(library/data/nat/basic): remove unnecessary {} 2014-10-31 09:49:45 -07:00
Leonardo de Moura
8a4d4409cd feat(frontends/lean/calc_proof_elaborator): add '{...⁻¹}' if needed in calc proofs, closes #268 
This commit also simplifies library/data/nat/basic.lean
 2014-10-31 01:02:49 -07:00
Leonardo de Moura
5f23179388 refactor(library/data/nat): remove unnecessary ! and eq.symm 
The calc command automatically adds them now.
 2014-10-30 23:28:35 -07:00
Leonardo de Moura
09c6c05e26 chore(library/data/quotient): replace 'let' with 'have' and cleanup 2014-10-30 18:44:05 -07:00
Leonardo de Moura
407e35692b feat(frontends/lean/calc): wrap calc proofs with 'proof-qed' annotation to identify places where proof influences what is being proved 
Later, we will add a custom annotation and elaborator for calc proofs.
This is the first step for issue #268.

Remark: we don't wrap the proof if it is of the form

   - `by tactic`
   - `begin tactic-seq end`
   - `{ expr }`
 2014-10-30 18:33:47 -07:00
Leonardo de Moura
ea739100b3 fix(library/unifier): broken optimization in the unifier 
See new comments and tests for details.
 2014-10-28 16:09:41 -07:00
Leonardo de Moura
777aa63660 fix(kernel/inductive): relax eliminator generation rules for empty types 
This commit also removes the workaround false.rec_type. It is not needed anymore
 2014-10-28 10:31:00 -07:00
Leonardo de Moura
aafdbf57f0 fix(library/data/unit): missing file 2014-10-25 18:34:41 -07:00
Leonardo de Moura
c7f6a6b94e feat(library/definitional/cases_on): automatically add 'cases_on' 2014-10-25 17:22:02 -07:00
Leonardo de Moura
758a17ab23 refactor(library/data/unit): break unit.lean into smaller pieces 
The unit datatype is used by automation.

We want to be able to access its declaration without having to access
all dependencies (e.g., decidable, subsingleton, inhabited, ...).

This is *not* an optimization, but a way to make sure we can "import" unit
before we import other declarations.
 2014-10-25 14:57:33 -07:00
Leonardo de Moura
354b50a1f5 refactor(library/data/unit): make unit universe polymorphic 
Motivation: we need it for "padding".
Example 1: defining a n-ary tuple type.
Example 2: defining cases-on for mutually recursive datatypes
 2014-10-25 13:55:03 -07:00
Leonardo de Moura
cdcde661ef feat(library/definitional/induction_on): automatically add 'induction_on' 2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8 feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes 2014-10-25 13:08:59 -07:00
Soonho Kong
51125c1577 fix(library/data/quotient/default.lean): remove classical 2014-10-24 07:41:29 -07:00
Leonardo de Moura
e24225fabf feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations 2014-10-21 15:39:47 -07:00
Leonardo de Moura
6c7e23ecaa refactor(library): use 'reserve' notation in the standard library 2014-10-21 15:39:47 -07:00
Leonardo de Moura
2e9141b7e1 refactor(library): remove unnecessary :max hack in notation declarations 
This hack is not needed anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-10-20 18:45:52 -07:00
Leonardo de Moura
854e72e665 refactor(library/data/list): minimize dependencies and avoid 'sorry' warning 2014-10-20 15:32:42 -07:00
Leonardo de Moura
f63d47fef3 feat(frontends/lean/pp): support foldl/foldr notation in the pretty printer 2014-10-19 11:16:24 -07:00
Leonardo de Moura
85339c0cc1 fix(library/data/list/basic): mark :: as infixr 2014-10-19 08:58:52 -07:00
Leonardo de Moura
5c1d5133dd fix(library/data/prod): make the notation for tuples and product types consistent 2014-10-13 06:48:37 -07:00
Leonardo de Moura
a26618e0f2 feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied 2014-10-12 13:06:00 -07:00
Leonardo de Moura
d6d0593afb refactor(library): remove some unnecessary sections 2014-10-10 16:33:58 -07:00
Leonardo de Moura
8f1b6178a7 chore(*): minimize the use of parameters 2014-10-09 07:13:06 -07:00
Floris van Doorn
ae3419f82f feat(library): add definition of subsingleton and some other minor changes 2014-10-08 23:14:44 -07:00
Leonardo de Moura
c9e5e40477 refactor(library/data/num): cleanup 2014-10-05 13:47:51 -07:00
Leonardo de Moura
86591c7272 refactor(library/data/prod): cleanup 2014-10-05 13:38:08 -07:00
Leonardo de Moura
d56266c524 refactor(data/sum): use sections 2014-10-05 13:20:04 -07:00
Leonardo de Moura
15779c5d1e refactor(data/list): use '!' operator, and new name convention for declaration names 2014-10-05 13:10:35 -07:00
Leonardo de Moura
efaeeb0726 refactor(data/nat/sub): use new policy for marking implicit arguments and '!' operator 2014-10-05 12:39:13 -07:00
Leonardo de Moura
fa96596bf7 refactor(data/int/order): use '!' operator 2014-10-05 11:44:18 -07:00
Leonardo de Moura
a0d4d82f3f refactor(data/nat/order): use new policy for marking implicit arguments and '!' operator 2014-10-05 11:36:39 -07:00
Leonardo de Moura
73aa024c31 refactor(library/logic): remove 'core' subdirectory 2014-10-05 10:50:13 -07:00
Leonardo de Moura
317e910054 refactor(library/data/bool): use new style 2014-10-05 09:50:55 -07:00
Leonardo de Moura
4946f55290 refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-10-02 17:55:34 -07:00
Leonardo de Moura
d42fd657fe refactor(library): is_inhabited "theorems" should be "definitions", they are "data" 2014-10-02 09:00:34 -07:00
Leonardo de Moura
153e3927ac feat(frontends/lean/elaborator): modify '!' semantics: it stops consuming arguments as soon it finds an argument that does not occur in the rest of the type. 2014-10-01 18:50:17 -07:00
Leonardo de Moura
e64d5c4a4a refactor(library/data/nat): use new operator '!' 2014-10-01 18:39:47 -07:00
Leonardo de Moura
a978e30c81 refactor(library/data/nat): rename to_nat to of_num 2014-10-01 17:52:33 -07:00
Leonardo de Moura
716cd4d651 refactor(library): rename namespace eq_ops to eq.ops 2014-10-01 17:51:17 -07:00
Leonardo de Moura
bc6ebf34be feat(library/data/bool): do not use ! as notation for bnot, rename band/bor -> and/or 2014-10-01 17:00:03 -07:00
Leonardo de Moura
3657d4c3ab feat(frontends/lean): coercion num -> int even when nat is not open, closes #219 
I also had to mark the coercions as reducible.
Otherwise, given the constraint

          ?M (int.of_num 0) =?= (int.of_nat (nat.to_nat 0))

the unifier will not generate the solution

          ?M := fun x, x
 2014-10-01 11:09:10 -07:00
Leonardo de Moura
3ca1264f61 refactor(library): mark 'decidable' theorems as definitions 
If we don't do that, then any 'if' term that uses one of these theorems
will get "stuck". That is, the kernel will not be able to reduce them
because theorems are always opaque
 2014-09-30 09:02:37 -07:00
Floris van Doorn
3a95734fae feat(library): changes in eq.lean sigma.lean and category.lean 
in eq.lean, make rec_on depend on the proof, and add congruence theorems for n-ary functions with n between 2 and 5
in sigma.lean, finish proving equality of triples
in category.lean, define the functor category, and make the proofs of the arrow and slice categories easier for the elaborator
 2014-09-26 19:45:23 -04:00
Floris van Doorn
05fb3aa060 feat(library/data/int): remove duplicate theorem, fix one sorry 2014-09-26 19:45:23 -04:00
Floris van Doorn
5396e422d2 feat(library): add constructions of categories, some changes in eq, sigma and path 
in eq, add theorem for proof irrelevance and congruence for binary functions
in sigma, add some support for triplets
in path, comment out two unneccesary definitions
in category, add Cat, slice, coslice, product and arrow categories, also add fully bundled approach
 2014-09-26 19:45:23 -04:00
Leonardo de Moura
86f06a54ea refactor(library/data/vector): rename 'vec' to 'vector' 2014-09-19 16:20:50 -07:00
Leonardo de Moura
e430dc8bab feat(frontends/lean): add 'irreducible' as syntax sugar for 'reducible [off]' 2014-09-19 15:54:32 -07:00
Leonardo de Moura
4e2377ddfc refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
5d8c7fbdf1 refactor(frontends/lean): replace '[private]' modifier with 'private 
definition' and 'private theorem', '[private]' is not a hint.
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
97b1998def refactor(frontends/lean): replace '[opaque]' modifier with 'opaque 
definition', '[opaque]' is not a hint, but a kind of definition
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
08ccd58eb6 feat(frontends/lean): add 'reducible' modifier for controlling which 
definitions are unfolded during elaboration

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
baf4c01de8 feat(frontends/lean): definitions are opaque by default 2014-09-19 15:54:32 -07:00
Leonardo de Moura
93c2c30310 feat(frontends/lean): allow transient coercions, i.e., coercions that 
are not saved in .olean files
 2014-09-19 15:54:32 -07:00
Leonardo de Moura
e3e2370a38 feat(frontends/lean): split 'opaque_hint' command into 'opaque' and 'transparent' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-16 18:03:40 -07:00
Jeremy Avigad
74cb289d48 refactor(library): rename algebra directory to struc, move categories.lean to algebra 2014-09-16 13:13:01 -07:00
Jeremy Avigad
9988914189 refactor(library/logic): move files in classes directory to core 2014-09-16 13:13:01 -07:00
Leonardo de Moura
7ea6a17ae8 feat(library/data/num): add 'mul' and 'add' for binary numerals 2014-09-16 08:05:00 -07:00
Leonardo de Moura
8e52c478b1 refactor(library/data/num): add 'succ', 'pred' and 'size' (aka number of bits), 
rename is_inhabited theorems
 2014-09-15 16:05:17 -07:00
Leonardo de Moura
b7023ce1d8 fix(frontends/lean/placeholder_elaborator): do not truncate stream of 
solutions during class-instance resolution, closes #183

For example, in theorem inverse_unique at category.lean, implicit
arguments are synthesized for inverse_compose. The first solution H' is
not good, and produces a type incorrect solution
 2014-09-12 16:12:23 -07:00
Leonardo de Moura
a305012ce5 fix(library/data/category): mark definitions as abbreviations 2014-09-12 09:28:33 -07:00
Leonardo de Moura
c8e20ff3c0 fix(library/data/category): minor problem that was being masked by bug #182, fixes #183 2014-09-11 16:58:32 -07:00
Floris van Doorn
7f1977694f feat(library/data/category.lean) the definition of category doesn't depend on 'mor' anymore; make iso a class; add theorems 2014-09-11 16:39:47 -07:00
Leonardo de Moura
7ffe73b8ca fix(frontends/lean): name clash inside section, fixes #181 2014-09-11 16:37:23 -07:00
Leonardo de Moura
8c11dc1ecd chore(library/data/quotient): rename aux.lean to util.lean (fix problem with cloning lean repository on Windows machine) 
See
http://stackoverflow.com/questions/3689137/error-git-checkout-index-unable-to-create-file
for additional details
 2014-09-11 14:57:15 -07:00
Leonardo de Moura
746f5bff0d refactor(library/data/list/basic): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-10 16:42:49 -07:00
Leonardo de Moura
1a896a670c refactor(library/data/list): cleanup, rename concat to assoc 2014-09-10 08:02:18 -07:00
Leonardo de Moura
9b9adf8831 refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
Leonardo de Moura
ff9a07500d feat(library/data/int/basic): create alias for int.int 2014-09-09 14:03:44 -07:00
Leonardo de Moura
b4793df653 feat(frontends/lean): rename '[fact]' to '[visible]' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-08 07:47:42 -07:00
Leonardo de Moura
35e68fea76 feat(library/logic/classes/decidable): generalize 'by_cases' theorem 2014-09-08 00:16:20 -07:00
Leonardo de Moura
fa25ddc8e6 chore(library/data/int/basic): remove unnecessary 'hinding' clause 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-07 22:50:43 -07:00
Leonardo de Moura
559dd586f2 feat(library): add 'decidable_eq' class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-07 22:23:36 -07:00
Leonardo de Moura
c446327ec3 feat(library/data/list): add mem_is_decidable and not_mem_find theorems 2014-09-07 21:22:07 -07:00
Leonardo de Moura
f9b62c53e6 feat(library/data/nat): add nat.is_inhabited theorem 2014-09-07 19:59:34 -07:00
Leonardo de Moura
4e2f5572f3 feat(library/data/vector): add vec.is_inhabited theorem 2014-09-07 19:08:31 -07:00
Leonardo de Moura
c378a58cc2 feat(frontends/lean): add [class] modifier for inductive datatypes as a shortcut for 'class' command. 2014-09-07 18:16:33 -07:00
Leonardo de Moura
bbff564a1c feat(frontends/lean): persistent notation in sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-06 11:14:20 -07:00
Floris van Doorn
02d72e4c40 feat(library/data/category): add vector 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-05 09:57:04 -07:00
Floris van Doorn
e9fc4f14a0 feat(library/data/category): add category theory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-05 09:56:57 -07:00
Floris van Doorn
d2a4bb8a27 feat(library/data/empty): add false.to_empty and false.rec_type theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-05 09:31:27 -07:00
Leonardo de Moura
561753e7f1 refactor(library/data/sigma): cleanup module 2014-09-05 08:01:24 -07:00
Leonardo de Moura
9412e604c8 refactor(library/data): cleanup datatypes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 22:31:52 -07:00
Leonardo de Moura
6632a50015 refactor(library): add namespaces 'or', 'and' and 'iff' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 21:25:21 -07:00
Leonardo de Moura
68d9bef860 refactor(library): add 'eq' and 'ne' namespaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 18:41:06 -07:00
Leonardo de Moura
2bc6f92d33 refactor(library): add 'and' namespace 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 17:44:53 -07:00
Leonardo de Moura
364bba2129 feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 17:26:36 -07:00
Leonardo de Moura
8743394627 refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-04 15:04:57 -07:00
Leonardo de Moura
7500761114 refactor(library/data/nat/basic): remove unnecessary nat_ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-03 16:14:29 -07:00
Leonardo de Moura
e51c4ad2e9 feat(frontends/lean): rename 'using' command to 'open' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-03 16:00:38 -07:00
Leonardo de Moura
f891485a26 refactor(library): use '[protected]' modifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-03 15:13:03 -07:00
Leonardo de Moura
6077b3158c fix(library): remove unnecessary [fact] modifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-02 16:06:55 -07:00
Leonardo de Moura
8dec18018c refactor(library/data/list): avoid placeholders '_', make first argument of false_elim implicit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-01 19:44:04 -07:00
Leonardo de Moura
aace5c37cd refactor(library/data/subtype): elaborator does not need help anymore (i.e., 'show'-expression) for this file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-01 19:04:15 -07:00
Leonardo de Moura
b43313ec43 fix(library/nat/div): remove unnecessary '_''s 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 17:40:57 -07:00
Jeremy Avigad
8094884c85 feat(library/data/nat/div.lean): remove dependence on funext 2014-08-28 17:37:32 -07:00
Leonardo de Moura
b51fa2b547 chore(library): minor cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 13:04:17 -07:00
Leonardo de Moura
d536475e49 refactor(library): more implicit_args for: and_assoc, and_comm, or_assoc, or_comm, if_pos, if_neg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 11:10:04 -07:00
Leonardo de Moura
6b7e79b62f feat(library/data/nat): mark more arguments implicit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 10:38:58 -07:00
Jeremy Avigad
00a049a667 refactor(library/logic): rename connectives -> core, basic -> connectives 2014-08-27 18:43:24 -07:00
Leonardo de Moura
2d78387541 refactor(library/logic/basic): rename absurd_elim to absurd, delete contrapos and trivial_not_true theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-27 18:34:09 -07:00
Leonardo de Moura
a8d58fdd33 refactor(library): mark absurd_elim argument as implicit 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-26 18:27:39 -07:00
Leonardo de Moura
44c597724b fix(frontends/lean): fail if theorem type has metavariables after type elaboration (and before proof elaboration) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-26 09:01:17 -07:00
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
dbaf81e16d refactor(library): remove unnecessary 'standard' subdirectory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:08:09 -07:00