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
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
Jakob von Raumer
25a5e29b7c
chore(hott) delete old hott lib
2014-12-16 13:11:32 -08:00
Leonardo de Moura
8ad9b84c85
feat(init): reserve notation for "not in"
2014-12-15 19:22:17 -08: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
2b56a2b891
feat(library/init): create markdown directory file
2014-12-15 16:43:42 -05:00
Jeremy Avigad
da719e6ee4
refactor(library/logic): rename theorems
2014-12-15 16:13:04 -05:00
Jeremy Avigad
3e9a484851
refactor(library/logic/connectives): rename theorems
2014-12-15 15:05:44 -05:00
Leonardo de Moura
7c8ab81cc6
feat(library/logic/quantifiers): add decidable_forall_eq and decidable_exists_eq theorems
2014-12-13 15:48:04 -08: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
6e84696960
fix(library/init/logic): expose inhabited basic instances
2014-12-13 14:26:44 -08:00
Leonardo de Moura
628faa10eb
refactor(library/algebra/ordered_ring): add workarounds to improve performance
2014-12-13 13:12:25 -08:00
Jeremy Avigad
6f775be1b6
feat(library/algebra/ordered_ring): start on ordered_ring, and minor changes elsewhere
2014-12-13 11:35:35 -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
d50b7a8ba1
refactor(library/init/logic): move theorems to logic/cast
2014-12-12 12:39:16 -08:00
Leonardo de Moura
b900e9171d
refactor(library/init/sigma): simplify lex.accessible proof using 'cases' tactic
2014-12-12 12:36:51 -08:00
Leonardo de Moura
b01cf73a91
feat(library/init/logic): add is_true and is_false
2014-12-11 18:14:03 -08:00
Leonardo de Moura
97552a8cfe
refactor(library/sigma): fix/use sigma notation
2014-12-11 15:50:44 -08:00
Floris van Doorn
fec45abda5
feat(library/hott): multiple changes in the HoTT library
...
Jakob accidentally undid some of my changes in commit aad4592
, reverted that;
made style changes in multiple files;
in types/sigma: finished porting Coq-HoTT, and finished unfinished proof;
in axioms/funext: rename path_forall, make arguments implicit and make instance visible
2014-12-09 21:32:35 -05:00
Jakob von Raumer
5278f70dea
feat(library/lean) add one types as instances of groupoids
2014-12-09 19:12:54 -05:00
Jakob von Raumer
86a38c6c3d
feat(library/hott) prove that each group is a contractible groupoid
2014-12-09 19:12:54 -05:00
Jakob von Raumer
f023e4999c
feat(library/hott) prove that a groupoid on contractible object type is a group
2014-12-09 19:12:54 -05:00
Jakob von Raumer
7bfd897f9d
feat(library/hott) add groupoid definition
2014-12-09 19:12:54 -05: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
Jakob von Raumer
116e7ff82e
feat(library/hott) port Jeremy's group file to use path equality
2014-12-09 10:00:37 -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
Jakob von Raumer
133f935fce
fix(library/hott): issues resulting from merge
2014-12-05 22:21:49 -08:00
Jakob von Raumer
7c1b75c818
feat(library/hott): add proof that the type of nat trafos is a set
...
The characteriszation of nat trafo by sigma types up to equivalence is still to be done (two unsuccessful proof attempts included)
2014-12-05 22:21:36 -08:00
Jakob von Raumer
cc2de8a8d9
feat(library/hott): complete proof that object types of proper hott categories are one truncated
2014-12-05 22:21:31 -08:00
Jakob von Raumer
aad4592cad
feat(library/hott): complete theorems about truncatedness of isomorphism sets
2014-12-05 22:21:26 -08:00
Jakob von Raumer
5923392395
chore(library/hott): make precategory use the isomorphic structure
2014-12-05 22:21:21 -08:00
Jakob von Raumer
63afac301c
chore(library/hott): turn isomorphic into structure
2014-12-05 22:21:16 -08:00
Jakob von Raumer
dbce41114a
feat(library/hott): add definition of category
2014-12-05 22:21:12 -08:00
Jakob von Raumer
39ba9429f5
chore(library/hott): make constructions.lean compile, still lots of work to do
2014-12-05 22:21:06 -08:00
Jakob von Raumer
91862926e3
chore(library/hott): change precategory to structure, fix morphism.lean
2014-12-05 22:20:57 -08:00
Jakob von Raumer
6124b87870
fix(library/hott): adjust expliciteness of arguments
2014-12-05 22:20:51 -08:00
Jakob von Raumer
cda828bfe8
chore(library/algebra): change category to be a structure
2014-12-05 22:20:46 -08:00
Jakob von Raumer
b37a77d25e
chore(library/hott): move precategory definition to its own folder
2014-12-05 22:20:40 -08:00
Jakob von Raumer
9631c6b1a1
feat(library/hott): add iso_of_path lemma for precategories
2014-12-05 22:20:33 -08:00
Jakob von Raumer
a1b468d104
feat(library/hott): port a part of algebra/category/constructions.lean, slice category still to do
2014-12-05 22:20:25 -08:00
Jakob von Raumer
67f71ee376
feat(library/hott): finish porting of natural_transformation.lean
2014-12-05 22:20:18 -08:00
Jakob von Raumer
ae618c20fb
fix(library/hott): finish associativity proof
2014-12-05 22:20:11 -08:00
Jakob von Raumer
d8e2206bbc
feat(library/hott): try to replace the proof irrelevance
2014-12-05 22:19:50 -08:00
Jakob von Raumer
5fe8ee606f
feat(library/hott): port Floris' category implementation
2014-12-05 22:19:26 -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
Floris van Doorn
e52157a8ea
feat(hott/types): start characterization of pi-types and W-types
2014-12-03 20:29:16 -08:00
Floris van Doorn
2913035a61
style(hott/types): some style fixes in prod and sigma
2014-12-03 20:29:16 -08:00
Floris van Doorn
ff5e3d4403
style(hott/path): indent within namespace, add variables
2014-12-03 20:29:16 -08:00
Floris van Doorn
4b799a9da4
fix(hott/trunc): add explicit coercion so that the notation works if nat is not opened
2014-12-03 20:29:16 -08:00
Floris van Doorn
b62b4754cb
feat(library/algebra): modify categories to use definitions, prove basic theorems about discrete categories
2014-12-03 20:29:16 -08:00
Leonardo de Moura
811bc6a31f
feat(library/init/measurable): add 'measurable' type class
2014-12-03 18:54:24 -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
fca97d5bb2
feat(library/definitional): add brec_on construction, closes #272
2014-12-03 10:39:32 -08:00
Jeremy Avigad
57effaf1a9
refactor(library/algebra): use new naming conventions, add information to speed up proofs
2014-12-02 12:14:14 -08:00
Jeremy Avigad
1bffd8dd21
refactor(library/algebra/order): change strong order pair, adopt new naming conventions
2014-12-02 12:14:14 -08:00
Leonardo de Moura
73429547ba
fix(init/reserved_notation): remove "invisible" character at \/
2014-12-02 12:06:39 -08:00
Leonardo de Moura
06f436840f
fix(library/unifier): postpone class-instance constraints whose type could not be inferred
2014-12-01 22:27:23 -08:00
Leonardo de Moura
e6672b958f
fix(library/tactic/inversion_tactic): add missing case
2014-12-01 19:11:44 -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
5d4b6a3de2
chore(library/logic/logic.md): adjust documentation
2014-11-30 21:19:56 -08:00
Leonardo de Moura
697d4359e3
refactor(library): add 'init' folder
2014-11-30 20:34:12 -08:00
Leonardo de Moura
8dfd22e66c
feat(frontends/lean): add 'prelude' command, and init directory
2014-11-30 17:03:08 -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
f24eed50af
refactor(library/logic/heq): minor change
2014-11-30 13:52:34 -08:00
Leonardo de Moura
c08f4672e4
feat(library/tactic): add 'assert' tactic, closes #349
2014-11-29 21:34:49 -08:00
Leonardo de Moura
1a7dd56f0f
fix(library/tools/tactic): 'cases' argument precedence
2014-11-29 21:03:45 -08:00
Leonardo de Moura
f51fa93292
feat(library/tactic): add 'fapply' tactic, closes #356
2014-11-29 19:20:41 -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
bed9467315
chore(library/hott/trunc): remove set_option
2014-11-29 08:55:47 -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
a9001166fd
fix(library/algebra/category/morphism): remove sorry that was introduced by accident
2014-11-28 22:54:15 -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
7571f50870
feat(library/binary, library/relation): introduce general properties for binary operations and relations
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
58e325f0af
feat(library/algebra): add to developments of group, ordered_group, and ring
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
Jakob von Raumer
7c81044a99
chore(library/hott) change is_pointed to structure
2014-11-28 22:50:43 -08:00
Jakob von Raumer
0417c21bbb
chore(library/hott) change naming in equiv_precomp
2014-11-28 22:50:43 -08:00
Jakob von Raumer
4587e46c67
chore(library/hott) change naming to leo's naming proposal
2014-11-28 22:50:43 -08:00
Jakob von Raumer
7374149758
chore(library/hott) change equiv.lean to use structures and more typeclass inference
2014-11-28 22:50:43 -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
e0debca771
feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses
2014-11-28 22:25:37 -08:00