feat: Hoare logic for monadic programs and verification condition generation (#8995)
This PR introduces a Hoare logic for monadic programs in `Std.Do.Triple`, and assorted tactics: * `mspec` for applying Hoare triple specifications * `mvcgen` to turn a Hoare triple proof obligation `⦃P⦄ prog ⦃Q⦄` into pure verification conditoins (i.e., without any traces of Hoare triples or weakest preconditions reminiscent of `prog`). The resulting verification conditions in the stateful logic of `Std.Do.SPred` can be discharged manually with the tactics coming with its custom proof mode or with automation such as `simp` and `grind`. This is pre-release of a planned feature and not yet intended for production use. We are grateful for feedback of early adopters, though. Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This commit is contained in:
Sebastian Graf
GitHub
parent
83e226204d
commit
f87d05ad4e
19 changed files with 2884 additions and 1 deletions
|
|
@ -2100,6 +2100,68 @@ introductions in sequence.
|
|||
macro (name := mintroMacro) (priority:=low) "mintro" : tactic =>
|
||||
Macro.throwError "to use `mintro`, please include `import Std.Tactic.Do`"
|
||||
|
||||
/--
|
||||
`mspec` is an `apply`-like tactic that applies a Hoare triple specification to the target of the
|
||||
stateful goal.
|
||||
|
||||
Given a stateful goal `H ⊢ₛ wp⟦prog⟧.apply Q'`, `mspec foo_spec` will instantiate
|
||||
`foo_spec : ... → ⦃P⦄ foo ⦃Q⦄`, match `foo` against `prog` and produce subgoals for
|
||||
the verification conditions `?pre : H ⊢ₛ P` and `?post : Q ⊢ₚ Q'`.
|
||||
|
||||
* If `prog = x >>= f`, then `mspec Specs.bind` is tried first so that `foo` is matched against `x`
|
||||
instead. Tactic `mspec_no_bind` does not attempt to do this decomposition.
|
||||
* If `?pre` or `?post` follow by `.rfl`, then they are discharged automatically.
|
||||
* `?post` is automatically simplified into constituent `⊢ₛ` entailments on
|
||||
success and failure continuations.
|
||||
* `?pre` and `?post.*` goals introduce their stateful hypothesis as `h`.
|
||||
* Any uninstantiated MVar arising from instantiation of `foo_spec` becomes a new subgoal.
|
||||
* If the goal looks like `fun s => _ ⊢ₛ _` then `mspec` will first `mintro ∀s`.
|
||||
* If `P` has schematic variables that can be instantiated by doing `mintro ∀s`, for example
|
||||
`foo_spec : ∀(n:Nat), ⦃⌜n = ‹Nat›ₛ⌝⦄ foo ⦃Q⦄`, then `mspec` will do `mintro ∀s` first to
|
||||
instantiate `n = s`.
|
||||
* Right before applying the spec, the `mframe` tactic is used, which has the following effect:
|
||||
Any hypothesis `Hᵢ` in the goal `h₁:H₁, h₂:H₂, ..., hₙ:Hₙ ⊢ₛ T` that is
|
||||
pure (i.e., equivalent to some `⌜φᵢ⌝`) will be moved into the pure context as `hᵢ:φᵢ`.
|
||||
|
||||
Additionally, `mspec` can be used without arguments or with a term argument:
|
||||
|
||||
* `mspec` without argument will try and look up a spec for `x` registered with `@[spec]`.
|
||||
* `mspec (foo_spec blah ?bleh)` will elaborate its argument as a term with expected type
|
||||
`⦃?P⦄ x ⦃?Q⦄` and introduce `?bleh` as a subgoal.
|
||||
This is useful to pass an invariant to e.g., `Specs.forIn_list` and leave the inductive step
|
||||
as a hole.
|
||||
-/
|
||||
macro (name := mspecMacro) (priority:=low) "mspec" : tactic =>
|
||||
Macro.throwError "to use `mspec`, please include `import Std.Tactic.Do`"
|
||||
|
||||
/--
|
||||
`mvcgen` will break down a Hoare triple proof goal like `⦃P⦄ prog ⦃Q⦄` into verification conditions,
|
||||
provided that all functions used in `prog` have specifications registered with `@[spec]`.
|
||||
|
||||
A verification condition is an entailment in the stateful logic of `Std.Do.SPred`
|
||||
in which the original program `prog` no longer occurs.
|
||||
Verification conditions are introduced by the `mspec` tactic; see the `mspec` tactic for what they
|
||||
look like.
|
||||
When there's no applicable `mspec` spec, `mvcgen` will try and rewrite an application
|
||||
`prog = f a b c` with the simp set registered via `@[spec]`.
|
||||
|
||||
When used like `mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat]`, `mvcgen` will additionally
|
||||
|
||||
* add a Hoare triple specification `foo_spec : ... → ⦃P⦄ foo ... ⦃Q⦄` to `spec` set for a
|
||||
function `foo` occurring in `prog`,
|
||||
* unfold a definition `def bar_def ... := ...` in `prog`,
|
||||
* unfold any method of the `instBEqFloat : BEq Float` instance in `prog`.
|
||||
* it will no longer substitute away `let`-expressions that occur at most once in `P`, `Q` or `prog`.
|
||||
|
||||
Furthermore, `mvcgen` tries to close trivial verification conditions by `SPred.entails.rfl` or
|
||||
the tactic sequence `try (mpure_intro; trivial)`. The variant `mvcgen_no_trivial` does not do this.
|
||||
|
||||
For debugging purposes there is also `mvcgen_step 42` which will do at most 42 VC generation
|
||||
steps. This is useful for bisecting issues with the generated VCs.
|
||||
-/
|
||||
macro (name := mvcgenMacro) (priority:=low) "mvcgen" : tactic =>
|
||||
Macro.throwError "to use `mvcgen`, please include `import Std.Tactic.Do`"
|
||||
|
||||
end Tactic
|
||||
|
||||
namespace Attr
|
||||
|
|
|
|||
|
|
@ -5,3 +5,8 @@ Authors: Sebastian Graf
|
|||
-/
|
||||
prelude
|
||||
import Lean.Elab.Tactic.Do.ProofMode
|
||||
import Lean.Elab.Tactic.Do.Syntax
|
||||
import Lean.Elab.Tactic.Do.Attr
|
||||
import Lean.Elab.Tactic.Do.LetElim
|
||||
import Lean.Elab.Tactic.Do.Spec
|
||||
import Lean.Elab.Tactic.Do.VCGen
|
||||
|
|
|
|||
235
src/Lean/Elab/Tactic/Do/Attr.lean
Normal file
235
src/Lean/Elab/Tactic/Do/Attr.lean
Normal file
|
|
@ -0,0 +1,235 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Lean.Meta
|
||||
import Std.Do.Triple.Basic
|
||||
import Std.Tactic.Do.Syntax
|
||||
|
||||
namespace Lean.Elab.Tactic.Do.SpecAttr
|
||||
|
||||
open Lean Meta Std.Do
|
||||
|
||||
builtin_initialize registerTraceClass `Elab.Tactic.Do.specAttr
|
||||
|
||||
/--
|
||||
This attribute should not be used directly.
|
||||
It is an implementation detail of the `mvcgen` tactic.
|
||||
-/
|
||||
builtin_initialize mvcgenSimpExt : Meta.SimpExtension ←
|
||||
Meta.registerSimpAttr `mvcgen_simp "simp theorems internally used by `mvcgen`"
|
||||
|
||||
/--
|
||||
The simp set accumulated by the `@[spec]` attribute.
|
||||
(This does not include Hoare triple specs.)
|
||||
It is an implementation detail of the `mvcgen` tactic.
|
||||
-/
|
||||
def getSpecSimpTheorems : CoreM SimpTheorems :=
|
||||
mvcgenSimpExt.getTheorems
|
||||
|
||||
inductive SpecProof where
|
||||
| global (declName : Name)
|
||||
| local (fvarId : FVarId)
|
||||
| stx (id : Name) (ref : Syntax) (proof : Expr)
|
||||
deriving Inhabited, BEq
|
||||
|
||||
/-- A unique identifier corresponding to the origin. -/
|
||||
def SpecProof.key : SpecProof → Name
|
||||
| .global declName => declName
|
||||
| .local fvarId => fvarId.name
|
||||
| .stx id _ _ => id
|
||||
|
||||
instance : Hashable SpecProof where
|
||||
hash sp := hash sp.key
|
||||
|
||||
def SpecProof.instantiate (proof : SpecProof) : MetaM (Array Expr × Array BinderInfo × Expr × Expr) := do
|
||||
let prf ← match proof with
|
||||
| .global declName => mkConstWithFreshMVarLevels declName
|
||||
| .local fvarId => pure <| mkFVar fvarId
|
||||
| .stx _ _ proof => pure proof -- TODO: Think about simp-like generalization
|
||||
-- We instantiate here deeply specifically for local hypotheses, the type of which
|
||||
-- may contain MVars at multiple levels.
|
||||
-- An example is `ih` in `serialize_bytesize` from the serialization schema test
|
||||
let type ← instantiateMVars (← inferType prf)
|
||||
let (xs, bs, type) ← forallMetaTelescope type
|
||||
return (xs, bs, prf.beta xs, type)
|
||||
|
||||
instance : ToMessageData SpecProof where
|
||||
toMessageData := fun
|
||||
| .global declName => m!"SpecProof.global {declName}"
|
||||
| .local fvarId => m!"SpecProof.local {mkFVar fvarId}"
|
||||
| .stx _ ref proof => m!"SpecProof.stx _ {ref} {proof}"
|
||||
|
||||
structure SpecTheorem where
|
||||
keys : Array DiscrTree.Key
|
||||
/--
|
||||
Expr key tested for matching, in ∀-quantified form.
|
||||
`keys = (← mkPath (← forallMetaTelescope prog).2.2)`.
|
||||
-/
|
||||
prog : Expr
|
||||
/-- The proof for the theorem. -/
|
||||
proof : SpecProof
|
||||
/--
|
||||
If `etaPotential` is non-zero, then the precondition contains meta variables that can be
|
||||
instantiated after applying `mintro ∀s` `etaPotential` many times.
|
||||
-/
|
||||
etaPotential : Nat := 0
|
||||
priority : Nat := eval_prio default
|
||||
deriving Inhabited, BEq
|
||||
|
||||
abbrev SpecEntry := SpecTheorem
|
||||
|
||||
structure SpecTheorems where
|
||||
specs : DiscrTree SpecTheorem := DiscrTree.empty
|
||||
erased : PHashSet SpecProof := {}
|
||||
deriving Inhabited
|
||||
|
||||
def SpecTheorems.isErased (d : SpecTheorems) (thmId : SpecProof) : Bool :=
|
||||
d.erased.contains thmId
|
||||
|
||||
def SpecTheorems.eraseCore (d : SpecTheorems) (thmId : SpecProof) : SpecTheorems :=
|
||||
{ d with erased := d.erased.insert thmId }
|
||||
|
||||
abbrev SpecExtension := SimpleScopedEnvExtension SpecEntry SpecTheorems
|
||||
|
||||
private partial def countBVarDependentMVars (xs : Array Expr) (e : Expr) : MetaM Nat :=
|
||||
go e
|
||||
where
|
||||
go (e : Expr) : MetaM Nat := do
|
||||
if !e.hasExprMVar then return 0
|
||||
match e with
|
||||
| .app f a =>
|
||||
if let some (_, lhs, rhs) := e.eq? then
|
||||
let l := lhs.getAppFn'
|
||||
let r := rhs.getAppFn'
|
||||
if l.isMVar && rhs.hasLooseBVars && xs.contains l then return 1
|
||||
if r.isMVar && lhs.hasLooseBVars && xs.contains r then return 1
|
||||
return ← (· + ·) <$> go lhs <*> go rhs
|
||||
return ← (· + ·) <$> go f <*> go a
|
||||
| .mdata _ e => go e
|
||||
| .lam _ ty b _ => (· + ·) <$> go ty <*> go b
|
||||
| .letE _ ty v b _ => (· + · + ·) <$> go ty <*> go v <*> go b
|
||||
| .forallE _ ty b _ => (· + ·) <$> go ty <*> go b
|
||||
| .proj _ _ e => go e
|
||||
| .mvar .. => return 0
|
||||
| .lit .. | .fvar .. | .bvar .. | .sort .. | .const .. => return 0
|
||||
|
||||
def simpSPredConfig : ConfigWithKey :=
|
||||
{ simpGlobalConfig.config with
|
||||
iota := true,
|
||||
beta := true,
|
||||
zeta := true,
|
||||
zetaDelta := true,
|
||||
proj := .yesWithDelta }.toConfigWithKey
|
||||
|
||||
/-- If `σs : List Type`, then `e : SPred σs`.
|
||||
Return the number of times `e` needs to be applied
|
||||
in order to assign closed solutions to meta variables. -/
|
||||
partial def computeMVarBetaPotentialForSPred (xs : Array Expr) (σs : Expr) (e : Expr) : MetaM Nat :=
|
||||
withNewMCtxDepth do
|
||||
withConfigWithKey simpSPredConfig do
|
||||
if xs.isEmpty then return 0
|
||||
let ctx ← Simp.Context.mkDefault
|
||||
let mut σs ← whnfR σs
|
||||
let mut e := e
|
||||
let mut n : Nat := 0
|
||||
let mut lastSuccess := 0
|
||||
let mut boundAssignments ← countBVarDependentMVars xs e
|
||||
while σs.isAppOfArity ``List.cons 3 do
|
||||
n := n+1
|
||||
let σ := σs.getArg! 1
|
||||
let s ← mkFreshExprMVar σ
|
||||
e := e.beta #[s]
|
||||
let (r, _) ← simp e ctx
|
||||
-- In practice we only need to reduce `fun s => ...`, `SVal.curry` and functions that operate
|
||||
-- on the state tuple bound by `SVal.curry`.
|
||||
-- We could write a custom function should `simp` become a bottleneck.
|
||||
e := r.expr
|
||||
let count ← countBVarDependentMVars xs e
|
||||
if count < boundAssignments || e.getAppFn'.isMVar then
|
||||
lastSuccess := n
|
||||
boundAssignments := count
|
||||
σs ← whnfR (σs.getArg! 2)
|
||||
return lastSuccess
|
||||
|
||||
private def mkSpecTheorem (type : Expr) (proof : SpecProof) (prio : Nat) : MetaM SpecTheorem := do
|
||||
-- cf. mkSimpTheoremCore
|
||||
let type ← instantiateMVars type
|
||||
unless (← isProp type) do
|
||||
throwError "invalid 'spec', proposition expected{indentExpr type}"
|
||||
withNewMCtxDepth do
|
||||
let (xs, _, type) ← withSimpGlobalConfig (forallMetaTelescopeReducing type)
|
||||
let type ← whnfR type
|
||||
let_expr Triple _m ps _inst _α prog P _Q := type
|
||||
| throwError "unexpected kind of spec theorem; not a triple{indentExpr type}"
|
||||
let keys ← DiscrTree.mkPath prog (noIndexAtArgs := false)
|
||||
-- beta potential of `P` describes how many times we want to `mintro ∀s`, that is,
|
||||
-- *eta*-expand the goal.
|
||||
let σs := mkApp (mkConst ``PostShape.args) ps
|
||||
let etaPotential ← computeMVarBetaPotentialForSPred xs σs P
|
||||
-- logInfo m!"Beta potential {etaPotential} for {P}"
|
||||
-- logInfo m!"mkSpecTheorem: {keys}, proof: {proof}"
|
||||
return { keys, prog := (← mkForallFVars xs prog), proof, etaPotential, priority := prio }
|
||||
|
||||
def mkSpecTheoremFromConst (declName : Name) (prio : Nat := eval_prio default) : MetaM SpecTheorem := do
|
||||
-- cf. mkSimpTheoremsFromConst
|
||||
let cinfo ← getConstInfo declName
|
||||
let us := cinfo.levelParams.map mkLevelParam
|
||||
let val := mkConst declName us
|
||||
-- withSimpGlobalConfig do -- This sets iota := false, which we do not want (for computeMVarBetaPotentialForSPred)
|
||||
let type ← inferType val
|
||||
mkSpecTheorem type (.global declName) prio
|
||||
|
||||
def mkSpecTheoremFromLocal (fvar : FVarId) (prio : Nat := eval_prio default) : MetaM SpecTheorem := do
|
||||
let some decl ← fvar.findDecl? | throwError "invalid 'spec', local constant not found"
|
||||
mkSpecTheorem decl.type (.local fvar) prio
|
||||
|
||||
def mkSpecTheoremFromStx (ref : Syntax) (proof : Expr) (prio : Nat := eval_prio default) : MetaM SpecTheorem := do
|
||||
let type ← inferType proof
|
||||
mkSpecTheorem type (.stx (← mkFreshId) ref proof) prio
|
||||
|
||||
def addSpecTheoremEntry (d : SpecTheorems) (e : SpecTheorem) : SpecTheorems :=
|
||||
{ d with specs := d.specs.insertCore e.keys e }
|
||||
|
||||
def addSpecTheorem (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) : MetaM Unit := do
|
||||
let thm ← mkSpecTheoremFromConst declName prio
|
||||
ext.add thm attrKind
|
||||
|
||||
def mkSpecExt : SimpleScopedEnvExtension.Descr SpecEntry SpecTheorems where
|
||||
name := `specMap
|
||||
initial := {}
|
||||
addEntry := fun d e => addSpecTheoremEntry d e
|
||||
|
||||
builtin_initialize specAttr : SpecExtension ← registerSimpleScopedEnvExtension mkSpecExt
|
||||
|
||||
def mkSpecAttr (ext : SpecExtension) : AttributeImpl where
|
||||
name := `spec
|
||||
descr := "Marks Hoare triple specifications and simp theorems to use with the `mspec` and `mvcgen` tactics"
|
||||
-- .afterCompilation seems unnecessarily conservative, but the simp attribute impl needs it.
|
||||
-- The reason is that we cannot annotate definitions with `@[spec]` otherwise; the error is
|
||||
-- > trying to realize id.eq_1 but `enableRealizationsForConst` must be called for 'id' first
|
||||
applicationTime := AttributeApplicationTime.afterCompilation
|
||||
add := fun declName stx attrKind => do
|
||||
let go : MetaM Unit := do
|
||||
let info ← getConstInfo declName
|
||||
let prio ← Attribute.Builtin.getPrio stx
|
||||
try
|
||||
addSpecTheorem ext declName prio attrKind
|
||||
catch _ =>
|
||||
let impl ← getBuiltinAttributeImpl `mvcgen_simp
|
||||
try
|
||||
impl.add declName stx attrKind
|
||||
catch e =>
|
||||
trace[Elab.Tactic.Do.specAttr] "Reason for failure to apply spec attribute: {e.toMessageData}"
|
||||
throwError "Invalid 'spec': target was neither a Hoare triple specification nor a 'simp' lemma"
|
||||
discard <| go.run {} {}
|
||||
|
||||
builtin_initialize registerBuiltinAttribute (mkSpecAttr specAttr)
|
||||
|
||||
def SpecExtension.getTheorems (ext : SpecExtension) : CoreM SpecTheorems :=
|
||||
return ext.getState (← getEnv)
|
||||
|
||||
def getSpecTheorems : CoreM SpecTheorems :=
|
||||
specAttr.getTheorems
|
||||
177
src/Lean/Elab/Tactic/Do/LetElim.lean
Normal file
177
src/Lean/Elab/Tactic/Do/LetElim.lean
Normal file
|
|
@ -0,0 +1,177 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Lean.Meta
|
||||
|
||||
namespace Lean.Elab.Tactic.Do
|
||||
|
||||
open Lean Meta Tactic
|
||||
|
||||
inductive Uses where
|
||||
| zero
|
||||
| one
|
||||
| many
|
||||
deriving BEq, Ord, Inhabited
|
||||
|
||||
def Uses.add : Uses → Uses → Uses
|
||||
| .zero, b => b
|
||||
| a, .zero => a
|
||||
| _, _ => .many
|
||||
|
||||
def Uses.toNat : Uses → Nat
|
||||
| .zero => 0
|
||||
| .one => 1
|
||||
| .many => 2
|
||||
|
||||
def Uses.fromNat : Nat → Uses
|
||||
| 0 => .zero
|
||||
| 1 => .one
|
||||
| _ => .many
|
||||
|
||||
instance : Add Uses where
|
||||
add := Uses.add
|
||||
|
||||
abbrev FVarUses := Std.HashMap FVarId Uses
|
||||
|
||||
def FVarUses.add (a b : FVarUses) : FVarUses :=
|
||||
a.fold (init := b) fun acc k v => acc.alter k fun
|
||||
| none => some v
|
||||
| some v' => some (v + v')
|
||||
|
||||
instance : Add FVarUses where
|
||||
add := FVarUses.add
|
||||
|
||||
inductive BVarUses (n : Nat) where
|
||||
| none
|
||||
| some (uses : Vector Uses n) -- indexed by BVars in reverse order
|
||||
|
||||
def BVarUses.single {numBVars : Nat} (n : Nat) (_ : n < numBVars := by get_elem_tactic) : BVarUses numBVars :=
|
||||
-- NB: BVarUses is indexed by BVars in reverse order
|
||||
.some <| .ofFn fun (i : Fin numBVars) => if i.val = numBVars - 1 - n then .one else .zero
|
||||
|
||||
def BVarUses.pop {numBVars : Nat} : BVarUses (numBVars + 1) → (Uses × BVarUses numBVars)
|
||||
| .none => (.zero, .none)
|
||||
| .some uses => (uses.back, .some uses.pop)
|
||||
|
||||
def BVarUses.add {numBVars : Nat} (a b : BVarUses numBVars) : BVarUses numBVars := match a, b with
|
||||
| .none, b => b
|
||||
| a, .none => a
|
||||
| .some a, .some b => .some (a.zipWith (fun a b => a + b) b)
|
||||
|
||||
instance : Add (BVarUses numBVars) where
|
||||
add := BVarUses.add
|
||||
|
||||
def over1Of2 (f : α₁ → α₂) (x : α₁ × β) : α₂ × β := (f x.1, x.2)
|
||||
|
||||
def addMData (d : MData) (e : Expr) : Expr := match e with
|
||||
| .mdata d' e => .mdata (d.mergeBy (fun _ new _ => new) d') e
|
||||
| _ => .mdata d e
|
||||
|
||||
private def okToDup (e : Expr) : Bool := match e with
|
||||
| .bvar .. => true
|
||||
| .fvar .. => false -- viable, but would invalidate use information (which we could work around)
|
||||
| .lit .. | .const .. | .sort .. | .mvar .. => true
|
||||
| .mdata _ e => okToDup e
|
||||
| .proj _ _ e => okToDup e -- Not sure about this one. Do we want to duplicate projs?
|
||||
| .app .. => Simp.isOfNatNatLit e || Simp.isOfScientificLit e || Simp.isCharLit e
|
||||
| .lam .. | .forallE .. | .letE .. => false
|
||||
|
||||
mutual
|
||||
partial def countUsesDecl (fvarId : FVarId) (ty : Expr) (val? : Option Expr) (bodyUses : FVarUses) (subst : Array FVarId := #[]) : MetaM (Expr × Option Expr × FVarUses) := do
|
||||
let (ty, tyUses) ← countUses ty subst
|
||||
let (val?, valUses) ← match val? with
|
||||
| none => pure (none, {})
|
||||
| some val => over1Of2 some <$> countUses val subst
|
||||
let uses := bodyUses.getD fvarId .zero
|
||||
let fvs := if uses == .zero then bodyUses else bodyUses + tyUses + valUses
|
||||
let fvs := fvs.erase fvarId
|
||||
let ty := addMData (MData.empty.setNat `uses uses.toNat) ty
|
||||
return (ty, val?, fvs)
|
||||
|
||||
partial def countUses (e : Expr) (subst : Array FVarId := #[]) : MetaM (Expr × FVarUses) := match e with
|
||||
| .bvar n =>
|
||||
if _ : n < subst.size then
|
||||
return (e, {(subst[n], .one)})
|
||||
else
|
||||
throwError "BVar index out of bounds: {n} >= {subst.size}"
|
||||
| .fvar fvarId => return (e, {(fvarId, .one)})
|
||||
| .letE x ty val body b => do
|
||||
let fv ← mkFreshFVarId
|
||||
let (body, fvs) ← countUses body (subst.push fv)
|
||||
let (ty, .some val, fvs) ← countUsesDecl fv ty (some val) fvs subst | failure
|
||||
return (.letE x ty val body b, fvs)
|
||||
| .lam x ty body bi => do
|
||||
let fv ← mkFreshFVarId
|
||||
let (ty, fvs₁) ← countUses ty subst
|
||||
let (body, fvs₂) ← countUses body (subst.push fv)
|
||||
let fvs := (fvs₁ + fvs₂).erase fv
|
||||
return (.lam x ty body bi, fvs) -- NB: We do not track uses of lam-bound x
|
||||
| .forallE x ty body bi => do -- (almost) identical to lam
|
||||
let fv ← mkFreshFVarId
|
||||
let (ty, fvs₁) ← countUses ty subst
|
||||
let (body, fvs₂) ← countUses body (subst.push fv)
|
||||
let fvs := (fvs₁ + fvs₂).erase fv
|
||||
return (.forallE x ty body bi, fvs) -- NB: We do not track uses of forall-bound x
|
||||
| .proj s i e => over1Of2 (Expr.proj s i) <$> countUses e subst
|
||||
| .mdata d e => over1Of2 (Expr.mdata d) <$> countUses e subst
|
||||
| .app f a => do
|
||||
let (f, fvarUses₁) ← countUses f subst
|
||||
let (a, fvarUses₂) ← countUses a subst
|
||||
return (.app f a, fvarUses₁ + fvarUses₂)
|
||||
| .lit .. | .const .. | .sort .. | .mvar .. => return (e, {})
|
||||
end
|
||||
|
||||
def countUsesLCtx (ctx : LocalContext) (targetUses : FVarUses) : MetaM LocalContext := do
|
||||
let decls : Array LocalDecl := Array.mkEmpty ctx.decls.size
|
||||
let decls ← Prod.fst <$> ctx.foldrM (init := (decls, targetUses)) fun decl (decls, targetUses) => do
|
||||
let (ty, val?, fvs) ← countUsesDecl decl.fvarId decl.type decl.value? targetUses
|
||||
let decl := match val? with
|
||||
| none => decl.setType ty
|
||||
| some val => decl.setType ty |>.setValue val
|
||||
return (decls.push decl, fvs)
|
||||
-- NB: decls are in reverse order; root comes first
|
||||
let decls ← StateRefT'.run' (ω:=IO.RealWorld) (s := decls) <| ctx.decls.mapM fun decl => do
|
||||
if decl.isNone then return decl
|
||||
modifyGet fun (decls : Array LocalDecl) => (some decls.back!, decls.pop)
|
||||
return { ctx with decls }
|
||||
|
||||
def doNotDup (u : Uses) (rhs : Expr) (elimTrivial : Bool) : Bool :=
|
||||
u == .many && not (elimTrivial && okToDup rhs)
|
||||
|
||||
def elimLetsCore (e : Expr) (elimTrivial := true) : MetaM Expr := StateRefT'.run' (s := Std.HashSet.emptyWithCapacity 10) do
|
||||
-- Figure out if we can make this work with Core.transform.
|
||||
-- I think that would entail keeping track of BVar shifts in `pre` and `post`.
|
||||
let pre (e : Expr) : StateRefT (Std.HashSet FVarId) MetaM TransformStep := do
|
||||
match e with
|
||||
| .letE _ ty val body _ => do
|
||||
let .mdata d _ := ty | return .continue
|
||||
let uses := Uses.fromNat (d.getNat `uses 2) -- 2 goes to .many
|
||||
if doNotDup uses val elimTrivial then return .continue
|
||||
return .visit (body.instantiate1 val) -- urgh O(n^2). See comment above
|
||||
| _ => return .continue
|
||||
Meta.transform e (pre := pre)
|
||||
|
||||
def elimLets (mvar : MVarId) (elimTrivial := true): MetaM MVarId := mvar.withContext do
|
||||
let ctx ← getLCtx
|
||||
let (ty, fvarUses) ← countUses (← mvar.getType)
|
||||
let ctx ← countUsesLCtx ctx fvarUses
|
||||
let mut fvs := #[]
|
||||
let mut vals := #[]
|
||||
for decl in ctx do
|
||||
let .some val := decl.value? | continue
|
||||
let .mdata d _ := decl.type | continue
|
||||
let uses := Uses.fromNat (d.getNat `uses 2) -- 2 goes to .many
|
||||
if doNotDup uses val elimTrivial then continue
|
||||
fvs := fvs.push (mkFVar decl.fvarId)
|
||||
vals := vals.push val
|
||||
let ty := ty.replaceFVars fvs vals
|
||||
let ty ← elimLetsCore ty elimTrivial
|
||||
let newMVar ← mkFreshExprSyntheticOpaqueMVar ty (← mvar.getTag)
|
||||
mvar.assign newMVar
|
||||
let mut mvar := newMVar.mvarId!
|
||||
for fvarId in fvs do
|
||||
mvar ← mvar.tryClear fvarId.fvarId!
|
||||
return mvar
|
||||
246
src/Lean/Elab/Tactic/Do/Spec.lean
Normal file
246
src/Lean/Elab/Tactic/Do/Spec.lean
Normal file
|
|
@ -0,0 +1,246 @@
|
|||
/-
|
||||
Copyright (c) 2022 Lars König. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Lars König, Mario Carneiro, Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Lean.Elab.Tactic.Do.ProofMode.Basic
|
||||
import Lean.Elab.Tactic.Do.ProofMode.Intro
|
||||
import Lean.Elab.Tactic.Do.ProofMode.Pure
|
||||
import Lean.Elab.Tactic.Do.ProofMode.Frame
|
||||
import Lean.Elab.Tactic.Do.ProofMode.Assumption
|
||||
import Lean.Elab.Tactic.Do.Attr
|
||||
import Std.Do.Triple
|
||||
|
||||
namespace Lean.Elab.Tactic.Do
|
||||
open Lean Elab Tactic Meta
|
||||
open Std.Do Do.SpecAttr Do.ProofMode
|
||||
|
||||
builtin_initialize registerTraceClass `Elab.Tactic.Do.spec
|
||||
|
||||
def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem := do
|
||||
let_expr WP.wp _m _ps _instWP _α prog := wp | throwError "target not a wp application {wp}"
|
||||
let prog ← instantiateMVarsIfMVarApp prog
|
||||
let prog := prog.headBeta
|
||||
let candidates ← database.specs.getMatch prog
|
||||
let candidates := candidates.filter fun spec => !database.erased.contains spec.proof
|
||||
let candidates := candidates.insertionSort fun s₁ s₂ => s₁.priority < s₂.priority
|
||||
trace[Elab.Tactic.Do.spec] "Candidates for {prog}: {candidates.map (·.proof)}"
|
||||
let specs ← candidates.filterM fun spec => do
|
||||
let (_, _, _, type) ← spec.proof.instantiate
|
||||
trace[Elab.Tactic.Do.spec] "{spec.proof} instantiates to {type}"
|
||||
let_expr Triple m ps instWP α specProg _P _Q := type | throwError "Not a triple: {type}"
|
||||
isDefEq wp (mkApp5 (← mkConstWithFreshMVarLevels ``WP.wp) m ps instWP α specProg)
|
||||
trace[Elab.Tactic.Do.spec] "Specs for {prog}: {specs.map (·.proof)}"
|
||||
if specs.isEmpty then throwError m!"No specs found for {indentExpr prog}\nCandidates: {candidates.map (·.proof)}"
|
||||
return specs[0]!
|
||||
|
||||
def elabTermIntoSpecTheorem (stx : TSyntax `term) (expectedTy : Expr) : TacticM (SpecTheorem × List MVarId) := do
|
||||
if stx.raw.isIdent then
|
||||
match ← Term.resolveId? stx.raw (withInfo := true) with
|
||||
| some (.const declName _) => return (← mkSpecTheoremFromConst declName, [])
|
||||
| some (.fvar fvarId) => return (← mkSpecTheoremFromLocal fvarId, [])
|
||||
| _ => pure ()
|
||||
try
|
||||
let (prf, mvars) ← --Term.withSynthesize <|
|
||||
elabTermWithHoles stx expectedTy `mspec (allowNaturalHoles := true)
|
||||
let specThm ← mkSpecTheoremFromStx stx.raw prf
|
||||
return (specThm, mvars)
|
||||
catch e : Exception =>
|
||||
trace[Elab.Tactic.Do.spec] "Internal error. This happens for example when the head symbol of the spec is wrong. Message:\n {e.toMessageData}"
|
||||
throw e
|
||||
|
||||
def elabSpec (stx? : Option (TSyntax `term)) (wp : Expr) : TacticM (SpecTheorem × List MVarId) := do
|
||||
let_expr f@WP.wp m ps instWP α prog := wp | throwError "target not a wp application {wp}"
|
||||
let P ← mkFreshExprMVar (mkApp (mkConst ``Assertion) ps) (userName := `P)
|
||||
let Q ← mkFreshExprMVar (mkApp2 (mkConst ``PostCond) α ps) (userName := `Q)
|
||||
let expectedTy := mkApp7 (mkConst ``Triple f.constLevels!) m ps instWP α prog P Q
|
||||
trace[Elab.Tactic.Do.spec] "spec syntax: {stx?}"
|
||||
trace[Elab.Tactic.Do.spec] "expected type: {← instantiateMVars expectedTy}"
|
||||
match stx? with
|
||||
| none => pure (← findSpec (← getSpecTheorems) wp, [])
|
||||
| some stx => elabTermIntoSpecTheorem stx expectedTy
|
||||
|
||||
variable {n} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n]
|
||||
|
||||
private def mkProj' (n : Name) (i : Nat) (Q : Expr) : MetaM Expr := do
|
||||
return (← projectCore? Q i).getD (mkProj n i Q)
|
||||
|
||||
mutual
|
||||
partial def dischargePostEntails (α : Expr) (ps : Expr) (Q : Expr) (Q' : Expr) (goalTag : Name) (discharge : Expr → Name → n Expr) : n Expr := do
|
||||
-- Often, Q' is fully instantiated while Q contains metavariables. Try refl
|
||||
if (← isDefEq Q Q') then
|
||||
return mkApp3 (mkConst ``PostCond.entails.refl) α ps Q'
|
||||
let Q ← whnfR Q
|
||||
let Q' ← whnfR Q'
|
||||
-- If Q (postcond of the spec) is just an fvar, we do not decompose further
|
||||
if let some _fvarId := Q.fvarId? then
|
||||
return ← discharge (mkApp4 (mkConst ``PostCond.entails) α ps Q Q') (goalTag ++ `post)
|
||||
-- Otherwise decompose the conjunction
|
||||
let prf₁ ← withLocalDeclD Name.anonymous α fun a => do
|
||||
let Q1a := (← mkProj' ``Prod 0 Q).betaRev #[a]
|
||||
let Q'1a := (← mkProj' ``Prod 0 Q').betaRev #[a]
|
||||
let σs := mkApp (mkConst ``PostShape.args) ps
|
||||
let uniq ← liftMetaM mkFreshId
|
||||
let goal := MGoal.mk σs (Hyp.mk `h uniq Q1a).toExpr Q'1a
|
||||
mkLambdaFVars #[a] (← discharge goal.toExpr (goalTag ++ `success))
|
||||
let prf₂ ← dischargeFailEntails ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except) discharge
|
||||
mkAppM ``And.intro #[prf₁, prf₂] -- This is just a bit too painful to construct by hand
|
||||
|
||||
partial def dischargeFailEntails (ps : Expr) (Q : Expr) (Q' : Expr) (goalTag : Name) (discharge : Expr → Name → n Expr) : n Expr := do
|
||||
if ps.isAppOf ``PostShape.pure then
|
||||
return mkConst ``True.intro
|
||||
if ← isDefEq Q Q' then
|
||||
return mkApp2 (mkConst ``FailConds.entails.refl) ps Q
|
||||
if ← isDefEq Q (mkApp (mkConst ``FailConds.false) ps) then
|
||||
return mkApp2 (mkConst ``FailConds.entails_false) ps Q'
|
||||
if ← isDefEq Q' (mkApp (mkConst ``FailConds.true) ps) then
|
||||
return mkApp2 (mkConst ``FailConds.entails_true) ps Q
|
||||
-- the remaining cases are recursive.
|
||||
if let some (_σ, ps) := ps.app2? ``PostShape.arg then
|
||||
return ← dischargeFailEntails ps Q Q' goalTag discharge
|
||||
if let some (ε, ps) := ps.app2? ``PostShape.except then
|
||||
let Q ← whnfR Q
|
||||
let Q' ← whnfR Q'
|
||||
let prf₁ ← withLocalDeclD Name.anonymous ε fun e => do
|
||||
let Q1e := (← mkProj' ``Prod 0 Q).betaRev #[e]
|
||||
let Q'1e := (← mkProj' ``Prod 0 Q').betaRev #[e]
|
||||
let σs := mkApp (mkConst ``PostShape.args) ps
|
||||
let uniq ← liftMetaM mkFreshId
|
||||
let goal := MGoal.mk σs (Hyp.mk `h uniq Q1e).toExpr Q'1e
|
||||
mkLambdaFVars #[e] (← discharge goal.toExpr (goalTag ++ `handle))
|
||||
let prf₂ ← dischargeFailEntails ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except) discharge
|
||||
return ← mkAppM ``And.intro #[prf₁, prf₂] -- This is just a bit too painful to construct by hand
|
||||
-- This case happens when decomposing with unknown `ps : PostShape`
|
||||
discharge (mkApp3 (mkConst ``FailConds.entails) ps Q Q') goalTag
|
||||
end
|
||||
|
||||
def dischargeMGoal (goal : MGoal) (goalTag : Name) (discharge : Expr → Name → n Expr) : n Expr := do
|
||||
-- controlAt MetaM (fun map => do trace[Elab.Tactic.Do.spec] "dischargeMGoal: {(← reduceProj? goal.target).getD goal.target}"; map (pure ()))
|
||||
-- simply try one of the assumptions for now. Later on we might want to decompose conjunctions etc; full xsimpl
|
||||
let some prf ← liftMetaM goal.assumption | discharge goal.toExpr goalTag
|
||||
return prf
|
||||
|
||||
def mkPreTag (goalTag : Name) : Name := Id.run do
|
||||
let dflt := goalTag ++ `pre1
|
||||
let .str p s := goalTag | return dflt
|
||||
unless "pre".isPrefixOf s do return dflt
|
||||
let some n := (s.toSubstring.drop 3).toString.toNat? | return dflt
|
||||
return .str p ("pre" ++ toString (n + 1))
|
||||
|
||||
/--
|
||||
Returns the proof and the list of new unassigned MVars.
|
||||
-/
|
||||
def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n (SpecTheorem × List MVarId)) (discharge : Expr → Name → n Expr) (goalTag : Name) (mkPreTag := mkPreTag) : n (Expr × List MVarId) := do
|
||||
-- First instantiate `fun s => ...` in the target via repeated `mintro ∀s`.
|
||||
let (holes, prf) ← mIntroForallN goal goal.target.consumeMData.getNumHeadLambdas fun goal => do
|
||||
-- Elaborate the spec for the wp⟦e⟧ app in the target
|
||||
let T := goal.target.consumeMData
|
||||
unless T.getAppFn.constName! == ``PredTrans.apply do
|
||||
liftMetaM (throwError "target not a PredTrans.apply application {indentExpr T}")
|
||||
let wp := T.getArg! 2
|
||||
liftMetaM <| do trace[Elab.Tactic.Do.spec] "before elabSpecAtWP {wp}"
|
||||
let (specThm, elabMVars) ← elabSpecAtWP wp
|
||||
liftMetaM <| do trace[Elab.Tactic.Do.spec] "after elabSpecAtWP {specThm.proof} {wp}"
|
||||
|
||||
-- The precondition of `specThm` might look like `⌜?n = ‹Nat›ₛ ∧ ?m = ‹Bool›ₛ⌝`, which expands to
|
||||
-- `SVal.curry (fun tuple => ?n = SVal.uncurry (getThe Nat tuple) ∧ ?m = SVal.uncurry (getThe Bool tuple))`.
|
||||
-- Note that the assignments for `?n` and `?m` depend on the bound variable `tuple`.
|
||||
-- Here, we further eta expand and simplify according to `etaPotential` so that the solutions for
|
||||
-- `?n` and `?m` do not depend on `tuple`.
|
||||
let residualEta := specThm.etaPotential - (T.getAppNumArgs - 4) -- 4 arguments expected for PredTrans.apply
|
||||
mIntroForallN goal residualEta fun goal => do
|
||||
|
||||
-- Compute a frame of `P` that we duplicate into the pure context using `Spec.frame`
|
||||
-- For now, frame = `P` or nothing at all
|
||||
mTryFrame goal fun goal => do
|
||||
|
||||
-- Fully instantiate the specThm without instantiating its MVars to `wp` yet
|
||||
let (schematicMVars, _, spec, specTy) ← specThm.proof.instantiate
|
||||
|
||||
-- Apply the spec to the excess arguments of the `wp⟦e⟧ Q` application
|
||||
let T := goal.target.consumeMData
|
||||
let args := T.getAppArgs
|
||||
let Q' := args[3]!
|
||||
let excessArgs := (args.extract 4 args.size).reverse
|
||||
|
||||
liftMetaM <| do trace[Elab.Tactic.Do.spec] "before WTF {wp} {spec} {specTy}"
|
||||
-- Actually instantiate the specThm using the expected type computed from `wp`.
|
||||
let_expr f@Triple m ps instWP α prog P Q := specTy | do liftMetaM (throwError "target not a Triple application {specTy}")
|
||||
let wp' := mkApp5 (mkConst ``WP.wp f.constLevels!) m ps instWP α prog
|
||||
unless (← withAssignableSyntheticOpaque <| isDefEq wp wp') do
|
||||
Term.throwTypeMismatchError none wp wp' spec
|
||||
liftMetaM <| do trace[Elab.Tactic.Do.spec] "WTF {wp} {wp'} {spec} {specTy}"
|
||||
|
||||
let P := P.betaRev excessArgs
|
||||
let spec := spec.betaRev excessArgs
|
||||
|
||||
-- often P or Q are schematic (i.e. an MVar app). Try to solve by rfl.
|
||||
let P ← instantiateMVarsIfMVarApp P
|
||||
let Q ← instantiateMVarsIfMVarApp Q
|
||||
let HPRfl ← withDefault <| withAssignableSyntheticOpaque <| isDefEqGuarded P goal.hyps
|
||||
let QQ'Rfl ← withDefault <| withAssignableSyntheticOpaque <| isDefEqGuarded Q Q'
|
||||
|
||||
-- Discharge the validity proof for the spec if not rfl
|
||||
let mut prePrf : Expr → Expr := id
|
||||
if !HPRfl then
|
||||
-- let P := (← reduceProjBeta? P).getD P
|
||||
-- Try to avoid creating a longer name if the postcondition does not need to create a goal
|
||||
let tag := if !QQ'Rfl then mkPreTag goalTag else goalTag
|
||||
let HPPrf ← dischargeMGoal { goal with target := P } tag discharge
|
||||
prePrf := mkApp6 (mkConst ``SPred.entails.trans) goal.σs goal.hyps P goal.target HPPrf
|
||||
|
||||
-- Discharge the entailment on postconditions if not rfl
|
||||
let mut postPrf : Expr → Expr := id
|
||||
if !QQ'Rfl then
|
||||
-- Try to avoid creating a longer name if the precondition does not need to create a goal
|
||||
let tag := if !HPRfl then goalTag ++ `post else goalTag
|
||||
let wpApplyQ := mkApp4 (mkConst ``PredTrans.apply) ps α wp Q -- wp⟦x⟧.apply Q; that is, T without excess args
|
||||
let wpApplyQ' := mkApp4 (mkConst ``PredTrans.apply) ps α wp Q' -- wp⟦x⟧.apply Q'
|
||||
let QQ' ← dischargePostEntails α ps Q Q' tag discharge
|
||||
let QQ'mono := mkApp6 (mkConst ``PredTrans.mono) ps α wp Q Q' QQ'
|
||||
postPrf := fun h =>
|
||||
mkApp6 (mkConst ``SPred.entails.trans) goal.σs P (wpApplyQ.betaRev excessArgs) (wpApplyQ'.betaRev excessArgs)
|
||||
h (QQ'mono.betaRev excessArgs)
|
||||
|
||||
-- finally build the proof; HPPrf.trans (spec.trans QQ'mono)
|
||||
let prf := prePrf (postPrf spec)
|
||||
let holes := elabMVars ++ schematicMVars.toList.map (·.mvarId!)
|
||||
let holes ← liftMetaM <| holes.filterM fun mv => not <$> mv.isAssignedOrDelayedAssigned
|
||||
return (holes, prf)
|
||||
|
||||
-- (This is after closing the `mForallIntro` and `mTryFrame` blocks.)
|
||||
-- Functions like `mkForallFVars` etc. might have instantiated some of the MVar holes and in
|
||||
-- doing so have introduced new MVars in turn.
|
||||
-- Thus we try and instantiate all MVars and collect the MVars of the instantiated expressions.
|
||||
let holes ← liftMetaM <| holes.flatMapM fun mv => do
|
||||
let e ← instantiateMVars (mkMVar mv)
|
||||
let mvs ← getMVars e
|
||||
let mvs ← mvs.filterM fun mv => not <$> mv.isAssignedOrDelayedAssigned
|
||||
return mvs.toList
|
||||
return (prf, holes)
|
||||
|
||||
private def addMVar (mvars : IO.Ref (List MVarId)) (goal : Expr) (name : Name) : MetaM Expr := do
|
||||
let m ← mkFreshExprSyntheticOpaqueMVar goal (tag := name)
|
||||
mvars.modify (m.mvarId! :: ·)
|
||||
return m
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.mspecNoBind]
|
||||
def evalMSpecNoBind : Tactic
|
||||
| `(tactic| mspec_no_bind $[$spec]?) => do
|
||||
let (mvar, goal) ← mStartMVar (← getMainGoal)
|
||||
mvar.withContext do
|
||||
let goals ← IO.mkRef []
|
||||
let (prf, specHoles) ← mSpec goal (elabSpec spec) (fun goal name => liftMetaM (addMVar goals goal name)) (← getMainTag)
|
||||
mvar.assign prf
|
||||
let goals ← goals.get
|
||||
if let [mvar'] := goals then mvar'.setTag (← mvar.getTag)
|
||||
replaceMainGoal (goals ++ specHoles)
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
-- TODO: Define the simp set as a list here and build `simpArgs` syntax from it
|
||||
macro_rules
|
||||
| `(tactic| mspec_no_simp $[$spec]?) =>
|
||||
`(tactic| ((try with_reducible mspec_no_bind $(mkIdent ``Std.Do.Spec.bind)); mspec_no_bind $[$spec]?))
|
||||
| `(tactic| mspec $[$spec]?) =>
|
||||
`(tactic| mspec_no_simp $[$spec]?; open Std.Do in all_goals ((try simp only [SPred.true_intro_simp, SPred.true_intro_simp_nil, SVal.curry_cons, SVal.uncurry_cons, SVal.getThe_here, SVal.getThe_there]); (try mpure_intro; trivial)))
|
||||
62
src/Lean/Elab/Tactic/Do/Syntax.lean
Normal file
62
src/Lean/Elab/Tactic/Do/Syntax.lean
Normal file
|
|
@ -0,0 +1,62 @@
|
|||
/-
|
||||
Copyright (c) 2022 Lars König. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Lars König, Mario Carneiro, Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Init.NotationExtra
|
||||
import Lean.Elab.BuiltinNotation
|
||||
import Std.Do.PostCond
|
||||
import Std.Do.Triple.Basic
|
||||
|
||||
namespace Std.Do
|
||||
|
||||
open Lean Parser Meta Elab Term
|
||||
|
||||
def post_syntax := leading_parser
|
||||
"post⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", " (allowTrailingSep := true))) >> "⟩"
|
||||
scoped syntax:max "post⟨" term,+ "⟩" : term
|
||||
macro_rules | `(post⟨$handlers,*⟩) => `(by exact ⟨$handlers,*, ()⟩)
|
||||
-- NB: Postponement through by exact is the entire point of this macro
|
||||
-- until https://github.com/leanprover/lean4/pull/8074 lands
|
||||
example : PostCond Nat .pure := post⟨fun s => True⟩
|
||||
example : PostCond (Nat × Nat) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) :=
|
||||
post⟨fun (r, xs) s => r ≤ 4 ∧ s = 4 ∧ r + xs > 4, fun e s => e = 42 ∧ s = 4⟩
|
||||
|
||||
open Lean Parser Term in
|
||||
def funArrow : Parser := unicodeSymbol " ↦ " " => "
|
||||
@[inherit_doc PostCond.total]
|
||||
scoped macro "⇓" xs:Lean.Parser.Term.funBinder+ funArrow e:term : term =>
|
||||
`(PostCond.total (by exact (fun $xs* => spred($e)))) -- NB: Postponement through by exact
|
||||
|
||||
@[app_unexpander PostCond.total]
|
||||
private def unexpandPostCondTotal : PrettyPrinter.Unexpander
|
||||
| `($_ fun $xs* => $e) => do `(⇓ $xs* => $(← SPred.Notation.unpack e))
|
||||
| _ => throw ()
|
||||
|
||||
elab_rules : term
|
||||
| `(⦃$P⦄ $x ⦃$Q⦄) => do
|
||||
-- In a simple world, this would just be a macro expanding to
|
||||
-- `Triple $x spred($P) spred($Q)`.
|
||||
-- However, currently we need to help type inference for P and Q.
|
||||
-- Specifically, if `x : StateT σ m α`, `[wp : WP m ps]` and `P : σ → Assertion ps`,
|
||||
-- then `Triple x P _` will not elaborate because `σ → Assertion ps =?= Assertion ?ps` fails.
|
||||
-- We must first instantiate `?ps` to `.arg σ ps` through the `outParam` of `WP`, hence this elaborator.
|
||||
-- This is tracked in #8766, and #8074 might be a fix.
|
||||
let x ← elabTerm x none
|
||||
let ty ← inferType x
|
||||
tryPostponeIfMVar ty
|
||||
let ty ← instantiateMVars ty
|
||||
let .app m α := ty.consumeMData | throwError "Not a type application {ty}"
|
||||
let some u ← Level.dec <$> getLevel ty | throwError "Wrong level 0 {ty}"
|
||||
let ps ← mkFreshExprMVar (mkConst ``PostShape)
|
||||
let inst ← synthInstance (mkApp2 (mkConst ``WP [u]) m ps)
|
||||
let P ← elabTerm (← `(spred($P))) (mkApp (mkConst ``Assertion) ps)
|
||||
let Q ← elabTerm (← `(spred($Q))) (mkApp2 (mkConst ``PostCond) α ps)
|
||||
return mkApp7 (mkConst ``Triple [u]) m ps inst α x P Q
|
||||
|
||||
@[app_unexpander Triple]
|
||||
private def unexpandTriple : PrettyPrinter.Unexpander
|
||||
| `($_ $x $P $Q) => do
|
||||
`(⦃$(← SPred.Notation.unpack P)⦄ $x ⦃$Q⦄)
|
||||
| _ => throw ()
|
||||
392
src/Lean/Elab/Tactic/Do/VCGen.lean
Normal file
392
src/Lean/Elab/Tactic/Do/VCGen.lean
Normal file
|
|
@ -0,0 +1,392 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Std.Do.WP
|
||||
import Std.Do.Triple
|
||||
import Lean.Elab.Tactic.Simp
|
||||
import Lean.Elab.Tactic.Meta
|
||||
import Lean.Elab.Tactic.Do.ProofMode.Basic
|
||||
import Lean.Elab.Tactic.Do.ProofMode.Intro
|
||||
import Lean.Elab.Tactic.Do.ProofMode.Cases
|
||||
import Lean.Elab.Tactic.Do.ProofMode.Specialize
|
||||
import Lean.Elab.Tactic.Do.LetElim
|
||||
import Lean.Elab.Tactic.Do.Spec
|
||||
import Lean.Elab.Tactic.Do.Attr
|
||||
import Lean.Elab.Tactic.Do.Syntax
|
||||
|
||||
namespace Lean.Elab.Tactic.Do
|
||||
|
||||
open Lean Parser Elab Tactic Meta Do ProofMode SpecAttr
|
||||
open Std.Do
|
||||
|
||||
builtin_initialize registerTraceClass `Elab.Tactic.Do.vcgen
|
||||
|
||||
register_builtin_option mvcgen.warning : Bool := {
|
||||
defValue := true
|
||||
group := "debug"
|
||||
descr := "disable `mvcgen` usage warning"
|
||||
}
|
||||
|
||||
inductive Fuel where
|
||||
| limited (n : Nat)
|
||||
| unlimited
|
||||
deriving DecidableEq
|
||||
|
||||
structure Config where
|
||||
/--
|
||||
If true, do not substitute away let-declarations that are used at most once before starting
|
||||
VC generation.
|
||||
-/
|
||||
noLetElim : Bool := false
|
||||
|
||||
declare_config_elab elabConfig Config
|
||||
|
||||
structure Context where
|
||||
config : Config
|
||||
specThms : SpecTheorems
|
||||
simpCtx : Simp.Context
|
||||
simprocs : Simp.SimprocsArray
|
||||
|
||||
structure State where
|
||||
fuel : Fuel := .unlimited
|
||||
simpState : Simp.State := {}
|
||||
/--
|
||||
The verification conditions that have been generated so far.
|
||||
Includes `Type`-valued goals arising from instantiation of specifications.
|
||||
-/
|
||||
vcs : Array MVarId := #[]
|
||||
|
||||
abbrev VCGenM := ReaderT Context (StateRefT State MetaM)
|
||||
|
||||
def burnOne : VCGenM PUnit := do
|
||||
let s ← get
|
||||
match s.fuel with
|
||||
| Fuel.limited 0 => return ()
|
||||
| Fuel.limited (n + 1) => set { s with fuel := .limited n }
|
||||
| Fuel.unlimited => return ()
|
||||
|
||||
def ifOutOfFuel (x : VCGenM α) (k : VCGenM α) : VCGenM α := do
|
||||
let s ← get
|
||||
match s.fuel with
|
||||
| Fuel.limited 0 => x
|
||||
| _ => k
|
||||
|
||||
def emitVC (subGoal : Expr) (name : Name) : VCGenM Expr := do
|
||||
let m ← liftM <| mkFreshExprSyntheticOpaqueMVar subGoal (tag := name)
|
||||
modify fun s => { s with vcs := s.vcs.push m.mvarId! }
|
||||
return m
|
||||
|
||||
def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
|
||||
modify fun s => { s with vcs := s.vcs.push goal }
|
||||
|
||||
def liftSimpM (x : SimpM α) : VCGenM α := do
|
||||
let ctx ← read
|
||||
let s ← get
|
||||
let mref := (Simp.mkDefaultMethodsCore ctx.simprocs).toMethodsRef
|
||||
let (a, simpState) ← x mref ctx.simpCtx |>.run s.simpState
|
||||
set { s with simpState }
|
||||
return a
|
||||
|
||||
instance : MonadLift SimpM VCGenM where
|
||||
monadLift x := liftSimpM x
|
||||
|
||||
syntax (name := mvcgen_step) "mvcgen_step" optConfig
|
||||
(num)? (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
|
||||
|
||||
syntax (name := mvcgen_no_trivial) "mvcgen_no_trivial" optConfig
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
|
||||
|
||||
syntax (name := mvcgen) "mvcgen" optConfig
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
|
||||
|
||||
private def mkSpecContext (optConfig : Syntax) (lemmas : Syntax) (ignoreStarArg := false) : TacticM Context := do
|
||||
let config ← elabConfig optConfig
|
||||
let mut specThms ← getSpecTheorems
|
||||
let mut simpStuff := #[]
|
||||
let mut starArg := false
|
||||
for arg in lemmas[1].getSepArgs do
|
||||
if arg.getKind == ``simpErase then
|
||||
try
|
||||
-- Try and build SpecTheorems for the lemma to erase to see if it's
|
||||
-- meant to be interpreted by SpecTheorems. Otherwise fall back to SimpTheorems.
|
||||
let specThm ←
|
||||
if let some fvar ← Term.isLocalIdent? arg[1] then
|
||||
mkSpecTheoremFromLocal fvar.fvarId!
|
||||
else
|
||||
let id := arg[1]
|
||||
if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
|
||||
mkSpecTheoremFromConst declName
|
||||
else
|
||||
withRef id <| throwUnknownConstant id.getId.eraseMacroScopes
|
||||
specThms := specThms.eraseCore specThm.proof
|
||||
catch _ =>
|
||||
simpStuff := simpStuff.push ⟨arg⟩ -- simp tracks its own erase stuff
|
||||
else if arg.getKind == ``simpLemma then
|
||||
unless arg[0].isNone && arg[1].isNone do
|
||||
-- When there is ←, →, ↑ or ↓ then this is for simp
|
||||
simpStuff := simpStuff.push ⟨arg⟩
|
||||
continue
|
||||
let term := arg[2]
|
||||
match ← Term.resolveId? term (withInfo := true) <|> Term.elabCDotFunctionAlias? ⟨term⟩ with
|
||||
| some (.const declName _) =>
|
||||
let info ← getConstInfo declName
|
||||
try
|
||||
let thm ← mkSpecTheoremFromConst declName
|
||||
specThms := addSpecTheoremEntry specThms thm
|
||||
catch _ =>
|
||||
simpStuff := simpStuff.push ⟨arg⟩
|
||||
| some (.fvar fvar) =>
|
||||
let decl ← getFVarLocalDecl (.fvar fvar)
|
||||
try
|
||||
let thm ← mkSpecTheoremFromLocal fvar
|
||||
specThms := addSpecTheoremEntry specThms thm
|
||||
catch _ =>
|
||||
simpStuff := simpStuff.push ⟨arg⟩
|
||||
| _ => withRef term <| throwError "Could not resolve {repr term}"
|
||||
else if arg.getKind == ``simpStar then
|
||||
starArg := true
|
||||
simpStuff := simpStuff.push ⟨arg⟩
|
||||
else
|
||||
throwUnsupportedSyntax
|
||||
-- Build a mock simp call to build a simp context that corresponds to `simp [simpStuff]`
|
||||
let stx ← `(tactic| simp +unfoldPartialApp [$(Syntax.TSepArray.ofElems simpStuff),*])
|
||||
-- logInfo s!"{stx}"
|
||||
let res ← mkSimpContext stx.raw
|
||||
(eraseLocal := false)
|
||||
(simpTheorems := getSpecSimpTheorems)
|
||||
(ignoreStarArg := ignoreStarArg)
|
||||
-- logInfo m!"{res.ctx.simpTheorems.map (·.toUnfold.toList)}"
|
||||
if starArg && !ignoreStarArg then
|
||||
let fvars ← getPropHyps
|
||||
for fvar in fvars do
|
||||
unless specThms.isErased (.local fvar) do
|
||||
try
|
||||
let thm ← mkSpecTheoremFromLocal fvar
|
||||
specThms := addSpecTheoremEntry specThms thm
|
||||
catch _ => continue
|
||||
return { config, specThms, simpCtx := res.ctx, simprocs := res.simprocs }
|
||||
|
||||
def isDuplicable (e : Expr) : Bool := match e with
|
||||
| .bvar .. => true
|
||||
| .mvar .. => true
|
||||
| .fvar .. => true
|
||||
| .const .. => true
|
||||
| .lit .. => true
|
||||
| .sort .. => true
|
||||
| .mdata _ e => isDuplicable e
|
||||
| .proj _ _ e => isDuplicable e
|
||||
| .lam .. => false
|
||||
| .forallE .. => false
|
||||
| .letE .. => false
|
||||
| .app .. => e.isAppOf ``OfNat.ofNat
|
||||
|
||||
def withSharing (name : Name) (type : Expr) (val : Expr) (k : Expr → (Expr → VCGenM Expr) → VCGenM α) (kind : LocalDeclKind := .default) : VCGenM α :=
|
||||
if isDuplicable val then
|
||||
k val pure
|
||||
else
|
||||
withLetDecl name type val (kind := kind) fun fv => do
|
||||
k fv (liftM <| mkForallFVars #[fv] ·)
|
||||
|
||||
/-- Reduces (1) Prod projection functions and (2) Projs in application heads,
|
||||
and (3) beta reduces. -/
|
||||
private partial def reduceProjBeta? (e : Expr) : MetaM (Option Expr) :=
|
||||
go none e.getAppFn e.getAppRevArgs
|
||||
where
|
||||
go lastReduction f rargs := do
|
||||
match f with
|
||||
| .mdata _ f => go lastReduction f rargs
|
||||
| .app f a => go lastReduction f (rargs.push a)
|
||||
| .lam .. =>
|
||||
if rargs.size = 0 then return lastReduction
|
||||
let e' := f.betaRev rargs
|
||||
go (some e') e'.getAppFn e'.getAppRevArgs
|
||||
| .const name .. =>
|
||||
let env ← getEnv
|
||||
match env.getProjectionStructureName? name with
|
||||
| some ``Prod => -- only reduce fst and snd for now
|
||||
match ← Meta.unfoldDefinition? (mkAppRev f rargs) with
|
||||
| some e' => go lastReduction e'.getAppFn e'.getAppRevArgs
|
||||
| none => pure lastReduction
|
||||
| _ => pure lastReduction
|
||||
| .proj .. => match ← reduceProj? f with
|
||||
| some f' =>
|
||||
let e' := mkAppRev f' rargs
|
||||
go (some e') e'.getAppFn e'.getAppRevArgs
|
||||
| none => pure lastReduction
|
||||
| _ => pure lastReduction
|
||||
|
||||
partial def step (ctx : Context) (fuel : Fuel) (goal : MGoal) (name : Name) : MetaM (Expr × Array MVarId) := do
|
||||
withReducible do
|
||||
let (res, state) ← StateRefT'.run (ReaderT.run (onGoal goal name) ctx) { fuel }
|
||||
return (res, state.vcs)
|
||||
where
|
||||
onFail (goal : MGoal) (name : Name) : VCGenM Expr := do
|
||||
-- logInfo m!"fail {goal.toExpr}"
|
||||
emitVC goal.toExpr name
|
||||
|
||||
tryGoal (goal : Expr) (name : Name) : VCGenM Expr := do
|
||||
forallTelescope goal fun xs body => do
|
||||
let res ← try mStart body catch _ =>
|
||||
return ← mkLambdaFVars xs (← emitVC goal name)
|
||||
let mut prf ← onGoal res.goal name
|
||||
-- logInfo m!"tryGoal: {res.goal.toExpr}"
|
||||
-- res.goal.checkProof prf
|
||||
if let some proof := res.proof? then
|
||||
prf := mkApp proof prf
|
||||
mkLambdaFVars xs prf
|
||||
|
||||
assignMVars (mvars : List MVarId) : VCGenM PUnit := do
|
||||
for mvar in mvars do
|
||||
-- trace[Elab.Tactics.Do.vcgen] "assignMVars {← mvar.getTag}, assigned: {← mvar.isAssigned}"
|
||||
if ← mvar.isAssigned then continue
|
||||
-- I used to filter for `isProp` here and add any non-Props directly as subgoals,
|
||||
-- but then we would get spurious instantiations of non-synthetic goals such as loop
|
||||
-- invariants.
|
||||
mvar.assign (← mvar.withContext <| tryGoal (← mvar.getType) (← mvar.getTag))
|
||||
|
||||
onGoal goal name : VCGenM Expr := do
|
||||
let T := goal.target
|
||||
let T := (← reduceProjBeta? T).getD T -- very slight simplification
|
||||
-- logInfo m!"target: {T}"
|
||||
let goal := { goal with target := T }
|
||||
|
||||
let f := T.getAppFn
|
||||
if f.isLambda then
|
||||
return ← onLambda goal name
|
||||
if f.isConstOf ``SPred.imp then
|
||||
return ← onImp goal name
|
||||
else if f.isConstOf ``PredTrans.apply then
|
||||
return ← onWPApp goal name
|
||||
onFail { goal with target := T } name
|
||||
|
||||
onImp goal name : VCGenM Expr := ifOutOfFuel (onFail goal name) do
|
||||
burnOne
|
||||
(·.2) <$> mIntro goal (← `(binderIdent| _)) (fun g =>
|
||||
do return ((), ← onGoal g name))
|
||||
|
||||
onLambda goal name : VCGenM Expr := ifOutOfFuel (onFail goal name) do
|
||||
burnOne
|
||||
(·.2) <$> mIntroForall goal (← `(binderIdent| _)) (fun g =>
|
||||
do return ((), ← onGoal g name))
|
||||
|
||||
onWPApp goal name : VCGenM Expr := ifOutOfFuel (onFail goal name) do
|
||||
let args := goal.target.getAppArgs
|
||||
let trans := args[2]!
|
||||
-- logInfo m!"trans: {trans}"
|
||||
let Q := args[3]!
|
||||
let wp ← instantiateMVarsIfMVarApp trans
|
||||
match_expr wp with
|
||||
| c@WP.wp m ps instWP α e =>
|
||||
let e ← instantiateMVarsIfMVarApp e
|
||||
let e := e.headBeta
|
||||
trace[Elab.Tactics.Do.vcgen] "Target: {e}"
|
||||
let goalWithNewProg e' :=
|
||||
let wp' := mkApp5 c m ps instWP α e'
|
||||
let args' := args.set! 2 wp'
|
||||
{ goal with target := mkAppN (mkConst ``PredTrans.apply) args' }
|
||||
|
||||
-- lambda-expressions
|
||||
if e.getAppFn'.isLambda && false then
|
||||
-- We are likely in the implementation of a StateT function; do `mintro ∀s`
|
||||
return ← onLambda goal name
|
||||
-- let-expressions
|
||||
if let .letE x ty val body _nonDep := e.getAppFn' then
|
||||
burnOne
|
||||
return ← withSharing x ty val fun fv leave => do
|
||||
let e' := ((body.instantiate1 fv).betaRev e.getAppRevArgs)
|
||||
leave (← onWPApp (goalWithNewProg e') name)
|
||||
-- match-expressions
|
||||
if let .some info := isMatcherAppCore? (← getEnv) e then
|
||||
-- Bring into simp NF
|
||||
let res? ← Simp.simpMatchDiscrs? info e
|
||||
let e ← -- returns/continues only if old e is defeq to new e
|
||||
if let .some res := res? then
|
||||
burnOne
|
||||
if let .some heq := res.proof? then
|
||||
let prf ← onWPApp (goalWithNewProg res.expr) name
|
||||
let prf := mkApp10 (mkConst ``Triple.rewrite_program c.constLevels!) m ps α goal.hyps Q instWP e res.expr heq prf
|
||||
return prf
|
||||
else
|
||||
pure res.expr
|
||||
else
|
||||
pure e
|
||||
-- Try reduce the matcher
|
||||
let e ← match (← reduceMatcher? e) with
|
||||
| .reduced e' =>
|
||||
burnOne
|
||||
return ← onWPApp (goalWithNewProg e') name
|
||||
| .stuck _ => pure e
|
||||
| _ => pure e
|
||||
-- Last resort: Split match
|
||||
-- logInfo m!"split match {e}"
|
||||
burnOne
|
||||
let mvar ← mkFreshExprSyntheticOpaqueMVar goal.toExpr (tag := name)
|
||||
let mvars ← Split.splitMatch mvar.mvarId! e
|
||||
assignMVars mvars
|
||||
return mvar
|
||||
-- Unfold local bindings (TODO don't do this unconditionally)
|
||||
let f := e.getAppFn'
|
||||
if let some (some val) ← f.fvarId?.mapM (·.getValue?) then
|
||||
burnOne
|
||||
let e' := val.betaRev e.getAppRevArgs
|
||||
-- logInfo m!"unfold local var {f}, new WP: {wpe}"
|
||||
return ← onWPApp (goalWithNewProg e') name
|
||||
-- Unfold definitions according to reducibility and spec attributes,
|
||||
-- apply specifications
|
||||
if f.isConst then
|
||||
burnOne
|
||||
try
|
||||
let specThm ← findSpec ctx.specThms wp
|
||||
trace[Elab.Tactics.Do.vcgen] "Candidate spec for {f.constName!}: {specThm.proof}"
|
||||
let (prf, specHoles) ← mSpec goal (fun _wp => return (specThm, [])) tryGoal name
|
||||
assignMVars specHoles
|
||||
return prf
|
||||
catch ex =>
|
||||
trace[Elab.Tactics.Do.vcgen] "Failed to find spec. Trying simp. Reason: {ex.toMessageData}"
|
||||
let res ← Simp.simp e
|
||||
unless res.expr != e do return ← onFail goal name
|
||||
burnOne
|
||||
if let .some heq := res.proof? then
|
||||
trace[Elab.Tactics.Do.vcgen] "Simplified"
|
||||
let prf ← onWPApp (goalWithNewProg res.expr) name
|
||||
let prf := mkApp10 (mkConst ``Triple.rewrite_program c.constLevels!) m ps α goal.hyps Q instWP e res.expr heq prf
|
||||
return prf
|
||||
else
|
||||
return ← onWPApp (goalWithNewProg res.expr) name
|
||||
return ← onFail goal name
|
||||
| _ => return ← onFail goal name
|
||||
|
||||
def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : TacticM (Array MVarId) := do
|
||||
let goal ← if ctx.config.noLetElim then pure goal else elimLets goal
|
||||
let (mvar, goal) ← mStartMVar goal
|
||||
mvar.withContext do
|
||||
let (prf, vcs) ← step ctx (fuel := fuel) goal (← mvar.getTag)
|
||||
mvar.assign prf
|
||||
replaceMainGoal vcs.toList
|
||||
return vcs
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.mvcgenStep]
|
||||
def evalMVCGenStep : Tactic := fun stx => withMainContext do
|
||||
let ctx ← mkSpecContext stx[1] stx[3]
|
||||
let n := if stx[2].isNone then 1 else stx[2][0].toNat
|
||||
discard <| genVCs (← getMainGoal) ctx (fuel := .limited n)
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.mvcgenNoTrivial]
|
||||
def evalMVCGenNoTrivial : Tactic := fun stx => withMainContext do
|
||||
let ctx ← mkSpecContext stx[0] stx[1]
|
||||
discard <| genVCs (← getMainGoal) ctx (fuel := .unlimited)
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.mvcgen]
|
||||
def evalMVCGen : Tactic := fun stx => withMainContext do
|
||||
if mvcgen.warning.get (← getOptions) then
|
||||
logWarningAt stx "The `mvcgen` tactic is experimental and still under development. Avoid using it in production projects."
|
||||
-- I would like to define this simply as a macro
|
||||
-- `(tactic| mvcgen_no_trivial $c $lemmas <;> try (guard_target =~ (⌜True⌝ ⊢ₛ _); mpure_intro; trivial))
|
||||
-- but optConfig is not a leading_parser, and neither is the syntax for `lemmas`
|
||||
let ctx ← mkSpecContext stx[1] stx[2]
|
||||
let vcs ← genVCs (← getMainGoal) ctx (fuel := .unlimited)
|
||||
let tac ← `(tactic| try (mpure_intro; trivial))
|
||||
for vc in vcs do discard <| runTactic vc tac
|
||||
|
|
@ -5,3 +5,7 @@ Authors: Sebastian Graf
|
|||
-/
|
||||
prelude
|
||||
import Std.Do.SPred
|
||||
import Std.Do.WP
|
||||
import Std.Do.Triple
|
||||
import Std.Do.PredTrans
|
||||
import Std.Do.PostCond
|
||||
|
|
|
|||
226
src/Std/Do/PostCond.lean
Normal file
226
src/Std/Do/PostCond.lean
Normal file
|
|
@ -0,0 +1,226 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Std.Do.SPred
|
||||
|
||||
/-!
|
||||
# Pre and postconditions
|
||||
|
||||
This module defines `Assertion` and `PostCond`, the types which constitute
|
||||
the pre and postconditions of a Hoare triple in the program logic.
|
||||
|
||||
## Predicate shapes
|
||||
|
||||
Since `WP` supports arbitrary monads, `PostCond` must be general enough to
|
||||
cope with state and exceptions.
|
||||
For this reason, `PostCond` is indexed by a `PostShape` which is an abstraction
|
||||
of the stack of effects supported by the monad, corresponding directly to
|
||||
`StateT` and `ExceptT` layers in a transformer stack.
|
||||
For every `StateT σ` effect, we get one `PostShape.arg σ` layer, whereas for every
|
||||
`ExceptT ε` effect, we get one `PostShape.except ε` layer.
|
||||
Currently, the only supported base layer is `PostShape.pure`.
|
||||
|
||||
## Pre and postconditions
|
||||
|
||||
The type of preconditions `Assertion ps` is distinct from the type of postconditions `PostCond α ps`.
|
||||
|
||||
This is because postconditions not only specify what happens upon successful termination of the
|
||||
program, but also need to specify a property that holds upon failure.
|
||||
We get one "barrel" for the success case, plus one barrel per `PostShape.except` layer.
|
||||
|
||||
It does not make much sense to talk about failure barrels in the context of preconditions.
|
||||
Hence, `Assertion ps` is defined such that all `PostShape.except` layers are discarded from `ps`,
|
||||
via `PostShape.args`.
|
||||
-/
|
||||
|
||||
namespace Std.Do
|
||||
|
||||
inductive PostShape : Type 1 where
|
||||
| pure : PostShape
|
||||
| arg : (σ : Type) → PostShape → PostShape
|
||||
| except : (ε : Type) → PostShape → PostShape
|
||||
|
||||
abbrev PostShape.args : PostShape → List Type
|
||||
| .pure => []
|
||||
| .arg σ s => σ :: PostShape.args s
|
||||
| .except _ s => PostShape.args s
|
||||
|
||||
/--
|
||||
An assertion on the `.arg`s in the given predicate shape.
|
||||
```
|
||||
example : Assertion (.arg ρ .pure) = (ρ → Prop) := rfl
|
||||
example : Assertion (.except ε .pure) = Prop := rfl
|
||||
example : Assertion (.arg σ (.except ε .pure)) = (σ → Prop) := rfl
|
||||
example : Assertion (.except ε (.arg σ .pure)) = (σ → Prop) := rfl
|
||||
```
|
||||
This is an abbreviation for `SPred` under the hood, so all theorems about `SPred` apply.
|
||||
-/
|
||||
abbrev Assertion (ps : PostShape) : Type :=
|
||||
SPred (PostShape.args ps)
|
||||
|
||||
/--
|
||||
Encodes one continuation barrel for each `PostShape.except` in the given predicate shape.
|
||||
```
|
||||
example : FailConds (.pure) = Unit := rfl
|
||||
example : FailConds (.except ε .pure) = ((ε → Prop) × Unit) := rfl
|
||||
example : FailConds (.arg σ (.except ε .pure)) = ((ε → Prop) × Unit) := rfl
|
||||
example : FailConds (.except ε (.arg σ .pure)) = ((ε → σ → Prop) × Unit) := rfl
|
||||
```
|
||||
-/
|
||||
def FailConds : PostShape → Type
|
||||
| .pure => Unit
|
||||
| .arg _ ps => FailConds ps
|
||||
| .except ε ps => (ε → Assertion ps) × FailConds ps
|
||||
|
||||
@[simp]
|
||||
def FailConds.const {ps : PostShape} (p : Prop) : FailConds ps := match ps with
|
||||
| .pure => ()
|
||||
| .arg _ ps => @FailConds.const ps p
|
||||
| .except _ ps => (fun _ε => spred(⌜p⌝), @FailConds.const ps p)
|
||||
|
||||
@[simp]
|
||||
def FailConds.true : FailConds ps := FailConds.const True
|
||||
|
||||
@[simp]
|
||||
def FailConds.false : FailConds ps := FailConds.const False
|
||||
|
||||
instance : Inhabited (FailConds ps) where
|
||||
default := FailConds.true
|
||||
|
||||
def FailConds.entails {ps : PostShape} (x y : FailConds ps) : Prop :=
|
||||
match ps with
|
||||
| .pure => True
|
||||
| .arg _ ps => @entails ps x y
|
||||
| .except _ ps => (∀ e, x.1 e ⊢ₛ y.1 e) ∧ @entails ps x.2 y.2
|
||||
|
||||
infixr:25 " ⊢ₑ " => FailConds.entails
|
||||
|
||||
@[simp, refl]
|
||||
theorem FailConds.entails.refl {ps : PostShape} (x : FailConds ps) : x ⊢ₑ x := by
|
||||
induction ps <;> simp [entails, *]
|
||||
|
||||
theorem FailConds.entails.rfl {ps : PostShape} {x : FailConds ps} : x ⊢ₑ x := refl x
|
||||
|
||||
theorem FailConds.entails.trans {ps : PostShape} {x y z : FailConds ps} : (x ⊢ₑ y) → (y ⊢ₑ z) → x ⊢ₑ z := by
|
||||
induction ps
|
||||
case pure => intro _ _; trivial
|
||||
case arg σ s ih => exact ih
|
||||
case except ε s ih => intro h₁ h₂; exact ⟨fun e => (h₁.1 e).trans (h₂.1 e), ih h₁.2 h₂.2⟩
|
||||
|
||||
@[simp]
|
||||
theorem FailConds.entails_false {x : FailConds ps} : FailConds.false ⊢ₑ x := by
|
||||
induction ps <;> simp_all [false, const, entails, SPred.false_elim]
|
||||
|
||||
@[simp]
|
||||
theorem FailConds.entails_true {x : FailConds ps} : x ⊢ₑ FailConds.true := by
|
||||
induction ps <;> simp_all [true, const, entails]
|
||||
|
||||
@[simp]
|
||||
def FailConds.and {ps : PostShape} (x : FailConds ps) (y : FailConds ps) : FailConds ps :=
|
||||
match ps with
|
||||
| .pure => ()
|
||||
| .arg _ ps => @FailConds.and ps x y
|
||||
| .except _ _ => (fun e => SPred.and (x.1 e) (y.1 e), FailConds.and x.2 y.2)
|
||||
|
||||
infixr:35 " ∧ₑ " => FailConds.and
|
||||
|
||||
theorem FailConds.and_true {x : FailConds ps} : x ∧ₑ FailConds.true ⊢ₑ x := by
|
||||
induction ps
|
||||
case pure => trivial
|
||||
case arg ih => exact ih
|
||||
case except ε ps ih =>
|
||||
simp_all only [true, and, const]
|
||||
constructor <;> simp only [SPred.and_true.mp, implies_true, ih]
|
||||
|
||||
theorem FailConds.true_and {x : FailConds ps} : FailConds.true ∧ₑ x ⊢ₑ x := by
|
||||
induction ps
|
||||
case pure => trivial
|
||||
case arg ih => exact ih
|
||||
case except ε ps ih =>
|
||||
simp_all only [true, and, const]
|
||||
constructor <;> simp only [SPred.true_and.mp, implies_true, ih]
|
||||
|
||||
theorem FailConds.and_false {x : FailConds ps} : x ∧ₑ FailConds.false ⊢ₑ FailConds.false := by
|
||||
induction ps
|
||||
case pure => trivial
|
||||
case arg ih => exact ih
|
||||
case except ε ps ih =>
|
||||
simp_all only [false, and, const]
|
||||
constructor <;> simp only [SPred.and_false.mp, implies_true, ih]
|
||||
|
||||
theorem FailConds.false_and {x : FailConds ps} : FailConds.false ∧ₑ x ⊢ₑ FailConds.false := by
|
||||
induction ps
|
||||
case pure => trivial
|
||||
case arg ih => exact ih
|
||||
case except ε ps ih =>
|
||||
simp_all only [and, false, const]
|
||||
constructor <;> simp only [SPred.false_and.mp, implies_true, ih]
|
||||
|
||||
theorem FailConds.and_eq_left {ps : PostShape} {p q : FailConds ps} (h : p ⊢ₑ q) :
|
||||
p = (p ∧ₑ q) := by
|
||||
induction ps
|
||||
case pure => trivial
|
||||
case arg ih => exact ih h
|
||||
case except ε ps ih =>
|
||||
simp_all only [and]
|
||||
apply Prod.ext
|
||||
· ext a; exact (SPred.and_eq_left.mp (h.1 a)).to_eq
|
||||
· exact ih h.2
|
||||
|
||||
/--
|
||||
A multi-barreled postcondition for the given predicate shape.
|
||||
```
|
||||
example : PostCond α (.arg ρ .pure) = ((α → ρ → Prop) × Unit) := rfl
|
||||
example : PostCond α (.except ε .pure) = ((α → Prop) × (ε → Prop) × Unit) := rfl
|
||||
example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → Prop) × (ε → Prop) × Unit) := rfl
|
||||
example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → Prop) × (ε → σ → Prop) × Unit) := rfl
|
||||
```
|
||||
-/
|
||||
abbrev PostCond (α : Type) (s : PostShape) : Type :=
|
||||
(α → Assertion s) × FailConds s
|
||||
|
||||
/-- A postcondition expressing total correctness. -/
|
||||
abbrev PostCond.total (p : α → Assertion ps) : PostCond α ps :=
|
||||
(p, FailConds.false)
|
||||
|
||||
/-- A postcondition expressing partial correctness. -/
|
||||
abbrev PostCond.partial (p : α → Assertion ps) : PostCond α ps :=
|
||||
(p, FailConds.true)
|
||||
|
||||
instance : Inhabited (PostCond α ps) where
|
||||
default := PostCond.total fun _ => default
|
||||
|
||||
@[simp]
|
||||
def PostCond.entails (p q : PostCond α ps) : Prop :=
|
||||
(∀ a, SPred.entails (p.1 a) (q.1 a)) ∧ FailConds.entails p.2 q.2
|
||||
|
||||
infixr:25 " ⊢ₚ " => PostCond.entails
|
||||
|
||||
@[refl,simp]
|
||||
theorem PostCond.entails.refl (Q : PostCond α ps) : Q ⊢ₚ Q := ⟨fun a => SPred.entails.refl (Q.1 a), FailConds.entails.refl Q.2⟩
|
||||
theorem PostCond.entails.rfl {Q : PostCond α ps} : Q ⊢ₚ Q := refl Q
|
||||
|
||||
theorem PostCond.entails.trans {P Q R : PostCond α ps} (h₁ : P ⊢ₚ Q) (h₂ : Q ⊢ₚ R) : P ⊢ₚ R :=
|
||||
⟨fun a => (h₁.1 a).trans (h₂.1 a), h₁.2.trans h₂.2⟩
|
||||
|
||||
@[simp]
|
||||
theorem PostCond.entails_total (p : α → Assertion ps) (q : PostCond α ps) : PostCond.total p ⊢ₚ q ↔ ∀ a, p a ⊢ₛ q.1 a := by
|
||||
simp only [entails, FailConds.entails_false, and_true]
|
||||
|
||||
@[simp]
|
||||
theorem PostCond.entails_partial (p : PostCond α ps) (q : α → Assertion ps) : p ⊢ₚ PostCond.partial q ↔ ∀ a, p.1 a ⊢ₛ q a := by
|
||||
simp only [entails, FailConds.entails_true, and_true]
|
||||
|
||||
abbrev PostCond.and (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
|
||||
(fun a => SPred.and (p.1 a) (q.1 a), FailConds.and p.2 q.2)
|
||||
|
||||
infixr:35 " ∧ₚ " => PostCond.and
|
||||
|
||||
theorem PostCond.and_eq_left {p q : PostCond α ps} (h : p ⊢ₚ q) :
|
||||
p = (p ∧ₚ q) := by
|
||||
ext
|
||||
· exact (SPred.and_eq_left.mp (h.1 _)).to_eq
|
||||
· exact FailConds.and_eq_left h.2
|
||||
239
src/Std/Do/PredTrans.lean
Normal file
239
src/Std/Do/PredTrans.lean
Normal file
|
|
@ -0,0 +1,239 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Init.Control.Lawful
|
||||
import Std.Do.PostCond
|
||||
|
||||
/-!
|
||||
# Predicate transformers for arbitrary postcondition shapes
|
||||
|
||||
This module defines the type `PredTrans ps` of *predicate transformers* for a given `ps :
|
||||
PostShape`.
|
||||
`PredTrans` forms the semantic domain of the weakest precondition interpretation
|
||||
`WP` in which we interpret monadic programs.
|
||||
|
||||
A predicate transformer `x : PredTrans ps α` is a function that takes a postcondition
|
||||
`Q : PostCond α ps` and returns a precondition `x.apply Q : Assertion ps`, with the additional
|
||||
monotonicity property that the precondition is stronger the stronger the postcondition is:
|
||||
`Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂`.
|
||||
|
||||
Since `PredTrans` itself forms a monad, we can interpret monadic programs by writing
|
||||
a monad morphism into `PredTrans`; this is exactly what `WP` encodes.
|
||||
This module defines interpretations of common monadic operations, such as `get`, `throw`,
|
||||
`liftM`, etc.
|
||||
-/
|
||||
|
||||
namespace Std.Do
|
||||
|
||||
/-- The stronger the postcondition, the stronger the transformed precondition. -/
|
||||
def PredTrans.Monotonic {ps : PostShape} {α : Type} (t : PostCond α ps → Assertion ps) : Prop :=
|
||||
∀ Q₁ Q₂, (Q₁ ⊢ₚ Q₂) → (t Q₁) ⊢ₛ (t Q₂)
|
||||
|
||||
/-- Transforming a conjunction of postconditions is the same as the conjunction of transformed
|
||||
postconditions. -/
|
||||
def PredTrans.Conjunctive {ps : PostShape} {α : Type} (t : PostCond α ps → Assertion ps) : Prop :=
|
||||
∀ Q₁ Q₂, t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂
|
||||
|
||||
/-- Any predicate transformer that is conjunctive is also monotonic. -/
|
||||
def PredTrans.Conjunctive.mono {ps : PostShape} {α : Type}
|
||||
(t : PostCond α ps → Assertion ps) (h : PredTrans.Conjunctive t) : PredTrans.Monotonic t := by
|
||||
intro Q₁ Q₂ hq
|
||||
replace hq : Q₁ = (Q₁ ∧ₚ Q₂) := PostCond.and_eq_left hq
|
||||
rw [hq, (h Q₁ Q₂).to_eq]
|
||||
exact SPred.and_elim_r
|
||||
|
||||
/--
|
||||
The type of predicate transformers for a given `ps : PostShape` and return type `α : Type`.
|
||||
A predicate transformer `x : PredTrans ps α` is a function that takes a postcondition
|
||||
`Q : PostCond α ps` and returns a precondition `x.apply Q : Assertion ps`, with the additional
|
||||
monotonicity property that the precondition is stronger the stronger the postcondition is:
|
||||
`Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂`.
|
||||
-/
|
||||
@[ext]
|
||||
structure PredTrans (ps : PostShape) (α : Type) : Type where
|
||||
apply : PostCond α ps → Assertion ps
|
||||
conjunctive : PredTrans.Conjunctive apply
|
||||
|
||||
namespace PredTrans
|
||||
|
||||
theorem mono {ps : PostShape} {α : Type} (t : PredTrans ps α) : Monotonic t.apply :=
|
||||
Conjunctive.mono t.apply t.conjunctive
|
||||
|
||||
/--
|
||||
Given a fixed postcondition, the *stronger* predicate transformer will yield a
|
||||
*weaker* precondition.
|
||||
-/
|
||||
def le {ps : PostShape} {α : Type} (x y : PredTrans ps α) : Prop :=
|
||||
∀ Q, y.apply Q ⊢ₛ x.apply Q -- the weaker the precondition, the smaller the PredTrans
|
||||
instance : LE (PredTrans ps α) := ⟨le⟩
|
||||
|
||||
def pure {ps : PostShape} {α : Type} (a : α) : PredTrans ps α :=
|
||||
{ apply := fun Q => Q.1 a, conjunctive := by intro _ _; simp }
|
||||
|
||||
def bind {ps : PostShape} {α β : Type} (x : PredTrans ps α) (f : α → PredTrans ps β) : PredTrans ps β :=
|
||||
{ apply := fun Q => x.apply (fun a => (f a).apply Q, Q.2),
|
||||
conjunctive := by
|
||||
intro Q₁ Q₂
|
||||
apply SPred.bientails.of_eq
|
||||
dsimp
|
||||
conv => rhs; rw [← (x.conjunctive _ _).to_eq]
|
||||
conv in (f _).apply _ => rw [((f _).conjunctive _ _).to_eq]
|
||||
}
|
||||
|
||||
def const {ps : PostShape} {α : Type} (p : Assertion ps) : PredTrans ps α :=
|
||||
{ apply := fun Q => p, conjunctive := by intro _ _; simp [SPred.and_self.to_eq] }
|
||||
|
||||
instance : Monad (PredTrans ps) where
|
||||
pure := pure
|
||||
bind := bind
|
||||
|
||||
@[simp]
|
||||
theorem pure_apply {ps : PostShape} {α : Type} (a : α) (Q : PostCond α ps) :
|
||||
(PredTrans.pure a : PredTrans ps α).apply Q = Q.1 a := by rfl
|
||||
|
||||
@[simp]
|
||||
theorem Pure_pure_apply {ps : PostShape} {α : Type} (a : α) (Q : PostCond α ps) :
|
||||
(Pure.pure a : PredTrans ps α).apply Q = Q.1 a := by rfl
|
||||
|
||||
@[simp]
|
||||
theorem map_apply {ps : PostShape} {α β : Type} (f : α → β) (x : PredTrans ps α) (Q : PostCond β ps) :
|
||||
(f <$> x).apply Q = x.apply (fun a => Q.1 (f a), Q.2) := by rfl
|
||||
|
||||
@[simp]
|
||||
theorem bind_apply {ps : PostShape} {α β : Type} (x : PredTrans ps α) (f : α → PredTrans ps β) (Q : PostCond β ps) :
|
||||
(x >>= f).apply Q = x.apply (fun a => (f a).apply Q, Q.2) := by rfl
|
||||
|
||||
@[simp]
|
||||
theorem seq_apply {ps : PostShape} {α β : Type} (f : PredTrans ps (α → β)) (x : PredTrans ps α) (Q : PostCond β ps) :
|
||||
(f <*> x).apply Q = f.apply (fun g => x.apply (fun a => Q.1 (g a), Q.2), Q.2) := by rfl
|
||||
|
||||
theorem bind_mono {ps : PostShape} {α β : Type} {x y : PredTrans ps α} {f : α → PredTrans ps β}
|
||||
(h : x ≤ y) : x >>= f ≤ y >>= f := by intro Q; exact (h (_, Q.2))
|
||||
|
||||
instance instLawfulMonad : LawfulMonad (PredTrans ps) :=
|
||||
LawfulMonad.mk' (PredTrans ps)
|
||||
(id_map := by simp +unfoldPartialApp [Functor.map, bind, pure])
|
||||
(pure_bind := by simp +unfoldPartialApp [Bind.bind, bind, Pure.pure, pure])
|
||||
(bind_assoc := by simp +unfoldPartialApp [Bind.bind, bind])
|
||||
|
||||
-- The interpretation of `StateT σ (PredTrans ps) α` into `PredTrans (.arg σ ps) α`.
|
||||
-- Think: modifyGetM
|
||||
def pushArg {ps : PostShape} {σ : Type} {α : Type} (x : StateT σ (PredTrans ps) α) : PredTrans (.arg σ ps) α :=
|
||||
{ apply := fun Q s => (x s).apply (fun (a, s) => Q.1 a s, Q.2),
|
||||
conjunctive := by
|
||||
intro Q₁ Q₂
|
||||
apply SPred.bientails.of_eq
|
||||
ext s
|
||||
dsimp
|
||||
rw [← ((x s).conjunctive _ _).to_eq]
|
||||
}
|
||||
|
||||
def popArg {ps : PostShape} {α} (x : PredTrans (.arg σ ps) α) : StateT σ (PredTrans ps) α := fun s =>
|
||||
{ apply Q := x.apply (fun r s' => Q.1 (r, s'), Q.2) s,
|
||||
conjunctive := by
|
||||
intro Q₁ Q₂
|
||||
apply SPred.bientails.of_eq
|
||||
dsimp
|
||||
have {Q₁ Q₂}: spred(x.apply Q₁ ∧ x.apply Q₂) s = spred(x.apply (Q₁ ∧ₚ Q₂) s) := by
|
||||
rw[congrFun (x.conjunctive _ _).to_eq _]
|
||||
simp only [SPred.and] at this
|
||||
simp only [this]
|
||||
rfl
|
||||
}
|
||||
|
||||
-- The interpretation of `ExceptT ε (PredTrans ps) α` into `PredTrans (.except ε ps) α`
|
||||
def pushExcept {ps : PostShape} {α ε} (x : ExceptT ε (PredTrans ps) α) : PredTrans (.except ε ps) α :=
|
||||
{ apply Q := x.apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2),
|
||||
conjunctive := by
|
||||
intro Q₁ Q₂
|
||||
apply SPred.bientails.of_eq
|
||||
dsimp
|
||||
rw[← (x.conjunctive _ _).to_eq]
|
||||
congr
|
||||
ext x
|
||||
cases x <;> simp
|
||||
}
|
||||
|
||||
def popExcept {ps : PostShape} {α} (x : PredTrans (.except ε ps) α) : ExceptT ε (PredTrans ps) α :=
|
||||
{ apply Q := x.apply (fun a => Q.1 (.ok a), fun e => Q.1 (.error e), Q.2),
|
||||
conjunctive := by
|
||||
intro Q₁ Q₂
|
||||
apply SPred.bientails.of_eq
|
||||
dsimp
|
||||
rw[← (x.conjunctive _ _).to_eq]
|
||||
rfl
|
||||
}
|
||||
|
||||
instance instMonadLiftArg : MonadLift (PredTrans m) (PredTrans (.arg σ m)) where
|
||||
monadLift x := pushArg (StateT.lift x)
|
||||
|
||||
instance instMonadLiftExcept : MonadLift (PredTrans m) (PredTrans (.except ε m)) where
|
||||
monadLift x := pushExcept (ExceptT.lift x)
|
||||
|
||||
instance instMonadFunctorArg : MonadFunctor (PredTrans m) (PredTrans (.arg σ m)) where
|
||||
monadMap f x := pushArg (fun s => f (popArg x s))
|
||||
|
||||
instance instMonadFunctorExcept : MonadFunctor (PredTrans m) (PredTrans (.except ε m)) where
|
||||
monadMap f x := pushExcept (f x.popExcept)
|
||||
|
||||
@[simp]
|
||||
def pushArg_apply {ps} {α : Type} {σ : Type} {Q : PostCond α (.arg σ ps)} (f : σ → PredTrans ps (α × σ)) :
|
||||
(pushArg f).apply Q = fun s => (f s).apply (fun ⟨a, s⟩ => Q.1 a s, Q.2) := rfl
|
||||
|
||||
@[simp]
|
||||
def pushExcept_apply {ps} {α ε} {Q : PostCond α (.except ε ps)} (x : PredTrans ps (Except ε α)) :
|
||||
(pushExcept x).apply Q = x.apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := rfl
|
||||
|
||||
def dite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : c → PredTrans ps α) (e : ¬ c → PredTrans ps α) :
|
||||
(if h : c then t h else e h).apply Q = if h : c then (t h).apply Q else (e h).apply Q := by split <;> rfl
|
||||
|
||||
def ite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : PredTrans ps α) (e : PredTrans ps α) :
|
||||
(if c then t else e).apply Q = if c then t.apply Q else e.apply Q := by split <;> rfl
|
||||
|
||||
@[simp]
|
||||
def monadLiftArg_apply {ps} {Q : PostCond α (.arg σ ps)} (t : PredTrans ps α) :
|
||||
(MonadLift.monadLift t : PredTrans (.arg σ ps) α).apply Q = fun s => t.apply (fun a => Q.1 a s, Q.2) := rfl
|
||||
|
||||
@[simp]
|
||||
def monadLiftExcept_apply {ps} {Q : PostCond α (.except ε ps)} (t : PredTrans ps α) :
|
||||
(MonadLift.monadLift t : PredTrans (.except ε ps) α).apply Q = t.apply (fun a => Q.1 a, Q.2.2) := rfl
|
||||
|
||||
@[simp]
|
||||
def monadMapArg_apply {ps} {Q : PostCond α (.arg σ ps)} (f : ∀{β}, PredTrans ps β → PredTrans ps β) (t : PredTrans (.arg σ ps) α) :
|
||||
(MonadFunctor.monadMap (m:=PredTrans ps) f t).apply Q = fun s => (f (t.popArg s)).apply (fun (a, s) => Q.1 a s, Q.2) := rfl
|
||||
|
||||
@[simp]
|
||||
def monadMapExcept_apply {ps} {Q : PostCond α (.except ε ps)} (f : ∀{β}, PredTrans ps β → PredTrans ps β) (t : PredTrans (.except ε ps) α) :
|
||||
(MonadFunctor.monadMap (m:=PredTrans ps) f t).apply Q = (f t.popExcept).apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := rfl
|
||||
|
||||
@[simp]
|
||||
def popArg_apply {ps} {Q : PostCond (α × σ) ps} (t : PredTrans (.arg σ ps) α) :
|
||||
(t.popArg s).apply Q = t.apply (fun a s => Q.1 (a, s), Q.2) s := rfl
|
||||
|
||||
@[simp]
|
||||
def popExcept_apply {ps} {Q : PostCond (Except ε α) ps} (t : PredTrans (.except ε ps) α) :
|
||||
(t.popExcept).apply Q = t.apply (fun a => Q.1 (.ok a), fun e => Q.1 (.error e), Q.2) := rfl
|
||||
|
||||
@[simp]
|
||||
theorem pushArg_popArg : pushArg (popArg x) = x := rfl
|
||||
|
||||
@[simp]
|
||||
theorem popArg_pushArg : popArg (pushArg f) = f := rfl
|
||||
|
||||
-- Just a reminder for me that the following would not hold for a suitable defn of pushReader and popReader:
|
||||
--theorem pushReader_popReader : pushReader (popReader x) = x := sorry
|
||||
-- goal: x.apply (fun a x => Q.1 a x✝, Q.2) x✝ = x.apply Q x✝
|
||||
|
||||
@[simp]
|
||||
theorem pushExcept_popExcept : pushExcept (popExcept x) = x := rfl
|
||||
|
||||
@[simp]
|
||||
theorem popExcept_pushExcept : popExcept (pushExcept x) = x := by
|
||||
ext Q
|
||||
simp only [ExceptT.run, popExcept, pushExcept]
|
||||
congr
|
||||
ext x
|
||||
cases x <;> simp
|
||||
8
src/Std/Do/Triple.lean
Normal file
8
src/Std/Do/Triple.lean
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Std.Do.Triple.Basic
|
||||
import Std.Do.Triple.SpecLemmas
|
||||
63
src/Std/Do/Triple/Basic.lean
Normal file
63
src/Std/Do/Triple/Basic.lean
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Std.Do.WP
|
||||
import Std.Do.SPred
|
||||
|
||||
/-!
|
||||
# Hoare triples
|
||||
|
||||
Hoare triples form the basis for compositional functional correctness proofs about monadic programs.
|
||||
|
||||
As usual, `Triple x P Q` holds iff the precondition `P` entails the weakest precondition
|
||||
`wp⟦x⟧.apply Q` of `x : m α` for the postcondition `Q`.
|
||||
It is thus defined in terms of an instance `WP m ps`.
|
||||
-/
|
||||
|
||||
namespace Std.Do
|
||||
|
||||
universe u
|
||||
variable {m : Type → Type u} {ps : PostShape}
|
||||
|
||||
/--
|
||||
A Hoare triple for reasoning about monadic programs.
|
||||
A proof for `Triple x P Q` is a *specification* for `x`:
|
||||
If assertion `P` holds before `x`, then postcondition `Q` holds after running `x`.
|
||||
|
||||
`⦃P⦄ x ⦃Q⦄` is convenient syntax for `Triple x P Q`.
|
||||
-/
|
||||
def Triple [WP m ps] {α} (x : m α) (P : Assertion ps) (Q : PostCond α ps) : Prop :=
|
||||
P ⊢ₛ wp⟦x⟧ Q
|
||||
|
||||
@[inherit_doc Std.Do.Triple]
|
||||
scoped syntax:lead (name := triple) "⦃" term "⦄ " term:lead " ⦃" term "⦄" : term
|
||||
|
||||
namespace Triple
|
||||
|
||||
instance [WP m ps] (x : m α) : SPred.Tactic.PropAsSPredTautology (Triple x P Q) spred(P → wp⟦x⟧ Q) where
|
||||
iff := (SPred.entails_true_intro P (wp⟦x⟧ Q)).symm
|
||||
|
||||
theorem pure [Monad m] [WPMonad m ps] {α} {Q : PostCond α ps} (a : α) (himp : P ⊢ₛ Q.1 a) :
|
||||
Triple (pure (f:=m) a) P Q := himp.trans (by simp)
|
||||
|
||||
theorem bind [Monad m] [WPMonad m ps] {α β} {P : Assertion ps} {Q : α → Assertion ps} {R : PostCond β ps} (x : m α) (f : α → m β)
|
||||
(hx : Triple x P (Q, R.2))
|
||||
(hf : ∀ b, Triple (f b) (Q b) R) :
|
||||
Triple (x >>= f) P R := by
|
||||
apply SPred.entails.trans hx
|
||||
simp only [WP.bind]
|
||||
apply (wp x).mono _ _
|
||||
simp only [PostCond.entails, Assertion, FailConds.entails.refl, and_true]
|
||||
exact hf
|
||||
|
||||
theorem and [WP m ps] (x : m α) (h₁ : Triple x P₁ Q₁) (h₂ : Triple x P₂ Q₂) : Triple x spred(P₁ ∧ P₂) (Q₁ ∧ₚ Q₂) :=
|
||||
(SPred.and_mono h₁ h₂).trans ((wp x).conjunctive Q₁ Q₂).mpr
|
||||
|
||||
theorem rewrite_program [WP m ps] {prog₁ prog₂ : m α}
|
||||
(heq : prog₁ = prog₂) (hprf : Triple prog₂ P Q) :
|
||||
Triple prog₁ P Q := heq ▸ hprf
|
||||
|
||||
end Triple
|
||||
481
src/Std/Do/Triple/SpecLemmas.lean
Normal file
481
src/Std/Do/Triple/SpecLemmas.lean
Normal file
|
|
@ -0,0 +1,481 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Std.Do.Triple.Basic
|
||||
import Std.Tactic.Do.Syntax
|
||||
import Std.Do.WP
|
||||
|
||||
/-!
|
||||
# Hoare triple specifications for select functions
|
||||
|
||||
This module contains Hoare triple specifications for some functions in Core.
|
||||
-/
|
||||
|
||||
namespace Std.Range
|
||||
|
||||
abbrev toList (r : Std.Range) : List Nat :=
|
||||
List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
|
||||
|
||||
theorem toList_range' (r : Std.Range) (h : r.step = 1) :
|
||||
toList r = List.range' r.start (r.stop - r.start) := by
|
||||
simp [toList, h]
|
||||
|
||||
end Std.Range
|
||||
|
||||
namespace Std.List
|
||||
|
||||
@[ext]
|
||||
structure Zipper {α : Type u} (l : List α) : Type u where
|
||||
rpref : List α
|
||||
suff : List α
|
||||
property : rpref.reverse ++ suff = l
|
||||
|
||||
abbrev Zipper.pref {α} {l : List α} (s : List.Zipper l) : List α := s.rpref.reverse
|
||||
|
||||
abbrev Zipper.begin (l : List α) : Zipper l := ⟨[],l,rfl⟩
|
||||
abbrev Zipper.end (l : List α) : Zipper l := ⟨l.reverse,[],by simp⟩
|
||||
abbrev Zipper.tail (s : Zipper l) (h : s.suff = hd::tl) : Zipper l :=
|
||||
{ rpref := hd::s.rpref, suff := tl, property := by simp [s.property, ←h] }
|
||||
|
||||
end Std.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 "⦃" P "⦄ " x:lead " ⦃" Q "⦄" => Triple x (spred(P)) spred(Q)
|
||||
|
||||
/-! # If/Then/Else -/
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.ite {α m ps} {P : Assertion ps} {Q : PostCond α ps} (c : Prop) [Decidable c] [WP m ps] (t : m α) (e : m α)
|
||||
(ifTrue : c → ⦃P⦄ t ⦃Q⦄) (ifFalse : ¬c → ⦃P⦄ e ⦃Q⦄) :
|
||||
⦃P⦄ if c then t else e ⦃Q⦄ := by
|
||||
split <;> apply_rules
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.dite {α m ps} {P : Assertion ps} {Q : PostCond α ps} (c : Prop) [Decidable c] [WP m ps] (t : c → m α) (e : ¬ c → m α)
|
||||
(ifTrue : (h : c) → ⦃P⦄ t h ⦃Q⦄) (ifFalse : (h : ¬ c) → ⦃P⦄ e h ⦃Q⦄) :
|
||||
⦃P⦄ if h : c then t h else e h ⦃Q⦄ := by
|
||||
split <;> apply_rules
|
||||
|
||||
/-! # `Monad` -/
|
||||
|
||||
universe u
|
||||
variable {m : Type → Type u} {ps : PostShape}
|
||||
|
||||
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
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.pure {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α} {a : α} {Q : PostCond α ps} :
|
||||
⦃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)
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.bind {m : Type → Type u} {ps : PostShape} [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
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.map {m : Type → Type u} {ps : PostShape} [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]
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.seq {m : Type → Type u} {ps : PostShape} [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]
|
||||
|
||||
/-! # `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]
|
||||
|
||||
-- @[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]
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.monadLift_ExceptT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except ε ps)) :
|
||||
Triple (ps:=.except ε ps)
|
||||
(MonadLift.monadLift x : ExceptT ε m α)
|
||||
(wp⟦x⟧ (fun a => Q.1 a, Q.2.2))
|
||||
Q := by simp [Triple, SPred.entails.refl]
|
||||
|
||||
/-! # `MonadLiftT` -/
|
||||
|
||||
-- attribute [spec] liftM instMonadLiftTOfMonadLift instMonadLiftT
|
||||
|
||||
/-! # `MonadFunctor` -/
|
||||
|
||||
-- @[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
|
||||
|
||||
-- @[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
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.monadMap_ExceptT [Monad m] [WP m ps]
|
||||
(f : ∀{β}, m β → m β) {α} (x : ExceptT ε m α) (Q : PostCond α (.except ε ps)) :
|
||||
Triple (ps:=.except ε ps)
|
||||
(MonadFunctor.monadMap (m:=m) f x)
|
||||
(wp⟦f x.run⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
|
||||
Q := by simp only [Triple, WP.monadMap_ExceptT]; rfl
|
||||
|
||||
/-! # `MonadFunctorT` -/
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.monadMap_trans [WP o ps] [MonadFunctor n o] [MonadFunctorT m n] :
|
||||
Triple (ps:=ps)
|
||||
(MonadFunctorT.monadMap f x : o α)
|
||||
(wp⟦MonadFunctor.monadMap (m:=n) (MonadFunctorT.monadMap (m:=m) f) x : o α⟧ Q)
|
||||
Q := by simp [Triple]
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.monadMap_refl [WP m ps] :
|
||||
⦃wp⟦f x : m α⟧ Q⦄
|
||||
(MonadFunctorT.monadMap f x : m α)
|
||||
⦃Q⦄ := by simp [Triple]
|
||||
|
||||
/-! # `ReaderT` -/
|
||||
|
||||
-- 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]
|
||||
|
||||
-- @[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]
|
||||
|
||||
/-! # `StateT` -/
|
||||
|
||||
-- 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]
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.set_StateT [Monad m] [WPMonad m psm] :
|
||||
⦃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 => Q.1 (f s).1 (f s).2⦄ (MonadStateOf.modifyGet f : StateT σ m α) ⦃Q⦄ := by
|
||||
simp [Triple]
|
||||
|
||||
/-! # `ExceptT` -/
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.run_ExceptT [WP m ps] (x : ExceptT ε m α) :
|
||||
Triple (ps:=ps)
|
||||
(x.run : m (Except ε α))
|
||||
(wp⟦x⟧ (fun a => Q.1 (.ok a), fun e => Q.1 (.error e), Q.2))
|
||||
Q := by simp [Triple]
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.throw_ExceptT [Monad m] [WPMonad m ps] :
|
||||
⦃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
|
||||
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
|
||||
|
||||
-- @[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
|
||||
simp [Triple]
|
||||
|
||||
/-! # `EStateM` -/
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.get_EStateM :
|
||||
⦃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
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.modifyGet_EStateM :
|
||||
⦃fun s => Q.1 (f s).1 (f s).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
|
||||
|
||||
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
|
||||
simp [Triple]
|
||||
|
||||
/-! # Lifting `MonadStateOf` -/
|
||||
|
||||
-- attribute [spec] modify modifyThe getThe
|
||||
-- instMonadStateOfMonadStateOf instMonadStateOfOfMonadLift
|
||||
|
||||
/-! # Lifting `MonadReaderOf` -/
|
||||
|
||||
-- attribute [spec] readThe withTheReader
|
||||
-- instMonadReaderOfMonadReaderOf instMonadReaderOfOfMonadLift
|
||||
-- instMonadWithReaderOfMonadWithReaderOf instMonadWithReaderOfOfMonadFunctor
|
||||
|
||||
/-! # Lifting `MonadExceptOf` -/
|
||||
|
||||
-- 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
|
||||
|
||||
-- @[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
|
||||
|
||||
-- @[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
|
||||
|
||||
-- @[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
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.throw_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) :
|
||||
Triple (ps:=.except ε' ps)
|
||||
(MonadExceptOf.throw e : ExceptT ε' m α)
|
||||
(wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
|
||||
Q := by
|
||||
simp [Triple]
|
||||
apply (wp _).mono
|
||||
simp
|
||||
intro x
|
||||
split <;> rfl
|
||||
|
||||
-- @[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
|
||||
|
||||
-- @[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
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) :
|
||||
Triple
|
||||
(ps:=.except ε' ps)
|
||||
(MonadExceptOf.tryCatch x h : ExceptT ε' m α)
|
||||
(wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2))
|
||||
Q := by
|
||||
simp only [Triple, WP.tryCatch_lift_ExceptT]
|
||||
apply (wp _).mono
|
||||
simp
|
||||
intro x
|
||||
split <;> rfl
|
||||
|
||||
/-! # `ForIn` -/
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.forIn'_list {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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]⟩)⦄
|
||||
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
|
||||
suffices h : ∀ rpref suff (h : xs = rpref.reverse ++ suff),
|
||||
⦃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)⦄
|
||||
from h [] xs rfl
|
||||
intro rpref suff h
|
||||
induction suff generalizing rpref init
|
||||
case nil => apply Triple.pure; simp [h]
|
||||
case cons x suff ih =>
|
||||
simp only [List.forIn'_cons]
|
||||
apply Triple.bind
|
||||
case hx => exact step init rpref x (by simp[h]) suff h
|
||||
case hf =>
|
||||
intro r
|
||||
split
|
||||
next => apply Triple.pure; simp [h]
|
||||
next b =>
|
||||
simp
|
||||
have := @ih b (x::rpref) (by simp [h])
|
||||
simp at this
|
||||
exact this
|
||||
|
||||
-- using the postcondition as a constant invariant:
|
||||
theorem Spec.forIn'_list_const_inv {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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⦄ :=
|
||||
Spec.forIn'_list (fun p => inv.1 p.1, inv.2) (fun b _ x hx _ _ => step x hx b)
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.forIn_list {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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]⟩)⦄
|
||||
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
|
||||
simp only [← forIn'_eq_forIn]
|
||||
exact Spec.forIn'_list inv (fun b rpref x _ suff h => step b rpref x suff h)
|
||||
|
||||
-- using the postcondition as a constant invariant:
|
||||
theorem Spec.forIn_list_const_inv {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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⦄ :=
|
||||
Spec.forIn_list (fun p => inv.1 p.1, inv.2) (fun b _ hd _ _ => step hd b)
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.foldlM_list {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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]⟩)⦄
|
||||
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
|
||||
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]
|
||||
apply Spec.forIn_list inv
|
||||
simp only [Triple, WPMonad.wp_map, PredTrans.map_apply]
|
||||
exact step
|
||||
|
||||
-- using the postcondition as a constant invariant:
|
||||
theorem Spec.foldlM_list_const_inv {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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⦄ :=
|
||||
Spec.foldlM_list (fun p => inv.1 p.1, inv.2) (fun b _ hd _ _ => step hd b)
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.forIn'_range {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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]⟩)⦄
|
||||
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
|
||||
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)
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.forIn_range {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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]⟩)⦄
|
||||
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
|
||||
simp only [Std.Range.forIn_eq_forIn_range', Std.Range.size]
|
||||
apply Spec.forIn_list inv step
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.forIn'_array {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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]⟩)⦄
|
||||
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
|
||||
cases xs
|
||||
simp
|
||||
apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (by simp[hx]) suff h)
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.forIn_array {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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]⟩)⦄
|
||||
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
|
||||
cases xs
|
||||
simp
|
||||
apply Spec.forIn_list inv step
|
||||
|
||||
-- @[spec]
|
||||
theorem Spec.foldlM_array {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
{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]⟩)⦄
|
||||
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
|
||||
cases xs
|
||||
simp
|
||||
apply Spec.foldlM_list inv step
|
||||
10
src/Std/Do/WP.lean
Normal file
10
src/Std/Do/WP.lean
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Std.Do.WP.Basic
|
||||
import Std.Do.WP.Monad
|
||||
import Std.Do.WP.IO
|
||||
import Std.Do.WP.SimpLemmas
|
||||
111
src/Std/Do/WP/Basic.lean
Normal file
111
src/Std/Do/WP/Basic.lean
Normal file
|
|
@ -0,0 +1,111 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Std.Do.PredTrans
|
||||
|
||||
/-!
|
||||
# Weakest precondition interpretation
|
||||
|
||||
This module defines the weakest precondition interpretation `WP` of monadic programs
|
||||
in terms of predicate transformers `PredTrans`.
|
||||
|
||||
This interpretation forms the basis of our notion of Hoare triples.
|
||||
It is the main mechanism of this library for reasoning about monadic programs.
|
||||
|
||||
An instance `WP m ps` determines an interpretation `wp⟦x⟧` of a program `x : m α` in terms of a
|
||||
predicate transformer `PredTrans ps α`; The monad `m` determines `ps : PostShape` and hence
|
||||
the particular shape of the predicate transformer.
|
||||
|
||||
This library comes with pre-defined instances for common monads and transformers such as
|
||||
|
||||
* `WP Id .pure`, interpreting pure computations `x : Id α` in terms of a function (isomorphic to)
|
||||
`(α → Prop) → Prop`.
|
||||
* `WP (StateT σ m) (.arg σ ps)` given an instance `WP m ps`, interpreting `StateM σ α` in terms of
|
||||
a function `(α → σ → Prop) → σ → Prop`.
|
||||
* `WP (ExceptT ε m) (.except ε ps)` given an instance `WP m ps`, interpreting `Except ε α` in terms
|
||||
of `(α → Prop) → (ε → Prop) → Prop`.
|
||||
* `WP (EStateM ε σ) (.except ε (.arg σ .pure))` interprets `EStateM ε σ α` in terms of
|
||||
a function `(α → σ → Prop) → (ε → σ → Prop) → σ → Prop`.
|
||||
|
||||
These instances are all monad morphisms, a fact which is properly encoded and exploited
|
||||
by the subclass `WPMonad`.
|
||||
-/
|
||||
|
||||
namespace Std.Do
|
||||
|
||||
universe u
|
||||
variable {m : Type → Type u}
|
||||
|
||||
/--
|
||||
A weakest precondition interpretation of a monadic program `x : m α` in terms of a
|
||||
predicate transformer `PredTrans ps α`.
|
||||
The monad `m` determines `ps : PostShape`. See the module comment for more details.
|
||||
-/
|
||||
class WP (m : Type → Type u) (ps : outParam PostShape) where
|
||||
wp {α} (x : m α) : PredTrans ps α
|
||||
|
||||
export WP (wp)
|
||||
|
||||
scoped syntax:max "wp⟦" term:min (":" term)? "⟧" : term
|
||||
macro_rules
|
||||
| `(wp⟦$x:term⟧) => `((WP.wp $x).apply)
|
||||
| `(wp⟦$x:term : $ty⟧) => `((WP.wp ($x : $ty)).apply)
|
||||
|
||||
@[app_unexpander PredTrans.apply]
|
||||
protected def unexpandWP : Lean.PrettyPrinter.Unexpander
|
||||
| `($_ $e) => match e with
|
||||
| `(wp ($x : $ty)) => `(wp⟦$x : $ty⟧)
|
||||
| `(wp $e) => `(wp⟦$e⟧)
|
||||
| _ => throw ()
|
||||
| _ => throw ()
|
||||
instance Id.instWP : WP Id .pure where
|
||||
wp x := PredTrans.pure x.run
|
||||
|
||||
instance StateT.instWP [WP m ps] : WP (StateT σ m) (.arg σ ps) where
|
||||
wp x := PredTrans.pushArg (fun s => wp (x s))
|
||||
|
||||
instance ReaderT.instWP [WP m ps] : WP (ReaderT ρ m) (.arg ρ ps) where
|
||||
wp x := PredTrans.pushArg (fun s => (·, s) <$> wp (x s))
|
||||
|
||||
instance ExceptT.instWP [WP m ps] : WP (ExceptT ε m) (.except ε ps) where
|
||||
wp x := PredTrans.pushExcept (wp x)
|
||||
|
||||
instance EStateM.instWP : WP (EStateM ε σ) (.except ε (.arg σ .pure)) where
|
||||
wp x := -- Could define as PredTrans.mkExcept (PredTrans.modifyGetM (fun s => pure (EStateM.Result.toExceptState (x s))))
|
||||
{ apply := fun Q s => match x s with
|
||||
| .ok a s' => Q.1 a s'
|
||||
| .error e s' => Q.2.1 e s'
|
||||
conjunctive := by
|
||||
intro _ _
|
||||
apply SPred.bientails.of_eq
|
||||
ext s
|
||||
dsimp
|
||||
cases (x s) <;> simp
|
||||
}
|
||||
|
||||
instance State.instWP : WP (StateM σ) (.arg σ .pure) :=
|
||||
inferInstanceAs (WP (StateT σ Id) (.arg σ .pure))
|
||||
instance Reader.instWP : WP (ReaderM ρ) (.arg ρ .pure) :=
|
||||
inferInstanceAs (WP (ReaderT ρ Id) (.arg ρ .pure))
|
||||
instance Except.instWP : WP (Except ε) (.except ε .pure) :=
|
||||
inferInstanceAs (WP (ExceptT ε Id) (.except ε .pure))
|
||||
|
||||
theorem Id.by_wp {α} {x : α} {prog : Id α} (h : Id.run prog = x) (P : α → Prop) :
|
||||
wp⟦prog⟧ (PostCond.total P) → P x := h ▸ id
|
||||
|
||||
theorem StateM.by_wp {α} {x : α × σ} {prog : StateM σ α} (h : StateT.run prog s = x) (P : α × σ → Prop) :
|
||||
wp⟦prog⟧ (PostCond.total (fun a s' => P (a, s'))) s → P x := by
|
||||
intro hspec
|
||||
simp only [wp, PredTrans.pure, PredTrans.pushArg_apply] at hspec
|
||||
exact h ▸ hspec
|
||||
|
||||
theorem EStateM.by_wp {α} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α} (h : EStateM.run prog s = x) (P : EStateM.Result ε σ α → Prop) :
|
||||
wp⟦prog⟧ (PostCond.total (fun a s' => P (EStateM.Result.ok a s'))) s → P x := by
|
||||
intro hspec
|
||||
simp only [wp, FailConds.false, FailConds.const, SVal.curry_cons, SVal.curry_nil] at hspec
|
||||
split at hspec
|
||||
case h_1 a s' heq => rw[← heq] at hspec; exact h ▸ hspec
|
||||
case h_2 => contradiction
|
||||
46
src/Std/Do/WP/IO.lean
Normal file
46
src/Std/Do/WP/IO.lean
Normal file
|
|
@ -0,0 +1,46 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Init.System.IO
|
||||
import Std.Do.WP.Monad
|
||||
|
||||
/-!
|
||||
# Barebones `WP` instance for `IO`
|
||||
|
||||
This module defines a `WP` instance for `IO` without any synthetic model of the `IO.RealWorld` whatsoever.
|
||||
This is useful for reasoning about `IO` programs when the precise result of a side-effect is irrelevant;
|
||||
for example it can be used to reason about random number generation.
|
||||
It is however inadequate for reasoning about, e.g., `IO.Ref`s.
|
||||
-/
|
||||
|
||||
namespace Std.Do.IO.Bare
|
||||
|
||||
open Std.Do
|
||||
|
||||
/--
|
||||
This is pretty much the instance for `EStateM` specialized to `σ = IO.RealWorld`.
|
||||
However, `IO.RealWorld` is ommitted in the `PredShape`.
|
||||
-/
|
||||
scoped instance instWP : WP (EIO ε) (.except ε .pure) where
|
||||
wp x := -- Could define as PredTrans.mkExcept (PredTrans.modifyGetM (fun s => pure (EStateM.Result.toExceptState (x s))))
|
||||
{ apply := fun Q => match x () with
|
||||
| .ok a _rw => Q.1 a
|
||||
| .error e _rw => Q.2.1 e
|
||||
conjunctive := by
|
||||
intro _ _
|
||||
apply SPred.bientails.of_eq
|
||||
dsimp
|
||||
cases (x ()) <;> rfl
|
||||
}
|
||||
|
||||
instance instLawfulMonad : LawfulMonad (EIO ε) := inferInstanceAs (LawfulMonad (EStateM ε IO.RealWorld))
|
||||
|
||||
scoped instance instWPMonad : WPMonad (EIO ε) (.except ε .pure) where
|
||||
wp_pure a := by simp only [wp, pure, EStateM.pure, PredTrans.pure]
|
||||
wp_bind x f := by
|
||||
ext Q : 2
|
||||
simp only [wp, bind, EStateM.bind, PredTrans.bind]
|
||||
cases (x ()) <;> rfl
|
||||
81
src/Std/Do/WP/Monad.lean
Normal file
81
src/Std/Do/WP/Monad.lean
Normal file
|
|
@ -0,0 +1,81 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Std.Do.WP.Basic
|
||||
|
||||
/-!
|
||||
# Monad morphisms and weakest precondition interpretations
|
||||
|
||||
A `WP m ps` is a `WPMonad m ps` if the interpretation `WP.wp` is also a monad morphism, that is,
|
||||
it preserves `pure` and `bind`.
|
||||
-/
|
||||
|
||||
namespace Std.Do
|
||||
|
||||
universe u
|
||||
variable {m : Type → Type u} {ps : PostShape}
|
||||
|
||||
/--
|
||||
A `WP` that is also a monad morphism, preserving `pure` and `bind`. (They all are.)
|
||||
-/
|
||||
class WPMonad (m : Type → Type u) (ps : outParam PostShape) [Monad m]
|
||||
extends LawfulMonad m, WP m ps where
|
||||
wp_pure : ∀ {α} (a : α), wp (pure a) = pure a
|
||||
wp_bind : ∀ {α β} (x : m α) (f : α → m β), wp (do let a ← x; f a) = do let a ← wp x; wp (f a)
|
||||
|
||||
theorem WPMonad.wp_map [Monad m] [WPMonad m ps] (f : α → β) (x : m α) :
|
||||
wp (f <$> x) = f <$> wp x := by simp [← bind_pure_comp, wp_pure, wp_bind]
|
||||
|
||||
theorem WPMonad.wp_seq [Monad m] [WPMonad m ps] (f : m (α → β)) (x : m α) :
|
||||
wp (f <*> x) = wp f <*> wp x := by simp [← bind_map, wp_map, wp_bind]
|
||||
|
||||
open WPMonad
|
||||
|
||||
instance Id.instWPMonad : WPMonad Id .pure where
|
||||
wp_pure a := by simp only [wp, PredTrans.pure, Pure.pure, Id.run]
|
||||
wp_bind x f := by simp only [wp, PredTrans.pure, Bind.bind, Id.run, PredTrans.bind]
|
||||
|
||||
instance StateT.instWPMonad [Monad m] [WPMonad m ps] : WPMonad (StateT σ m) (.arg σ ps) where
|
||||
wp_pure a := by ext; simp only [wp, pure, StateT.pure, WPMonad.wp_pure, PredTrans.pure,
|
||||
PredTrans.pushArg_apply]
|
||||
wp_bind x f := by ext; simp only [wp, bind, StateT.bind, WPMonad.wp_bind, PredTrans.bind,
|
||||
PredTrans.pushArg_apply]
|
||||
|
||||
instance ReaderT.instWPMonad [Monad m] [WPMonad m ps] : WPMonad (ReaderT ρ m) (.arg ρ ps) where
|
||||
wp_pure a := by ext; simp only [wp, pure, ReaderT.pure, WPMonad.wp_pure, PredTrans.pure,
|
||||
PredTrans.pushArg_apply, PredTrans.map_apply]
|
||||
wp_bind x f := by ext; simp only [wp, bind, ReaderT.bind, WPMonad.wp_bind, PredTrans.bind,
|
||||
PredTrans.pushArg_apply, PredTrans.map_apply]
|
||||
|
||||
instance ExceptT.instWPMonad [Monad m] [WPMonad m ps] : WPMonad (ExceptT ε m) (.except ε ps) where
|
||||
wp_pure a := by ext; simp only [wp, pure, ExceptT.pure, ExceptT.mk, WPMonad.wp_pure,
|
||||
PredTrans.pure, PredTrans.pushExcept_apply]
|
||||
wp_bind x f := by
|
||||
ext Q
|
||||
simp only [wp, bind, ExceptT.bind, ExceptT.mk, WPMonad.wp_bind, PredTrans.bind,
|
||||
ExceptT.bindCont, PredTrans.pushExcept_apply]
|
||||
congr
|
||||
ext b
|
||||
cases b
|
||||
case error a => simp [wp_pure]
|
||||
case ok a => rfl
|
||||
|
||||
instance EStateM.instWPMonad : WPMonad (EStateM ε σ) (.except ε (.arg σ .pure)) where
|
||||
wp_pure a := by simp only [wp, pure, EStateM.pure, PredTrans.pure]
|
||||
wp_bind x f := by
|
||||
ext Q : 2
|
||||
simp only [wp, bind, EStateM.bind, PredTrans.bind]
|
||||
ext s : 1
|
||||
cases (x s) <;> rfl
|
||||
|
||||
instance Except.instWPMonad : WPMonad (Except ε) (.except ε .pure) where
|
||||
wp_pure a := rfl
|
||||
wp_bind x f := by cases x <;> rfl
|
||||
|
||||
instance State.instWPMonad : WPMonad (StateM σ) (.arg σ .pure) :=
|
||||
inferInstanceAs (WPMonad (StateT σ Id) (.arg σ .pure))
|
||||
instance Reader.instWPMonad : WPMonad (ReaderM ρ) (.arg ρ .pure) :=
|
||||
inferInstanceAs (WPMonad (ReaderT ρ Id) (.arg ρ .pure))
|
||||
374
src/Std/Do/WP/SimpLemmas.lean
Normal file
374
src/Std/Do/WP/SimpLemmas.lean
Normal file
|
|
@ -0,0 +1,374 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sebastian Graf
|
||||
-/
|
||||
prelude
|
||||
import Std.Do.WP.Basic
|
||||
import Std.Do.WP.Monad
|
||||
|
||||
/-!
|
||||
# Simp lemmas for working with weakest preconditions
|
||||
|
||||
Many weakest preconditions are so simple that we can compute them directly or
|
||||
express them in terms of "simpler" weakest preconditions.
|
||||
This module provides simp lemmas targeting expressions of the form `wp⟦x⟧ Q`
|
||||
and rewrites them to expressions of simpler weakest preconditions.
|
||||
-/
|
||||
|
||||
namespace Std.Do.WP
|
||||
|
||||
open WPMonad
|
||||
|
||||
universe u
|
||||
variable {m : Type → Type u} {ps : PostShape}
|
||||
|
||||
/-! ## `WP` -/
|
||||
|
||||
@[simp]
|
||||
theorem ReaderT_run [WP m ps] (x : ReaderT ρ m α) :
|
||||
wp⟦x.run r⟧ Q = wp⟦x⟧ (fun a _ => Q.1 a, Q.2) r := rfl
|
||||
|
||||
@[simp]
|
||||
theorem StateT_run [WP m ps] (x : StateT σ m α) :
|
||||
wp⟦x.run s⟧ Q = wp⟦x⟧ (fun a s => Q.1 (a, s), Q.2) s := rfl
|
||||
|
||||
@[simp]
|
||||
theorem ExceptT_run [WP m ps] (x : ExceptT ε m α) :
|
||||
wp⟦x.run⟧ Q = wp⟦x⟧ (fun a => Q.1 (.ok a), fun e => Q.1 (.error e), Q.2) := by
|
||||
simp [wp, ExceptT.run]
|
||||
congr
|
||||
(ext x; cases x) <;> rfl
|
||||
|
||||
/-! ## `WPMonad` -/
|
||||
|
||||
@[simp]
|
||||
theorem pure [Monad m] [WPMonad m ps] (a : α) (Q : PostCond α ps) :
|
||||
wp⟦pure (f:=m) a⟧ Q = Q.1 a := by simp [WPMonad.wp_pure]
|
||||
|
||||
@[simp]
|
||||
theorem bind [Monad m] [WPMonad m ps] (x : m α) (f : α → m β) (Q : PostCond β ps) :
|
||||
wp⟦x >>= f⟧ Q = wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2) := by simp [WPMonad.wp_bind]
|
||||
|
||||
@[simp]
|
||||
theorem map [Monad m] [WPMonad m ps] (f : α → β) (x : m α) (Q : PostCond β ps) :
|
||||
wp⟦f <$> x⟧ Q = wp⟦x⟧ (fun a => Q.1 (f a), Q.2) := by simp [WPMonad.wp_map]
|
||||
|
||||
@[simp]
|
||||
theorem seq [Monad m] [WPMonad m ps] (f : m (α → β)) (x : m α) (Q : PostCond β ps) :
|
||||
wp⟦f <*> x⟧ Q = wp⟦f⟧ (fun f => wp⟦x⟧ (fun a => Q.1 (f a), Q.2), Q.2) := by simp [WPMonad.wp_seq]
|
||||
|
||||
/-! ## `MonadLift`
|
||||
|
||||
The definitions that follow interpret `liftM` and thus instances of, e.g., `MonadStateOf`.
|
||||
|
||||
-/
|
||||
|
||||
section MonadLift
|
||||
|
||||
@[simp]
|
||||
theorem monadLift_StateT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg σ ps)) :
|
||||
wp⟦MonadLift.monadLift x : StateT σ m α⟧ Q = fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2) := by simp [wp, MonadLift.monadLift, StateT.lift]
|
||||
|
||||
@[simp]
|
||||
theorem monadLift_ReaderT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg ρ ps)) :
|
||||
wp⟦MonadLift.monadLift x : ReaderT ρ m α⟧ Q = fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2) := rfl
|
||||
|
||||
@[simp]
|
||||
theorem monadLift_ExceptT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except ε ps)) :
|
||||
wp⟦MonadLift.monadLift x : ExceptT ε m α⟧ Q = wp⟦x⟧ (fun a => Q.1 a, Q.2.2) := by
|
||||
simp [wp, MonadLift.monadLift, ExceptT.lift, ExceptT.mk]
|
||||
|
||||
@[simp]
|
||||
theorem monadLift_trans [WP o ps] [MonadLift n o] [MonadLiftT m n] :
|
||||
wp⟦MonadLiftT.monadLift x : o α⟧ Q = wp⟦MonadLift.monadLift (m:=n) (MonadLiftT.monadLift (m:=m) x) : o α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem monadLift_refl [WP m ps] :
|
||||
wp⟦MonadLiftT.monadLift x : m α⟧ Q = wp⟦x : m α⟧ Q := rfl
|
||||
|
||||
-- instances
|
||||
|
||||
@[simp]
|
||||
theorem lift_StateT [WP m ps] [Monad m] (x : m α) :
|
||||
wp⟦StateT.lift x : StateT σ m α⟧ Q = wp⟦MonadLift.monadLift x : StateT σ m α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem lift_ExceptT [WP m ps] [Monad m] (x : m α) :
|
||||
wp⟦ExceptT.lift x : ExceptT ε m α⟧ Q = wp⟦MonadLift.monadLift x : ExceptT ε m α⟧ Q := rfl
|
||||
|
||||
|
||||
-- MonadReader
|
||||
|
||||
@[simp]
|
||||
theorem read_MonadReaderOf [MonadReaderOf ρ m] [MonadLift m n] [WP n _] :
|
||||
wp⟦MonadReaderOf.read : n ρ⟧ Q = wp⟦MonadLift.monadLift (MonadReader.read : m ρ) : n ρ⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem readThe [MonadReaderOf ρ m] [WP m ps] :
|
||||
wp⟦readThe ρ : m ρ⟧ Q = wp⟦MonadReaderOf.read : m ρ⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem read_MonadReader [MonadReaderOf ρ m] [WP m ps] :
|
||||
wp⟦MonadReader.read : m ρ⟧ Q = wp⟦MonadReaderOf.read : m ρ⟧ Q := rfl
|
||||
|
||||
-- MonadState
|
||||
|
||||
@[simp]
|
||||
theorem get_MonadStateOf [MonadStateOf σ m] [MonadLift m n] [WP n _] :
|
||||
wp⟦MonadStateOf.get : n σ⟧ Q = wp⟦MonadLift.monadLift (MonadStateOf.get : m σ) : n σ⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem get_MonadState [WP m ps] [MonadStateOf σ m] :
|
||||
wp⟦MonadState.get : m σ⟧ Q = wp⟦MonadStateOf.get : m σ⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem getThe_MonadStateOf [WP m ps] [MonadStateOf σ m] :
|
||||
wp⟦getThe σ : m σ⟧ Q = wp⟦MonadStateOf.get : m σ⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem set_MonadStateOf [MonadStateOf σ m] [MonadLift m n] [WP n _] :
|
||||
wp⟦MonadStateOf.set x : n PUnit⟧ Q = wp⟦MonadLift.monadLift (MonadStateOf.set (σ:=σ) x : m PUnit) : n PUnit⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem set_MonadState [WP m ps] [MonadStateOf σ m] :
|
||||
wp⟦MonadState.set x : m PUnit⟧ Q = wp⟦MonadStateOf.set x : m PUnit⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem modifyGet_MonadStateOf [MonadStateOf σ m] [MonadLift m n] [WP n _]
|
||||
(f : σ → α × σ) :
|
||||
wp⟦MonadStateOf.modifyGet f : n α⟧ Q = wp⟦MonadLift.monadLift (MonadState.modifyGet f : m α) : n α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem modifyGet_MonadState [WP m ps] [MonadStateOf σ m] (f : σ → α × σ) :
|
||||
wp⟦MonadState.modifyGet f : m α⟧ Q = wp⟦MonadStateOf.modifyGet f : m α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem modifyGetThe_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → α × σ) :
|
||||
wp⟦modifyGetThe σ f : m α⟧ Q = wp⟦MonadStateOf.modifyGet f : m α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem modify_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → σ) :
|
||||
wp⟦modify f : m PUnit⟧ Q = wp⟦MonadStateOf.modifyGet fun s => ((), f s) : m PUnit⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem modifyThe_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → σ) :
|
||||
wp⟦modifyThe σ f : m PUnit⟧ Q = wp⟦MonadStateOf.modifyGet fun s => ((), f s) : m PUnit⟧ Q := rfl
|
||||
|
||||
-- instances
|
||||
|
||||
@[simp]
|
||||
theorem read_ReaderT [Monad m] [WPMonad m ps] :
|
||||
wp⟦MonadReaderOf.read : ReaderT ρ m ρ⟧ Q = fun r => Q.1 r r := by
|
||||
simp [wp, MonadReaderOf.read, ReaderT.read]
|
||||
|
||||
@[simp]
|
||||
theorem get_StateT [Monad m] [WPMonad m ps] :
|
||||
wp⟦MonadStateOf.get : StateT σ m σ⟧ Q = fun s => Q.1 s s := by
|
||||
simp [wp, MonadStateOf.get, StateT.get]
|
||||
|
||||
@[simp]
|
||||
theorem set_StateT [Monad m] [WPMonad m ps] (x : σ) :
|
||||
wp⟦MonadStateOf.set x : StateT σ m PUnit⟧ Q = fun _ => Q.1 ⟨⟩ x := by
|
||||
simp [wp, set, StateT.set]
|
||||
|
||||
@[simp]
|
||||
theorem modifyGet_StateT [Monad m] [WPMonad m ps] (f : σ → α × σ) :
|
||||
wp⟦MonadStateOf.modifyGet f : StateT σ m α⟧ Q = fun s => Q.1 (f s).1 (f s).2 := by
|
||||
simp [wp, MonadStateOf.modifyGet, StateT.modifyGet]
|
||||
|
||||
@[simp]
|
||||
theorem get_EStateM :
|
||||
wp⟦MonadStateOf.get : EStateM ε σ σ⟧ Q = fun s => Q.1 s s := by
|
||||
simp [wp, MonadStateOf.get, EStateM.get]
|
||||
|
||||
@[simp]
|
||||
theorem set_EStateM (x : σ) :
|
||||
wp⟦MonadStateOf.set x : EStateM ε σ PUnit⟧ Q = fun _ => Q.1 ⟨⟩ x := by
|
||||
simp [wp, set, EStateM.set]
|
||||
|
||||
@[simp]
|
||||
theorem modifyGet_EStateM (f : σ → α × σ) :
|
||||
wp⟦MonadStateOf.modifyGet f : EStateM ε σ α⟧ Q = fun s => Q.1 (f s).1 (f s).2 := by
|
||||
simp [wp, MonadStateOf.modifyGet, EStateM.modifyGet]
|
||||
|
||||
end MonadLift
|
||||
|
||||
/-! ## `MonadFunctor`
|
||||
|
||||
The definitions that follow interpret `monadMap` and thus instances of, e.g., `MonadReaderWithOf`.
|
||||
|
||||
-/
|
||||
|
||||
section MonadFunctor
|
||||
|
||||
open MonadFunctor renaming monadMap → mmap
|
||||
|
||||
-- The following 3 theorems are analogous to *.monadLift_apply.
|
||||
-- In the past, we experimented with a more tricky definition by rewriting to special monadMap defns on PredTrans, involving
|
||||
-- wp1 : (∀ {α}, m α → m α) → PredTrans ps α → PredTrans ps α
|
||||
-- that enjoys quite a tricky definition.
|
||||
-- However, we found that relying on specialised lemmas is both much simpler and more reliable.
|
||||
@[simp]
|
||||
theorem monadMap_StateT (m : Type → Type u) [Monad m] [WP m ps]
|
||||
(f : ∀{β}, m β → m β) {α} (x : StateT σ m α) (Q : PostCond α (.arg σ ps)) :
|
||||
wp⟦mmap (m:=m) f x⟧ Q = fun s => wp⟦f (x.run s)⟧ (fun (a, s) => Q.1 a s, Q.2) := by
|
||||
simp [wp, MonadFunctor.monadMap, StateT.run]
|
||||
|
||||
@[simp]
|
||||
theorem monadMap_ReaderT (m : Type → Type u) [Monad m] [WP m ps]
|
||||
(f : ∀{β}, m β → m β) {α} (x : ReaderT ρ m α) (Q : PostCond α (.arg ρ ps)) :
|
||||
wp⟦mmap (m:=m) f x⟧ Q = fun s => wp⟦f (x.run s)⟧ (fun a => Q.1 a s, Q.2) := by
|
||||
simp [wp, MonadFunctor.monadMap, ReaderT.run]
|
||||
|
||||
@[simp]
|
||||
theorem monadMap_ExceptT (m : Type → Type u) [Monad m] [WP m ps]
|
||||
(f : ∀{β}, m β → m β) {α} (x : ExceptT ε m α) (Q : PostCond α (.except ε ps)) :
|
||||
wp⟦mmap (m:=m) f x⟧ Q = wp⟦f x.run⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
|
||||
simp [wp, MonadFunctor.monadMap, ExceptT.run]
|
||||
congr; ext; split <;> rfl
|
||||
|
||||
@[simp]
|
||||
theorem monadMap_trans [WP o ps] [MonadFunctor n o] [MonadFunctorT m n] :
|
||||
wp⟦MonadFunctorT.monadMap f x : o α⟧ Q = wp⟦MonadFunctor.monadMap (m:=n) (MonadFunctorT.monadMap (m:=m) f) x : o α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem monadMap_refl [WP m ps] :
|
||||
wp⟦MonadFunctorT.monadMap f x : m α⟧ Q = wp⟦f x : m α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem withReader_ReaderT [WP m ps] :
|
||||
wp⟦MonadWithReaderOf.withReader f x : ReaderT ρ m α⟧ Q = fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r) := rfl
|
||||
|
||||
@[simp]
|
||||
theorem withReader_MonadWithReaderOf [MonadWithReaderOf ρ m] [WP n nsh] [MonadFunctor m n] (f : ρ → ρ) (x : n α) :
|
||||
wp⟦MonadWithReaderOf.withReader f x⟧ Q = wp⟦mmap (m:=m) (MonadWithReaderOf.withReader f) x⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem withReader_MonadWithReader [MonadWithReaderOf ρ m] [WP m ps] (f : ρ → ρ) (x : m α) :
|
||||
wp⟦MonadWithReader.withReader f x⟧ Q = wp⟦MonadWithReaderOf.withReader f x⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem withTheReader [MonadWithReaderOf ρ m] [WP m ps] (f : ρ → ρ) (x : m α) :
|
||||
wp⟦withTheReader ρ f x⟧ Q = wp⟦MonadWithReaderOf.withReader f x⟧ Q := rfl
|
||||
|
||||
end MonadFunctor
|
||||
|
||||
/-! ## `MonadExceptOf`
|
||||
|
||||
The definitions that follow interpret `throw`, `throwThe`, `tryCatch`, etc.
|
||||
|
||||
Since `MonadExceptOf` cannot be lifted through `MonadLift` or `MonadFunctor`, there is one lemma per
|
||||
`MonadExceptOf` operation and instance to lift through; the classic m*n instances problem.
|
||||
|
||||
-/
|
||||
|
||||
section MonadExceptOf
|
||||
|
||||
@[simp]
|
||||
theorem throw_MonadExcept [MonadExceptOf ε m] [WP m ps] :
|
||||
wp⟦throw e : m α⟧ Q = wp⟦MonadExceptOf.throw e : m α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem throwThe [MonadExceptOf ε m] [WP m ps] :
|
||||
wp⟦throwThe ε e : m α⟧ Q = wp⟦MonadExceptOf.throw e : m α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem throw_Except :
|
||||
wp⟦MonadExceptOf.throw e : Except ε α⟧ Q = Q.2.1 e := by
|
||||
simp [wp, MonadExceptOf.throw, Id.run]
|
||||
|
||||
@[simp]
|
||||
theorem throw_ExceptT [Monad m] [WPMonad m ps] :
|
||||
wp⟦MonadExceptOf.throw e : ExceptT ε m α⟧ Q = Q.2.1 e := by
|
||||
simp [wp, MonadExceptOf.throw, ExceptT.mk]
|
||||
|
||||
@[simp]
|
||||
theorem throw_EStateM :
|
||||
wp⟦MonadExceptOf.throw e : EStateM ε σ α⟧ Q = Q.2.1 e := by
|
||||
simp [wp, MonadExceptOf.throw, EStateM.throw]
|
||||
|
||||
@[simp]
|
||||
theorem throw_ReaderT [WP m sh] [Monad m] [MonadExceptOf ε m] :
|
||||
wp⟦MonadExceptOf.throw (ε:=ε) e : ReaderT ρ m α⟧ Q = wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : ReaderT ρ m α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem throw_StateT [WP m sh] [Monad m] [MonadExceptOf ε m] :
|
||||
wp⟦MonadExceptOf.throw (ε:=ε) e : StateT ρ m α⟧ Q = wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : StateT ρ m α⟧ Q := rfl
|
||||
|
||||
-- The following lemma is structurally different to StateT and others because of weird definitions
|
||||
-- for lifting throw
|
||||
@[simp]
|
||||
theorem throw_lift_ExceptT [WP m sh] [Monad m] [MonadExceptOf ε m] :
|
||||
wp⟦MonadExceptOf.throw (ε:=ε) e : ExceptT ε' m α⟧ Q = wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
|
||||
simp only [wp, MonadExceptOf.throw, PredTrans.pushExcept_apply]
|
||||
congr
|
||||
ext x
|
||||
split <;> rfl
|
||||
|
||||
@[simp]
|
||||
theorem tryCatch_MonadExcept [MonadExceptOf ε m] [WP m ps] :
|
||||
wp⟦tryCatch x h : m α⟧ Q = wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem tryCatchThe [MonadExceptOf ε m] [WP m ps] :
|
||||
wp⟦tryCatchThe ε x h : m α⟧ Q = wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem tryCatch_Except :
|
||||
wp⟦MonadExceptOf.tryCatch x h : Except ε α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by
|
||||
simp only [wp, PredTrans.pure, Id.run, MonadExceptOf.tryCatch, Except.tryCatch,
|
||||
PredTrans.pushExcept_apply]
|
||||
cases x <;> simp
|
||||
|
||||
@[simp]
|
||||
theorem tryCatch_ExceptT [Monad m] [WPMonad m ps] :
|
||||
wp⟦MonadExceptOf.tryCatch x h : ExceptT ε m α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by
|
||||
simp only [wp, MonadExceptOf.tryCatch, ExceptT.tryCatch, ExceptT.mk, bind, PredTrans.pushExcept_apply]
|
||||
congr
|
||||
ext x
|
||||
split <;> simp
|
||||
|
||||
open EStateM.Backtrackable in
|
||||
@[simp]
|
||||
theorem tryCatch_EStateM {ε σ δ α x h Q} [EStateM.Backtrackable δ σ]:
|
||||
wp⟦MonadExceptOf.tryCatch x h : EStateM ε σ α⟧ Q = fun s => wp⟦x⟧ (Q.1, fun e s' => wp⟦h e⟧ Q (restore s' (save s)), Q.2.2) s := by
|
||||
ext s
|
||||
simp only [wp, MonadExceptOf.tryCatch, EStateM.tryCatch]
|
||||
cases x s <;> simp
|
||||
|
||||
@[simp]
|
||||
theorem tryCatch_ReaderT [WP m sh] [Monad m] [MonadExceptOf ε m] :
|
||||
wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : ReaderT ρ m α⟧ Q = fun r => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run r) (fun e => (h e).run r) : m α⟧ (fun a => Q.1 a r, Q.2) := by
|
||||
simp [wp, MonadExceptOf.tryCatch, tryCatchThe, ReaderT.run]
|
||||
|
||||
@[simp]
|
||||
theorem tryCatch_StateT [WP m sh] [Monad m] [MonadExceptOf ε m] :
|
||||
wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : StateT σ m α⟧ Q = 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) := by
|
||||
simp [wp, MonadExceptOf.tryCatch, tryCatchThe, StateT.run]
|
||||
|
||||
@[simp]
|
||||
theorem tryCatch_lift_ExceptT [WP m sh] [Monad m] [MonadExceptOf ε m] :
|
||||
wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : ExceptT ε' m α⟧ Q = wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by
|
||||
simp only [wp, MonadExceptOf.tryCatch, tryCatchThe, PredTrans.pushExcept_apply, ExceptT.mk]
|
||||
congr
|
||||
ext x
|
||||
split <;> rfl
|
||||
|
||||
/-
|
||||
example :
|
||||
wp (m:= ReaderT Char (StateT Bool (ExceptT Nat Id))) (do set true; throw 42; set false; get) =
|
||||
wp (m:= ReaderT Char (StateT Bool (ExceptT Nat Id))) (do set true; throw 42; get) := by
|
||||
ext Q : 4
|
||||
simp
|
||||
|
||||
example :
|
||||
wp (m:= ReaderT Char (StateT Bool (ExceptT Nat Id))) (do try { set true; throw 42 } catch _ => set false; get) =
|
||||
wp (m:= ReaderT Char (StateT Bool (ExceptT Nat Id))) (do set false; get) := by
|
||||
ext Q : 4
|
||||
simp
|
||||
-- This gets stuck because ExceptT.instMonad is not defeq to Except.instMonad and thus the `bind` rewrite does not apply.
|
||||
admit
|
||||
-/
|
||||
|
||||
end MonadExceptOf
|
||||
|
|
@ -6,7 +6,25 @@ Authors: Sebastian Graf
|
|||
prelude
|
||||
import Init.NotationExtra
|
||||
|
||||
namespace Lean.Parser.Tactic
|
||||
|
||||
namespace Lean.Parser
|
||||
|
||||
namespace Attr
|
||||
|
||||
/--
|
||||
Theorems tagged with the `spec` attribute are used by the `mspec` and `mvcgen` tactics.
|
||||
|
||||
* When used on a theorem `foo_spec : Triple (foo a b c) P Q`, then `mspec` and `mvcgen` will use
|
||||
`foo_spec` as a specification for calls to `foo`.
|
||||
* Otherwise, when used on a definition that `@[simp]` would work on, it is added to the internal
|
||||
simp set of `mvcgen` that is used within `wp⟦·⟧` contexts to simplify match discriminants and
|
||||
applications of constants.
|
||||
-/
|
||||
syntax (name := specAttr) "spec" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
|
||||
|
||||
end Attr
|
||||
|
||||
namespace Tactic
|
||||
|
||||
@[inherit_doc Lean.Parser.Tactic.massumptionMacro]
|
||||
syntax (name := massumption) "massumption" : tactic
|
||||
|
|
@ -152,3 +170,46 @@ syntax "∀" binderIdent : mintroPat
|
|||
|
||||
@[inherit_doc Lean.Parser.Tactic.mintroMacro]
|
||||
syntax (name := mintro) "mintro" (ppSpace colGt mintroPat)+ : tactic
|
||||
|
||||
@[inherit_doc Lean.Parser.Tactic.mspecMacro]
|
||||
syntax (name := mspec) "mspec" (ppSpace colGt term)? : tactic
|
||||
|
||||
/--
|
||||
Like `mspec`, but does not attempt slight simplification and closing of trivial sub-goals.
|
||||
`mspec $spec` is roughly (the set of simp lemmas below might not be up to date)
|
||||
```
|
||||
mspec_no_simp $spec
|
||||
all_goals
|
||||
((try simp only [SPred.true_intro_simp, SPred.true_intro_simp_nil, SVal.curry_cons,
|
||||
SVal.uncurry_cons, SVal.getThe_here, SVal.getThe_there]);
|
||||
(try mpure_intro; trivial))
|
||||
```
|
||||
-/
|
||||
syntax (name := mspecNoSimp) "mspec_no_simp" (ppSpace colGt term)? : tactic
|
||||
|
||||
/--
|
||||
`mspec_no_simp $spec` first tries to decompose `Bind.bind`s before applying `$spec`.
|
||||
This variant of `mspec_no_simp` does not; `mspec_no_bind $spec` is defined as
|
||||
```
|
||||
try with_reducible mspec_no_bind Std.Do.Spec.bind
|
||||
mspec_no_bind $spec
|
||||
```
|
||||
-/
|
||||
syntax (name := mspecNoBind) "mspec_no_bind" (ppSpace colGt term)? : tactic
|
||||
|
||||
@[inherit_doc Lean.Parser.Tactic.mvcgenMacro]
|
||||
syntax (name := mvcgen) "mvcgen" optConfig
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
|
||||
|
||||
/--
|
||||
Like `mvcgen`, but does not attempt to prove trivial VCs via `mpure_intro; trivial`.
|
||||
-/
|
||||
syntax (name := mvcgenNoTrivial) "mvcgen_no_trivial" optConfig
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
|
||||
|
||||
/--
|
||||
Like `mvcgen_no_trivial`, but `mvcgen_step 42` will only do 42 steps of the VC generation procedure.
|
||||
This is helpful for bisecting bugs in `mvcgen` and tracing its execution.
|
||||
-/
|
||||
syntax (name := mvcgenStep) "mvcgen_step" optConfig
|
||||
(num)? (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue