Commit 2023-05-17 16:14 48c72e85

View on Github →

feat: more simp lemmas about streams (#3929) This marks many existing lemmas for Stream' as simp, and adds a few new ones. Notably, I've removed the simp attribute from take_succ because that lemma can result in huge goal states (since it duplicates the stream).

Estimated changes

Modified Mathlib/Data/Seq/Computation.lean

Modified Mathlib/Data/Seq/Seq.lean

Modified Mathlib/Data/Stream/Defs.lean

modified def Stream'.drop

deleted def Stream'.head

modified def Stream'.tail

deleted def Stream'.unfolds

Modified Mathlib/Data/Stream/Init.lean

added theorem Stream'.concat_take_nth

modified theorem Stream'.cycle_singleton

added theorem Stream'.dropLast_take

modified theorem Stream'.drop_drop

added theorem Stream'.drop_tail'

added theorem Stream'.drop_zero

added theorem Stream'.get?_take

modified theorem Stream'.get?_take_succ

modified theorem Stream'.head_drop

added theorem Stream'.nth_succ_iterate'

added theorem Stream'.nth_tail

added theorem Stream'.tail_drop'

modified theorem Stream'.tail_drop

modified theorem Stream'.tail_map

added theorem Stream'.take_succ'

added theorem Stream'.take_succ_cons

added theorem Stream'.take_take