Leonardo de Moura
a06b288deb
fix(library/data/set/finite): the powerset notation has already been fixed
2015-08-16 18:47:20 -07:00
Leonardo de Moura
40ef589d8c
fix(library/data/finset,library/data/list): fixes #799
...
Make sure standard library - theories folder can be compiled with --to_axiom
2015-08-15 09:49:40 -07:00
Jeremy Avigad
e416291135
feat(library/algebra/*,library/data/*): small additions and changes
2015-08-14 18:49:57 -07:00
Jeremy Avigad
4a36f843f7
refactor(library/algebra/group_power,library/*): change definition of pow
...
I changed the definition of pow so that a^(succ n) reduces to a * a^n rather than a^n * a.
This has the nice effect that on nat and int, where multiplication is defined by recursion on the right,
a^1 reduces to a, and a^2 reduces to a * a.
The change was a pain in the neck, and in retrospect maybe not worth it, but oh, well.
2015-08-14 18:49:57 -07:00
Jeremy Avigad
f9f4cd2197
feat(library/algebra/ordered_field,library/data/int/div): prove sign a = a / abs a
2015-08-14 18:49:57 -07:00
Jeremy Avigad
a56a7d2736
feat(library/data/rat/basic): prove numerator and denominator are coprime
2015-08-14 18:49:57 -07:00
Leonardo de Moura
49eb7166f0
refactor(library/data): rename fixed_list -> tuple
2015-08-13 16:45:34 -07:00
Leonardo de Moura
9bb778dc7c
feat(library/data/hf): define head and tail for hf
2015-08-13 16:00:32 -07:00
Leonardo de Moura
a6b1c84874
feat(library/data/hf): add basic list functions to hf
2015-08-13 15:36:54 -07:00
Leonardo de Moura
50983c4573
feat(library/data/hf): prove that s₁ ⊆ s₂ → s₁ ≤ s₂ for hereditarily finite sets
2015-08-13 15:36:26 -07:00
Leonardo de Moura
aa2a417483
feat(library/data/hf): add induction and total order for hf
2015-08-13 14:11:44 -07:00
Leonardo de Moura
f4a81fdd73
fix(library/data): powerset notation
2015-08-13 09:04:00 -07:00
Leonardo de Moura
51c48277c8
feat(library/data/hf): add hf.powerset
2015-08-13 08:52:45 -07:00
Leonardo de Moura
6bec3ba58b
feat(library/data/hf): add hf.image
2015-08-13 08:22:58 -07:00
Leonardo de Moura
bf65acb126
feat(library/data/rat): show that the rationals are encodable and countable
2015-08-12 21:31:24 -07:00
Leonardo de Moura
710b7b6e40
feat(library/data/int/countable): show that int is encodable, isomorphic to nat, and countable
2015-08-12 21:31:24 -07:00
Leonardo de Moura
52f902bc33
feat(library/data/encodable): show that the quotient A/R is encodable if A is encodable and R is decidable
2015-08-12 21:31:24 -07:00
Leonardo de Moura
d2eb99bf11
refactor(library/logic): move logic/choice.lean to init/classical.lean
...
choice axiom is now in the classical namespace.
2015-08-12 18:37:33 -07:00
Leonardo de Moura
cb9830beaf
refactor(library/logic/choice): move prop_decidable instance into namespace 'classical'
2015-08-12 17:06:15 -07:00
Leonardo de Moura
b4024982a2
refactor(library/data): move vector as indexed family to examples folder
2015-08-12 15:05:14 -07:00
Leonardo de Moura
840c1a3693
refactor(library/data): rename vec to fixed_list
2015-08-12 14:38:21 -07:00
Leonardo de Moura
cee9d6b092
feat(library/data/hf): define Hereditarily finite sets
2015-08-11 16:56:06 -07:00
Leonardo de Moura
6fd3affeb1
feat(library/data/finset/equiv): show that (finset nat) is isomorphic to nat
2015-08-11 15:54:14 -07:00
Leonardo de Moura
1cacac2789
feat(library/data/nat/parity): add auxiliary lemma
2015-08-11 14:20:58 -07:00
Leonardo de Moura
a5615a6ea7
feat(library/data/finset/equiv): start bijection from (finset nat) to nat
2015-08-10 19:42:09 -07:00
Leonardo de Moura
0e98f10c96
feat(library/data/nat/div): add div_div_eq_div_mul theorem for nat
2015-08-10 19:30:00 -07:00
Leonardo de Moura
de3d0e4162
feat(library/data/list/comb): show that (list A) is isomorphic to A if A is isomorphic to nat
2015-08-10 16:04:02 -07:00
Leonardo de Moura
303e9031d6
feat(library/data/encodable): add encodable subtypes
2015-08-10 09:54:48 -07:00
Leonardo de Moura
56e2e0c0a5
feat(library/data/encodable): show that (finset A) is encodable when A is encodable
2015-08-10 07:47:00 -07:00
Leonardo de Moura
70bd95d931
feat(library/data/list): show that (sort R l1 = sort R l2) when R is a decidable total order and l1 is a permutation of l2
2015-08-09 23:36:08 -07:00
Leonardo de Moura
2a22c75e52
feat(library/data/list/sort): prove that (sort R l) is strongly_sorted
2015-08-09 23:36:07 -07:00
Leonardo de Moura
5ca37dace0
fix(library/data/nat/order): fixes #786
2015-08-09 23:36:07 -07:00
Leonardo de Moura
f9b2b93f7a
refactor(library/algebra/complete_lattice): add alternative definitions of complete_lattice and convertions between them
2015-08-09 20:40:07 -07:00
Jeremy Avigad
d17f72eb7c
fix(library/data/set/filter): adapt to change in complete_lattice structure
2015-08-09 22:36:04 -04:00
Jeremy Avigad
b130a144c8
feat(library/data/set/filter): add filters, show they form a complete lattice
2015-08-09 22:14:25 -04:00
Jeremy Avigad
244052b413
refactor(library/data/set/*): rename setext to ext
2015-08-09 22:14:25 -04:00
Jeremy Avigad
209d7b07aa
feat(library/data/set/basic): add a few theorems
2015-08-09 22:13:18 -04:00
Leonardo de Moura
276771e6ca
feat(library/data/list/sort): add sort for lists
...
TODO: prove the result is sorted, prove that l1 ~ l2 -> sort R l1 = sort R l2
2015-08-09 14:23:09 -07:00
Leonardo de Moura
b4828283fa
feat(library/data/list/sorted): add locally_sorted, sorted and strongly_sorted predicates for lists
2015-08-09 10:28:41 -07:00
Leonardo de Moura
b2415f7b4b
feat(library/data/set/basic): add basic 'set' theorems
2015-08-08 23:18:20 -07:00
Jeremy Avigad
8f815cabc0
refactor(library/data/finset/comb,library/data/set/basic,library/*): rename 'filter' to 'sep' to free up 'set.filter'
2015-08-08 18:10:44 -04:00
Jeremy Avigad
4b39400439
feat(library/data/{int,rat,real}/bigops): add bigops for int, rat, real
...
Because migrate does not handle parameters, we have to migrate by hand.
2015-08-08 17:20:23 -04:00
Jeremy Avigad
f97298394b
feat(library/data/nat/bigops,library/data/set/card,library/*): add set versions of bigops for nat
...
This required splitting data/set/card.lean from data/set/finite.lean, to avoid dependencies
2015-08-08 17:20:23 -04:00
Jeremy Avigad
eaf886cb5a
refactor(library/algebra/group_bigops,library/*): put group_bigops in 'finset' namespace, in preparation for set versions
2015-08-08 04:23:52 -07:00
Jeremy Avigad
31eed7faea
feat(library/data/set,finset): finish porting properties of card to sets
2015-08-08 04:23:52 -07:00
Jeremy Avigad
1b0773b604
feat(library/data/set/basic,finite): add more finiteness facts
2015-08-08 04:23:52 -07:00
Leonardo de Moura
06f20694c8
fix(frontends/lean/builtin_exprs): fixes #768
2015-08-08 04:20:17 -07:00
Jeremy Avigad
7df59d8b12
feat(library/data/set/finite): add more finiteness facts
2015-08-07 13:45:16 -07:00
Jeremy Avigad
eb181485eb
feat(library/data/set/finite): start the theory of finite sets
2015-08-07 13:45:16 -07:00
Jeremy Avigad
d6bde18b46
feat,refactor(library/data/{finset,set}/*,src/emacs/lean-input.el): add powerset and notation, and some tidying
2015-08-07 13:45:15 -07:00