Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-29 02:46 a7e36e48

View on Github →

refactor(data/seq): scope seq and wseq to namespace stream (#18284) Adds namespace stream to seq and wseq to ease the Mathlib4 port (as Seq now name clashes with class Seq (has_seq in Lean 3). This requires disambiguation between stream and computation where lemmas in each namespace have the same name, and requires explicit scoping to mathlib files that reference seq and wseq (often by open stream.seq as seq)

Estimated changes

deleted def seq.append
deleted theorem seq.append_assoc
deleted theorem seq.append_nil
deleted def seq.bisim_o
deleted theorem seq.coinduction2
deleted theorem seq.coinduction
deleted def seq.cons
deleted theorem seq.cons_append
deleted theorem seq.cons_injective2
deleted theorem seq.cons_left_injective
deleted theorem seq.cons_right_injective
deleted def seq.corec.F
deleted def seq.corec
deleted theorem seq.corec_eq
deleted def seq.destruct
deleted theorem seq.destruct_cons
deleted theorem seq.destruct_eq_cons
deleted theorem seq.destruct_eq_nil
deleted theorem seq.destruct_nil
deleted def seq.drop
deleted theorem seq.dropn_add
deleted theorem seq.dropn_tail
deleted def seq.enum
deleted theorem seq.enum_cons
deleted theorem seq.enum_nil
deleted theorem seq.eq_of_bisim
deleted theorem seq.eq_or_mem_of_mem_cons
deleted theorem seq.exists_of_mem_map
deleted theorem seq.ge_stable
deleted def seq.head
deleted theorem seq.head_cons
deleted theorem seq.head_dropn
deleted theorem seq.head_eq_destruct
deleted theorem seq.head_nil
deleted def seq.is_bisimulation
deleted def seq.join
deleted theorem seq.join_append
deleted theorem seq.join_cons
deleted theorem seq.join_cons_cons
deleted theorem seq.join_cons_nil
deleted theorem seq.join_nil
deleted theorem seq.le_stable
deleted def seq.map
deleted theorem seq.map_append
deleted theorem seq.map_comp
deleted theorem seq.map_cons
deleted theorem seq.map_id
deleted theorem seq.map_nil
deleted theorem seq.map_nth
deleted theorem seq.map_tail
deleted theorem seq.mem_append_left
deleted theorem seq.mem_cons
deleted theorem seq.mem_cons_iff
deleted theorem seq.mem_cons_of_mem
deleted theorem seq.mem_map
deleted theorem seq.mem_rec_on
deleted def seq.nats
deleted theorem seq.nats_nth
deleted def seq.nil
deleted theorem seq.nil_append
deleted theorem seq.not_mem_nil
deleted theorem seq.not_terminates_iff
deleted def seq.nth
deleted theorem seq.nth_cons_succ
deleted theorem seq.nth_cons_zero
deleted theorem seq.nth_enum
deleted theorem seq.nth_mk
deleted theorem seq.nth_nil
deleted theorem seq.nth_tail
deleted theorem seq.nth_zip
deleted theorem seq.nth_zip_with
deleted def seq.of_lazy_list
deleted def seq.of_list
deleted theorem seq.of_list_append
deleted theorem seq.of_list_cons
deleted theorem seq.of_list_nil
deleted theorem seq.of_list_nth
deleted theorem seq.of_mem_append
deleted def seq.of_stream
deleted theorem seq.of_stream_append
deleted theorem seq.of_stream_cons
deleted def seq.omap
deleted def seq.rec_on
deleted def seq.split_at
deleted def seq.tail
deleted theorem seq.tail_cons
deleted theorem seq.tail_nil
deleted def seq.take
deleted def seq.terminated_at
deleted theorem seq.terminated_stable
deleted def seq.terminates
deleted def seq.to_list'
deleted def seq.to_list
deleted def seq.to_stream
deleted def seq.unzip
deleted theorem seq.val_cons
deleted def seq.zip
deleted def seq.zip_with
deleted def seq1.bind
deleted theorem seq1.bind_assoc
deleted theorem seq1.bind_ret
deleted def seq1.join
deleted theorem seq1.join_cons
deleted theorem seq1.join_join
deleted theorem seq1.join_map_ret
deleted theorem seq1.join_nil
deleted def seq1.map
deleted theorem seq1.map_id
deleted theorem seq1.map_join'
deleted theorem seq1.map_join
deleted def seq1.ret
deleted theorem seq1.ret_bind
deleted def seq1.to_seq
deleted def seq1
deleted def seq
modified def stream.is_seq
added theorem stream.seq.append_nil
added theorem stream.seq.coinduction
added def stream.seq.cons
added theorem stream.seq.cons_append
added def stream.seq.corec
added theorem stream.seq.corec_eq
added def stream.seq.drop
added theorem stream.seq.dropn_add
added theorem stream.seq.dropn_tail
added def stream.seq.enum
added theorem stream.seq.enum_cons
added theorem stream.seq.enum_nil
added theorem stream.seq.eq_of_bisim
added theorem stream.seq.ge_stable
added def stream.seq.head
added theorem stream.seq.head_cons
added theorem stream.seq.head_dropn
added theorem stream.seq.head_nil
added def stream.seq.join
added theorem stream.seq.join_append
added theorem stream.seq.join_cons
added theorem stream.seq.join_nil
added theorem stream.seq.le_stable
added def stream.seq.map
added theorem stream.seq.map_append
added theorem stream.seq.map_comp
added theorem stream.seq.map_cons
added theorem stream.seq.map_id
added theorem stream.seq.map_nil
added theorem stream.seq.map_nth
added theorem stream.seq.map_tail
added theorem stream.seq.mem_cons
added theorem stream.seq.mem_map
added theorem stream.seq.mem_rec_on
added def stream.seq.nats
added theorem stream.seq.nats_nth
added def stream.seq.nil
added theorem stream.seq.nil_append
added theorem stream.seq.not_mem_nil
added def stream.seq.nth
added theorem stream.seq.nth_enum
added theorem stream.seq.nth_mk
added theorem stream.seq.nth_nil
added theorem stream.seq.nth_tail
added theorem stream.seq.nth_zip
added theorem stream.seq.of_list_nil
added theorem stream.seq.of_list_nth
added def stream.seq.omap
added def stream.seq.tail
added theorem stream.seq.tail_cons
added theorem stream.seq.tail_nil
added def stream.seq.take
added def stream.seq.unzip
added theorem stream.seq.val_cons
added def stream.seq.zip
added def stream.seq1.bind
added theorem stream.seq1.bind_assoc
added theorem stream.seq1.bind_ret
added def stream.seq1.join
added theorem stream.seq1.join_cons
added theorem stream.seq1.join_join
added theorem stream.seq1.join_nil
added def stream.seq1.map
added theorem stream.seq1.map_id
added theorem stream.seq1.map_join'
added theorem stream.seq1.map_join
added def stream.seq1.ret
added theorem stream.seq1.ret_bind
added def stream.seq1
added def stream.seq
added def stream.wseq.all
added def stream.wseq.any
added theorem stream.wseq.append_nil
added def stream.wseq.bind
added theorem stream.wseq.bind_assoc
added theorem stream.wseq.bind_congr
added theorem stream.wseq.bind_ret
added def stream.wseq.cons
added theorem stream.wseq.cons_congr
added def stream.wseq.drop
added theorem stream.wseq.dropn_add
added theorem stream.wseq.dropn_cons
added theorem stream.wseq.dropn_nil
added theorem stream.wseq.dropn_tail
added theorem stream.wseq.equiv.ext
added theorem stream.wseq.equiv.refl
added theorem stream.wseq.equiv.symm
added def stream.wseq.find
added def stream.wseq.get
added def stream.wseq.head
added theorem stream.wseq.head_congr
added theorem stream.wseq.head_cons
added theorem stream.wseq.head_nil
added theorem stream.wseq.head_think
added def stream.wseq.join
added theorem stream.wseq.join_congr
added theorem stream.wseq.join_cons
added theorem stream.wseq.join_join
added theorem stream.wseq.join_nil
added theorem stream.wseq.join_ret
added theorem stream.wseq.join_think
added def stream.wseq.map
added theorem stream.wseq.map_append
added theorem stream.wseq.map_comp
added theorem stream.wseq.map_congr
added theorem stream.wseq.map_cons
added theorem stream.wseq.map_id
added theorem stream.wseq.map_join
added theorem stream.wseq.map_nil
added theorem stream.wseq.map_ret
added theorem stream.wseq.map_think
added theorem stream.wseq.mem_congr
added theorem stream.wseq.mem_cons
added theorem stream.wseq.mem_map
added theorem stream.wseq.mem_rec_on
added theorem stream.wseq.mem_think
added def stream.wseq.nil
added theorem stream.wseq.nil_append
added def stream.wseq.nth
added theorem stream.wseq.nth_add
added theorem stream.wseq.nth_congr
added theorem stream.wseq.nth_mem
added theorem stream.wseq.nth_of_seq
added theorem stream.wseq.nth_tail
added def stream.wseq.ret
added theorem stream.wseq.ret_bind
added def stream.wseq.tail
added theorem stream.wseq.tail_congr
added theorem stream.wseq.tail_cons
added theorem stream.wseq.tail_nil
added theorem stream.wseq.tail_think
added def stream.wseq.take
added def stream.wseq.zip
added def stream.wseq
deleted def wseq.all
deleted def wseq.any
deleted def wseq.append
deleted theorem wseq.append_assoc
deleted theorem wseq.append_nil
deleted def wseq.bind
deleted theorem wseq.bind_assoc
deleted theorem wseq.bind_congr
deleted theorem wseq.bind_ret
deleted theorem wseq.bisim_o.imp
deleted def wseq.bisim_o
deleted def wseq.collect
deleted def wseq.compute
deleted def wseq.cons
deleted theorem wseq.cons_append
deleted theorem wseq.cons_congr
deleted def wseq.destruct
deleted theorem wseq.destruct_append
deleted theorem wseq.destruct_congr
deleted theorem wseq.destruct_congr_iff
deleted theorem wseq.destruct_cons
deleted theorem wseq.destruct_dropn
deleted theorem wseq.destruct_flatten
deleted theorem wseq.destruct_join
deleted theorem wseq.destruct_map
deleted theorem wseq.destruct_nil
deleted theorem wseq.destruct_of_seq
deleted theorem wseq.destruct_tail
deleted theorem wseq.destruct_think
deleted def wseq.drop.aux
deleted theorem wseq.drop.aux_none
deleted def wseq.drop
deleted theorem wseq.dropn_add
deleted theorem wseq.dropn_congr
deleted theorem wseq.dropn_cons
deleted theorem wseq.dropn_nil
deleted theorem wseq.dropn_of_seq
deleted theorem wseq.dropn_tail
deleted theorem wseq.dropn_think
deleted theorem wseq.eq_or_mem_iff_mem
deleted theorem wseq.equiv.equivalence
deleted theorem wseq.equiv.ext
deleted theorem wseq.equiv.refl
deleted theorem wseq.equiv.symm
deleted theorem wseq.equiv.trans
deleted def wseq.equiv
deleted theorem wseq.exists_dropn_of_mem
deleted theorem wseq.exists_nth_of_mem
deleted theorem wseq.exists_of_mem_bind
deleted theorem wseq.exists_of_mem_join
deleted theorem wseq.exists_of_mem_map
deleted def wseq.filter
deleted def wseq.filter_map
deleted def wseq.find
deleted def wseq.find_index
deleted def wseq.find_indexes
deleted def wseq.flatten
deleted theorem wseq.flatten_congr
deleted theorem wseq.flatten_equiv
deleted theorem wseq.flatten_ret
deleted theorem wseq.flatten_think
deleted def wseq.get
deleted def wseq.head
deleted theorem wseq.head_congr
deleted theorem wseq.head_cons
deleted theorem wseq.head_nil
deleted theorem wseq.head_of_seq
deleted theorem wseq.head_terminates_iff
deleted theorem wseq.head_think
deleted def wseq.index_of
deleted def wseq.indexes_of
deleted def wseq.inits
deleted def wseq.is_empty
deleted def wseq.join
deleted theorem wseq.join_append
deleted theorem wseq.join_congr
deleted theorem wseq.join_cons
deleted theorem wseq.join_join
deleted theorem wseq.join_map_ret
deleted theorem wseq.join_nil
deleted theorem wseq.join_ret
deleted theorem wseq.join_think
deleted def wseq.length
deleted theorem wseq.length_eq_map
deleted theorem wseq.lift_rel.equiv
deleted theorem wseq.lift_rel.refl
deleted theorem wseq.lift_rel.swap
deleted theorem wseq.lift_rel.swap_lem
deleted theorem wseq.lift_rel.symm
deleted theorem wseq.lift_rel.trans
deleted def wseq.lift_rel
deleted theorem wseq.lift_rel_append
deleted theorem wseq.lift_rel_bind
deleted theorem wseq.lift_rel_cons
deleted theorem wseq.lift_rel_destruct
deleted theorem wseq.lift_rel_flatten
deleted theorem wseq.lift_rel_join.lem
deleted theorem wseq.lift_rel_join
deleted theorem wseq.lift_rel_map
deleted theorem wseq.lift_rel_nil
deleted theorem wseq.lift_rel_o.imp
deleted theorem wseq.lift_rel_o.imp_right
deleted theorem wseq.lift_rel_o.swap
deleted def wseq.lift_rel_o
deleted theorem wseq.lift_rel_think_left
deleted theorem wseq.lift_rel_think_right
deleted def wseq.map
deleted theorem wseq.map_append
deleted theorem wseq.map_comp
deleted theorem wseq.map_congr
deleted theorem wseq.map_cons
deleted theorem wseq.map_id
deleted theorem wseq.map_join
deleted theorem wseq.map_nil
deleted theorem wseq.map_ret
deleted theorem wseq.map_think
deleted theorem wseq.mem_append_left
deleted theorem wseq.mem_congr
deleted theorem wseq.mem_cons
deleted theorem wseq.mem_cons_iff
deleted theorem wseq.mem_cons_of_mem
deleted theorem wseq.mem_map
deleted theorem wseq.mem_of_mem_dropn
deleted theorem wseq.mem_of_mem_tail
deleted theorem wseq.mem_rec_on
deleted theorem wseq.mem_think
deleted def wseq.nil
deleted theorem wseq.nil_append
deleted theorem wseq.not_mem_nil
deleted def wseq.nth
deleted theorem wseq.nth_add
deleted theorem wseq.nth_congr
deleted theorem wseq.nth_mem
deleted theorem wseq.nth_of_seq
deleted theorem wseq.nth_tail
deleted theorem wseq.nth_terminates_le
deleted def wseq.of_list
deleted theorem wseq.of_list_cons
deleted theorem wseq.of_list_nil
deleted theorem wseq.of_mem_append
deleted def wseq.of_seq
deleted def wseq.of_stream
deleted theorem wseq.productive_congr
deleted theorem wseq.productive_iff
deleted def wseq.rec_on
deleted def wseq.remove_nth
deleted def wseq.ret
deleted theorem wseq.ret_bind
deleted def wseq.scanl
deleted theorem wseq.seq_destruct_cons
deleted theorem wseq.seq_destruct_nil
deleted theorem wseq.seq_destruct_think
deleted def wseq.split_at
deleted def wseq.tail.aux
deleted def wseq.tail
deleted theorem wseq.tail_congr
deleted theorem wseq.tail_cons
deleted theorem wseq.tail_nil
deleted theorem wseq.tail_of_seq
deleted theorem wseq.tail_think
deleted def wseq.take
deleted def wseq.think
deleted theorem wseq.think_append
deleted theorem wseq.think_congr
deleted theorem wseq.think_equiv
deleted theorem wseq.to_list'_cons
deleted theorem wseq.to_list'_map
deleted theorem wseq.to_list'_nil
deleted theorem wseq.to_list'_think
deleted def wseq.to_list
deleted theorem wseq.to_list_cons
deleted theorem wseq.to_list_nil
deleted theorem wseq.to_list_of_list
deleted def wseq.to_seq
deleted theorem wseq.to_seq_of_seq
deleted def wseq.union
deleted def wseq.update_nth
deleted def wseq.zip
deleted def wseq.zip_with
deleted def wseq