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.
This commit is contained in:
Sebastian Graf
GitHub
parent
cf48c6004d
commit
8f575bf986
1 changed files with 72 additions and 72 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue