Floris van Doorn
74779dd855
feat(hott/trunc): clean up some theorems, prove some basic theorems
2014-11-08 19:12:54 -08:00
Floris van Doorn
08c56188b6
feat(library/hott/trunc): prove that n-types are (n+1)-types.
2014-11-08 19:12:54 -08:00
Jeremy Avigad
4a955c0f92
feat(library/algebra/order): begin theory of orders
...
feat(library/algebra/order): begin theory of orders
2014-11-08 19:07:59 -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
ad2ecfb7a8
refactor(library/logic/cast): move heq declaration to a separate module
...
heq is be needed for some automatically generated constructions.
So, we want it available with the least number of dependencies.
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
Jeremy Avigad
c28227d7a1
feat(library/algebra/group): add multiplicative and additive structures
2014-11-07 10:23:37 -08:00
Jeremy Avigad
05ec76185d
fix(library/hott/fibrant): set arguments for type class resolution
2014-11-07 10:23:37 -08:00
Leonardo de Moura
92b0a538c5
refactor(library/logic/wf): add well_founded class, and cleanup file
2014-11-07 10:18:24 -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
85d0521d48
feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305
2014-11-06 21:34:05 -08:00
Jakob von Raumer
754901cf64
fix(library/hott) make universe index in ua.lean variable
2014-11-06 20:02:10 -05:00
Jakob von Raumer
b8ec1a1649
chore(library/hott) cleanup
2014-11-06 19:41:08 -05:00
Jakob von Raumer
f1cc0c4bd8
chore(library/hott) add note referring to missing substitution lemma
2014-11-06 19:27:27 -05:00
Jakob von Raumer
7dbd7b31f6
Added substitution lemma for equivalence calculations
2014-11-06 19:22:57 -05:00
Jakob von Raumer
fa9cbb1f6a
chore(library/hott) adapted univalence axiom to suit notation in book and def in Coq.
2014-11-06 19:22:57 -05:00
Jakob von Raumer
d842be9c52
feat(library/hott) add univalence axiom
2014-11-06 19:22:57 -05:00
Jakob von Raumer
28d1c6c5e4
chore(library/hott) move function extensionality into new axioms folder, adjust file(s) using it
2014-11-06 19:22:57 -05:00
Jakob von Raumer
9ad75108a3
chore(library/hott) clean up file and add class inference
2014-11-06 15:57:30 -08:00
Jakob von Raumer
1f5be44f51
chore(library/hott) clean up Equiv namespace
2014-11-06 15:57:30 -08:00
Jakob von Raumer
8e1949e9aa
feat(library/hott) add calc environment for equivalences
2014-11-06 15:57:29 -08:00
Jakob von Raumer
c50db9899d
feat(library/hott) add thm: to give a section of a fibration it suffices to provide it for the image of an equivalence
2014-11-06 15:57:29 -08:00
Leonardo de Moura
781f709bb4
feat(library/logic): import wf.lean in logic/default.lean
...
We will use well-founded recursion in the definitional package
2014-11-06 15:03:13 -08:00
Leonardo de Moura
194247f75b
refactor(library/logic/wf): minimize dependencies
2014-11-06 14:59:03 -08:00
Leonardo de Moura
b177c84b06
feat(library/logic): add well-founded recursion
...
It also removes the old well-founded induction theorem based on
classical principles
2014-11-06 14:49:53 -08:00
Leonardo de Moura
d306c42a1f
refactor(library/logic): cleanup some of the proofs in cast.lean, remove piext axiom
...
Remark: the main motivation for piext was Lean 0.1 simplifier.
We are using a different approach in Lean 0.2.
The axiom is not needed anymore.
It is also not used in any part of the standard library
2014-11-05 16:43:31 -08:00
Jakob von Raumer
09b533a965
fix(library/hott) rename IsEquiv.ap to IsEquiv.ap_closed to avoid name clashes
2014-11-05 15:14:14 -08:00
Jakob von Raumer
02abc5c2ad
chore(library/hott) fixed the copyright in equiv_precomp.lean
2014-11-05 15:14:14 -08:00
Jakob von Raumer
807224f3c1
chore(library/hott) cleaned up the proof a bit
2014-11-05 15:14:14 -08:00
Jakob von Raumer
2712b9b18f
feat(library/hott) add theorem: if f is an equivalence, so is ap f
2014-11-05 15:14:14 -08:00
Jakob von Raumer
588ad210a2
feat(library/hott) add theorem: assuming function extensionality, precomposing and postcomposing of equivalences is an equivalence
2014-11-04 18:47:34 -08:00
Jakob von Raumer
efa33c5b52
chore(library/hott) move theorem about precomposition to its own file
2014-11-04 18:47:34 -08:00
Jakob von Raumer
0ed046ed80
fix(library/hott) fix funext.lean by making funext an instance
2014-11-04 18:47:34 -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
795f664964
fix(library/hott/funext): compilation error
2014-11-04 06:53:21 -08:00
Jakob von Raumer
261f8a014a
feat(library/hott) use class inference for IsEquiv
2014-11-04 06:49:42 -08:00
Jakob von Raumer
479eabb416
feat(library/hott) add: if precompositions with f are equivalences, then f is
2014-11-04 06:49:42 -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
4bdee07af2
refactor(library/algebra/category/basic): use calc assistant
2014-10-31 09:49:45 -07: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
591e566472
feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator
...
This is part of #268
2014-10-30 23:24:09 -07:00
