Jeremy Avigad
3bf18c174e
feat(library/algebra/ordered_group): define abs in terms of max, make some theorems constructively valid
2015-06-29 15:23:11 +10:00
Jeremy Avigad
b19331f28f
feat(library/data/nat/order): add theorems for max and min
2015-06-29 15:23:11 +10:00
Jeremy Avigad
1a164d8fc9
feat(library/algebra/ordered_group): add theorems for max and min
2015-06-29 15:23:11 +10:00
Jeremy Avigad
70e551c6d6
feat(library/algebra/order,library/data/nat/order,library/*): instantiate nat to lattice, add theorems
2015-06-29 15:23:11 +10:00
Jeremy Avigad
93e5124d71
feat(library/algebra/order): add lattices, min, max
2015-06-29 15:23:11 +10:00
Jeremy Avigad
0d25831111
refactor(library/algebra/order): cleanup, and remove unused class
2015-06-29 15:23:11 +10:00
Leonardo de Moura
52564ecc0f
refactor(library/algebra/group_power): open namespaces in the "right" order
2015-06-27 14:51:00 -07:00
Leonardo de Moura
ca0aa4eb47
feat(library/composition_manager): simplify compositions of the form (mk ... (proj (mk ...)) ...)
...
closes #666
2015-06-27 14:07:32 -07:00
Leonardo de Moura
3cd81051c6
refactor(library/data/real/division): remove unnecessary 'xrewrite'
2015-06-27 14:07:32 -07:00
Leonardo de Moura
3215af3926
feat(frontends/lean): add '[trans-instance]' attribute
...
see issue #666
2015-06-27 14:07:29 -07:00
Jeremy Avigad
54128eb45f
feat(library/theories/number_theory/bezout): add Bezout's theorem, adapted from William Peterson's project
2015-06-27 19:13:36 +10:00
Jeremy Avigad
f8d8a2aed6
feat(library/data/nat/div): add characterization of mod
2015-06-27 18:51:44 +10:00
Jeremy Avigad
829c3fb22c
refactor(library/data/int/div): reorient of_nat_div and of_nat_mod
2015-06-27 18:47:36 +10:00
Jeremy Avigad
7c118f40fe
feat(library/data/nat/sub): add calculation facts for sub
2015-06-27 18:41:57 +10:00
Leonardo de Moura
97b3fd45ce
fix(library/logic/axioms/prop_decidable): fixes #704
2015-06-26 19:14:36 -07:00
Leonardo de Moura
a2cbf3dbca
refactor(library/data/fin): adjust proofs to support new approach for projections
2015-06-26 17:18:29 -07:00
Floris van Doorn
124c9d3d8a
feat(hott): various cleanup and fixes, rename \~ to ~, expand types.pointed
2015-06-25 22:31:40 -04:00
Floris van Doorn
0b9c8e14a4
fix(*/init/nat): fix occurrences where both theorem and [unfold-c] were used
2015-06-25 22:31:40 -04:00
Leonardo de Moura
1b414d36e7
refactor(library/init): define prod as an inductive datatype
...
Motivation: prod is used internally in the definitional package.
If we define prod as a structure, then Lean will tag pr1 and pr2 as
projections. This creates problems when we add special support for
projections in the elaborator. The heuristics avoid some case-splits
that are currently performed, and without them some files break.
2015-06-25 17:59:06 -07:00
Leonardo de Moura
d2e64d30e8
refactor(library/data/quotient): make proofs more robust
2015-06-25 17:48:58 -07:00
Leonardo de Moura
c9f3b766f8
refactor(library/algebra/category/constructions): modify proof
...
It was affected by the new way of handling projections that we will implement
2015-06-25 17:48:26 -07:00
Floris van Doorn
fa1979c128
feat(datatypes): let the type of unit be the lowest non-Prop universe
...
The definitional package (brec_on and cases_on) now use poly_unit instead of unit
closes #698
2015-06-25 17:33:46 -07:00
Jeremy Avigad
a0461262d0
feat(library/data/real/*.lean): migrate theorems from algebra
2015-06-25 17:30:12 -07:00
Rob Lewis
4161b9ccbf
feat(library/data/real): rearrange constant sequence theorems to introduce rat coercion earlier. begin migrating theorems from algebra
2015-06-25 17:30:12 -07:00
Rob Lewis
82950e1c52
chore(library/algebra/ordered_field): remove redundant line in calc
2015-06-25 17:30:12 -07:00
Rob Lewis
afcf785f03
chore(library/data): update data.md
2015-06-25 17:30:12 -07:00
Leonardo de Moura
8967f57818
refactor(library/data/list): reduce reliance on definitional equality
2015-06-24 15:58:19 -07:00
Leonardo de Moura
018518f0cf
refactor(library/algebra/ring): more robust proofs
2015-06-22 15:31:03 -07:00
Leonardo de Moura
7ffabeb245
refactor(library/algebra/group): avoid abuse of rewrite tactic
...
The two instances are relying on the fact that (a - b) reduces to (a + -b)
2015-06-22 15:11:14 -07:00
Leonardo de Moura
cfafc90cc0
refactor(hott,library): make sure files compile even without using "projection macros"
2015-06-22 12:22:11 -07:00
Jeremy Avigad
d28eb919f1
refactor(library/logic/axioms/examples/diaconescu.lean): mild reformatting, to match tutorial
2015-06-20 21:13:00 -07:00
Jeremy Avigad
7d204fdd91
refactor(library/data/finset/card.lean): add useful facts, shorter proof of eq_card_of_eq_subset
2015-06-20 21:13:00 -07:00
Leonardo de Moura
ee0d919c6f
feat(library/data/finset/card): add eq_of_card_eq_of_subset theorem
2015-06-19 20:05:32 -07:00
Leonardo de Moura
2910c780d0
feat(library/data/finset/basic): add auxiliary card lemma
2015-06-19 20:05:32 -07:00
Leonardo de Moura
4246a64913
feat(library/data/finset/basic): add more theorems for finset erase
2015-06-19 20:05:32 -07:00
Leonardo de Moura
5f293cee9c
refactor(library/algebra/ordered_field): improve compilation time
2015-06-18 16:12:24 -07:00
Leonardo de Moura
70fc05294b
refactor(library/local_context): avoid hack in local_context
2015-06-18 15:41:00 -07:00
Leonardo de Moura
a4c0699e81
feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic
...
See issue #676
Add new test demonstrating why it is useful to have the old semantics
for 'constructor'
2015-06-17 23:48:54 -07:00
Leonardo de Moura
d12b5613c6
feat(library/data/set): show that (set A) is a comm_semiring
2015-06-17 09:53:50 -07:00
Haitao Zhang
1aff1f7cde
fix(library/data/fintype/function): make inj_of_nodup and nodup_of_inj more general
2015-06-16 19:17:53 -07:00
Haitao Zhang
8817042318
feat(library/data/fin) : establish add_comm_group on fin using madd
2015-06-16 16:38:47 -07:00
Leonardo de Moura
d43e0891ae
fix(library/init/logic): make sure library can be compiled using '--to_axiom' option
2015-06-16 13:10:08 -07:00
Leonardo de Moura
b80a391d63
fix(library/init/sigma): make sure file compiles even when '--to_axiom' is used
2015-06-16 12:52:08 -07:00
Rob Lewis
a72ca936c0
chore(library/real): replace theorems with versions from algebra
2015-06-16 11:30:12 -07:00
Rob Lewis
f7ab2780d4
feat(library/algebra): move more theorems from reals to algebra)
2015-06-16 11:30:12 -07:00
Rob Lewis
b94d0a948d
chore(library/data/real): replace theorems with more general versions from algebra
2015-06-16 11:30:12 -07:00
Rob Lewis
b23e23061f
feat(library/algebra): finish/move more general theorems from reals to algebra)
2015-06-16 11:30:12 -07:00
Rob Lewis
8d0518444d
chore(library/data/{pnat, real}): rename pnat theorems
2015-06-16 11:30:12 -07:00
Rob Lewis
ff0ba6687e
feat(library/algebra/ordered_field): move identity about abs to ordered_field
2015-06-16 11:30:12 -07:00
Rob Lewis
090f00458d
chore(library/data/real): remove redundant theorems
2015-06-16 11:30:12 -07:00
