From 1b0d83e7fc207fadda64bcf66f30635077709f92 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 18 Aug 2025 18:41:26 +0200 Subject: [PATCH] fix: remove local `Triple` notation from SpecLemmas.lean to fix stage2 (#9967) This PR removes local `Triple` notation from SpecLemmas.lean to work around a bug that breaks the stage2 build. --- src/Std/Do/Triple/SpecLemmas.lean | 232 +++++++++++++++--------------- 1 file changed, 117 insertions(+), 115 deletions(-) diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index b81a8e516c..a1a0d12de5 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/src/Std/Do/Triple/SpecLemmas.lean @@ -98,12 +98,6 @@ end List 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) - /-! # `Monad` -/ universe u v @@ -111,37 +105,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 + Triple (Pure.pure (f:=m) a) (spred(P)) spred(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 + Triple (Pure.pure (f:=m) a) (spred(Q.1 a)) spred(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 : Triple x (spred(P)) (spred(fun a => wp⟦f a⟧ Q), Q.2)) : + Triple (x >>= f) (spred(P)) spred(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 + Triple (x >>= f) (spred(wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2))) spred(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] + Triple (f <$> x) (spred(wp⟦x⟧ (fun a => Q.1 (f a), Q.2))) spred(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] + Triple (x <*> y) (spred(wp⟦x⟧ (fun f => wp⟦y⟧ (fun a => Q.1 (f a), Q.2), Q.2))) spred(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] + Triple (MonadLift.monadLift x : StateT σ m α) (spred(fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2))) spred(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] + Triple (MonadLift.monadLift x : ReaderT ρ m α) (spred(fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2))) spred(Q) := by simp [Triple, SPred.entails.refl] @[spec] theorem Spec.monadLift_ExceptT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except ε ps)) : @@ -159,12 +153,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 + Triple (MonadFunctor.monadMap (m:=m) f x) (spred(fun s => wp⟦f (x.run s)⟧ (fun (a, s) => Q.1 a s, Q.2))) spred(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 + Triple (MonadFunctor.monadMap (m:=m) f x) (spred(fun s => wp⟦f (x.run s)⟧ (fun a => Q.1 a s, Q.2))) spred(Q) := .rfl @[spec] theorem Spec.monadMap_ExceptT [Monad m] [WP m ps] @@ -185,9 +179,7 @@ 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} - (MonadFunctorT.monadMap f x : m α) - ⦃Q} := by simp [Triple] + Triple (MonadFunctorT.monadMap f x : m α) (spred(wp⟦f x : m α⟧ Q)) spred(Q) := by simp [Triple] /-! # `ReaderT` -/ @@ -195,11 +187,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] + Triple (MonadReaderOf.read : ReaderT ρ m ρ) (spred(fun r => Q.1 r r)) spred(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] + Triple (MonadWithReaderOf.withReader f x : ReaderT ρ m α) (spred(fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r))) spred(Q) := by simp [Triple] /-! # `StateT` -/ @@ -207,15 +199,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] + Triple (MonadStateOf.get : StateT σ m σ) (spred(fun s => Q.1 s s)) spred(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] + Triple (MonadStateOf.set s : StateT σ m PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) spred(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 + Triple (MonadStateOf.modifyGet f : StateT σ m α) (spred(fun s => let t := f s; Q.1 t.1 t.2)) spred(Q) := by simp [Triple] /-! # `ExceptT` -/ @@ -229,47 +221,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 + Triple (MonadExceptOf.throw e : ExceptT ε m α) (spred(Q.2.1 e)) spred(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 + Triple (MonadExceptOf.tryCatch x h : ExceptT ε m α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) spred(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 + Triple (MonadExceptOf.throw e : Except ε α) (spred(Q.2.1 e)) spred(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 + Triple (MonadExceptOf.tryCatch x h : Except ε α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) spred(Q) := by simp [Triple] /-! # `EStateM` -/ @[spec] theorem Spec.get_EStateM : - ⦃fun s => Q.1 s s} (MonadStateOf.get : EStateM ε σ σ) ⦃Q} := SPred.entails.rfl + Triple (MonadStateOf.get : EStateM ε σ σ) (spred(fun s => Q.1 s s)) spred(Q) := SPred.entails.rfl @[spec] theorem Spec.set_EStateM : - ⦃fun _ => Q.1 () s} (MonadStateOf.set s : EStateM ε σ PUnit) ⦃Q} := SPred.entails.rfl + Triple (MonadStateOf.set s : EStateM ε σ PUnit) (spred(fun _ => Q.1 () s)) spred(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 + Triple (MonadStateOf.modifyGet f : EStateM ε σ α) (spred(fun s => let t := f s; Q.1 t.1 t.2)) spred(Q) := SPred.entails.rfl @[spec] theorem Spec.throw_EStateM : - ⦃Q.2.1 e} (MonadExceptOf.throw e : EStateM ε σ α) ⦃Q} := SPred.entails.rfl + Triple (MonadExceptOf.throw e : EStateM ε σ α) (spred(Q.2.1 e)) spred(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 + Triple (MonadExceptOf.tryCatch x h : EStateM ε σ α) (spred(fun s => wp⟦x⟧ (Q.1, fun e s' => wp⟦h e⟧ Q (restore s' (save s)), Q.2.2) s)) spred(Q) := by simp [Triple] /-! # Lifting `MonadStateOf` -/ @@ -289,19 +281,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 + Triple (throw e : m α) (spred(wp⟦MonadExceptOf.throw e : m α⟧ Q)) spred(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 + Triple (tryCatch x h : m α) (spred(wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q)) spred(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 + Triple (MonadExceptOf.throw e : ReaderT ρ m α) (spred(wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : ReaderT ρ m α⟧ Q)) spred(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 + Triple (MonadExceptOf.throw e : StateT σ m α) (spred(wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : StateT σ m α⟧ Q)) spred(Q) := SPred.entails.rfl @[spec] theorem Spec.throw_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) : @@ -317,15 +309,11 @@ 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)} - (MonadExceptOf.tryCatch x h : ReaderT ρ m α) - ⦃Q} := SPred.entails.rfl + Triple (MonadExceptOf.tryCatch x h : ReaderT ρ m α) (spred(fun r => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run r) (fun e => (h e).run r) : m α⟧ (fun a => Q.1 a r, Q.2))) spred(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)} - (MonadExceptOf.tryCatch x h : StateT σ m α) - ⦃Q} := SPred.entails.rfl + Triple (MonadExceptOf.tryCatch x h : StateT σ m α) (spred(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))) spred(Q) := SPred.entails.rfl @[spec] theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) : @@ -394,16 +382,18 @@ theorem Spec.forIn'_list {α β : Type u} {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs β ps) (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f cur (by simp [h]) b - ⦃(fun r => match r with - | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') - | .done b' => inv.1 (⟨xs, [], by simp⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} := by + Triple (m:=m) + (f cur (by simp [h]) b) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun r => match r with + | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') + | .done b' => inv.1 (⟨xs, [], by simp⟩, b'), inv.2)) : + Triple (forIn' xs init f) (inv.1 (⟨[], xs, rfl⟩, init)) (fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2) := by suffices h : ∀ c, - ⦃inv.1 (c, init)} - forIn' (m:=m) c.suffix init (fun a ha => f a (by simp [←c.property, ha])) - ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} + Triple + (forIn' (m:=m) c.suffix init (fun a ha => f a (by simp [←c.property, ha]))) + (inv.1 (c, init)) + (fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2) from h ⟨[], xs, rfl⟩ rintro ⟨pref, suff, h⟩ induction suff generalizing pref init @@ -428,10 +418,11 @@ 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} - 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} := + Triple + (f x hx b) + (inv.1 b) + (fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)) : + Triple (forIn' xs init f) (inv.1 init) inv := Spec.forIn'_list (fun p => inv.1 p.2, inv.2) (fun _p c _s h b => step c (by simp [h]) b) @[spec] @@ -440,12 +431,13 @@ theorem Spec.forIn_list {α β : Type u} {xs : List α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs β ps) (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f cur b - ⦃(fun r => match r with - | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') - | .done b' => inv.1 (⟨xs, [], by simp⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} := by + Triple + (f cur b) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun r => match r with + | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') + | .done b' => inv.1 (⟨xs, [], by simp⟩, b'), inv.2)) : + Triple (forIn xs init f) (inv.1 (⟨[], xs, rfl⟩, init)) (fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2) := by simp only [← forIn'_eq_forIn] exact Spec.forIn'_list inv step @@ -455,10 +447,11 @@ theorem Spec.forIn_list_const_inv {α β : Type u} {xs : List α} {init : β} {f : α → β → m (ForInStep β)} {inv : PostCond β ps} (step : ∀ hd 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} := + Triple + (f hd b) + (inv.1 b) + (fun r => match r with | .yield b' => inv.1 b' | .done b' => inv.1 b', inv.2)) : + Triple (forIn xs init f) (inv.1 init) inv := Spec.forIn_list (fun p => inv.1 p.2, inv.2) (fun _p c _s _h b => step c b) @[spec] @@ -467,10 +460,11 @@ theorem Spec.foldlM_list {α β : Type u} {xs : List α} {init : β} {f : β → α → m β} (inv : Invariant xs β ps) (step : ∀ pref cur suff (h : xs = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f b cur - ⦃(fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs, rfl⟩, init)} List.foldlM f init xs ⦃(fun b => inv.1 (⟨xs, [], by simp⟩, b), inv.2)} := by + Triple + (f b cur) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)) : + Triple (List.foldlM f init xs) (inv.1 (⟨[], xs, rfl⟩, init)) (fun b => inv.1 (⟨xs, [], by simp⟩, b), 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] @@ -484,10 +478,11 @@ theorem Spec.foldlM_list_const_inv {α β : Type u} {xs : List α} {init : β} {f : β → α → m β} {inv : PostCond β ps} (step : ∀ hd b, - ⦃inv.1 b} - f b hd - ⦃(fun b' => inv.1 b', inv.2)}) : - ⦃inv.1 init} List.foldlM f init xs ⦃inv} := + Triple + (f b hd) + (inv.1 b) + (fun b' => inv.1 b', inv.2)) : + Triple (List.foldlM f init xs) (inv.1 init) inv := Spec.foldlM_list (fun p => inv.1 p.2, inv.2) (fun _p c _s _h b => step c b) @[spec] @@ -496,12 +491,13 @@ theorem Spec.forIn'_range {β : Type} {m : Type → Type v} {ps : PostShape} {xs : Std.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β ps) (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f cur (by simp [Std.Range.mem_of_mem_range', h]) b - ⦃(fun r => match r with - | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') - | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by + Triple + (f cur (by simp [Std.Range.mem_of_mem_range', h]) b) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun r => match r with + | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') + | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) : + Triple (forIn' xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), 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 c hcur b => step c hcur b) @@ -511,12 +507,13 @@ theorem Spec.forIn_range {β : Type} {m : Type → Type v} {ps : PostShape} {xs : Std.Range} {init : β} {f : Nat → β → m (ForInStep β)} (inv : Invariant xs.toList β ps) (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f cur b - ⦃(fun r => match r with - | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') - | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by + Triple + (f cur b) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun r => match r with + | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') + | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) : + Triple (forIn xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by simp only [Std.Range.forIn_eq_forIn_range', Std.Range.size] apply Spec.forIn_list inv step @@ -531,12 +528,13 @@ theorem Spec.forIn'_prange {α β : Type u} {xs : PRange ⟨sl, su⟩ α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β ps) (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f cur (by simp [←mem_toList_iff_mem, h]) b - ⦃(fun r => match r with - | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') - | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by + Triple + (f cur (by simp [←mem_toList_iff_mem, h]) b) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun r => match r with + | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') + | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) : + Triple (forIn' xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by simp only [forIn'_eq_forIn'_toList] apply Spec.forIn'_list inv step @@ -551,12 +549,13 @@ theorem Spec.forIn_prange {α β : Type u} {xs : PRange ⟨sl, su⟩ α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β ps) (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f cur b - ⦃(fun r => match r with - | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') - | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by + Triple + (f cur b) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun r => match r with + | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') + | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) : + Triple (forIn xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by simp only [forIn] apply Spec.forIn'_prange inv step @@ -566,12 +565,13 @@ theorem Spec.forIn'_array {α β : Type u} {xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β ps) (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f cur (by simp [←Array.mem_toList_iff, h]) b - ⦃(fun r => match r with - | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') - | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn' xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by + Triple + (f cur (by simp [←Array.mem_toList_iff, h]) b) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun r => match r with + | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') + | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) : + Triple (forIn' xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by cases xs simp apply Spec.forIn'_list inv step @@ -582,12 +582,13 @@ theorem Spec.forIn_array {α β : Type u} {xs : Array α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β ps) (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f cur b - ⦃(fun r => match r with - | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') - | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} forIn xs init f ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by + Triple + (f cur b) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun r => match r with + | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b') + | .done b' => inv.1 (⟨xs.toList, [], by simp⟩, b'), inv.2)) : + Triple (forIn xs init f) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by cases xs simp apply Spec.forIn_list inv step @@ -598,10 +599,11 @@ theorem Spec.foldlM_array {α β : Type u} {xs : Array α} {init : β} {f : β → α → m β} (inv : Invariant xs.toList β ps) (step : ∀ pref cur suff (h : xs.toList = pref ++ cur :: suff) b, - ⦃inv.1 (⟨pref, cur::suff, h.symm⟩, b)} - f b cur - ⦃(fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)}) : - ⦃inv.1 (⟨[], xs.toList, rfl⟩, init)} Array.foldlM f init xs ⦃(fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2)} := by + Triple + (f b cur) + (inv.1 (⟨pref, cur::suff, h.symm⟩, b)) + (fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)) : + Triple (Array.foldlM f init xs) (inv.1 (⟨[], xs.toList, rfl⟩, init)) (fun b => inv.1 (⟨xs.toList, [], by simp⟩, b), inv.2) := by cases xs simp apply Spec.foldlM_list inv step