max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: remove local Triple notation from SpecLemmas.lean to fix stage2 (#9967)

Browse source 
This PR removes local `Triple` notation from SpecLemmas.lean to work
around a bug that breaks the stage2 build.
This commit is contained in:
Sebastian Graf 2025-08-18 18:41:26 +02:00 • committed by GitHub
parent 2d52d44710
commit 1b0d83e7fc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 117 additions and 115 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

232
src/Std/Do/Triple/SpecLemmas.lean
View file

@ -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