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 |
|