Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-24 00:42 aa78466d

View on Github →

refactor(*): move in some nat lemmas and other lemmas from init

Estimated changes

Created data/array/lemmas.lean

added theorem array.mem_iff_list_mem

added theorem array.mem_iff_rev_list_mem

added theorem array.mem_iff_rev_list_mem_core

added theorem array.push_back_rev_list

added theorem array.push_back_rev_list_core

added theorem array.push_back_to_list

added def array.read_foreach

added def array.read_foreach_aux

added def array.read_map

added def array.read_map₂

added theorem array.read_write

added theorem array.read_write_eq

added theorem array.read_write_ne

added theorem array.rev_list_length

added theorem array.rev_list_length_aux

added theorem array.rev_list_reverse

added theorem array.rev_list_reverse_core

added theorem array.to_array_to_list

added theorem array.to_list_length

added theorem array.to_list_nth

added theorem array.to_list_nth_core

added theorem array.to_list_reverse

added theorem array.to_list_to_array

Modified data/bitvec.lean

Modified data/fin.lean

deleted theorem lt_succ_of_lt

Modified data/hash_map.lean

Modified data/int/basic.lean

added theorem int.abs_div_le_abs

added theorem int.add_mod_eq_add_mod_left

added theorem int.add_mod_eq_add_mod_right

added theorem int.add_mod_mod

added theorem int.add_mod_self

added theorem int.add_mod_self_left

added theorem int.add_mul_mod_self

added theorem int.add_mul_mod_self_left

added theorem int.bit0_val

added theorem int.bit1_val

added theorem int.bit_coe_nat

added theorem int.bit_decomp

added theorem int.bit_neg_succ

added theorem int.bit_val

added theorem int.bit_zero

added theorem int.bitwise_and

added theorem int.bitwise_bit

added theorem int.bitwise_diff

added theorem int.bitwise_or

added theorem int.bitwise_xor

added theorem int.bodd_add

added theorem int.bodd_add_div2

added theorem int.bodd_bit

added theorem int.bodd_mul

added theorem int.bodd_neg

added theorem int.bodd_neg_of_nat

added theorem int.bodd_one

added theorem int.bodd_sub_nat_nat

added theorem int.bodd_two

added theorem int.bodd_zero

added theorem int.coe_nat_dvd_coe_nat_iff

added theorem int.coe_nat_dvd_coe_nat_of_dvd

added theorem int.div2_bit

added theorem int.div2_val

added theorem int.div_dvd_div

added theorem int.div_eq_div_of_mul_eq_mul

added theorem int.div_eq_zero_of_lt

added theorem int.div_eq_zero_of_lt_abs

added theorem int.div_le_self

added theorem int.div_mul_cancel_of_mod_eq_zero

added theorem int.div_neg'

added theorem int.div_of_neg_of_pos

added theorem int.div_pos_of_pos_of_dvd

added theorem int.dvd_antisymm

added theorem int.dvd_iff_mod_eq_zero

added theorem int.dvd_of_coe_nat_dvd_coe_nat

added theorem int.dvd_of_mod_eq_zero

added theorem int.eq_one_of_dvd_one

added theorem int.eq_one_of_mul_eq_one_left

added theorem int.eq_one_of_mul_eq_one_right

added theorem int.land_bit

added theorem int.ldiff_bit

added theorem int.le_of_dvd

added theorem int.lnot_bit

added theorem int.lor_bit

added theorem int.lt_div_add_one_mul_self

added theorem int.lxor_bit

added theorem int.mod_abs

added theorem int.mod_add_div

added theorem int.mod_add_div_aux

added theorem int.mod_add_mod

added theorem int.mod_def

added theorem int.mod_eq_mod_of_add_mod_eq_add_mod_left

added theorem int.mod_eq_mod_of_add_mod_eq_add_mod_right

added theorem int.mod_eq_of_lt

added theorem int.mod_eq_zero_of_dvd

added theorem int.mod_lt

