Commit 2022-12-22 21:50 ca97e7ba

View on Github →

feat: port Data.Stream.Init (#849) e574b1a4e891376b0ef974b926da39e05da12a06 Due to name collisions with Stream in Lean 4, the structure is Stream' as earlier defined. Recursive proofs were changed a bit to show termination.

Estimated changes

added theorem Stream'.all_def
added theorem Stream'.any_def
added theorem Stream'.bisim_simple
added theorem Stream'.coinduction
added theorem Stream'.composition
added theorem Stream'.const_eq
added theorem Stream'.corec'_eq
added theorem Stream'.corec_def
added theorem Stream'.corec_eq
added theorem Stream'.cycle_eq
added theorem Stream'.drop_const
added theorem Stream'.drop_drop
added theorem Stream'.drop_map
added theorem Stream'.drop_succ
added theorem Stream'.drop_zip
added theorem Stream'.enum_eq_zip
added theorem Stream'.eq_of_bisim
added theorem Stream'.even_cons_cons
added theorem Stream'.even_tail
added theorem Stream'.head_cons
added theorem Stream'.head_drop
added theorem Stream'.head_even
added theorem Stream'.head_iterate
added theorem Stream'.head_map
added theorem Stream'.head_zip
added theorem Stream'.homomorphism
added theorem Stream'.identity
added theorem Stream'.inits_core_eq
added theorem Stream'.inits_eq
added theorem Stream'.inits_tail
added theorem Stream'.interchange
added theorem Stream'.interleave_eq
added theorem Stream'.iterate_eq
added theorem Stream'.iterate_id
added theorem Stream'.length_take
added theorem Stream'.map_cons
added theorem Stream'.map_const
added theorem Stream'.map_eq
added theorem Stream'.map_eq_apply
added theorem Stream'.map_id
added theorem Stream'.map_iterate
added theorem Stream'.map_map
added theorem Stream'.map_tail
added theorem Stream'.mem_cons
added theorem Stream'.mem_const
added theorem Stream'.mem_cycle
added theorem Stream'.mem_map
added theorem Stream'.mem_of_mem_odd
added theorem Stream'.mem_of_nth_eq
added theorem Stream'.nats_eq
added theorem Stream'.nth_const
added theorem Stream'.nth_drop
added theorem Stream'.nth_enum
added theorem Stream'.nth_even
added theorem Stream'.nth_inits
added theorem Stream'.nth_map
added theorem Stream'.nth_nats
added theorem Stream'.nth_odd
added theorem Stream'.nth_of_bisim
added theorem Stream'.nth_succ
added theorem Stream'.nth_succ_cons
added theorem Stream'.nth_tails
added theorem Stream'.nth_take_succ
added theorem Stream'.nth_zero_cons
added theorem Stream'.nth_zip
added theorem Stream'.odd_eq
added theorem Stream'.tail_cons
added theorem Stream'.tail_const
added theorem Stream'.tail_drop
added theorem Stream'.tail_eq_drop
added theorem Stream'.tail_even
added theorem Stream'.tail_inits
added theorem Stream'.tail_iterate
added theorem Stream'.tail_map
added theorem Stream'.tail_zip
added theorem Stream'.tails_eq
added theorem Stream'.take_succ
added theorem Stream'.take_theorem
added theorem Stream'.take_zero
added theorem Stream'.unfolds_eq
added theorem Stream'.zip_eq