Rob Lewis
6dfcc4610b
feat(data): update orderings on int and nat to conform to new algebraic hierarchy
2015-05-29 14:11:51 +10:00
Rob Lewis
4b67cd1f97
feat(library/algebra): update algebraic hierarchy to be more constructive
2015-05-29 14:11:50 +10:00
Leonardo de Moura
00232e70d6
feat(hott,library): auxiliary theorems for simplifier
2015-05-27 16:35:56 -07:00
Leonardo de Moura
85409a59d3
feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants
...
closes #511
2015-05-27 16:32:43 -07:00
Leonardo de Moura
dc6411b903
feat(library/inductive_unifier_plugin): restrict rule that was generating non-terminating behavior
...
see issue #632
2015-05-27 14:41:12 -07:00
Leonardo de Moura
5da4922397
feat(library/data/list/perm): cleanup proofs
...
refl and symm were refering to the setoid.refl and setoid.symm.
Moreover, they were producing harder elaboration problems
2015-05-27 12:30:56 -07:00
Leonardo de Moura
47e5633498
feat(frontends/lean/calc_proof_elaborator): avoid unnecessary unfolding in the calc tactic
2015-05-27 12:07:39 -07:00
Floris van Doorn
8056f326d7
feat(reserved_notation): make is_typeof parsing-only, add ^ to HoTT
2015-05-26 21:37:01 -07:00
Floris van Doorn
0c7e16e017
feat(library.data.int.basic): move theorems about successor and predecessor from HoTT to standard library
2015-05-26 21:37:01 -07:00
Leonardo de Moura
7f0951b8e7
feat(library/tactic): improve assumption tactic performance
2015-05-25 20:22:37 -07:00
Rob Lewis
393cefcf97
feat(library/data/real): define real numbers, prove they form a commutative ring
2015-05-26 12:05:53 +10:00
Rob Lewis
681f431d4b
feat(library/data/rat): make rat subtraction reducible, fix migration of min/max
2015-05-26 11:52:34 +10:00
Rob Lewis
eb537daa1c
feat(library/algebra): add min/max to ordered algebraic structures
2015-05-26 11:45:09 +10:00
Leonardo de Moura
4152ebfa23
refactor(library/data/nat): use new tactics
2015-05-25 18:14:52 -07:00
Jeremy Avigad
39129f112b
refactor(library/*): do various renamings
2015-05-25 16:50:42 -07:00
Jeremy Avigad
a64c0ea845
feat/refactor(library/data/{int,rat}/*): improve casting from nat to int to rat
2015-05-25 16:50:42 -07:00
Jeremy Avigad
4ed9e46532
refactor(library/data/int/*): use better direction for of_nat theorems
2015-05-25 16:50:42 -07:00
Jeremy Avigad
fdc89cd285
refactor(library/algebra/order.lean,library/{data,algebra}/*): use better names for order theorems
2015-05-25 16:50:42 -07:00
Jeremy Avigad
81c0ef8c89
refactor(library/data/nat/*): cleanup, additions, renaming
2015-05-25 16:50:42 -07:00
Jeremy Avigad
7c92161e49
refactor(library/data/finset/basic.lean): change order of arguments to induction tactic
2015-05-25 16:50:42 -07:00
Jeremy Avigad
716da2488b
fix(hott/*.md,library/*.md): use the word 'file' instead of 'module'
2015-05-25 16:50:42 -07:00
Leonardo de Moura
6db08c5519
test(library): test new tactics in the standard library
2015-05-25 16:48:33 -07:00
Leonardo de Moura
d0987eb3ac
feat(library/tactic): add 'subtvars' tactic
2015-05-25 16:36:44 -07:00
Leonardo de Moura
7e875c8d85
refactor(library): simplify theorems using improved tactics
2015-05-25 10:43:28 -07:00
Leonardo de Moura
88975927e6
fix(library/tactic/relation_tactics): beta-reduce goal before trying to extract head symbol
2015-05-24 18:56:35 -07:00
Leonardo de Moura
c453bb52a9
feat(library/data/stream): add notation and commonly used definitions
2015-05-24 16:53:58 -07:00
Leonardo de Moura
880027ea0e
feat(library/data/stream): define stream mem predicate and prove basic theorems
2015-05-24 15:47:33 -07:00
Leonardo de Moura
607a5fbb86
feat(library/data/stream): define cycle, inits, tails for streams and prove basic theorems
2015-05-24 13:42:51 -07:00
Leonardo de Moura
3181471024
feat(library/data/list/basic): add nth_eq_some aux theorem
2015-05-24 10:10:23 -07:00
Leonardo de Moura
32a2425e02
feat(library/data/stream): prove take lemma for infinite streams
2015-05-23 23:01:54 -07:00
Leonardo de Moura
75901157a1
feat(library/data/stream): add more declarations and examples demonstrating how to use eq_of_bisim
2015-05-23 22:03:17 -07:00
Leonardo de Moura
d987d6cc84
feat(library/data/stream): simplify corecursion proofs, define interleave operation by corecursion, add one example of proof by bisimulation
2015-05-23 16:00:08 -07:00
Leonardo de Moura
8685e8ad7e
feat(library/data/stream): define corec for infinite streams
2015-05-23 14:32:52 -07:00
Leonardo de Moura
dd4dd154ec
feat(library/data/stream): add bisimulation for streams
2015-05-23 12:07:27 -07:00
Jeremy Avigad
8bebd104ff
refactor(library/*): remove 'Module:' lines
2015-05-23 20:52:23 +10:00
Jeremy Avigad
db7bdce451
refactor(logic/funext.lean, algebra/function.lean): delete logic/funext, merge into algebra/function
2015-05-23 16:16:36 +10:00
Jeremy Avigad
f65a49b2c3
feat/fix(library/data/nat,int): add power to int, add trans attributes, power notation
2015-05-23 15:38:42 +10:00
Jeremy Avigad
a662f925cb
refactor(library/data/quotient.lean): improve comments
2015-05-23 14:21:16 +10:00
Jeremy Avigad
d33c91d7b9
fix({hott,library}/algebra/*): fix names
2015-05-23 14:05:06 +10:00
Jeremy Avigad
4bc93b59e3
feat(library/data/rat/{basic,order}.lean): add property of of_int
2015-05-23 12:34:07 +10:00
Jeremy Avigad
59c1801921
refactor(library/data/{list,set,finset}/basic.lean): make subset reserved notation
2015-05-23 12:34:07 +10:00
Leonardo de Moura
fe32b9fa7f
feat(library/data/stream): add infinite streams
2015-05-22 18:08:11 -07:00
Leonardo de Moura
1665ee39e8
feat(library/data/finset/card): test 'induction' tactic at finset
2015-05-19 15:56:51 -07:00
Leonardo de Moura
3e87f09d78
feat(library/tactic/induction_tactic): add support for user-defined recursors that contain parameters that should be synthesized by type class resolution
2015-05-19 15:33:46 -07:00
Leonardo de Moura
e1c2340db2
fix(frontends/lean): consistent behavior for protected declarations
...
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608
closes #609
2015-05-18 22:35:18 -07:00
Floris van Doorn
2144036cdb
feat(hott.circle): prove that the fundamental group of the circle is equal to the integers, as groups
...
Also many minor fixes at various places
2015-05-18 15:59:55 -07:00
Leonardo de Moura
19361f0196
feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables
...
see discussion at #604
2015-05-18 15:45:23 -07:00
Leonardo de Moura
b1ece388a6
feat(frontends/lean,library/tactic/induction_tactic): improve induction tactic notation, expand induction tactic implementation
2015-05-18 09:25:07 -07:00
Jeremy Avigad
566acf4b31
feat(library/data/finset/card.lean): add card_Union_of_disjoint and other theorems
2015-05-17 19:06:10 +10:00
Jeremy Avigad
6549940c63
feat(library/data/finset/bigops.lean): add Union for finsets
2015-05-17 17:50:32 +10:00
Jeremy Avigad
783dd61083
feat(library/data/finset/basic.lean): add useful calculation rules for quantifiers
2015-05-17 17:49:02 +10:00
Jeremy Avigad
9720d84095
refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): add ext principle, clean up file
2015-05-17 16:00:38 +10:00
Jeremy Avigad
4764f6e8ec
refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): simplify naming scheme for bigops
2015-05-17 15:24:37 +10:00
Jeremy Avigad
6dc1cfca3c
feat(library/init/nat.lean): add notation <= and >= for nat
2015-05-17 12:57:48 +10:00
Jeremy Avigad
7bde8193fe
feat(library/algebra/order): add alternate names for le.antisymm etc.
2015-05-17 12:54:36 +10:00
Jeremy Avigad
981bf93ce0
feat(library/data/default.lean): add rat and vector
2015-05-17 12:19:47 +10:00
Jeremy Avigad
ff701a9812
feat(library/data/nat/bigops.lean): add finite products and sums for nat
2015-05-16 22:26:59 +10:00
Jeremy Avigad
eae047bd31
refactor,feat(library/{data,algebra}): move bigops to algebra, define sums
2015-05-16 18:42:13 +10:00
Jeremy Avigad
87e4f7a951
feat(library/algebra/group.lean): add coercions from additive (comm) monoid to (comm) monoid
2015-05-16 18:27:49 +10:00
Jeremy Avigad
63bb4b558a
fix(library/data/set/{classical_inverse.lean,map.lean}): protect definitions in map, to avoid ambiguity
2015-05-16 18:24:19 +10:00
Jeremy Avigad
26ad6dde69
fix(library/data/fintype.lean): reduce imports, to avoid cyclic dependencies
2015-05-16 17:53:35 +10:00
Jeremy Avigad
daf53e4de2
fix(library/algebra/order.lean): rename decidable_eq to had_decidable_eq to avoid conflict
2015-05-16 17:53:35 +10:00
Jeremy Avigad
81d0d4aa53
fix(library/data/{set,finset}/basic.lean: delete \{{ \}}} notation (conflicts with records)
2015-05-16 17:53:35 +10:00
Sebastian Ullrich
77c20e99ff
feat(library/tactic/inversion_tactic): consistent orientation of generated equalities
...
Generated equalities in proof irrelevant environments were inverted
compared with the documentation and the proof relevant case, which
resulted in newly generated local vars replacing equivalent old ones
instead of the other way around.
2015-05-14 23:32:54 +02:00
Jeremy Avigad
8de6a4bb4c
feat(library/algebra/group_pow.lean,library/data/nat/power.lean): add generic power operation on monoids and groups
2015-05-13 22:19:02 -07:00
Leonardo de Moura
51a30892a1
chore(examples/ex): move example to library
2015-05-13 17:07:10 -07:00
Leonardo de Moura
065a1f7501
feat(library/tactic): add 'induction' tactic skeleton
2015-05-12 20:21:25 -07:00
Jeremy Avigad
05e28aaf19
feat(library/data/nat/{basic.lean,order.lean}): use migrate
2015-05-12 06:20:51 -07:00
Jeremy Avigad
42616f766f
refactor(library/data/{nat,int,rat}/{basic.lean,order.lean}: make algebra instance declarations local
2015-05-12 06:20:47 -07:00
Leonardo de Moura
f25c301c98
fix(library/data/rat): migrate for rat
2015-05-12 04:46:34 -07:00
Leonardo de Moura
d2adf922b7
refactor(library/data/int): use "migrate" command
2015-05-12 04:24:13 -07:00
Leonardo de Moura
396f77aa68
fix(library,hott): comment 'exit' commands to avoid warnings during compilation
2015-05-11 11:49:23 -07:00
Leonardo de Moura
f59a81d744
refactor(library/data): use new 'obtain' expression
2015-05-11 09:14:48 -07:00
Jeremy Avigad
a009cf24e3
feat(library/data/finset/{basic,card,comb}.lean: add theorems, including card of an injective image
2015-05-11 09:03:57 -07:00
Jeremy Avigad
3e07716b5d
feat(library/data/finset/to_set.lean): add finset/set translation theorems
2015-05-11 09:03:56 -07:00
Jeremy Avigad
efbca4c78e
feat(library/data/finset/finset.md): add markdown file
2015-05-11 09:03:56 -07:00
Jeremy Avigad
9d73aa657b
feat(library/data/{finset,list}/comb.lean): add 'any' for finsets
2015-05-11 09:03:56 -07:00
Leonardo de Moura
379af8a04e
feat(library): avoid 'definition' hack for theorems
2015-05-09 12:15:30 -07:00
Leonardo de Moura
bd28396be0
feat(kernel): transparent theorems
...
closes #576
2015-05-09 11:42:29 -07:00
Leonardo de Moura
8086ad7461
feat(library/init): define quot.hrec_on and quot.hrec_on₂ based on heterogeneous equality
...
They are easier to use than the version with nested eq.rec's
2015-05-09 09:49:41 -07:00
Leonardo de Moura
4f0f739ea6
feat(library): remove occurrences of 'opaque' keyword
2015-05-08 16:40:03 -07:00
Leonardo de Moura
6c958a25e7
refactor(library/tactic/expr_to_tactic): make sure builtin tactics don't need to be marked opaque
...
This modification is needed since we will remove opaque definitions from
the kernel.
see issue #576
2015-05-08 16:06:16 -07:00
Leonardo de Moura
57ea660963
refactor(*): start process for eliminating of opaque
definitions from the kernel
...
see issue #576
2015-05-08 16:06:04 -07:00
Leonardo de Moura
3aac370629
fix(library/data/finset/basic): type error on the finset.induction proof
2015-05-08 11:08:24 -07:00
Jeremy Avigad
624b664950
refactor(library/data/list/basic.lean): make minor renaming
2015-05-08 20:25:28 +10:00
Jeremy Avigad
75e50fd371
feat(library/data): update defaults and markdown files
2015-05-08 20:23:15 +10:00
Jeremy Avigad
b56f7a06d5
refactor(library/data/finset/bigop.lean): use inter eq empty rather than disjoint
2015-05-08 20:06:21 +10:00
Jeremy Avigad
6fce01385c
feat(library/data/{finset,list}/bigop.lean: generalize bigops from group to monoid
2015-05-08 19:51:37 +10:00
Jeremy Avigad
42f2fc973a
refactor(library/data/{finset,list,fintype}: rename cross_product to product
2015-05-08 19:51:37 +10:00
Jeremy Avigad
68f7afa053
feat(library/data/finset/card.lean): begin theory of cardinality
2015-05-08 19:51:37 +10:00
Jeremy Avigad
9e04d09381
feat(library/data/finset/comb.lean): add filter, diff, theorems
2015-05-08 19:51:37 +10:00
Jeremy Avigad
4db4c86d37
feat(library/data/finset/basic.lean): add lots of theorems, do minor renaming
2015-05-08 19:51:37 +10:00
Jeremy Avigad
a54a98c1ec
feat(library/data/set): add distributivity, diff, uniformize with finset
2015-05-08 19:51:37 +10:00
Jeremy Avigad
9e26dddaf3
feat(library/data/list/perm): add perm_filter
2015-05-08 19:51:37 +10:00
Jeremy Avigad
86a039b6d5
feat(library/data/list/set.lean): add two theorems
2015-05-08 19:51:37 +10:00
Jeremy Avigad
e4c75ae8ae
feat(library/logic/connective.lean): add distributivity laws
2015-05-08 19:51:37 +10:00
Jeremy Avigad
ba78cc42f9
fix(library/data/set/basic.lean, function.lean): fix typos
2015-05-08 19:51:37 +10:00
Leonardo de Moura
0b57f7d00a
refactor(library/tactic): refine interface between tactic and proof-term modes
...
Some constraints were being lost with the previous interface.
This is why we had a workaround in fintype.lean.
We can also remove some hacks we have used in the past.
2015-05-07 18:02:51 -07:00
Floris van Doorn
9893de6194
feat(hit/circle): prove partly that the fundamental group of the circle is int
...
Also add markdown files for nat and int
2015-05-07 16:39:04 -07:00
Floris van Doorn
0a8f4f6dab
feat(function): add unfold hints to function.[h]lean
2015-05-07 16:39:03 -07:00
Floris van Doorn
7cfac38eda
feat(hott): port parts of natural numbers and integers from standard library to HoTT
...
This also involves:
- adding definitions about logic and natural numbers existing in the standard library to init
- porting the current algebraic hierarchy
2015-05-07 16:39:03 -07:00
Leonardo de Moura
e2c1dc92a8
chore(library/data/fintype): add workaround until problem in the elaborator is fixed
2015-05-07 16:32:26 -07:00
Leonardo de Moura
aff9257c72
feat(frontends/lean): allow → to be used in calc proofs
...
see issue #586
2015-05-07 12:28:47 -07:00
Leonardo de Moura
b03266be70
feat(library/normalize,frontends/lean): rename '[unfold-m]' hint to '[constructor]', and allow it to be attached to constants
...
closes #587
2015-05-07 12:00:34 -07:00
Leonardo de Moura
5798ac43de
fix(frontends/lean/structure_cmd): 'structure' command must set unfold-c attribute for auxiliary recursors
...
fixes #582
2015-05-07 09:09:07 -07:00
Leonardo de Moura
64cc710ff7
refactor(ordered_group): replace 'match' with 'obtain'
2015-05-06 10:34:43 -07:00
Leonardo de Moura
84deddcca9
feat(library/tactic/rewrite_tactic): apply 'reflexivity' tactic after 'rewrite' instead of hard coded solution
2015-05-05 20:23:49 -07:00
Leonardo de Moura
7aa0e466a5
test(library): test new 'obtain' expression in the standard library
2015-05-05 18:30:16 -07:00
Leonardo de Moura
616f49c2e4
feat(frontends/lean): improved 'obtains' expression
2015-05-05 18:30:16 -07:00
Jeremy Avigad
f7a610faa3
feat(library/data/set/basic,function): mark set reducible, and add theorem from Haitao Zhang
2015-05-05 08:55:58 -07:00
Leonardo de Moura
11f74363e2
refactor(library): rename 'intersection' to 'inter' in list and finset, add finset abbreviation at top level
2015-05-05 08:53:31 -07:00
Leonardo de Moura
a46abbb9ce
refactor(library/data): test new tactics in the standard library
2015-05-03 21:40:33 -07:00
Leonardo de Moura
3cd8f38b8d
feat(library/data/string): prove that string and char have decidable equality
2015-05-03 21:08:09 -07:00
Leonardo de Moura
4e1146a2d5
refactor(hott,library): test new tactics in the HoTT and standard libraries
2015-05-02 22:22:31 -07:00
Leonardo de Moura
b39fe17dee
feat(library/tactic): add 'transitiviy', 'reflexivity' and 'symmetry' tactics
...
closes #500
2015-05-02 15:48:25 -07:00
Leonardo de Moura
cd17618f4a
refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]'
...
These attributes are used by the calc command.
They will also be used by tactics such as 'reflexivity', 'symmetry' and
'transitivity'.
See issue #500
2015-05-02 15:15:35 -07:00
Leonardo de Moura
415ca2b93f
feat(library/tactic): add 'congruence' tactic
...
It is the f_equal described at issue #500 .
2015-05-02 12:58:46 -07:00
Leonardo de Moura
458d13025f
refactor(library,hott): define 'congr' in the initialization files
2015-05-02 11:29:31 -07:00
Leonardo de Moura
ac8ba6a3cf
feat(library/tactic): add 'subst' tactic
...
see issue #500
2015-05-01 19:31:24 -07:00
Leonardo de Moura
e8affed020
refactor(library): test new tactics in the standard library
2015-05-01 18:18:29 -07:00
Leonardo de Moura
de369a0a0a
feat(library/tactic/injection_tactic): improve 'injection' tactic
...
see issue #500
2015-05-01 15:49:56 -07:00
Leonardo de Moura
9ba8b284a1
fix(library/tactic/apply_tactic): add eapply, and fix issue #361
2015-05-01 15:08:00 -07:00
Leonardo de Moura
e948dd239c
feat(library/data/list/perm): use new 'injection' tactic
2015-05-01 13:08:36 -07:00
Leonardo de Moura
63eb155c7e
feat(library/tactic): add 'injection' tactic
...
see issue #500
2015-05-01 12:45:21 -07:00
Leonardo de Moura
1e18a76bdb
chore(library/init/nat): replace 'no_confusion' with 'by contradiction'
2015-04-30 21:26:52 -07:00
Leonardo de Moura
2d9c950144
feat(library/tactic/constructor_tactic): allow 'constructor' tactic without index
...
see issue #500
2015-04-30 21:15:07 -07:00
Leonardo de Moura
d152f38518
feat(library/tactic): add 'constructor', 'split', 'left', 'right' and 'existsi' tactics
...
see issue #500
2015-04-30 17:52:29 -07:00
Leonardo de Moura
1c6067bac2
feat(library/tactic): add 'exfalso' tactic
...
see issue #500
2015-04-30 15:43:07 -07:00
Leonardo de Moura
59b11c815c
refactor(library/data/list/perm): remove unnessary lambda abstractions
...
The contradiction tactic takes care of it.
2015-04-30 14:02:19 -07:00
Leonardo de Moura
9760968b45
refactor(library,hott): use/test new 'contradiction' tactic in the standard and hott libraries
2015-04-30 13:56:12 -07:00
Leonardo de Moura
9c8a63caec
feat(library/tactic): add 'contradiction' tactic
...
see issue #500
Remark: this tactic also applies no_confusion to take care of a contradiction
2015-04-30 13:47:40 -07:00
Leonardo de Moura
3233008039
feat(library/tactic): allow user to name generalized term in the 'generalize' tactic
...
closes #421
2015-04-30 11:57:40 -07:00
Leonardo de Moura
3912bc24c8
feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears'
2015-04-30 11:00:39 -07:00
Leonardo de Moura
f60dc8ae8f
refactor(library/init/nat): cleanup
2015-04-30 10:10:13 -07:00
Leonardo de Moura
018f768555
chore(library): remove some unnecessary parentheses
2015-04-29 14:39:59 -07:00
Leonardo de Moura
d2c7b5c319
feat(library/tactic): add 'let' tactic
...
closes #555
2015-04-28 17:24:43 -07:00
Leonardo de Moura
a23118d357
feat(frontends/lean): add tactic_notation command
...
This addresses the first part of issue #461
We still need support for tactic definitions
2015-04-27 17:46:13 -07:00
Leonardo de Moura
ca8943f45b
feat(library,hott): remove rapply tactic
2015-04-27 15:06:16 -07:00
Leonardo de Moura
17c07cdb02
feat(library/data/rat/order): define abs and sign for rat before migrate
2015-04-27 12:59:02 -07:00
Jeremy Avigad
7a1064b7e8
refactor(library/algebra/order.lean): rename a field in an order structure
2015-04-27 12:03:41 -07:00
Jeremy Avigad
d8e40d90d6
feat(library/data/rat/order.lean): make rat a linear ordered field
2015-04-27 12:03:41 -07:00
Leonardo de Moura
76c773ad3d
feat(library/data/examples/depchoice): add dependent choice example
2015-04-26 12:56:23 -07:00
Leonardo de Moura
072bf0b3b4
refactor(library): make sure "choose" compute inside the kernel
2015-04-25 23:10:48 -07:00
Leonardo de Moura
d455bb4c5b
feat(library/data/fintype): add decidable_exists_finite
2015-04-25 21:38:03 -07:00
Leonardo de Moura
6bb6644c25
feat(library/data/squash): define squash type using quotients
2015-04-24 18:11:25 -07:00
Leonardo de Moura
9d01868361
feat(frontends/lean): use rewrite tactic to implement unfold (it has a unfold step)
...
closes #502
2015-04-24 17:23:12 -07:00
Leonardo de Moura
1149ead14c
chore(library/logic/examples/colog88): remove unnecessary annotation
2015-04-24 12:45:06 -07:00
Leonardo de Moura
a5306e70eb
feat(library/logic/examples/negative): add example showing that allowing negative inductive datatypes would lead to inconsistency
2015-04-24 09:33:09 -07:00
Leonardo de Moura
15c331591e
feat(library/logic/examples/colog88): add example from COLOG-88 paper
2015-04-24 09:33:09 -07:00
Leonardo de Moura
2613e7c444
fix(frontends/lean): bug when handling identifiers in tactics
...
This bug was reported by Jeremy in the Lean Google group:
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/ZKJ8WPPEVJA/n05x6rPRzvMJ
2015-04-22 16:03:22 -07:00
Floris van Doorn
9d805437f0
fix(reserved_notation): lower binding power of 'iff'
2015-04-22 13:06:11 -07:00
Leonardo de Moura
670eac9d50
refactor(library): avoid 'context' command in the standard library
2015-04-21 19:13:19 -07:00
Leonardo de Moura
bf8a7eb9b4
fix(library/scoped_ext): bug in local metadata in sections
...
The problem is described in issue #554
2015-04-21 18:56:28 -07:00
Leonardo de Moura
6f6d106a10
feat(library/tactic): add "check_expr" tactic
...
closes #486
2015-04-19 19:00:05 -07:00
Leonardo de Moura
306087b5d3
refactor(library/data): rename 'countable' to 'encodable', define countable in the usual way, and prove all 'encodable' type is 'countable'
2015-04-19 14:20:47 -07:00
Jeremy Avigad
f4398115b4
feat(library/data/rat/basic.lean): begin theory of rationals, show rat is a field
2015-04-18 11:39:52 -07:00
Jeremy Avigad
6359132b67
refactor(library/algebra/field.lean): rename has_decidable_eq and declare instance
2015-04-18 11:39:52 -07:00
Jeremy Avigad
dfaeb475cc
feat(library/init/reserved_notation.lean): add equiv relation symbol
2015-04-18 11:39:52 -07:00
Jeremy Avigad
5eb7fef564
feat(library/algebra/order.lean, data/int/{basic,order}.lean): add theorem, correct gt_trans
2015-04-18 11:39:52 -07:00
Jeremy Avigad
53919699bc
refactor(library/logic/axioms/prop_decidable.lean): simplify proof of prop_decidable (using arbitrary instead of epsilon)
2015-04-18 11:39:52 -07:00
Leonardo de Moura
cc63a40a01
feat(library): enforce name conventions on old nat declarations
2015-04-18 10:50:30 -07:00
Leonardo de Moura
10954a073c
feat(library/logic/examples): add new example from Martín Escardó paper
2015-04-17 15:22:52 -07:00
Leonardo de Moura
9cb759e0a9
feat(library/logic/axioms/examples/leftinv_of_inj): add classical example
2015-04-16 22:39:51 -07:00
Leonardo de Moura
3b84a63874
fix(library/algebra/function): terminology
2015-04-16 20:52:18 -07:00
Leonardo de Moura
2e675c1bdd
feat(library/data/examples/notcountable): add example showing that nat -> nat is not countable
2015-04-16 14:54:34 -07:00
Leonardo de Moura
df8ebeeefc
feat(library/logic/axioms/examples/diaconescu): remove redundant hypothesis
2015-04-16 14:04:09 -07:00
Leonardo de Moura
7529ee0a5c
feat(library/data/countable): prove axiom of choice and skolem theorem for countable types and decidable relations
2015-04-16 12:36:27 -07:00
Leonardo de Moura
0dd7667836
feat(library/data/countable): choice function for countable types
2015-04-16 12:29:06 -07:00
Leonardo de Moura
7a4f43d6ab
feat(library/data/nat/choose): choice function for natural numbers
2015-04-16 11:33:26 -07:00
Leonardo de Moura
b14d3dbeba
chore(library/data/countable): add copyright notice
2015-04-16 09:24:53 -07:00
Leonardo de Moura
036900280d
feat(library/data/countable): show that a type is countable by providing an injection to a type already known to be countable
2015-04-15 10:30:24 -07:00
Leonardo de Moura
039f1de524
fix(library/data/countable): typos
2015-04-14 21:26:56 -07:00
Leonardo de Moura
9534cfe92f
feat(library/data/countable): prove that (list A) is countable if A is countable
2015-04-14 21:17:18 -07:00
Leonardo de Moura
a7db8a2bac
theorem(library/data/countable): prove that the product of two countable types is countable
2015-04-14 20:39:58 -07:00
Leonardo de Moura
38b880b939
feat(library/data/nat/pairing): add unpair_mkpair theorem
2015-04-14 20:28:20 -07:00
Leonardo de Moura
f7a43c7997
feat(library/data/nat/sqrt): generalize sqrt_eq theorem
2015-04-14 20:10:18 -07:00
Leonardo de Moura
faca0acd26
feat(library/data/nat/sqrt): add sqrt_eq theorem
2015-04-14 15:38:54 -07:00
Leonardo de Moura
11dbcda9d2
feat(library/data/nat/pairing): add "elegant" pairing/unpairing function
2015-04-14 09:01:15 -07:00
Leonardo de Moura
2eb7538c96
fix(library/data/nat/sqrt): adjust to reflect recent changes
2015-04-14 09:01:15 -07:00
Leonardo de Moura
4180b80df6
feat(library/data/nat/power): define power and add basic theorems
2015-04-14 09:01:15 -07:00
Leonardo de Moura
ff72a520ff
feat(library/data/nat/div): add mul_cancel theorems
2015-04-14 09:01:15 -07:00
Leonardo de Moura
c73c1dbb63
feat(library/data/nat/sub): add two extra theorems
2015-04-14 09:01:15 -07:00
Leonardo de Moura
11c9bb4626
feat(library/data/nat): naive square root function
2015-04-14 09:01:15 -07:00
Leonardo de Moura
2453a6ab45
feat(library/data/countable): define countable type class
2015-04-14 09:01:15 -07:00
Leonardo de Moura
a24d4e47cd
feat(library/init/nat): add missing decidable_ge and decidable_lt
2015-04-14 09:01:15 -07:00
Leonardo de Moura
82eada7d56
feat(library/data/list/basic): add find nth theorem
2015-04-14 09:01:15 -07:00
Leonardo de Moura
07e195e9f1
feat(library/data/fintype): add decidable_finite_pred instance
2015-04-12 20:07:04 -07:00
Leonardo de Moura
00d68cadc8
refactor(library/data/fintype): cleanup and mark location that exposes bug in the 'cases' tactic
2015-04-12 17:52:41 -07:00
Leonardo de Moura
f523d3a995
feat(library/data): add structure for converting a list of elements into a type, and then show the resultant type is a finite type
2015-04-12 17:33:58 -07:00
Leonardo de Moura
d9f8b0f3d7
feat(library/data/finset/comb): add cross_product to finset
2015-04-11 19:46:04 -07:00
Leonardo de Moura
4c827293a8
feat(library/data/list/perm): add perm_cross_product theorem
2015-04-11 19:13:34 -07:00
Leonardo de Moura
41ddc97e0d
feat(library/data/list): define filter function for lists
2015-04-11 18:22:22 -07:00
Leonardo de Moura
c437fbe0bc
feat(library/data/fintype): prove that A->B has decidable equality when A is a finite type and B has decidable equality
2015-04-11 16:45:27 -07:00
Leonardo de Moura
3df7fe120c
feat(library/algebra/function): define curry and uncurry functions
2015-04-11 16:45:07 -07:00
Leonardo de Moura
3edf0dffdf
feat(library/data/finset): define subset for finsets
2015-04-11 15:29:12 -07:00
Leonardo de Moura
dfef4c5daf
feat(library/data): define fintype type class
2015-04-11 14:55:41 -07:00
Leonardo de Moura
06d4ae971d
feat(library/data/list): add nodup_cross_product theorem
2015-04-11 14:31:01 -07:00
Leonardo de Moura
54a2d9750e
refactor(library/data): simplify definition of disjoint
2015-04-11 14:04:09 -07:00
Leonardo de Moura
ee895e00dd
feat(library/data/list): define cross_product for lists
2015-04-11 13:52:50 -07:00
Leonardo de Moura
fefddcd0f9
fix(library/data/list/perm): broken theorem
2015-04-11 09:42:24 -07:00
Leonardo de Moura
1b34f40f36
feat(library/data/list/set): add decidable_nodup
2015-04-11 09:39:26 -07:00
Leonardo de Moura
dff05557a3
feat(library/data/finset): add all combinator theorems
2015-04-11 09:28:27 -07:00
Leonardo de Moura
5304c5afb8
feat(library/data/list/set): add 'all' theorems
2015-04-11 09:28:05 -07:00
Leonardo de Moura
32b07c4561
feat(library/data/finset): define map for finset
2015-04-10 17:14:10 -07:00
Leonardo de Moura
a24c0bf1db
feat(library/data/finset): define intersection for finsets
2015-04-10 16:45:25 -07:00
Leonardo de Moura
49d6d43926
feat(library/data/list): define intersection for lists
2015-04-10 16:31:44 -07:00
Leonardo de Moura
d59c671054
feat(library/data/list/comb): define upto list generator
2015-04-10 15:32:44 -07:00
Leonardo de Moura
9d8b5aa347
feat(library/data/list/comb): add any/all theorems
2015-04-10 07:01:14 -07:00
Floris van Doorn
d1b98b6919
fix(reserved_notation): make is_typeof an abbreviation
2015-04-10 06:35:15 -07:00
Leonardo de Moura
5caa983919
feat(library/data/finset): redefine bigop for finset
2015-04-10 06:13:32 -07:00
Leonardo de Moura
53f730ec82
feat(library/data/list/bigop): add bigop perm theorem
2015-04-10 06:01:23 -07:00
Leonardo de Moura
608e2838bf
feat(library/data/list): define bigop for lists
2015-04-10 05:52:19 -07:00
Leonardo de Moura
4be8741a39
feat(library/data/list): break list/basic.lean into smaller files
2015-04-10 05:19:52 -07:00
Leonardo de Moura
a223b9b1f7
feat(library/data/finset): add bigop for finset + commutative groups
2015-04-09 20:00:00 -07:00
Leonardo de Moura
795acc70a6
refactor(library/data/finset): move finset to its own directory
2015-04-09 19:30:09 -07:00
Leonardo de Moura
ca377e5f8b
feat(library/data/list/basic): add foldr/foldl theorems
2015-04-09 18:48:04 -07:00
Leonardo de Moura
b209f442f7
refactor(library/data/list) fix theorem name, and do not rely on implementation of mem
2015-04-09 16:27:48 -07:00
Leonardo de Moura
2ab2f7dc9d
feat(library/data/finset): add basic support for finite sets
2015-04-09 15:51:23 -07:00
Leonardo de Moura
571ff76080
feat(library/data/list/perm): add perm_ext theorem
2015-04-09 15:27:32 -07:00
Leonardo de Moura
64173ddf93
feat(library/data/list/basic): more nodup theorems
2015-04-09 14:50:00 -07:00
Leonardo de Moura
b4611ba33d
feat(library/data/list/basic): add mem erase theorems
2015-04-09 13:19:51 -07:00
Leonardo de Moura
5ba5e66665
feat(library/algebra/binary): add auxiliary theorems
2015-04-09 11:00:59 -07:00
Leonardo de Moura
d5176ebae5
refactor(library/algebra/binary): define right_commutative and left_commutative
2015-04-09 10:54:28 -07:00
Leonardo de Moura
8522fbec4b
feat(library/data/list): more general theorems for perm foldl and foldr, and other minor improvements
2015-04-09 09:29:58 -07:00
Leonardo de Moura
07ff0900aa
feat(library/data/list): add permutation theorems for union and insert
2015-04-08 19:02:35 -07:00
Leonardo de Moura
33422a387a
feat(library/data/list/basic): define 'union' and 'insert' for lists
2015-04-08 18:12:51 -07:00
Leonardo de Moura
c95bd8ba61
feat(library/data/list): add erase_dup and theorems
2015-04-08 12:28:48 -07:00
Leonardo de Moura
05bd6b5fe7
feat(library/data/list): add foldr/foldl equality theorems for permutations
2015-04-08 10:36:05 -07:00
Jeremy Avigad
eb5089bf27
feat(library/data/set): add theory of functions and maps between sets
2015-04-08 09:46:34 -07:00
Jeremy Avigad
1f4ddd7a0f
refactor(library/init/funext.lean): break out definition of equivalence, and hide auxiliary theorems
2015-04-08 09:46:34 -07:00
Jeremy Avigad
5812b35d93
feat(library/data/set/function.lean): begin theory of functions on sets
2015-04-08 09:46:34 -07:00
Leonardo de Moura
afc75f141c
refactor(library/data/list/perm): prove auxiliary theorems using 'match-with'
2015-04-08 09:43:17 -07:00
Leonardo de Moura
56d20852aa
refactor(library/data/list/perm): remove dead code
2015-04-08 09:32:28 -07:00
Leonardo de Moura
ef1b057b63
refactor(library/data/list/perm): cleanup theorem
2015-04-08 09:29:40 -07:00
Leonardo de Moura
e0e65705db
feat(library/data/list/perm): add perm inversion theorems
2015-04-07 18:54:02 -07:00
Leonardo de Moura
c6a35e718d
refactor(library/data/list/perm): use by_cases instead of dependent-if
2015-04-07 09:26:24 -07:00
Leonardo de Moura
9306830d8c
feat(library/data/list): perm is decidable
2015-04-07 09:12:10 -07:00
Leonardo de Moura
1d87016f03
refactor(library): move some theorems to init
2015-04-07 07:46:11 -07:00
Leonardo de Moura
2bc13f6bfd
feat(library/tactic/exact): enforce goal type during elaboration when executing 'exact' tactic
...
Remark: this was the behavior of the 'sexact' tactic.
This commit also adds the 'rexact' (relaxed exact) tactic which does not
enforce the goal type.
closes #495
2015-04-06 13:23:38 -07:00
Leonardo de Moura
754276a660
feat(frontends/lean): round parenthesis for [tactic1 | tactic2]
...
This commit also replaces the notation for divides
`(` a `|` b `)`
with
a `∣` b
The character `∣` is entered by typing \|
closes #516
2015-04-06 09:24:09 -07:00
Leonardo de Moura
3b959c9e6c
refactor(library/data): move perm to list folder
2015-04-05 12:01:32 -07:00
Jeremy Avigad
c563548980
feat(library/data/set/basic.lean): add definitions and simplify proofs
2015-04-05 12:36:54 -04:00
Jeremy Avigad
e76e445ece
feat(library/logic/connectives.lean): add calculation rules for true and false, and move exists unique to quantifiers
2015-04-05 12:15:21 -04:00
Jeremy Avigad
c6c50a61b3
refactor(library/data/set/basic.lean): take advantage of extensionality in sets
2015-04-05 10:12:27 -04:00
Jeremy Avigad
74ff43a543
refactor(library/init/{funext,quot}.lean): adjust comments and headers
2015-04-05 10:11:53 -04:00
Jeremy Avigad
6596217a84
refactor(library/data/set): expand set.lean to set directory
2015-04-05 09:27:15 -04:00
Leonardo de Moura
4ec0e1b07c
feat(frontends/lean): improve calc mode
...
Now, it automatically supports transitivity of the form
(R a b) -> (b = c) -> R a c
(a = b) -> (R b c) -> R a c
closes #507
2015-04-04 08:58:35 -07:00
Leonardo de Moura
f1b7021ed0
feat(library/data/list/basic): add more theorems for disjoint predicate
2015-04-03 22:55:16 -07:00
Leonardo de Moura
23a1f5fa4b
feat(library/data/list/basic): define nodup and disjoint
2015-04-03 15:44:07 -07:00
Leonardo de Moura
3b0f666646
feat(library/algebra/function): define injective
2015-04-03 15:43:44 -07:00
Leonardo de Moura
01f5dd9fa8
feat(library/data/list): add "erase" function lemmas
2015-04-03 13:18:48 -07:00
Leonardo de Moura
fc0ed5e46c
feat(library/data/list/basic): define erase and prove basic theorems
2015-04-02 23:58:47 -07:00
Leonardo de Moura
44ba0e10c0
feat(library/init/logic): add rewrite rules for decidable
2015-04-02 23:31:40 -07:00
Leonardo de Moura
9f3ba66295
feat(library/data/perm): add more theorems
2015-04-02 20:00:46 -07:00
Leonardo de Moura
e47c8c2d9e
feat(library/data/list/basic): add quasiequality predicate l₁≈a|l₂, l₁ is equal to l₂ with 'a' inserted somewhere
2015-04-02 20:00:46 -07:00
Leonardo de Moura
5a394ac7ea
feat(library/data/perm): add more theorems
2015-04-02 09:21:20 -07:00
Leonardo de Moura
92d6e93971
feat(library/data/perm): cleanup and add calculational proof support to perm
2015-04-02 08:50:05 -07:00
Leonardo de Moura
54136c1ec0
feat(library/data/perm): add list permutation module
2015-04-01 23:00:02 -07:00
Leonardo de Moura
dbe54c4fb5
feat(library/data): define unordered pairs using quotients
2015-04-01 17:30:49 -07:00
Leonardo de Moura
3951b50282
feat(library/data/prod): define swap
2015-04-01 17:30:37 -07:00
Leonardo de Moura
7b64a47221
refactor(library/init): add auxiliary function mk_equivalence
2015-04-01 17:30:20 -07:00
Leonardo de Moura
4fcb560ea7
feat(library/init/funext): add subsingleton_pi instance using funext
2015-04-01 13:05:05 -07:00
Leonardo de Moura
ced742083a
feat(library/init/quot): add helper function quot.rec_on_subsingleton₂
2015-04-01 13:04:41 -07:00
Leonardo de Moura
ed1acd9fb0
feat(library/init): move propext to init/quot, add Jeremy's funext theorem
2015-04-01 12:36:33 -07:00
Leonardo de Moura
0da4f191fc
feat(library/init/quot): add rec_on for subsingleton types
2015-04-01 11:57:39 -07:00
Leonardo de Moura
ce5e83eb3e
refactor(library/init): move subsingleton to init folder
2015-04-01 11:57:29 -07:00
Leonardo de Moura
b960e123b1
feat(kernel): add experimental support for quotient types
2015-03-31 22:04:16 -07:00
Leonardo de Moura
a52cb009dc
refactor(library): reorganize init folder and add setoid
2015-03-31 19:56:05 -07:00
Leonardo de Moura
6e6cc749a8
feat(library/logic/axioms): break prop_complete into propext and em
...
The user may want to use propext without assuming em.
2015-03-31 18:51:43 -07:00
Leonardo de Moura
e35de54cee
feat(library/data/list/basic): add aux theorems
2015-03-31 18:38:05 -07:00
Leonardo de Moura
4c0ce9a619
feat(library/data/list/basic): missing theorems
2015-03-30 19:11:45 -07:00
Leonardo de Moura
87f6fc6b6a
feat(library/algebra/ring): remove sorrys
2015-03-30 11:55:48 -07:00
Leonardo de Moura
56af7ba535
feat(library/algebra/ordered_ring): remove sorry
2015-03-30 11:01:26 -07:00
Leonardo de Moura
3d4a02089a
feat(library/logic/examples/propositional): add different encoding
2015-03-30 07:13:19 -07:00
Leonardo de Moura
9d34431bb6
feat(library/logic/examples/propositional/soundness): cleanup precedence levels
2015-03-30 05:42:47 -07:00
Leonardo de Moura
5ef88bfbc8
feat(library/logic/examples/propositional): add example based on Floris Coq files formalizing propositional Calculus
2015-03-30 05:12:29 -07:00
Leonardo de Moura
299cbe4b25
feat(library/data/bool): add auxiliary theorems for bool
2015-03-30 04:55:28 -07:00
Leonardo de Moura
42fe87d7cc
feat(library/data/list/basic): add sublist predicate
2015-03-30 03:20:42 -07:00
Leonardo de Moura
66bb22f268
feat(library/data/list/basic): cleanup
2015-03-30 02:14:33 -07:00
Leonardo de Moura
ec1a60b02c
feat(library/init/logic): add helper function for proving decidable equality
2015-03-30 02:14:26 -07:00
Leonardo de Moura
5b9d52c0dd
refactor(library/data/int/order): cleanup
2015-03-28 12:58:40 -07:00
Leonardo de Moura
75621df52b
feat(frontends/lean): uniform notation for lists in tactics
...
closes #504
2015-03-27 17:54:48 -07:00
Rob Lewis
abcc56a2a7
feat(library/algebra):refactor field and ordered_field more appropriately
2015-03-27 11:54:11 -07:00
Rob Lewis
b79f600fbc
style(library/algebra/ordered_field):fix indentation, shorten calc statements
2015-03-27 11:52:30 -07:00
Rob Lewis
94b9aaea45
feat(library/algebra/ordered_field): prove more theorems
2015-03-27 11:52:30 -07:00
Rob Lewis
a1028922bd
feat(library/algebra/ordered_field): complete proofs of many theorems. Define discrete linear ordered field
2015-03-27 11:52:30 -07:00
Rob Lewis
4099de7754
feat(library/algebra/field): redefine field so that 1/0=0. Many theorems lose hypotheses in discrete setting.
2015-03-27 11:52:29 -07:00
Rob Lewis
365f1ebcb6
feat(library/algebra/ordered_field): prove more theorems for ordered field
2015-03-27 11:45:57 -07:00
Rob Lewis
11f82eacfb
feat(library/algebra/ordered_field.lean): add ordered fields
2015-03-27 11:45:57 -07:00
Jeremy Avigad
e019ab5500
fix(library/init/logic.lean): rename inhabited_imp_nonempty
2015-03-25 18:29:06 -07:00
Jeremy Avigad
8e007b3441
feat(library/logic/axioms/hilbert.lean): add 'some' operator
2015-03-25 18:29:06 -07:00
Jeremy Avigad
765f6f21f8
fix(library/algebra/ring.lean): allow degenerate semirings and rings, but not degenerate ordered_semirings and ordered_rings. Closes #478 .
2015-03-25 18:29:06 -07:00
Leonardo de Moura
b9e3c474c9
feat(library/tactic): add all_goals tactic
...
closes #501
2015-03-25 17:42:34 -07:00
Leonardo de Moura
74b28f6ad9
feat(library,hott): new notation for typeof
2015-03-24 18:35:21 -07:00
Leonardo de Moura
9b577a7b3e
feat(frontends/lean): add 'migrate' command
2015-03-14 21:48:00 -07:00
Leonardo de Moura
ba913876e0
feat(library/data/list/basic): enforce name conventions, add foldl_eq_foldr theorem
2015-03-14 13:06:09 -07:00
Leonardo de Moura
bed0d6df6b
fix(frontends/lean/elaborator): inaccessible over coercion
2015-03-13 23:04:45 -07:00
Leonardo de Moura
27e58dc534
refactor(library/data): cleanup vector and list modules
2015-03-13 22:25:21 -07:00
Jeremy Avigad
ec05e83a2a
feat(library/data/int/div.lean): add theorems about div
2015-03-12 20:54:49 -07:00
Leonardo de Moura
14aeac180a
refactor(library/algebra/category/constructions): more rewrite tactic tests
2015-03-12 20:27:11 -07:00
Leonardo de Moura
d7c6028a3e
refactor(hott,library): use/test the rewrite tactic in more places
...
The performance also improved.
2015-03-12 17:25:31 -07:00
Leonardo de Moura
167675a397
feat(library/data/vector): add nth and decidable_eq
2015-03-09 08:41:36 -07:00
Leonardo de Moura
a628836f28
feat(library/data/vector): add theorems
2015-03-08 22:51:11 -07:00
Leonardo de Moura
f6cd604a44
chore(library/data/bool): enforce naming conventions
2015-03-06 19:20:48 -08:00
Leonardo de Moura
4fdac068b0
chore(library/data/vector): cleanup vector proofs
2015-03-06 17:37:03 -08:00
Leonardo de Moura
1490bdad49
feat(frontends/lean): add version of 'exact' tactic (sexact) that enforces goal type during term elaboration
2015-03-06 17:34:45 -08:00
Leonardo de Moura
78d8e79000
fix(library/data/num): naming convention
2015-03-05 23:48:08 -08:00
Leonardo de Moura
fa201bce9b
feat(library/algebra/group): cleanup some proofs
2015-03-05 18:46:07 -08:00
Leonardo de Moura
368f9d347e
refactor(frontends/lean): approach used to parse tactics
...
The previous approach was too fragile
TODO: we should add separate parsing tables for tactics
2015-03-05 18:11:21 -08:00
Leonardo de Moura
57ec52b6f1
refactor(library/data/fin): cleanup pattern matching equations
2015-03-05 14:42:42 -08:00
Leonardo de Moura
e4060a5614
feat(frontends/lean): do not force user to type the function name in the left-hand-side of recursive equations
2015-03-05 12:08:36 -08:00
Leonardo de Moura
53df3d86ee
feat(library/data/list/basic): use 'show' instead of 'change' tactic
2015-03-04 20:40:06 -08:00
Leonardo de Moura
b8afba47ad
feat(library/data/list/basic): add some map, foldl, foldl, zip and unzip
2015-03-04 20:30:19 -08:00
Leonardo de Moura
c78734874d
feat(library/data/list/basic): list A has decidable equality if A has
2015-03-04 18:48:13 -08:00
Jeremy Avigad
c09f1c4eaf
feat(*.md): create markdown files for HoTT library, update ones in standard library
2015-03-04 18:33:18 -08:00
Leonardo de Moura
cc2d988aea
feat(library/data/num): prove many theorems for pos_num.lt and pos_num.le
2015-03-04 18:30:31 -08:00
Leonardo de Moura
f60fc5183a
feat(library/data/bool): add auxiliary theorems
2015-03-04 18:30:31 -08:00
Floris van Doorn
5b922aad5c
feat(init): add 'do' tactic
2015-03-04 00:17:41 -05:00
Leonardo de Moura
6ad469e717
fix(library/algebra/order): duplicate argument
2015-03-03 17:04:26 -08:00
Leonardo de Moura
e2bef88a33
fix(library/algebra/order): duplicate arguments
...
There is a 'include s' in the section
2015-03-03 16:52:12 -08:00
Leonardo de Moura
efd096e85c
feat(library/init/num): define sub and le for binary numerals
2015-03-03 15:55:16 -08:00
Leonardo de Moura
b254c78c44
refactor(library/algebra): move bundled structures to separate module
...
Motivation: performance.
After this commit, the bundled instances do not participate in the
class/instance resolution if we do not import algebra.bundled.
2015-03-02 18:45:08 -08:00
Leonardo de Moura
02d3f7c37c
refactor(library/data/list): use 'change' tactic
2015-03-01 14:27:22 -08:00
Leonardo de Moura
df13588b93
chore(library/data): remove unnecessary parentheses
2015-03-01 14:18:36 -08:00
Leonardo de Moura
ca57b43698
feat(library/tactic): add 'change' tactic
2015-03-01 14:15:39 -08:00
Leonardo de Moura
a1066ebdf4
feat(library/algebra/ordered_group): improve performance using rewrite tactic
2015-03-01 11:38:27 -08:00
Leonardo de Moura
18ab9ce4e1
feat(library/algebra/ordered_ring): improve performance using rewrite tactic
2015-03-01 10:10:44 -08:00
Leonardo de Moura
9c0375b6e2
feat(library/init/logic): add transitivity theorems for = + <->
2015-03-01 10:09:46 -08:00
Leonardo de Moura
e8ef1f97b6
feat(library/data/set): use Prop instead of bool when defining set
2015-03-01 08:23:39 -08:00
Leonardo de Moura
25df44ea43
refactor(library/algebra/category/morphism): restore previous (and more readable) proofs
2015-03-01 06:54:52 -08:00
Rob Lewis
10f1232296
feat(library/algebra/field): fix broken theorems
2015-02-28 08:49:28 -08:00
Rob Lewis
8ef2849b67
feat(library/algebra/fields): prove more theorems about division rings
2015-02-28 08:49:28 -08:00
Jeremy Avigad
a8cf58d97c
feat(library/algebra/field): define discrete field
2015-02-28 08:49:28 -08:00
Rob Lewis
eef2e99a1c
feat(library/algebra/field): add theorems about division rings
2015-02-28 08:49:05 -08:00
Rob Lewis
b8f0341119
feat(library/algebra): add field.lean
2015-02-28 08:48:48 -08:00
Floris van Doorn
23a248ab28
style(hott): let inverse notation have higher binding power than application
2015-02-28 01:16:23 -05:00
Floris van Doorn
9201bd7ca6
feat (hott/init): move nat.of_num to init.num and make it reducible outside namespace nat
...
This is so that init.trunc can already use nat.of_num.
Also make nat.of_num reducible in the standard library
Also make gt and ge abbreviations
2015-02-26 12:28:57 -05:00
Leonardo de Moura
68110faa4d
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
2015-02-25 17:00:10 -08:00
Leonardo de Moura
5ca52d81ec
feat(frontends/lean): ML-like notation for match and recursive equations
2015-02-25 16:20:44 -08:00
Leonardo de Moura
3c24461e51
refactor(*): modify '|' binding power, use 'abs a' instead of '|a|', and '(a | b)' instead of 'a | b'
2015-02-25 15:18:21 -08:00
Leonardo de Moura
c04c610b7b
feat(frontends/lean): add 'assert H : A, ...' as notation for 'have H [visible] : A, ...'
2015-02-25 14:30:42 -08:00
Jeremy Avigad
e513b0ead4
refactor(library,hott): rename theorems for decidable and inhabited
...
The convention is this: we use e.g. nat.is_inhabited and nat.has_decidable_eq
for these two purposes only, to avoid clashing with "inhabited" and "decidable_eq"
in a namespace. Otherwise, we use "decidable_foo" and "inhabited_foo".
2015-02-25 14:05:07 -08:00
Jeremy Avigad
e555531eb6
feat(library/data/int/div): start on div for integers
2015-02-25 14:05:07 -08:00
Jeremy Avigad
7a57908d62
feat/refactor(library/data/int): revise and add theorems
2015-02-25 14:05:07 -08:00
Jeremy Avigad
cfdaffb6f5
feat/refactor(library/data/nat): do some housecleaning, add facts to div
2015-02-25 14:05:07 -08:00
Jeremy Avigad
a607e7dd57
feat(library/algebra/group): add rules for sub equalities
2015-02-25 14:05:06 -08:00
Leonardo de Moura
577a6da119
refactor(library/algebra/category/morphism): reduce compilation time using rewrite tactic
2015-02-25 14:04:17 -08:00
Leonardo de Moura
4f79d12da7
refactor(library/algebra/category/morphism): improve performance using rewrite tactic
2015-02-24 18:28:49 -08:00
Leonardo de Moura
909ebfc5f1
feat(frontends/lean/elaborator): try coercions after each overload
...
We try only the easy cases since the more general case is too expensive.
closes #444
2015-02-24 17:41:20 -08:00
Leonardo de Moura
3ede8e9150
refactor(library): use []
binder annotation when declaring instances
2015-02-24 16:12:39 -08:00
Leonardo de Moura
1cd44e894b
feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible
...
closes #442
2015-02-24 16:12:35 -08:00
Leonardo de Moura
3197e6d403
feat(frontends/lean/parse_rewrite_tactic): improve rewrite tactic parser
2015-02-23 19:40:03 -08:00
Leonardo de Moura
74b8499fa9
refactor(library/data/nat/div): simplify proof of dvd_of_dvd_add_left
2015-02-17 18:55:44 -08:00
Leonardo de Moura
421a30d75c
feat(library): export [reducible] annotations from function namespace to top-level
...
see issue #433
2015-02-16 18:52:41 -08:00
Leonardo de Moura
a35cce38b3
feat(frontends/lean): new semantics for "protected" declarations
...
closes #426
2015-02-11 14:09:25 -08:00
Leonardo de Moura
c7ee831c69
refactor(library/algebra/ordered_group): use rewrite tactic at ordered_group
2015-02-08 17:35:28 -08:00
Leonardo de Moura
f9ff4ee6bd
refactor(library/algebra/ring): use rewrite tactic at ring module
2015-02-08 17:35:01 -08:00
Leonardo de Moura
d143b525f7
feat(library/algebra/ordered_group): reduce compilation time
2015-02-06 18:34:41 -08:00
Leonardo de Moura
96c161a659
feat(library/algebra/ring): simplify ring theorems using rewrite tactic
2015-02-05 18:48:02 -08:00
Leonardo de Moura
0ae6e2b3e4
feat(library/algebra/group): use rewrite tactic in the algebraic hierarchy
2015-02-05 18:03:02 -08:00
Leonardo de Moura
2ffdbba8b0
feat(library): replace same 'calc' proofs with 'rewrite'
2015-02-05 10:39:25 -08:00
Leonardo de Moura
b4dd2cc729
refactor(library/tactic/rewrite_tactic): more general rewrite step
...
The rule can be an arbitrary expression.
Allow user to provide a pattern that restricts the application of the rule.
2015-02-04 11:51:39 -08:00
Leonardo de Moura
c845e44777
feat(frontends/lean): parse rewrite tactic
2015-02-04 11:51:39 -08:00
Jeremy Avigad
77e8439012
feat(library/data/nat/div): add theorems for coprime, etc.
2015-02-03 13:50:59 -08:00
Leonardo de Moura
7e5fb3e493
fix(library/algebra/function): remove notation that conflicts with top-level notation for dependent pairs
2015-02-01 11:35:01 -08:00
Jeremy Avigad
90da0290f4
fix(library/init/{prod,sigma},library/data/sum): move notation in/out of namespaces
2015-02-01 11:17:45 -08:00
Jeremy Avigad
d48a332876
refactor(library/data/prod): move specialized theorems to quotient
2015-02-01 11:17:45 -08:00
Jeremy Avigad
3e92cd4922
feat(library/data,init/prod,sigma,sum): make more notation available at top level
2015-02-01 11:17:45 -08:00
Jeremy Avigad
5ef510f290
feat(library/logic/axioms/prop_complete): add by_cases, by_contradiction
2015-02-01 11:17:45 -08:00
Jeremy Avigad
003a2c1e2c
refactor(library/logic/axioms): rename files, import logic.axioms.classical now imports all classical axioms
2015-02-01 11:17:45 -08:00
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