added theorem int.mod_lt_of_pos

added theorem int.mod_neg

added theorem int.mod_nonneg

added theorem int.mod_one

added theorem int.mod_self

added theorem int.mod_zero

added theorem int.mul_div_cancel_of_mod_eq_zero

added theorem int.mul_div_mul_of_pos

added theorem int.mul_div_mul_of_pos_left

added theorem int.mul_mod_left

added theorem int.mul_mod_mul_of_pos

added theorem int.mul_mod_right

added theorem int.neg_div_of_dvd

added theorem int.neg_succ_of_nat_div

added theorem int.neg_succ_of_nat_mod

added theorem int.of_nat_div

added theorem int.of_nat_mod

added theorem int.one_shiftl

added theorem int.shiftl_add

added theorem int.shiftl_coe_nat

added theorem int.shiftl_eq_mul_pow

added theorem int.shiftl_neg

added theorem int.shiftl_neg_succ

added theorem int.shiftl_sub

added theorem int.shiftr_add

added theorem int.shiftr_coe_nat

added theorem int.shiftr_eq_div_pow

added theorem int.shiftr_neg

added theorem int.shiftr_neg_succ

added theorem int.test_bit_bitwise

added theorem int.test_bit_land

added theorem int.test_bit_ldiff

added theorem int.test_bit_lnot

added theorem int.test_bit_lor

added theorem int.test_bit_lxor

added theorem int.test_bit_succ

added theorem int.test_bit_zero

added theorem int.zero_mod

added theorem int.zero_shiftl

added theorem int.zero_shiftr

added def int.{u}

deleted def nat_succ_eq_int_succ

deleted theorem neg_nat_succ

deleted theorem neg_pred

deleted theorem neg_succ

deleted theorem neg_succ_of_nat_eq'

deleted theorem of_nat_sub

deleted def pred

deleted theorem pred_nat_succ

deleted theorem pred_neg_pred

deleted theorem pred_succ

deleted def rec_nat_on

deleted theorem rec_nat_on_neg

deleted def succ

deleted theorem succ_neg_nat_succ

deleted theorem succ_neg_succ

deleted theorem succ_pred

Modified data/int/order.lean

added theorem int.exists_greatest_of_bdd

added theorem int.exists_least_of_bdd

Modified data/list/basic.lean

added theorem list.app_subset_of_subset_of_subset

deleted theorem list.append.assoc

added theorem list.append_foldl

added theorem list.append_foldr

added theorem list.append_inj

added theorem list.append_inj_left

added theorem list.append_inj_right

added theorem list.append_ne_nil_of_ne_nil_left

added theorem list.append_ne_nil_of_ne_nil_right

added theorem list.append_right_inj

added theorem list.concat_eq_reverse_cons

added theorem list.cons_head_tail

modified theorem list.cons_ne_nil

added theorem list.cons_sublist_cons

added theorem list.cons_subset_of_subset_of_mem

added theorem list.eq_nil_of_forall_not_mem

added theorem list.eq_nil_of_infix_nil

added theorem list.eq_nil_of_length_eq_zero

added theorem list.eq_nil_of_map_eq_nil

added theorem list.eq_nil_of_prefix_nil

added theorem list.eq_nil_of_sublist_nil

added theorem list.eq_nil_of_subset_nil

added theorem list.eq_nil_of_suffix_nil

added theorem list.eq_of_map_const

added theorem list.exists_of_mem_bind

added theorem list.exists_of_mem_join

added theorem list.exists_of_mem_map

added theorem list.ext

added theorem list.ext_le

added theorem list.filter_subset

added theorem list.foldl_hom

added theorem list.foldl_map

added theorem list.foldr_eta

added theorem list.foldr_hom

added theorem list.foldr_map

added theorem list.head_append

added theorem list.infix_append

added theorem list.infix_iff_prefix_suffix

added theorem list.infix_of_prefix

added theorem list.infix_of_suffix

added theorem list.infix_refl

