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
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
Jakob von Raumer
fdafb1c11f
fix(library/hott) adapt trunc.lean to missing equiv coercion
2014-11-17 18:39:02 -08:00
Jakob von Raumer
59fbe8b53e
chore(library/hott) fix universe issue. note: this should be fixed when contr is not bound to universe level 1 anymore
2014-11-17 18:39:02 -08:00
Jakob von Raumer
992aad9661
feat(library/hott) postcomposition from ua lemma is done up to the last gap
2014-11-17 18:39:02 -08:00
Jeremy Avigad
4420f0dc0c
feat(library/algebra/group): add ordered semigroups
2014-11-17 18:32:14 -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
627c7cb531
chore(library/logic/wf): remove unnecessary :max
2014-11-14 17:37:05 -08:00
Jeremy Avigad
0d982cceed
feat(library/algebra/ring): begin theory of semirings and rings
2014-11-14 17:27:35 -08:00
Leonardo de Moura
e7a7458922
feat(library/general_notation): reserve unary minus
2014-11-13 22:08:20 -08:00
Jeremy Avigad
1ed7794264
feat(library/algebra/group): add theorems for calculation
2014-11-13 20:44:58 -08:00
Jakob von Raumer
e740fbe8c4
chore(library/hott) remove hott.axoims.ua from imports of funext_from_ua.lean
2014-11-13 20:43:46 -08:00
Jakob von Raumer
b514a978b2
fix(library/hott) changed pointed.lean to use trunc.lean correctly
2014-11-13 20:43:46 -08:00
Jakob von Raumer
8dfa78e070
feat(library/hott) almost completed portin UnivalenceImpliesFunext.v
2014-11-13 20:43:46 -08:00
Jakob von Raumer
df4a8db23d
feat(library/hott) add to trunc.lean: contractible types are equivalent to unit
2014-11-13 20:43:46 -08:00
Jakob von Raumer
3ee703f5d5
feat(library/hott) Ported part of UnivalenceImpliesFunext.v
2014-11-13 20:43:46 -08:00
Jakob von Raumer
2ed7032997
chore(library/hott) cleaned up the proof a bit
2014-11-13 20:43:46 -08:00
Jakob von Raumer
b5d564431a
feat(library/hott) port the rest of Funext_Varieties.v
2014-11-13 20:43:46 -08:00
Jakob von Raumer
6296f8e092
feat(library/hott) port a good portion of FunextVarieties.v
2014-11-13 20:43:46 -08:00
Jakob von Raumer
be8c758be1
feat(library/hott) ported Pointed.v
2014-11-13 20:43:45 -08:00
Leonardo de Moura
edd04881ee
fix(library/logic): import prod and unit declarations in logic
...
Reason: we need them for automatically generating constructions needed
by the definitional package
2014-11-12 16:54:50 -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
9c93816211
chore(library/logic/wf): cleanup
2014-11-10 21:19:38 -08:00
Leonardo de Moura
4ebd3e2c27
feat(library/logic/wf): transitive closure of a well-founded relation is well-founded
2014-11-10 21:07:28 -08:00
Leonardo de Moura
22b7a0615f
fix(frontends/lean): coercion affects other modules
2014-11-10 20:14:19 -08:00
Leonardo de Moura
64043094f4
feat(library/logic/wf): some basic definitions for constructing well_founded relations
2014-11-10 17:57:55 -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
107a9cf8e4
feat(library): port more of truncation library from Coq HoTT
...
Everything directly about truncations in the basic truncation library is ported.
Some theorems about other structures still need to be ported.
Also made some minor changes in hott.equiv
2014-11-08 19:12:54 -08:00
Floris van Doorn
780e949992
feat(empty): define negation of types
2014-11-08 19:12:54 -08:00
Floris van Doorn
bf27a17dec
style(library): add some comments
2014-11-08 19:12:54 -08:00
