Documentation

Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile

theorem Std.Iterators.IterM.Intermediate.dropWhileM_eq_dropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : βm (ULift Bool)} {dropping : Bool} :
theorem Std.Iterators.IterM.Intermediate.dropWhile_eq_dropWhileM {dropping : Bool} {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : βBool} :
dropWhile P dropping it = dropWhileM (pure ULift.up P) dropping it
theorem Std.Iterators.IterM.dropWhileM_eq_intermediateDropWhileM {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : βm (ULift Bool)} :
theorem Std.Iterators.IterM.dropWhile_eq_intermediateDropWhile {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : βBool} :
theorem Std.Iterators.IterM.step_intermediateDropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : βPostconditionT m (ULift Bool)} {dropping : Bool} :
(Intermediate.dropWhileWithPostcondition P dropping it).step = do let __do_liftit.step match __do_lift with | IterStep.yield it' out, h => if h' : dropping = true then do let __do_lift(P out).operation match __do_lift with | { down := true }, h'' => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P true it') ) | { down := false }, h'' => pure (PlausibleIterStep.yield (Intermediate.dropWhileWithPostcondition P false it') out ) else pure (PlausibleIterStep.yield (Intermediate.dropWhileWithPostcondition P false it') out ) | IterStep.skip it', h => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P dropping it') ) | IterStep.done, h => pure (PlausibleIterStep.done )
theorem Std.Iterators.IterM.step_dropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : βPostconditionT m (ULift Bool)} :
(dropWhileWithPostcondition P it).step = do let __do_liftit.step match __do_lift with | IterStep.yield it' out, h => do let __do_lift(P out).operation match __do_lift with | { down := true }, h'' => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P true it') ) | { down := false }, h'' => pure (PlausibleIterStep.yield (Intermediate.dropWhileWithPostcondition P false it') out ) | IterStep.skip it', h => pure (PlausibleIterStep.skip (Intermediate.dropWhileWithPostcondition P true it') ) | IterStep.done, h => pure (PlausibleIterStep.done )
theorem Std.Iterators.IterM.step_intermediateDropWhileM {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] {it : IterM m β} {P : βm (ULift Bool)} {dropping : Bool} :
(Intermediate.dropWhileM P dropping it).step = do let __do_liftit.step match __do_lift with | IterStep.yield it' out, h => if h' : dropping = true then do let __do_liftP out match __do_lift with | { down := true } => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ) | { down := false } => pure (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ) else pure (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ) | IterStep.skip it', h => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P dropping it') ) | IterStep.done, h => pure (PlausibleIterStep.done )
theorem Std.Iterators.IterM.step_dropWhileM {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] {it : IterM m β} {P : βm (ULift Bool)} :
(dropWhileM P it).step = do let __do_liftit.step match __do_lift with | IterStep.yield it' out, h => do let __do_liftP out match __do_lift with | { down := true } => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ) | { down := false } => pure (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ) | IterStep.skip it', h => pure (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ) | IterStep.done, h => pure (PlausibleIterStep.done )
theorem Std.Iterators.IterM.step_intermediateDropWhile {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] {it : IterM m β} {P : βBool} {dropping : Bool} :
(Intermediate.dropWhile P dropping it).step = do let __do_liftit.step match __do_lift with | IterStep.yield it' out, h => if h' : dropping = true then match P out with | true => pure (PlausibleIterStep.skip (Intermediate.dropWhile P true it') ) | false => pure (PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ) else pure (PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ) | IterStep.skip it', h => pure (PlausibleIterStep.skip (Intermediate.dropWhile P dropping it') ) | IterStep.done, h => pure (PlausibleIterStep.done )
theorem Std.Iterators.IterM.step_dropWhile {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [LawfulMonad m] [Iterator α m β] {it : IterM m β} {P : βBool} :
(dropWhile P it).step = do let __do_liftit.step match __do_lift with | IterStep.yield it' out, h => match P out with | true => pure (PlausibleIterStep.skip (Intermediate.dropWhile P true it') ) | false => pure (PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ) | IterStep.skip it', h => pure (PlausibleIterStep.skip (Intermediate.dropWhile P true it') ) | IterStep.done, h => pure (PlausibleIterStep.done )