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
28c63e685b
feat(frontends/lean): add '[local]' notation, closes #322
2014-11-16 21:15:04 -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
e81d9c9184
perf(kernel/level): apply two simple normalization rules at mk_max
...
They are variations of:
max l1 (max l1 l2) == (max l1 l2)
2014-11-16 18:16:57 -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
a171f8fbc3
test(tests/lean/run): simple diag for square matrices
2014-11-15 18:49:17 -08:00
Leonardo de Moura
1b95b69251
test(tests/lean/run): define subterm relation for vectors
2014-11-15 16:17:51 -08:00
Leonardo de Moura
ea640257bf
feat(frontends/lean/structure_cmd): generate no_confusion for structures too
2014-11-15 16:00:09 -08:00
Leonardo de Moura
b87559dac5
test(tests/lean/run): define subterm relation for trees by hand
2014-11-15 13:29:23 -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
8b659ae679
fix(util/lean_path): change the default LEAN_PATH, a file in the current directory cannot shadow a library file, fixes #321
2014-11-14 17:23:09 -08:00
Leonardo de Moura
7685516d1e
feat(frontends/lean): better default for atomic notation
2014-11-14 16:25:13 -08:00
Leonardo de Moura
67de3b06f3
feat(kernel/level): improve universe level pretty printer
...
Example: produce `l+2` instead of `succ (succ l)`.
2014-11-14 14:51:03 -08:00
Leonardo de Moura
00df34a1c4
feat(library/unifier): generalize method process_succ_eq_max_core
2014-11-14 14:25:41 -08:00
Leonardo de Moura
ffffabad95
feat(kernel/level): improve is_geq procedure for universe levels
...
Now, it also returns true for
(succ^k1 a) =?= k2
where k1 >= k2
2014-11-14 14:20:35 -08:00
Leonardo de Moura
488f989c46
fix(frontends/lean/inductive_cmd): generate error for inductive datatype declarations that will produce an eliminator that can only eliminate to Prop
2014-11-14 13:57:42 -08:00
Leonardo de Moura
e7a7458922
feat(library/general_notation): reserve unary minus
2014-11-13 22:08:20 -08:00
Leonardo de Moura
58525905d0
fix(frontends/lean/notation_cmd): bugs in 'reserve notation' command
2014-11-13 22:05:55 -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
51719145f9
feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2)
2014-11-12 17:28:33 -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
97609d1625
test(tests/lean/run/nateq): add example that triggered previous modification
2014-11-12 15:11:08 -08:00
Leonardo de Moura
b07b82cf43
fix(library/definitional): marking cases_on and rec_on as reducible
...
The idea is to avoid counter-intuitive behavior
2014-11-12 15:03:30 -08:00
Leonardo de Moura
858538a329
refactor(library/definitional): add new to_telescope procedure, and remove code duplication in no_confusion.cpp
2014-11-12 13:31:31 -08:00
Leonardo de Moura
a3066e3eaa
fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator
2014-11-12 13:10:19 -08:00
Leonardo de Moura
b4c37d180b
refactor(library/definitional): add some helper functions
2014-11-12 12:24:22 -08:00
Leonardo de Moura
463e70332d
test(tests/lean/run): define brec_on and binduction_on for a reflexive type
...
We say an inductive type T is reflexive if it contains at least one constructor that
takes as an argument a function returning T.
For reflexive types it doesn't seen to be possible to define a single
brec_on that can eliminate to Type.{>=1} and Prop.
The universe level expressions get too complicated.
Even if we extend the universe constraint solver in the kernel, the
additional complexity might be a problem.
We workaround this issue by defining two versions of brec_on:
- One (brec_on) that eliminates to Type.{>=1}, and
- binduction_on that eliminates to Prop.
For non-reflexive types, we can combine both of them.
2014-11-12 10:52:32 -08:00
Leonardo de Moura
5312afa7ec
feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes
...
The new test contains examples that required explicit levels.
2014-11-12 10:52:32 -08:00
Leonardo de Moura
ef5a3e83ad
feat(library/data/vector): expand 'vector' module
2014-11-11 22:33:47 -08:00
Leonardo de Moura
faf90c4b87
test(tests/lean/run): test brec_on on vectors
2014-11-11 17:23:59 -08:00
Leonardo de Moura
e2bfe6ee36
refactor(library/definitional/no_confusion): cleanup API
2014-11-11 16:12:44 -08:00
Leonardo de Moura
f6889951c6
fix(library/definitional/cases_on): bug in inductive datatypes with higher-order recursion
2014-11-11 15:14:08 -08:00
Leonardo de Moura
902a551048
feat(definitional/brec_on): add 'mk_below' skeleton
2014-11-11 14:55:21 -08:00
