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
Leonardo de Moura
c2602baf2b
feat(library/tools/tactic): add 'cases' alias for 'inversion' tactic
2014-11-28 19:33:11 -08:00
Leonardo de Moura
ebd320a6b3
feat(library/tactic): add first step of 'inversion' tactic
2014-11-26 21:28:00 -08:00
Leonardo de Moura
f7deabfd19
feat(library/rename): add notation for rename
2014-11-26 19:02:11 -08:00
Leonardo de Moura
e55397d422
feat(library/tactic): add 'clears' and 'reverts' variants
2014-11-26 14:49:48 -08:00
Leonardo de Moura
2bd8f969d5
feat(library/tactic): add 'revert' tactic, closes #346
2014-11-26 14:23:42 -08:00
Leonardo de Moura
df51ba8b7c
feat(library/definitional/projection): use strict implicit inference, closes #344
2014-11-25 18:04:06 -08:00
Jakob von Raumer
53d66c91fc
chore(library/hott) made ua_implies_funext a class instance
2014-11-23 17:43:55 -08:00
Jakob von Raumer
757cdcb130
feat(library/hott) funext from ua now with arbitrary universe levels for funext!
2014-11-23 17:43:55 -08:00
Jakob von Raumer
228205634d
chore(library/hott) make funext more general
2014-11-23 17:43:55 -08:00
Jakob von Raumer
12429c93c8
fix(library/hott) fix equiv_precomp, doesn't look nice now
2014-11-23 17:43:55 -08:00
Jakob von Raumer
1f6b6ff8e6
chore(library/hott) adjust funext_from_ua.lea to typeclass axioms
2014-11-23 17:43:55 -08:00
Jakob von Raumer
2d9621892b
fix(library/hott) fill both gaps (I don't know why it works that way), change name from funext.apply to funext.ap, since apply seems to be a tactic name?
2014-11-23 17:43:55 -08:00
Jakob von Raumer
fd47a162de
chore(library/hott) adapted theories to typeclass axioms
2014-11-23 17:43:55 -08:00
Jakob von Raumer
d8d2ea998d
feat(library/hott) change axioms to Leo's axioms-as-typeclass proposal
2014-11-23 17:43:55 -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
Leonardo de Moura
13fba433b0
feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327
2014-11-23 17:30:22 -08:00
Floris van Doorn
3523a70b4c
fix(hott/path): make recursion-like definitions reducible
2014-11-22 17:44:13 -08:00
Floris van Doorn
e97b0b4e8e
feat(hott/types): port more of the sigma library from Coq
...
prove theorems about interaction of sigma types and n-types, including the fact that sigmas preserve n-types
2014-11-22 17:44:12 -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
24e35a9f2c
fix(hott/trunc): comment out sorry
2014-11-22 17:44:12 -08:00
Floris van Doorn
bc807212ac
feat(hott/path): add notation for higher and dependent transports
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
faf736a9d2
feat(library/logic/default): add wf_k
2014-11-22 13:25:46 -08:00
Leonardo de Moura
a3daff702a
fix(library/logic/wf): typo
2014-11-22 13:25:46 -08:00
Leonardo de Moura
47b6cfb28d
feat(library/logic/if): add dependent if-then-else: dite
2014-11-22 09:56:32 -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
29a0d3109b
refactor(library/logic/connectives): mark theorems used to prove 'decidable' theorems as transparent
...
if we don't this, then 'if-then-else' expressions depending on theorems
such as 'and_decidable', 'or_decidable' will not compute inside the kernel
2014-11-22 09:32:43 -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
7c54dbce10
refactor(library/logic/if): mark basic theorem transparent
2014-11-22 00:19:05 -08:00
Leonardo de Moura
acf1c501ad
refactor(library/logic/prop): allow 'absurd' to generate Type
2014-11-22 00:19:05 -08:00
Leonardo de Moura
2e121182de
refactor(library/logic/decidable): rename decidable_rel -> decidable_pred, and decidable_rel2 -> decidable_rel
2014-11-21 11:49:31 -08:00
Jakob von Raumer
19d0afe160
feat(library/hott) completed the funext_from_ua proof with a somewhat restricted generality on universe levels
2014-11-21 10:46:16 -08:00
Jakob von Raumer
bc33af9f51
feat(library/hott) add universe polymorphism to paths, truncation, etc... get stuck at ua to funext proof anyway
2014-11-21 10:46:16 -08:00
Leonardo de Moura
47e3f0e770
fix(library/logic/wf_k): missing file
2014-11-21 10:03:20 -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
