From 8f575bf9868a11f7d74bbcf2e1b26c30a5b8a85e Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Sun, 3 Aug 2025 18:00:24 +0200 Subject: [PATCH] fix: Use non-overloading `Std.Do.Triple` notation in SpecLemmas.lean (#9701) This PR switches to a non-verloading local `Std.Do.Triple` notation in SpecLemmas.lean to work around a stage2 build failure. --- src/Std/Do/Triple/SpecLemmas.lean | 144 +++++++++++++++--------------- 1 file changed, 72 insertions(+), 72 deletions(-) diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index 8cded1a2e7..8a03c7e8c8 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/src/Std/Do/Triple/SpecLemmas.lean @@ -62,8 +62,8 @@ namespace Std.Do -- We override the `Triple` notation in `Std.Do.Triple.Basic` just in this module. -- The reason is that the actual `Triple` notation is implemented as an elaborator in -- `Lean.Elab.Tactic.Do.Syntax` for reasons such as #8766. Perhaps #8074 will help. -@[inherit_doc Std.Do.triple] -local notation:lead (priority := high) "⦃" P "⦄ " x:lead " ⦃" Q "⦄" => Triple x (spred(P)) spred(Q) +@[inherit_doc Std.Do.Triple] +local notation:lead (priority := high) "⦃" P "} " x:lead " ⦃" Q "}" => Triple x (spred(P)) spred(Q) /-! # `Monad` -/ @@ -72,37 +72,37 @@ variable {m : Type u → Type v} {ps : PostShape.{u}} theorem Spec.pure' [Monad m] [WPMonad m ps] {P : Assertion ps} {Q : PostCond α ps} (h : P ⊢ₛ Q.1 a) : - ⦃P⦄ Pure.pure (f:=m) a ⦃Q⦄ := Triple.pure a h + ⦃P} Pure.pure (f:=m) a ⦃Q} := Triple.pure a h @[spec] theorem Spec.pure [Monad m] [WPMonad m ps] {α} {a : α} {Q : PostCond α ps} : - ⦃Q.1 a⦄ Pure.pure (f:=m) a ⦃Q⦄ := Spec.pure' .rfl + ⦃Q.1 a} Pure.pure (f:=m) a ⦃Q} := Spec.pure' .rfl theorem Spec.bind' [Monad m] [WPMonad m ps] {x : m α} {f : α → m β} {P : Assertion ps} {Q : PostCond β ps} - (h : ⦃P⦄ x ⦃(fun a => wp⟦f a⟧ Q, Q.2)⦄) : - ⦃P⦄ (x >>= f) ⦃Q⦄ := Triple.bind x f h (fun _ => .rfl) + (h : ⦃P} x ⦃(fun a => wp⟦f a⟧ Q, Q.2)}) : + ⦃P} (x >>= f) ⦃Q} := Triple.bind x f h (fun _ => .rfl) @[spec] theorem Spec.bind [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → m β} {Q : PostCond β ps} : - ⦃wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2)⦄ (x >>= f) ⦃Q⦄ := Spec.bind' .rfl + ⦃wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2)} (x >>= f) ⦃Q} := Spec.bind' .rfl @[spec] theorem Spec.map [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → β} {Q : PostCond β ps} : - ⦃wp⟦x⟧ (fun a => Q.1 (f a), Q.2)⦄ (f <$> x) ⦃Q⦄ := by simp [Triple, SPred.entails.refl] + ⦃wp⟦x⟧ (fun a => Q.1 (f a), Q.2)} (f <$> x) ⦃Q} := by simp [Triple, SPred.entails.refl] @[spec] theorem Spec.seq [Monad m] [WPMonad m ps] {α β} {x : m (α → β)} {y : m α} {Q : PostCond β ps} : - ⦃wp⟦x⟧ (fun f => wp⟦y⟧ (fun a => Q.1 (f a), Q.2), Q.2)⦄ (x <*> y) ⦃Q⦄ := by simp [Triple, SPred.entails.refl] + ⦃wp⟦x⟧ (fun f => wp⟦y⟧ (fun a => Q.1 (f a), Q.2), Q.2)} (x <*> y) ⦃Q} := by simp [Triple, SPred.entails.refl] /-! # `MonadLift` -/ @[spec] theorem Spec.monadLift_StateT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg σ ps)) : - ⦃fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2)⦄ (MonadLift.monadLift x : StateT σ m α) ⦃Q⦄ := by simp [Triple, SPred.entails.refl] + ⦃fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2)} (MonadLift.monadLift x : StateT σ m α) ⦃Q} := by simp [Triple, SPred.entails.refl] @[spec] theorem Spec.monadLift_ReaderT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg ρ ps)) : - ⦃fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2)⦄ (MonadLift.monadLift x : ReaderT ρ m α) ⦃Q⦄ := by simp [Triple, SPred.entails.refl] + ⦃fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2)} (MonadLift.monadLift x : ReaderT ρ m α) ⦃Q} := by simp [Triple, SPred.entails.refl] @[spec] theorem Spec.monadLift_ExceptT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except ε ps)) : @@ -120,12 +120,12 @@ attribute [spec] liftM instMonadLiftTOfMonadLift instMonadLiftT @[spec] theorem Spec.monadMap_StateT [Monad m] [WP m ps] (f : ∀{β}, m β → m β) {α} (x : StateT σ m α) (Q : PostCond α (.arg σ ps)) : - ⦃fun s => wp⟦f (x.run s)⟧ (fun (a, s) => Q.1 a s, Q.2)⦄ (MonadFunctor.monadMap (m:=m) f x) ⦃Q⦄ := .rfl + ⦃fun s => wp⟦f (x.run s)⟧ (fun (a, s) => Q.1 a s, Q.2)} (MonadFunctor.monadMap (m:=m) f x) ⦃Q} := .rfl @[spec] theorem Spec.monadMap_ReaderT [Monad m] [WP m ps] (f : ∀{β}, m β → m β) {α} (x : ReaderT ρ m α) (Q : PostCond α (.arg ρ ps)) : - ⦃fun s => wp⟦f (x.run s)⟧ (fun a => Q.1 a s, Q.2)⦄ (MonadFunctor.monadMap (m:=m) f x) ⦃Q⦄ := .rfl + ⦃fun s => wp⟦f (x.run s)⟧ (fun a => Q.1 a s, Q.2)} (MonadFunctor.monadMap (m:=m) f x) ⦃Q} := .rfl @[spec] theorem Spec.monadMap_ExceptT [Monad m] [WP m ps] @@ -146,9 +146,9 @@ theorem Spec.monadMap_trans [WP o ps] [MonadFunctor n o] [MonadFunctorT m n] : @[spec] theorem Spec.monadMap_refl [WP m ps] : - ⦃wp⟦f x : m α⟧ Q⦄ + ⦃wp⟦f x : m α⟧ Q} (MonadFunctorT.monadMap f x : m α) - ⦃Q⦄ := by simp [Triple] + ⦃Q} := by simp [Triple] /-! # `ReaderT` -/ @@ -156,11 +156,11 @@ attribute [spec] ReaderT.run @[spec] theorem Spec.read_ReaderT [Monad m] [WPMonad m psm] : - ⦃fun r => Q.1 r r⦄ (MonadReaderOf.read : ReaderT ρ m ρ) ⦃Q⦄ := by simp [Triple] + ⦃fun r => Q.1 r r} (MonadReaderOf.read : ReaderT ρ m ρ) ⦃Q} := by simp [Triple] @[spec] theorem Spec.withReader_ReaderT [Monad m] [WPMonad m psm] : - ⦃fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r)⦄ (MonadWithReaderOf.withReader f x : ReaderT ρ m α) ⦃Q⦄ := by simp [Triple] + ⦃fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r)} (MonadWithReaderOf.withReader f x : ReaderT ρ m α) ⦃Q} := by simp [Triple] /-! # `StateT` -/ @@ -168,15 +168,15 @@ attribute [spec] StateT.run @[spec] theorem Spec.get_StateT [Monad m] [WPMonad m psm] : - ⦃fun s => Q.1 s s⦄ (MonadStateOf.get : StateT σ m σ) ⦃Q⦄ := by simp [Triple] + ⦃fun s => Q.1 s s} (MonadStateOf.get : StateT σ m σ) ⦃Q} := by simp [Triple] @[spec] theorem Spec.set_StateT [Monad m] [WPMonad m psm] : - ⦃fun _ => Q.1 ⟨⟩ s⦄ (MonadStateOf.set s : StateT σ m PUnit) ⦃Q⦄ := by simp [Triple] + ⦃fun _ => Q.1 ⟨⟩ s} (MonadStateOf.set s : StateT σ m PUnit) ⦃Q} := by simp [Triple] @[spec] theorem Spec.modifyGet_StateT [Monad m] [WPMonad m ps] : - ⦃fun s => let t := f s; Q.1 t.1 t.2⦄ (MonadStateOf.modifyGet f : StateT σ m α) ⦃Q⦄ := by + ⦃fun s => let t := f s; Q.1 t.1 t.2} (MonadStateOf.modifyGet f : StateT σ m α) ⦃Q} := by simp [Triple] /-! # `ExceptT` -/ @@ -190,47 +190,47 @@ theorem Spec.run_ExceptT [WP m ps] (x : ExceptT ε m α) : @[spec] theorem Spec.throw_ExceptT [Monad m] [WPMonad m ps] : - ⦃Q.2.1 e⦄ (MonadExceptOf.throw e : ExceptT ε m α) ⦃Q⦄ := by + ⦃Q.2.1 e} (MonadExceptOf.throw e : ExceptT ε m α) ⦃Q} := by simp [Triple] @[spec] theorem Spec.tryCatch_ExceptT [Monad m] [WPMonad m ps] (Q : PostCond α (.except ε ps)) : - ⦃wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2)⦄ (MonadExceptOf.tryCatch x h : ExceptT ε m α) ⦃Q⦄ := by + ⦃wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2)} (MonadExceptOf.tryCatch x h : ExceptT ε m α) ⦃Q} := by simp [Triple] /-! # `Except` -/ @[spec] theorem Spec.throw_Except [Monad m] [WPMonad m ps] : - ⦃Q.2.1 e⦄ (MonadExceptOf.throw e : Except ε α) ⦃Q⦄ := SPred.entails.rfl + ⦃Q.2.1 e} (MonadExceptOf.throw e : Except ε α) ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.tryCatch_Except (Q : PostCond α (.except ε .pure)) : - ⦃wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2)⦄ (MonadExceptOf.tryCatch x h : Except ε α) ⦃Q⦄ := by + ⦃wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2)} (MonadExceptOf.tryCatch x h : Except ε α) ⦃Q} := by simp [Triple] /-! # `EStateM` -/ @[spec] theorem Spec.get_EStateM : - ⦃fun s => Q.1 s s⦄ (MonadStateOf.get : EStateM ε σ σ) ⦃Q⦄ := SPred.entails.rfl + ⦃fun s => Q.1 s s} (MonadStateOf.get : EStateM ε σ σ) ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.set_EStateM : - ⦃fun _ => Q.1 () s⦄ (MonadStateOf.set s : EStateM ε σ PUnit) ⦃Q⦄ := SPred.entails.rfl + ⦃fun _ => Q.1 () s} (MonadStateOf.set s : EStateM ε σ PUnit) ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.modifyGet_EStateM : - ⦃fun s => let t := f s; Q.1 t.1 t.2⦄ (MonadStateOf.modifyGet f : EStateM ε σ α) ⦃Q⦄ := SPred.entails.rfl + ⦃fun s => let t := f s; Q.1 t.1 t.2} (MonadStateOf.modifyGet f : EStateM ε σ α) ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.throw_EStateM : - ⦃Q.2.1 e⦄ (MonadExceptOf.throw e : EStateM ε σ α) ⦃Q⦄ := SPred.entails.rfl + ⦃Q.2.1 e} (MonadExceptOf.throw e : EStateM ε σ α) ⦃Q} := SPred.entails.rfl open EStateM.Backtrackable in @[spec] theorem Spec.tryCatch_EStateM (Q : PostCond α (.except ε (.arg σ .pure))) : - ⦃fun s => wp⟦x⟧ (Q.1, fun e s' => wp⟦h e⟧ Q (restore s' (save s)), Q.2.2) s⦄ (MonadExceptOf.tryCatch x h : EStateM ε σ α) ⦃Q⦄ := by + ⦃fun s => wp⟦x⟧ (Q.1, fun e s' => wp⟦h e⟧ Q (restore s' (save s)), Q.2.2) s} (MonadExceptOf.tryCatch x h : EStateM ε σ α) ⦃Q} := by simp [Triple] /-! # Lifting `MonadStateOf` -/ @@ -250,19 +250,19 @@ attribute [spec] throwThe tryCatchThe @[spec] theorem Spec.throw_MonadExcept [MonadExceptOf ε m] [WP m _]: - ⦃wp⟦MonadExceptOf.throw e : m α⟧ Q⦄ (throw e : m α) ⦃Q⦄ := SPred.entails.rfl + ⦃wp⟦MonadExceptOf.throw e : m α⟧ Q} (throw e : m α) ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.tryCatch_MonadExcept [MonadExceptOf ε m] [WP m ps] (Q : PostCond α ps) : - ⦃wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q⦄ (tryCatch x h : m α) ⦃Q⦄ := SPred.entails.rfl + ⦃wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q} (tryCatch x h : m α) ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.throw_ReaderT [WP m sh] [Monad m] [MonadExceptOf ε m] : - ⦃wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : ReaderT ρ m α⟧ Q⦄ (MonadExceptOf.throw e : ReaderT ρ m α) ⦃Q⦄ := SPred.entails.rfl + ⦃wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : ReaderT ρ m α⟧ Q} (MonadExceptOf.throw e : ReaderT ρ m α) ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.throw_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg σ ps)) : - ⦃wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : StateT σ m α⟧ Q⦄ (MonadExceptOf.throw e : StateT σ m α) ⦃Q⦄ := SPred.entails.rfl + ⦃wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : StateT σ m α⟧ Q} (MonadExceptOf.throw e : StateT σ m α) ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.throw_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) : @@ -278,15 +278,15 @@ theorem Spec.throw_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : Po @[spec] theorem Spec.tryCatch_ReaderT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg ρ ps)) : - ⦃fun r => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run r) (fun e => (h e).run r) : m α⟧ (fun a => Q.1 a r, Q.2)⦄ + ⦃fun r => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run r) (fun e => (h e).run r) : m α⟧ (fun a => Q.1 a r, Q.2)} (MonadExceptOf.tryCatch x h : ReaderT ρ m α) - ⦃Q⦄ := SPred.entails.rfl + ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.tryCatch_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg σ ps)) : - ⦃fun s => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run s) (fun e => (h e).run s) : m (α × σ)⟧ (fun xs => Q.1 xs.1 xs.2, Q.2)⦄ + ⦃fun s => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run s) (fun e => (h e).run s) : m (α × σ)⟧ (fun xs => Q.1 xs.1 xs.2, Q.2)} (MonadExceptOf.tryCatch x h : StateT σ m α) - ⦃Q⦄ := SPred.entails.rfl + ⦃Q} := SPred.entails.rfl @[spec] theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) : @@ -309,16 +309,16 @@ theorem Spec.forIn'_list {α β : Type u} {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs) ps) (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs = rpref.reverse ++ x :: suff), - ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄ + ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)} f x hx b ⦃(fun r => match r with | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩) - | .done b' => inv.1 (b', ⟨xs.reverse, [], by simp⟩), inv.2)⦄) : - ⦃inv.1 (init, ⟨[], xs, by simp⟩)⦄ forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)⦄ := by + | .done b' => inv.1 (b', ⟨xs.reverse, [], by simp⟩), inv.2)}) : + ⦃inv.1 (init, ⟨[], xs, by simp⟩)} forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)} := by suffices h : ∀ rpref suff (h : xs = rpref.reverse ++ suff), - ⦃inv.1 (init, ⟨rpref, suff, by simp [h]⟩)⦄ + ⦃inv.1 (init, ⟨rpref, suff, by simp [h]⟩)} forIn' (m:=m) suff init (fun a ha => f a (by simp[h,ha])) - ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp [h]⟩), inv.2)⦄ + ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp [h]⟩), inv.2)} from h [] xs rfl intro rpref suff h induction suff generalizing rpref init @@ -343,10 +343,10 @@ theorem Spec.forIn'_list_const_inv {α β : Type u} {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} {inv : PostCond β ps} (step : ∀ x (hx : x ∈ xs) b, - ⦃inv.1 b⦄ + ⦃inv.1 b} f x hx b - ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)⦄) : - ⦃inv.1 init⦄ forIn' xs init f ⦃inv⦄ := + ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)}) : + ⦃inv.1 init} forIn' xs init f ⦃inv} := Spec.forIn'_list (fun p => inv.1 p.1, inv.2) (fun b _ x hx _ _ => step x hx b) @[spec] @@ -355,12 +355,12 @@ theorem Spec.forIn_list {α β : Type u} {xs : List α} {init : β} {f : α → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs) ps) (step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff), - ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄ + ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)} f x b ⦃(fun r => match r with | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩) - | .done b' => inv.1 (b', ⟨xs.reverse, [], by simp⟩), inv.2)⦄) : - ⦃inv.1 (init, ⟨[], xs, by simp⟩)⦄ forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)⦄ := by + | .done b' => inv.1 (b', ⟨xs.reverse, [], by simp⟩), inv.2)}) : + ⦃inv.1 (init, ⟨[], xs, by simp⟩)} forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)} := by simp only [← forIn'_eq_forIn] exact Spec.forIn'_list inv (fun b rpref x _ suff h => step b rpref x suff h) @@ -370,10 +370,10 @@ theorem Spec.forIn_list_const_inv {α β : Type u} {xs : List α} {init : β} {f : α → β → m (ForInStep β)} {inv : PostCond β ps} (step : ∀ hd b, - ⦃inv.1 b⦄ + ⦃inv.1 b} f hd b - ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)⦄) : - ⦃inv.1 init⦄ forIn xs init f ⦃inv⦄ := + ⦃(fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)}) : + ⦃inv.1 init} forIn xs init f ⦃inv} := Spec.forIn_list (fun p => inv.1 p.1, inv.2) (fun b _ hd _ _ => step hd b) @[spec] @@ -382,10 +382,10 @@ theorem Spec.foldlM_list {α β : Type u} {xs : List α} {init : β} {f : β → α → m β} (inv : PostCond (β × List.Zipper xs) ps) (step : ∀ b rpref x suff (h : xs = rpref.reverse ++ x :: suff), - ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄ + ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)} f b x - ⦃(fun b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩), inv.2)⦄) : - ⦃inv.1 (init, ⟨[], xs, by simp⟩)⦄ List.foldlM f init xs ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)⦄ := by + ⦃(fun b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩), inv.2)}) : + ⦃inv.1 (init, ⟨[], xs, by simp⟩)} List.foldlM f init xs ⦃(fun b => inv.1 (b, ⟨xs.reverse, [], by simp⟩), inv.2)} := by have : xs.foldlM f init = forIn xs init (fun a b => .yield <$> f b a) := by simp only [List.forIn_yield_eq_foldlM, id_map'] rw[this] @@ -399,10 +399,10 @@ theorem Spec.foldlM_list_const_inv {α β : Type u} {xs : List α} {init : β} {f : β → α → m β} {inv : PostCond β ps} (step : ∀ hd b, - ⦃inv.1 b⦄ + ⦃inv.1 b} f b hd - ⦃(fun b' => inv.1 b', inv.2)⦄) : - ⦃inv.1 init⦄ List.foldlM f init xs ⦃inv⦄ := + ⦃(fun b' => inv.1 b', inv.2)}) : + ⦃inv.1 init} List.foldlM f init xs ⦃inv} := Spec.foldlM_list (fun p => inv.1 p.1, inv.2) (fun b _ hd _ _ => step hd b) @[spec] @@ -411,12 +411,12 @@ theorem Spec.forIn'_range {β : Type} {m : Type → Type v} {ps : PostShape} {xs : Std.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs.toList) ps) (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff), - ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄ + ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)} f x hx b ⦃(fun r => match r with | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩) - | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄) : - ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by + | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)}) : + ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by simp only [Std.Range.forIn'_eq_forIn'_range', Std.Range.size, Std.Range.size.eq_1] apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (Std.Range.mem_of_mem_range' hx) suff h) @@ -426,12 +426,12 @@ theorem Spec.forIn_range {β : Type} {m : Type → Type v} {ps : PostShape} {xs : Std.Range} {init : β} {f : Nat → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs.toList) ps) (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff), - ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄ + ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)} f x b ⦃(fun r => match r with | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩) - | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄) : - ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by + | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)}) : + ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by simp only [Std.Range.forIn_eq_forIn_range', Std.Range.size] apply Spec.forIn_list inv step @@ -441,12 +441,12 @@ theorem Spec.forIn'_array {α β : Type u} {xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs.toList) ps) (step : ∀ b rpref x (hx : x ∈ xs) suff (h : xs.toList = rpref.reverse ++ x :: suff), - ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄ + ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)} f x hx b ⦃(fun r => match r with | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩) - | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄) : - ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by + | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)}) : + ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} forIn' xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by cases xs simp apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (by simp[hx]) suff h) @@ -457,12 +457,12 @@ theorem Spec.forIn_array {α β : Type u} {xs : Array α} {init : β} {f : α → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs.toList) ps) (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff), - ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄ + ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)} f x b ⦃(fun r => match r with | .yield b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩) - | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄) : - ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by + | .done b' => inv.1 (b', ⟨xs.toList.reverse, [], by simp⟩), inv.2)}) : + ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} forIn xs init f ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by cases xs simp apply Spec.forIn_list inv step @@ -473,10 +473,10 @@ theorem Spec.foldlM_array {α β : Type u} {xs : Array α} {init : β} {f : β → α → m β} (inv : PostCond (β × List.Zipper xs.toList) ps) (step : ∀ b rpref x suff (h : xs.toList = rpref.reverse ++ x :: suff), - ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)⦄ + ⦃inv.1 (b, ⟨rpref, x::suff, by simp [h]⟩)} f b x - ⦃(fun b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩), inv.2)⦄) : - ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)⦄ Array.foldlM f init xs ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)⦄ := by + ⦃(fun b' => inv.1 (b', ⟨x::rpref, suff, by simp [h]⟩), inv.2)}) : + ⦃inv.1 (init, ⟨[], xs.toList, by simp⟩)} Array.foldlM f init xs ⦃(fun b => inv.1 (b, ⟨xs.toList.reverse, [], by simp⟩), inv.2)} := by cases xs simp apply Spec.foldlM_list inv step