modified def list.inth

deleted theorem list.inth_succ

deleted theorem list.inth_zero

deleted def list.ith

deleted theorem list.ith_succ

deleted theorem list.ith_zero

added theorem list.last_append

added theorem list.last_concat

added theorem list.last_cons

added theorem list.length_le_of_infix

added theorem list.length_map₂

added theorem list.length_pos_of_mem

added theorem list.length_remove_nth

added theorem list.length_reverse

added theorem list.length_take

added theorem list.length_take_le

deleted theorem list.length_taken_le

added theorem list.map_id'

added theorem list.map_reverse

added theorem list.mem_append_of_mem_or_mem

added theorem list.mem_bind

added theorem list.mem_bind_iff

added theorem list.mem_filter_of_mem

added theorem list.mem_inits

added theorem list.mem_join

added theorem list.mem_join_iff

added theorem list.mem_map

added theorem list.mem_map_iff

added theorem list.mem_of_mem_cons_of_mem

added theorem list.mem_of_mem_filter

added theorem list.mem_of_ne_of_mem

added theorem list.mem_or_mem_of_mem_append

added theorem list.mem_reverse

added theorem list.mem_singleton

added theorem list.mem_singleton_iff

added theorem list.mem_split

added theorem list.mem_sublists

added theorem list.mem_tails

added theorem list.ne_and_not_mem_of_not_mem_cons

added theorem list.ne_nil_of_length_eq_succ

added theorem list.ne_of_not_mem_cons

added theorem list.nil_sublist

added theorem list.not_mem_append

added theorem list.not_mem_cons_of_ne_of_not_mem

added theorem list.not_mem_of_not_mem_append_left

added theorem list.not_mem_of_not_mem_append_right

added theorem list.not_mem_of_not_mem_cons

deleted theorem list.nth_eq_some

added theorem list.nth_ge_len

added theorem list.nth_le_nth

added theorem list.nth_le_reverse

added theorem list.nth_le_reverse_aux1

added theorem list.nth_le_reverse_aux2

added theorem list.of_mem_filter

added theorem list.prefix_append

added theorem list.prefix_refl

added theorem list.reverse_append

added theorem list.reverse_cons

added theorem list.reverse_nil

added theorem list.reverse_reverse

added theorem list.reverse_singleton

added theorem list.scanr_aux_cons

added theorem list.scanr_cons

added theorem list.scanr_nil

added theorem list.span_eq_take_drop

added theorem list.split_at_eq_take_drop

added theorem list.sublist.refl

added theorem list.sublist.trans

added theorem list.sublist_app_of_sublist_left

added theorem list.sublist_app_of_sublist_right

added theorem list.sublist_append_left

added theorem list.sublist_append_right

added theorem list.sublist_cons

added theorem list.sublist_cons_of_sublist

added theorem list.sublist_of_cons_sublist

added theorem list.sublist_of_cons_sublist_cons

added theorem list.sublist_of_infix

added theorem list.sublists_aux_cons_cons

added theorem list.sublists_aux_eq_foldl

added theorem list.subset_app_of_subset_left

added theorem list.subset_app_of_subset_right

added theorem list.subset_of_sublist

added theorem list.suffix_append

added theorem list.suffix_refl

added theorem list.take_all

added theorem list.take_all_of_ge

added theorem list.take_append_drop

added theorem list.take_cons

added theorem list.take_nil

added theorem list.take_take

added theorem list.take_while_append_drop

added theorem list.take_zero

deleted theorem list.taken_all

deleted theorem list.taken_all_of_ge

deleted theorem list.taken_cons

deleted theorem list.taken_nil

deleted theorem list.taken_zero

Modified data/list/perm.lean

Modified data/nat/basic.lean

deleted def iterate

added theorem nat.add_div_left

added theorem nat.add_div_right

added theorem nat.add_mod_left

added theorem nat.add_mod_right

added theorem nat.add_mul_div_left

added theorem nat.add_mul_div_right

