Jeremy Avigad
cdecc309b3
fix(library/data/finset/to_set.lean): to_set does not require decidable equality
2015-06-01 12:35:44 +10:00
Leonardo de Moura
1238f43575
feat(library/logic/examples): add "double-negation translation" example
2015-05-31 18:18:10 -07:00
Leonardo de Moura
ca110012d8
feat(library/tactic): automate "generalize-intro-induction/cases" idiom
...
closes #645
2015-05-30 21:57:28 -07:00
Jeremy Avigad
b76445df39
feat(library/data/{nat,int}/div.lean,*): improve and extend div in nat and int
2015-05-30 22:10:21 +10:00
Jeremy Avigad
c986ee305b
refactor(library/data/nat/gcd.lean): move gcd to a new file
2015-05-30 22:10:21 +10:00
Jeremy Avigad
cc0a620db1
feat(library/data/{nat,int}/div.lean): add to and improve div library
2015-05-30 22:10:21 +10:00
Rob Lewis
82f85a574d
feat(library/data/real): prove reals form an ordered ring
2015-05-29 14:11:51 +10:00
Rob Lewis
2273dc669e
feat(library/data): fill in sorrys in int and rat orderings
2015-05-29 14:11:51 +10:00
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