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
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
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
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
Leonardo de Moura
6db08c5519
test(library): test new tactics in the standard library
2015-05-25 16:48:33 -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
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
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
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
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
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
81d0d4aa53
fix(library/data/{set,finset}/basic.lean: delete \{{ \}}} notation (conflicts with records)
2015-05-16 17:53:35 +10: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
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
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
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
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
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
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
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
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
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
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
3912bc24c8
feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears'
2015-04-30 11:00:39 -07:00
Leonardo de Moura
018f768555
chore(library): remove some unnecessary parentheses
2015-04-29 14:39:59 -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
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
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
5eb7fef564
feat(library/algebra/order.lean, data/int/{basic,order}.lean): add theorem, correct gt_trans
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
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
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
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
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
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
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
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
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
c6c50a61b3
refactor(library/data/set/basic.lean): take advantage of extensionality in sets
2015-04-05 10:12:27 -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
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
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
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
ce5e83eb3e
refactor(library/init): move subsingleton to init folder
2015-04-01 11:57:29 -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
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
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
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
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
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
78d8e79000
fix(library/data/num): naming convention
2015-03-05 23:48:08 -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
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
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
e8ef1f97b6
feat(library/data/set): use Prop instead of bool when defining set
2015-03-01 08:23:39 -08: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
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
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
a35cce38b3
feat(frontends/lean): new semantics for "protected" declarations
...
closes #426
2015-02-11 14:09:25 -08:00
Leonardo de Moura
2ffdbba8b0
feat(library): replace same 'calc' proofs with 'rewrite'
2015-02-05 10:39:25 -08:00
Jeremy Avigad
77e8439012
feat(library/data/nat/div): add theorems for coprime, etc.
2015-02-03 13:50:59 -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
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
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
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
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
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
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
Jeremy Avigad
b11064a90e
fix(library/data/nat,int): fix instance declarations for nat and int
2015-01-03 22:27:21 -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
0f0da64264
refactor(library/data/int): make int instance of integral domain
2014-12-22 15:33:42 -05: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
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
3e9a484851
refactor(library/logic/connectives): rename theorems
2014-12-15 15:05:44 -05: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
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
97552a8cfe
refactor(library/sigma): fix/use sigma notation
2014-12-11 15:50:44 -08:00
Leonardo de Moura
05f27b8f0e
feat(frontends/lean/structure): add option for controlling whether we automatically generate eta and projection-over-intro theorems for structures
...
It seems most of the time these theorems are not used at all.
They are just polluting the namespace.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-12-09 12:40:09 -08:00
Jeremy Avigad
057615532e
feat(library/data/int): replace int definition with structure and better computational behavior
2014-12-05 22:24:42 -08:00
Leonardo de Moura
e72c4977f0
feat(frontends/lean): nicer notation for dependent if-then-else
2014-12-04 11:13:09 -08:00
Leonardo de Moura
7d19b5b743
refactor(library/data/vector): cleanup
2014-12-03 21:06:17 -08:00
Leonardo de Moura
af978e40e8
refactor(library/data/option): move 'option' declaration to init.datatypes
2014-12-03 18:53:23 -08:00
Leonardo de Moura
b094c1cf43
refactor(library/init): move num->nat coercion to init
2014-12-01 08:23:31 -08:00
Leonardo de Moura
697d4359e3
refactor(library): add 'init' folder
2014-11-30 20:34:12 -08:00
Leonardo de Moura
7dc055cfc9
chore(library/data/nat/decl): remove leftover
2014-11-30 15:10:10 -08:00
Leonardo de Moura
dad94eafbe
refactor(data/nat/decl): use new naming convention at data/nat/decl.lean
2014-11-30 15:07:09 -08:00
Leonardo de Moura
2281fb30c8
refactor(library): use "symbolic" precedences in the standard library
2014-11-29 19:08:37 -08:00
Leonardo de Moura
2c0472252e
feat(frontends/lean): allow expressions to be used to define precedence, closes #335
2014-11-29 18:29:48 -08:00
Leonardo de Moura
d7042c4618
fix(library/logic/heq): heq.to_eq must be transparent because it is needed in the 'inversion' tactic used by definitional package
2014-11-28 23:49:17 -08:00
Leonardo de Moura
cab99e2e22
refactor(library/data/vector): simplify 'vector' using new 'inversion' tactic
2014-11-28 23:19:53 -08:00
Leonardo de Moura
ae0daf9639
fix(library/data/prod/decl): give preference to unicode version when pretty printing
2014-11-28 23:02:19 -08:00
Jeremy Avigad
bb8d436e75
refactor(library/algebra/relation, library/logic/instances): revise equivalence relations and congruences to use structure command
2014-11-28 22:54:15 -08:00
Jeremy Avigad
89380f088e
feat(library): reorganize and declare some notation
2014-11-28 22:54:15 -08:00
Jeremy Avigad
f923d6a24c
feat(library/data/sum): use + notation for sum
2014-11-28 22:54:15 -08:00
Leonardo de Moura
011e955fed
refactor(library/data/fin): simplify 'fin' module using new inversion tactic
2014-11-28 22:46:06 -08:00
Leonardo de Moura
64686c1278
feat(frontends/lean): allow user to associate precedence to binders, closes #323
2014-11-23 17:30:46 -08:00
Leonardo de Moura
7231a36ec7
refactor(library/data/nat/div): remove unnecessary annotations
2014-11-23 17:30:46 -08:00
Floris van Doorn
25f5c56bb2
refactor(data/sigma): move notation from sigma.thms to sigma.decl
2014-11-22 17:44:12 -08:00
Floris van Doorn
7bfbe039d9
refactor(data.prod): move theorems about products from data.quotient.util to data.prod.thms
2014-11-22 17:44:12 -08:00
Floris van Doorn
e8b076e460
feat(hott/types/sigma): port large part of the sigma library from the hott library
...
most importantly, prove the characterization of paths in sigma types
2014-11-22 17:44:12 -08:00
Leonardo de Moura
616f2d9b82
fix(library/data/nat/div): notation should be local
2014-11-22 17:33:42 -08:00
Leonardo de Moura
ab9c51bd4b
refactor(library/data/nat/div): simplify 'gcd' definition
2014-11-22 17:19:24 -08:00
Leonardo de Moura
2af5ce364d
feat(library/data/nat/decl): add 'measure'
2014-11-22 17:19:03 -08:00
Leonardo de Moura
d07481f60f
feat(library/data/nat/div): remove some 'sorry's
2014-11-22 14:59:35 -08:00
Leonardo de Moura
9368b879bf
refactor(library/data/nat/div): use well-founded library for defining div, mod and gcd
2014-11-22 13:26:55 -08:00
Leonardo de Moura
21b16fd97c
feat(library/data/nat): add more basic theorems for definitional package
2014-11-22 13:25:46 -08:00
Leonardo de Moura
9c9f5bba1a
refactor(library/data/nat): prove auxiliary theorems about < and sub asap for the definitional package
2014-11-22 09:36:33 -08:00
Leonardo de Moura
064ecd3e3d
refactor(library/data/nat): declare lt and le asap using inductive definitions, and make key theorems transparent for definitional package
...
We also define key theorems that will be used to generate the
automatically generated a well-founded subterm relation for inductive
datatypes.
We also prove decidability and wf theorems asap.
2014-11-22 00:19:39 -08:00
Leonardo de Moura
dbb3b7c72a
refactor(library/data/nat/sub): cleanup 'max' theorems
2014-11-18 17:56:42 -08:00
Leonardo de Moura
e77cd59368
refactor(library/logic): add basic definitions for relations at logic/relation.lean
...
We need them for wf and definitional package
2014-11-18 17:32:22 -08:00
Leonardo de Moura
99c30db805
feat(library/data/fin): add fin type
2014-11-17 23:44:57 -08:00
Leonardo de Moura
e2ceb86884
feat(library/data/nat/order): add calc_trans commands for lt and le
2014-11-17 23:44:27 -08:00
Leonardo de Moura
5dc42762de
feat(library/data): define 'nat.addl' addition using recursion on the first argument, prove it to be equivalent to 'add', and use it to define vector.append
2014-11-17 22:03:39 -08:00
Leonardo de Moura
3cd3da5a84
refactor(library/data/prod/wf): remove duplication, and import wf's for sigma and prod
2014-11-16 21:19:10 -08:00
Leonardo de Moura
b7725c2949
feat(library/data/sigma/wf): define 'lex' for 'sigma' types and prove wf theorem
2014-11-16 20:08:52 -08:00
Leonardo de Moura
dd0b1ecdbf
refactor(library/data/sigma): break file into smaller pieces to reduce dependencies
2014-11-16 18:22:03 -08:00
Leonardo de Moura
53ac754328
refactor(library/data/option): cleanup using 'no_confusion'
2014-11-16 17:56:51 -08:00
Leonardo de Moura
de209f929e
feat(library/data/prod/wf): define relational product and prove wf theorem for it
2014-11-16 17:47:07 -08:00
Leonardo de Moura
bf5f48730c
refactor(library/data/subtype): define subtype using 'structure' command
2014-11-16 15:01:14 -08:00
Leonardo de Moura
b5404cd979
refactor(library/data/vector): cleanup, use variables, add concat
2014-11-15 22:36:52 -08:00
Leonardo de Moura
85f24e4c80
feat(library/data/vector): add 'zip' and 'unzip' functions
2014-11-15 22:19:23 -08:00
Leonardo de Moura
a7adfde84f
feat(library/data/vector): use 'mechanical' definitions, and add 'last' function
...
The 'mechanical' definitions are "mimicking" what the definitional
package will do.
2014-11-15 20:21:18 -08:00
Leonardo de Moura
e7a7458922
feat(library/general_notation): reserve unary minus
2014-11-13 22:08:20 -08:00
Leonardo de Moura
6bc89f0916
feat(library/definitional): define ibelow and below
...
These are helper definitions for brec_on and binduction_on
2014-11-12 16:38:46 -08:00
Leonardo de Moura
ef5a3e83ad
feat(library/data/vector): expand 'vector' module
2014-11-11 22:33:47 -08:00
Leonardo de Moura
21b93bd2e5
chore(library/data/prod/wf): remove dependency on opaque theorem
2014-11-11 00:39:53 -08:00
Leonardo de Moura
54213b48dc
feat(library/data/prod/wf): lex of well-founded relations is well-founded
2014-11-11 00:29:21 -08:00
Leonardo de Moura
76711d00c1
feat(library/data/nat/wf): define measure using inverse image
2014-11-11 00:28:46 -08:00
Leonardo de Moura
4623a62ec3
feat(library/data/nat/wf): predecessor relation is well-founded
2014-11-10 22:15:15 -08:00
Leonardo de Moura
189e5e6b48
refactor(library/data/nat/wf): mark theorem as transparent
...
It doesn't really help since
le_imp_lt_or_eq, succ_le_cancel, lt_imp_le_succ and or.elim
are still opaque
2014-11-10 12:52:02 -08:00
Floris van Doorn
780e949992
feat(empty): define negation of types
2014-11-08 19:12:54 -08:00
Leonardo de Moura
b97d437011
refactor(library/data/nat/basic): use no_confusion
construction to simplify proofs
2014-11-08 19:00:40 -08:00
Leonardo de Moura
ac5a963db3
refactor(library/data/sum): use no_confusion
construction to simplify proofs
2014-11-08 18:58:56 -08:00
Leonardo de Moura
46149d0d50
refactor(library/data/prod): break into pieces to reduce dependencies
...
prod is needed for some automatically generated constructions.
So, it is important it is loaded in the environment as early as possible.
2014-11-08 10:19:29 -08:00
Leonardo de Moura
64d2cc60c2
feat(library/data/nat/wf): add nat.lt is well founded theorem
2014-11-07 10:48:31 -08:00
Leonardo de Moura
f16f215c2a
refactor(data/num/string): break into pieces to reduce dependencies
2014-11-07 08:53:14 -08:00
Leonardo de Moura
fd34fd17de
refactor(library/data/bool): break into pieces to reduce dependencies
2014-11-07 08:41:14 -08:00
Leonardo de Moura
e993486301
refactor(library/data/num): break into pieces to reduce dependencies
2014-11-07 08:24:29 -08:00
Leonardo de Moura
60eac0195d
feat(frontends/lean/structure_cmd): generate projection over constructor theorems for structures
2014-11-04 09:10:25 -08:00
Leonardo de Moura
b24165dc7b
feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on'
2014-11-03 23:06:33 -08:00
Leonardo de Moura
d2b5af237e
refactor(library): use new 'structure' command to define prod and sigma
2014-11-03 18:57:55 -08:00
Floris van Doorn
d8a616fa70
refactor(library): major changes in the library
...
I made some major changes in the library. I wanted to wait with pushing
until I had finished the formalization of the slice functor, but for
some reason that is very hard to formalize, requiring a lot of casts and
manipulation of casts. So I've not finished that yet.
Changes:
- in multiple files make more use of variables
- move dependent congr_arg theorems to logic.cast and proof them using heq (which doesn't involve nested inductions and fewer casts).
- prove some more theorems involving heq, e.g. hcongr_arg3 (which do not
require piext)
- in theorems where casts are used in the statement use eq.rec_on
instead of eq.drec_on
- in category split basic into basic, functor and natural_transformation
- change the definition of functor to use fully bundled
categories. @avigad: this means that the file semisimplicial.lean will
also need changes (but I'm quite sure nothing major). You want to
define the fully bundled category Delta, and use only fully bundled
categories (type and ᵒᵖ are notations for the fully bundled
Type_category and Opposite if you open namespace category.ops). If you
want I can make the changes.
- lots of minor changes
2014-11-03 18:45:12 -08:00
Leonardo de Moura
ae9d11c9c4
refactor(library/data): rename prod_ext and dpair_ext to prod.eta and sigma.eta
...
Reason: they will be generated automatically by definitional package.
2014-11-03 08:29:05 -08:00
Leonardo de Moura
8d3e9fdc20
refactor(library/data/nat/basic): remove unnecessary {}
2014-10-31 09:49:45 -07:00
Leonardo de Moura
8a4d4409cd
feat(frontends/lean/calc_proof_elaborator): add '{...⁻¹}' if needed in calc proofs, closes #268
...
This commit also simplifies library/data/nat/basic.lean
2014-10-31 01:02:49 -07:00
Leonardo de Moura
5f23179388
refactor(library/data/nat): remove unnecessary !
and eq.symm
...
The calc command automatically adds them now.
2014-10-30 23:28:35 -07:00
Leonardo de Moura
09c6c05e26
chore(library/data/quotient): replace 'let' with 'have' and cleanup
2014-10-30 18:44:05 -07:00
Leonardo de Moura
407e35692b
feat(frontends/lean/calc): wrap calc proofs with 'proof-qed' annotation to identify places where proof influences what is being proved
...
Later, we will add a custom annotation and elaborator for calc proofs.
This is the first step for issue #268 .
Remark: we don't wrap the proof if it is of the form
- `by tactic`
- `begin tactic-seq end`
- `{ expr }`
2014-10-30 18:33:47 -07:00
Leonardo de Moura
ea739100b3
fix(library/unifier): broken optimization in the unifier
...
See new comments and tests for details.
2014-10-28 16:09:41 -07:00
Leonardo de Moura
777aa63660
fix(kernel/inductive): relax eliminator generation rules for empty types
...
This commit also removes the workaround false.rec_type. It is not needed anymore
2014-10-28 10:31:00 -07:00
Leonardo de Moura
aafdbf57f0
fix(library/data/unit): missing file
2014-10-25 18:34:41 -07:00
Leonardo de Moura
c7f6a6b94e
feat(library/definitional/cases_on): automatically add 'cases_on'
2014-10-25 17:22:02 -07:00
Leonardo de Moura
758a17ab23
refactor(library/data/unit): break unit.lean into smaller pieces
...
The unit datatype is used by automation.
We want to be able to access its declaration without having to access
all dependencies (e.g., decidable, subsingleton, inhabited, ...).
This is *not* an optimization, but a way to make sure we can "import" unit
before we import other declarations.
2014-10-25 14:57:33 -07:00
Leonardo de Moura
354b50a1f5
refactor(library/data/unit): make unit universe polymorphic
...
Motivation: we need it for "padding".
Example 1: defining a n-ary tuple type.
Example 2: defining cases-on for mutually recursive datatypes
2014-10-25 13:55:03 -07:00
Leonardo de Moura
cdcde661ef
feat(library/definitional/induction_on): automatically add 'induction_on'
2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
2014-10-25 13:08:59 -07:00
Soonho Kong
51125c1577
fix(library/data/quotient/default.lean): remove classical
2014-10-24 07:41:29 -07:00
Leonardo de Moura
e24225fabf
feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations
2014-10-21 15:39:47 -07:00
Leonardo de Moura
6c7e23ecaa
refactor(library): use 'reserve' notation in the standard library
2014-10-21 15:39:47 -07:00
Leonardo de Moura
2e9141b7e1
refactor(library): remove unnecessary :max
hack in notation declarations
...
This hack is not needed anymore.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-20 18:45:52 -07:00
Leonardo de Moura
854e72e665
refactor(library/data/list): minimize dependencies and avoid 'sorry' warning
2014-10-20 15:32:42 -07:00
Leonardo de Moura
f63d47fef3
feat(frontends/lean/pp): support foldl/foldr notation in the pretty printer
2014-10-19 11:16:24 -07:00
Leonardo de Moura
85339c0cc1
fix(library/data/list/basic): mark ::
as infixr
2014-10-19 08:58:52 -07:00
Leonardo de Moura
5c1d5133dd
fix(library/data/prod): make the notation for tuples and product types consistent
2014-10-13 06:48:37 -07:00
Leonardo de Moura
a26618e0f2
feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
2014-10-12 13:06:00 -07:00
Leonardo de Moura
d6d0593afb
refactor(library): remove some unnecessary sections
2014-10-10 16:33:58 -07:00
Leonardo de Moura
8f1b6178a7
chore(*): minimize the use of parameters
2014-10-09 07:13:06 -07:00
Floris van Doorn
ae3419f82f
feat(library): add definition of subsingleton and some other minor changes
2014-10-08 23:14:44 -07:00
Leonardo de Moura
c9e5e40477
refactor(library/data/num): cleanup
2014-10-05 13:47:51 -07:00
Leonardo de Moura
86591c7272
refactor(library/data/prod): cleanup
2014-10-05 13:38:08 -07:00
Leonardo de Moura
d56266c524
refactor(data/sum): use sections
2014-10-05 13:20:04 -07:00
Leonardo de Moura
15779c5d1e
refactor(data/list): use '!' operator, and new name convention for declaration names
2014-10-05 13:10:35 -07:00
Leonardo de Moura
efaeeb0726
refactor(data/nat/sub): use new policy for marking implicit arguments and '!' operator
2014-10-05 12:39:13 -07:00
Leonardo de Moura
fa96596bf7
refactor(data/int/order): use '!' operator
2014-10-05 11:44:18 -07:00
Leonardo de Moura
a0d4d82f3f
refactor(data/nat/order): use new policy for marking implicit arguments and '!' operator
2014-10-05 11:36:39 -07:00
Leonardo de Moura
73aa024c31
refactor(library/logic): remove 'core' subdirectory
2014-10-05 10:50:13 -07:00
Leonardo de Moura
317e910054
refactor(library/data/bool): use new style
2014-10-05 09:50:55 -07:00
Leonardo de Moura
4946f55290
refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-02 17:55:34 -07:00