added theorem nat.add_mul_mod_self_left

added theorem nat.add_mul_mod_self_right

deleted theorem nat.add_one

added theorem nat.binary_rec_eq

added theorem nat.bitwise_bit

added theorem nat.bitwise_bit_aux

added theorem nat.bitwise_swap

added theorem nat.bitwise_zero

added theorem nat.bitwise_zero_left

added theorem nat.bitwise_zero_right

added theorem nat.bodd_bit

added theorem nat.cond_to_bool_mod_two

modified theorem nat.discriminate

added theorem nat.div2_bit

added theorem nat.div_mul_le_self

added theorem nat.dvd_antisymm

added theorem nat.dvd_iff_mod_eq_zero

added theorem nat.dvd_mod_iff

added theorem nat.dvd_of_mod_eq_zero

added theorem nat.dvd_of_mul_dvd_mul_left

added theorem nat.dvd_of_mul_dvd_mul_right

added theorem nat.dvd_sub

added theorem nat.eq_one_of_dvd_one

added theorem nat.eq_zero_of_mul_eq_zero

added def nat.iterate

added theorem nat.land_bit

added theorem nat.ldiff_bit

added theorem nat.le_lt_antisymm

added theorem nat.le_mul_self

added theorem nat.le_of_dvd

added theorem nat.le_succ_of_pred_le

added theorem nat.lor_bit

added theorem nat.lt_le_antisymm

added theorem nat.lt_succ_of_lt

added theorem nat.lxor_bit

added theorem nat.min_succ_succ

added theorem nat.mod_eq_zero_of_dvd

added theorem nat.mod_le

added theorem nat.mod_pow_succ

added theorem nat.mul_div_left

added theorem nat.mul_div_right

added theorem nat.mul_mod_left

added theorem nat.mul_mod_mul_left

added theorem nat.mul_mod_mul_right

added theorem nat.mul_mod_right

added theorem nat.mul_pred_left

added theorem nat.mul_pred_right

added theorem nat.mul_self_le_mul_self

added theorem nat.mul_self_le_mul_self_iff

added theorem nat.mul_self_lt_mul_self

added theorem nat.mul_self_lt_mul_self_iff

added theorem nat.mul_sub_div

added def nat.one_pos

added theorem nat.one_shiftl

added theorem nat.pos_of_dvd_of_pos

added theorem nat.pos_pow_of_pos

added theorem nat.pow_le_pow_of_le_left

added theorem nat.pow_le_pow_of_le_right

added theorem nat.pow_lt_pow_of_lt_left

added theorem nat.pow_lt_pow_of_lt_right

added theorem nat.pow_one

added theorem nat.pred_inj

added theorem nat.shiftl'_add

added theorem nat.shiftl'_sub

added theorem nat.shiftl'_tt_eq_mul_pow

added theorem nat.shiftl_add

added theorem nat.shiftl_eq_mul_pow

added theorem nat.shiftl_sub

added theorem nat.shiftr_add

added theorem nat.shiftr_eq_div_pow

added theorem nat.sub_add_min_cancel

added theorem nat.sub_eq_sub_min

added theorem nat.sub_mul_div

added theorem nat.sub_mul_mod

added theorem nat.sub_one_sub_lt

added theorem nat.succ_mul_succ_eq

added theorem nat.succ_sub

added theorem nat.succ_sub_sub_succ

added theorem nat.test_bit_bitwise

added theorem nat.test_bit_land

added theorem nat.test_bit_ldiff

added theorem nat.test_bit_lor

added theorem nat.test_bit_lxor

added theorem nat.test_bit_succ

added theorem nat.test_bit_zero

added theorem nat.zero_pow

added theorem nat.zero_shiftl

added theorem nat.zero_shiftr

Modified data/nat/gcd.lean

Modified data/nat/sub.lean

Created data/option.lean

added def option.iget

Modified data/seq/computation.lean

Modified data/seq/wseq.lean

Modified data/stream.lean