feat: concrete invariant? suggestions based on start and end (#10566)
This PR improves `mvcgen invariants?` to suggest concrete invariants
based on how invariants are used in VCs.
These suggestions are intentionally simplistic and boil down to "this
holds at the start of the loop and this must hold at the end of the
loop":
```lean
def mySum (l : List Nat) : Nat := Id.run do
let mut acc := 0
for x in l do
acc := acc + x
return acc
/--
info: Try this:
invariants
· ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
-/
#guard_msgs (info) in
theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
generalize h : mySum l = r
apply Id.of_wp_run_eq h
mvcgen invariants?
all_goals admit
```
It still is the user's job to weaken this invariant such that it
interpolates over all loop iterations, but it *is* a good starting point
for iterating. It is also useful because the user does not need to
remember the exact syntax.
This commit is contained in:
Sebastian Graf
GitHub
parent
e6dd41255b
commit
71e09ca883
4 changed files with 639 additions and 105 deletions
|
|
@ -2176,6 +2176,8 @@ macro (name := mspecMacro) (priority:=low) "mspec" : tactic =>
|
|||
`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]`.
|
||||
|
||||
### Verification Conditions and specifications
|
||||
|
||||
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
|
||||
|
|
@ -2183,6 +2185,8 @@ 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]`.
|
||||
|
||||
### Features
|
||||
|
||||
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
|
||||
|
|
@ -2191,11 +2195,59 @@ When used like `mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat]`, `mvcgen` w
|
|||
* 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.
|
||||
### Config options
|
||||
|
||||
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.
|
||||
`+noLetElim` is just one config option of many. Check out `Lean.Elab.Tactic.Do.VCGen.Config` for all
|
||||
options. Of particular note is `stepLimit = some 42`, which is useful for bisecting bugs in
|
||||
`mvcgen` and tracing its execution.
|
||||
|
||||
### Extended syntax
|
||||
|
||||
Often, `mvcgen` will be used like this:
|
||||
```
|
||||
mvcgen [...]
|
||||
case inv1 => by exact I1
|
||||
case inv2 => by exact I2
|
||||
all_goals (mleave; try grind)
|
||||
```
|
||||
There is special syntax for this:
|
||||
```
|
||||
mvcgen [...] invariants
|
||||
· I1
|
||||
· I2
|
||||
with grind
|
||||
```
|
||||
|
||||
### Invariant suggestions
|
||||
|
||||
`mvcgen` will suggest invariants for you if you use the `invariants?` keyword.
|
||||
```
|
||||
mvcgen [...] invariants?
|
||||
```
|
||||
This is useful if you do not recall the exact syntax to construct invariants.
|
||||
Furthermore, it will suggest a concrete invariant encoding "this holds at the start of the loop and
|
||||
this must hold at the end of the loop" by looking at the corresponding VCs.
|
||||
Although the suggested invariant is a good starting point, it is too strong and requires users to
|
||||
interpolate it such that the inductive step can be proved. Example:
|
||||
```
|
||||
def mySum (l : List Nat) : Nat := Id.run do
|
||||
let mut acc := 0
|
||||
for x in l do
|
||||
acc := acc + x
|
||||
return acc
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
|
||||
generalize h : mySum l = r
|
||||
apply Id.of_wp_run_eq h
|
||||
mvcgen invariants?
|
||||
all_goals admit
|
||||
```
|
||||
-/
|
||||
macro (name := mvcgenMacro) (priority:=low) "mvcgen" : tactic =>
|
||||
Macro.throwError "to use `mvcgen`, please include `import Std.Tactic.Do`"
|
||||
|
|
|
|||
|
|
@ -7,47 +7,113 @@ module
|
|||
|
||||
prelude
|
||||
public import Lean.Elab.Tactic.Basic
|
||||
public import Lean.Meta.Tactic.Simp.Types
|
||||
import Lean.Meta.Tactic.Simp.Rewrite
|
||||
import Lean.Meta.Tactic.Simp.Main
|
||||
import Lean.Util.OccursCheck
|
||||
import Lean.PrettyPrinter.Delaborator
|
||||
import Lean.Elab.Tactic.Do.ProofMode.MGoal
|
||||
import Lean.Util.CollectFVars
|
||||
import Std.Do.Triple
|
||||
import Std.Tactic.Do -- Needed for use of `mleave` in quote
|
||||
|
||||
public section
|
||||
|
||||
namespace Lean.Elab.Tactic.Do
|
||||
|
||||
open Lean Elab Tactic Meta
|
||||
open Lean Elab Tactic Meta ProofMode
|
||||
open Std.Do
|
||||
|
||||
private def duplicateMVar (m : MVarId) : MetaM MVarId := do
|
||||
let d ← m.getDecl
|
||||
let e ← mkFreshExprMVarAt d.lctx d.localInstances d.type d.kind d.userName d.numScopeArgs
|
||||
return e.mvarId!
|
||||
/--
|
||||
If the target of `vc` looks like `(H ⊢ₛ T) args`, return `H args` and `T args`.
|
||||
If the target looks like `ULift.down (T args)`, then this is likely a result of `mframe` and
|
||||
`mleave`. In this case, the last decl in the local context of `vc` will look like
|
||||
`ULift.down (H args)`. Then return `H args` and `T args`.
|
||||
|
||||
private def eraseMacroScopesFromSyntax : Syntax → Syntax
|
||||
| Syntax.ident info rawVal val preresolved =>
|
||||
Syntax.ident info rawVal val.eraseMacroScopes preresolved
|
||||
| Syntax.node info kind args =>
|
||||
Syntax.node info kind (args.map eraseMacroScopesFromSyntax)
|
||||
| Syntax.atom info val => Syntax.atom info val
|
||||
| Syntax.missing => Syntax.missing
|
||||
This means that both `H args` and `T args` have type `SPred []`.
|
||||
-/
|
||||
def getSPredGoalHypsAndTarget (type : Expr) : MetaM (Option (Level × Expr × Expr)) := do
|
||||
let args := type.getAppArgs
|
||||
if (type.isAppOf ``Std.Tactic.Do.MGoalEntails || type.isAppOf ``SPred.entails) && args.size > 2 then
|
||||
return (type.getAppFn.constLevels![0]!, (type.getArg! 1).beta args[3:], (type.getArg! 2).beta args[3:])
|
||||
let some decl := (← getLCtx).lastDecl | return none
|
||||
let hyps := decl.type.consumeMData
|
||||
let lvl := (getULiftDownLevel type <|> getULiftDownLevel hyps).getD .zero
|
||||
-- logWarning m!"getSPredGoalHypsAndTarget: {hyps} ⊢ₛ {type}"
|
||||
return (lvl, toAssertion lvl hyps, toAssertion lvl type)
|
||||
where
|
||||
getULiftDownLevel (expr : Expr) : Option Level :=
|
||||
if expr.isAppOfArity ``ULift.down 2 then some expr.getAppFn.constLevels![0]! else none
|
||||
toAssertion (lvl : Level) (prop : Expr) : Expr :=
|
||||
if prop.isAppOfArity ``ULift.down 2 then
|
||||
prop.getArg! 1
|
||||
else
|
||||
SPred.mkPure lvl (TypeList.mkNil lvl) prop
|
||||
|
||||
private def eraseMacroScopesFromTSyntax (syn : TSyntax name) : TSyntax name :=
|
||||
⟨eraseMacroScopesFromSyntax syn.raw⟩
|
||||
structure InvariantUse where
|
||||
/-- Index 0 is the success condition, all the others are exception conditions. -/
|
||||
conditionIdx : Nat
|
||||
/-- The prefix expression of the call to `Cursor.mk`. -/
|
||||
cursorPrefix : Expr
|
||||
/-- The suffix expression of the call to `Cursor.mk`. -/
|
||||
cursorSuffix : Expr
|
||||
/-- The argument expressions of the `let mut` variables. -/
|
||||
letMuts : Array Expr
|
||||
letMutsTuple : Expr
|
||||
stateArgs : Array Expr
|
||||
|
||||
inductive ClassifyInvariantUseResult where
|
||||
| success (invariantUse : InvariantUse)
|
||||
| notAnInvariantUse
|
||||
| unknownInvariantUse
|
||||
|
||||
def classifyInvariantUse (assertion : Expr) (inv : MVarId) : ClassifyInvariantUseResult := Id.run do
|
||||
-- Looking through metadata here is important because of the name hints the proof mode leaves behind
|
||||
let assertion := assertion.consumeMData
|
||||
-- `assertion` looks like `?inv.2.2....1 payload args`. The number of `2`s is the condition index.
|
||||
-- The 0 index case is the success condition case and by far the most common.
|
||||
-- There we have `assertion = ?inv.1 payload args`.
|
||||
-- The chain of `.2.2...1` is normalized to nested applications of `Prod.fst` and `Prod.snd`:
|
||||
-- `@Prod.fst _ _ (@Prod.snd _ _ (@Prod.snd _ _ ... ?inv)) payload args`
|
||||
if !assertion.isAppOf ``Prod.fst then return .notAnInvariantUse
|
||||
let mut head := assertion.getArg! 2 -- indices 0 and 1 are type args
|
||||
let mut conditionIdx := 0
|
||||
while head != mkMVar inv do
|
||||
if !head.isAppOfArity ``Prod.snd 4 then return .notAnInvariantUse -- cannot classify as a use of the invariant!
|
||||
conditionIdx := conditionIdx + 1
|
||||
head := head.getRevArg! 1
|
||||
-- `head` is ?inv => Found the end of the chain.
|
||||
-- conditionIdx is the number of `Prod.snd`s in the chain, and ?inv really is the end of the chain.
|
||||
|
||||
let args := assertion.getAppArgs
|
||||
-- logWarning m!"Found Prod.fst. Args: {args}"
|
||||
if args.size < 4 then return .notAnInvariantUse -- not an overapplication of `Prod.fst`. Types should prohibit this case
|
||||
let payload := args[3]!
|
||||
let stateArgs := args[4:]
|
||||
-- `stateArgs` can be non-empty when `σs` is non-empty.
|
||||
-- logWarning m!"Payload: {payload}"
|
||||
|
||||
let_expr Prod.mk _ _ cursor letMutsTuple := payload | return .unknownInvariantUse -- NB: be conservative here
|
||||
let_expr List.Cursor.mk _α _l pref suff _prf := cursor | return .unknownInvariantUse -- dito
|
||||
let mut acc := letMutsTuple
|
||||
let mut letMuts := #[]
|
||||
while acc.isAppOfArity ``MProd.mk 4 do
|
||||
letMuts := letMuts.push (acc.getArg! 2)
|
||||
acc := acc.getArg! 3
|
||||
letMuts := letMuts.push acc
|
||||
return .success { conditionIdx, cursorPrefix := pref, cursorSuffix := suff, letMuts, letMutsTuple, stateArgs }
|
||||
|
||||
/--
|
||||
Returns `some (ρ, σ)` if `doStateTupleTy` is of the form `MProd (Option ρ) σ` and every VC in `vcs`
|
||||
Returns `some (ρ, σ)` if `letMutsTy` is of the form `MProd (Option ρ) σ` and every VC in `vcs`
|
||||
uses the `Option ρ` component according to early return semantics.
|
||||
* `ρ` is the type of early return (`Unit` in case of `break`)
|
||||
* `σ` is an `n`-ary `MProd`, carrying the current value of the `let mut` variables.
|
||||
NB: When `n=0`, we have `MProd (Option ρ) PUnit` rather than `Option ρ`.
|
||||
-/
|
||||
private def hasEarlyReturn (vcs : Array MVarId) (inv : MVarId) (doStateTupleTy : Expr) : MetaM (Option (Expr × Expr)) := do
|
||||
if !(doStateTupleTy.isAppOf ``MProd) || doStateTupleTy.getAppNumArgs < 2 then return none
|
||||
let_expr Option ρ := doStateTupleTy.getArg! 0 | return none
|
||||
let σ := doStateTupleTy.getArg! 1
|
||||
def hasEarlyReturn (vcs : Array MVarId) (inv : MVarId) (letMutsTy : Expr) : MetaM (Option (Expr × Expr)) := do
|
||||
if !(letMutsTy.isAppOf ``MProd) || letMutsTy.getAppNumArgs < 2 then return none
|
||||
let_expr Option ρ := letMutsTy.getArg! 0 | return none
|
||||
let σ := letMutsTy.getArg! 1
|
||||
|
||||
-- The predicate on `doStateTupleTy` above is not sufficient; after all the user might just have
|
||||
-- The predicate on `letMutsTy` above is not sufficient; after all the user might just have
|
||||
-- introduced `let mut ret : Option α` and not use this variable according to "early return
|
||||
-- semantics", meaning that *if* `ret = some r` for some `r : ρ`, then the loop body returns
|
||||
-- `ForInStep.done (ret, ...)`. This is a property upheld by the `do` elaborator.
|
||||
|
|
@ -78,69 +144,334 @@ private def hasEarlyReturn (vcs : Array MVarId) (inv : MVarId) (doStateTupleTy :
|
|||
-- Hence we check all VCs for the property above.
|
||||
|
||||
for vc in vcs do
|
||||
-- No point in traversing the VC if the invariant is not used in it.
|
||||
let type ← instantiateMVars (← vc.getType)
|
||||
if ← occursCheck inv type then continue
|
||||
-- log m!"Looking at {vc}."
|
||||
let some spredTarget :=
|
||||
if type.isAppOf ``ULift.down && type.getAppNumArgs > 1 then some (type.getArg! 1)
|
||||
else if type.isAppOf ``Std.Tactic.Do.MGoalEntails && type.getAppNumArgs > 2 then some (type.getArg! 2)
|
||||
else if type.isAppOf ``SPred.entails && type.getAppNumArgs > 2 then some (type.getArg! 2)
|
||||
else none
|
||||
| continue
|
||||
-- `spredTarget` should be an overapplication of `Prod.fst`: `spredTarget = Prod.fst ?inv payload args`
|
||||
-- `args` can be non-empty when `σs` is non-empty.
|
||||
if !spredTarget.isAppOf ``Prod.fst then continue
|
||||
let args := spredTarget.getAppArgs
|
||||
-- log m!"Found Prod.fst. Args: {args}"
|
||||
if args.size < 4 then continue -- not an overapplication. Types should prohibit this case
|
||||
if args[2]! != mkMVar inv then continue -- not ?inv that is applied
|
||||
let payload := args[3]!
|
||||
-- log m!"Payload: {payload}"
|
||||
|
||||
let_expr Prod.mk _ _ cursor acc := payload | return none -- NB: be conservative here
|
||||
let_expr List.Cursor.mk _α _l _pref suff _prop := cursor | return none -- dito
|
||||
-- logWarning m!"Looking at {vc}."
|
||||
let type ← Expr.consumeMData <$> instantiateMVars (← vc.getType)
|
||||
let some (_, _, spredTarget) ← vc.withContext <| getSPredGoalHypsAndTarget type | continue
|
||||
-- logWarning m!"Found spredTarget: {spredTarget}"
|
||||
match classifyInvariantUse spredTarget inv with
|
||||
| .notAnInvariantUse => continue
|
||||
| .unknownInvariantUse => return none -- conservative
|
||||
| .success invariantUse =>
|
||||
-- logWarning m!"Invariant use: {invariantUse.letMuts}"
|
||||
-- The following check could be smarter. Essentially it tries to construct a proof that
|
||||
-- `suff = []` or `acc = (none, _)` and returns `none` upon failure.
|
||||
if !suff.isAppOf ``List.nil && !(acc.isAppOf ``MProd.mk && (acc.getArg! 2 |>.isAppOf ``Option.none)) then
|
||||
-- log m!"No early return! Not a `List.nil`: {suff} and not an `Option.none`: {acc.getArg! 2}"
|
||||
-- NB: There always is at least one `invariantUse.letMuts`.
|
||||
if !invariantUse.cursorSuffix.isAppOf ``List.nil && !invariantUse.letMuts[0]!.isAppOf ``Option.none then
|
||||
-- logWarning m!"No early return! Not a `List.nil`: {invariantUse.cursorSuffix} and not an `Option.none`: {invariantUse.letMuts[0]!}"
|
||||
return none
|
||||
|
||||
return (ρ, σ)
|
||||
|
||||
/-- Largely lifted from `Lean.MetavarContext.MkBinding.mkAuxMVarType`. -/
|
||||
def revertFVarsInTypeExcept (e : Expr) (dontRevert : FVarId → Bool) : MetaM Expr := do
|
||||
let xs := (collectFVars {} e).fvarIds
|
||||
|>.filter (not ∘ dontRevert)
|
||||
|>.map mkFVar
|
||||
let xs ← collectForwardDeps xs false
|
||||
let lctx ← getLCtx
|
||||
let_expr c@SPred _σs := (← inferType e) | return e
|
||||
let lvl := c.constLevels![0]!
|
||||
-- logWarning m!"Reverting {xs} in {e}, {lvl}"
|
||||
let e ← xs.size.foldRevM (init := e.abstract xs) fun i _ e => do
|
||||
let x := xs[i]
|
||||
match lctx.getFVar! x with
|
||||
| LocalDecl.cdecl _ _ n type bi _ =>
|
||||
let type := type.headBeta
|
||||
let type := type.abstractRange i xs
|
||||
return mkApp3 (mkConst ``SPred.forall [← getLevel type, lvl]) type (TypeList.mkNil lvl) (Lean.mkLambda n bi type e)
|
||||
| LocalDecl.ldecl (nondep := true) _ _ n type _ _ =>
|
||||
let type := type.headBeta
|
||||
let type := type.abstractRange i xs
|
||||
return mkApp3 (mkConst ``SPred.forall [← getLevel type, lvl]) type (TypeList.mkNil lvl) (Lean.mkLambda n .default type e)
|
||||
| LocalDecl.ldecl (nondep := false) _ _ n type value _ =>
|
||||
if e.hasLooseBVar 0 then
|
||||
let type := type.headBeta
|
||||
let type := type.abstractRange i xs
|
||||
let value := value.abstractRange i xs
|
||||
return mkLet n type value e false
|
||||
else
|
||||
return e.lowerLooseBVars 1 1
|
||||
return e
|
||||
|
||||
structure SuccessPoint where
|
||||
/-- The level of the `SPred` state tuple. -/
|
||||
lvl : Level
|
||||
/-- An `SPred` like `⌜xs.prefix = []⌝` or `⌜xs.suffix = []⌝`. -/
|
||||
cursorPred : Expr
|
||||
/-- An arbitrary `SPred` on `letMuts`. -/
|
||||
letMutsPred : Expr
|
||||
|
||||
def SPredNil.mkAnd (lvl : Level) (lhs rhs : Expr) : Expr :=
|
||||
mkApp3 (mkConst ``SPred.and [lvl]) (TypeList.mkNil lvl) lhs rhs
|
||||
|
||||
def SPredNil.mkOr (lvl : Level) (lhs rhs : Expr) : Expr :=
|
||||
mkApp3 (mkConst ``SPred.or [lvl]) (TypeList.mkNil lvl) lhs rhs
|
||||
|
||||
def SuccessPoint.clause (p : SuccessPoint) : Expr :=
|
||||
SPredNil.mkAnd p.lvl p.cursorPred p.letMutsPred
|
||||
|
||||
/-- The last syntactic element of a `FailureCond`. -/
|
||||
inductive ExceptCondsDefault where
|
||||
/-- `()`. This means we can suggest `post⟨...⟩`. -/
|
||||
| unit
|
||||
/-- `ExceptConds.false`. This means we can suggest `⇓ _ => _`. -/
|
||||
| false
|
||||
/-- `ExceptConds.true`. This means we can suggest `⇓? _ => _`. -/
|
||||
| true
|
||||
/-- Something else. This means we can only suggest `by exact ⟨..., e⟩`. -/
|
||||
| other (e : Expr)
|
||||
|
||||
/--
|
||||
If `points[n]` is `fun e => assertion`, then the invariant should look like
|
||||
```
|
||||
post⟨... success ..., ... n except conds ..., fun e => assertion, ... other stuff ...⟩
|
||||
```
|
||||
So each entry describes a non-`False` exception condition.
|
||||
|
||||
When the default is not defeq to `ExceptConds.false`, we use it as the default.
|
||||
-/
|
||||
structure FailureCondHints where
|
||||
points : Array Expr := #[]
|
||||
default : ExceptCondsDefault := .unit
|
||||
|
||||
/-- Look at how `inv` is used in the `vcs` and collect hints about how `inv` should be instantiated.
|
||||
In case it succeeds, there will be
|
||||
* A `SuccessPoint` for the `xs.prefix = []` case
|
||||
* A `SuccessPoint` for all the `xs.suffix = []` case (control flow splits can introduce multiple
|
||||
relevant VCs)
|
||||
* A `FailureCondHints` with the default exception condition (i.e., `FailureConds.false`, `()` or
|
||||
something else?) and the non-defaulted exception conditions.
|
||||
-/
|
||||
def collectInvariantHints (vcs : Array MVarId) (inv : MVarId) (xs : Expr) (letMuts : Expr) : MetaM (Option (SuccessPoint × SuccessPoint × FailureCondHints)) := do
|
||||
let lctx ← getLCtx -- this is the local context of `inv` extended by `xs` and `letMuts`
|
||||
let mut prefixPoint? : Option SuccessPoint := none
|
||||
let mut suffixPoint? : Option SuccessPoint := none
|
||||
let mut failureConds : FailureCondHints := {}
|
||||
for vc in vcs do
|
||||
-- logWarning m!"Looking at {vc}."
|
||||
let target ← Expr.consumeMData <$> instantiateMVars (← vc.getType)
|
||||
if let some (lvl, spredHyps, spredTarget) ← vc.withContext <| getSPredGoalHypsAndTarget target then
|
||||
let mkPure p := SPred.mkPure lvl (TypeList.mkNil lvl) p
|
||||
-- vc.withContext <| logWarning m!"collectPoint: {spredHyps} ⊢ₛ {spredTarget}"
|
||||
if let .success invariantUse := classifyInvariantUse spredTarget inv then
|
||||
-- This is the `xs.prefix = []` case.
|
||||
-- vc.withContext <| logWarning m!"Invariant use: {invariantUse.letMutsTuple}"
|
||||
if invariantUse.conditionIdx != 0 then continue -- concerns the success conditions
|
||||
if invariantUse.cursorPrefix.isAppOf ``List.nil then
|
||||
-- eqNil := `(xs.prefix = [])
|
||||
let xsPrefix ← mkProjection xs `prefix
|
||||
let eqNil ← mkEq xsPrefix invariantUse.cursorPrefix
|
||||
-- eqLetMuts := `(letMuts = $(invariantUse.letMutsTuple))
|
||||
let eqLetMuts ← mkPure <$> mkEq letMuts invariantUse.letMutsTuple
|
||||
-- logWarning m!"Found prefix point: {eqLetMuts}"
|
||||
prefixPoint? := some { lvl, cursorPred := mkPure eqNil, letMutsPred := eqLetMuts }
|
||||
if let .success invariantUse := classifyInvariantUse spredHyps inv then
|
||||
-- This is a `xs.suffix = []` case.
|
||||
-- vc.withContext <| logWarning m!"Found spredHyp: {spredHyps}"
|
||||
if invariantUse.conditionIdx != 0 then continue -- concerns the success conditions
|
||||
if invariantUse.cursorSuffix.isAppOf ``List.nil && invariantUse.letMutsTuple.isFVar then
|
||||
let xsPrefix ← mkProjection xs `suffix
|
||||
let eqNil ← mkEq xsPrefix invariantUse.cursorSuffix
|
||||
let dontRevert fvarId := fvarId == invariantUse.letMutsTuple.fvarId! || lctx.contains fvarId
|
||||
let eqLetMuts ← vc.withContext <| revertFVarsInTypeExcept spredTarget dontRevert
|
||||
let eqLetMuts := eqLetMuts.replaceFVar invariantUse.letMutsTuple letMuts
|
||||
-- logWarning m!"Reverted to {eqLetMuts}"
|
||||
if let some suffixPoint := suffixPoint? then
|
||||
suffixPoint? := some { suffixPoint with letMutsPred := SPredNil.mkAnd lvl suffixPoint.letMutsPred eqLetMuts }
|
||||
else
|
||||
suffixPoint? := some { lvl, cursorPred := mkPure eqNil, letMutsPred := eqLetMuts }
|
||||
if let some (_ps, lhs, rhs) := target.app3? ``ExceptConds.entails then
|
||||
-- This is a exception condition case.
|
||||
-- logWarning m!"Found ExceptConds.entails: {lhs}, {rhs}"
|
||||
-- We are targeting `Prod.snd ?inv ⊢ₑ blah` specifically
|
||||
unless lhs.isAppOfArity ``Prod.snd 3 && lhs.getArg! 2 == mkMVar inv do continue
|
||||
let mut n := 0
|
||||
let mut conds := rhs
|
||||
let mut points := #[]
|
||||
while conds.isAppOfArity ``Prod.mk 4 do
|
||||
points := points.push (conds.getArg! 2)
|
||||
n := n + 1
|
||||
conds := conds.getArg! 3
|
||||
if points.size > failureConds.points.size then
|
||||
-- Just overwrite the existing entry. Computing a join here is overkill for the few cases
|
||||
-- where this is going to be used.
|
||||
failureConds := { failureConds with points := points }
|
||||
if conds.isConstOf ``Unit.unit then
|
||||
failureConds := { failureConds with default := .unit }
|
||||
else if conds.isAppOfArity ``ExceptConds.false 1 then
|
||||
failureConds := { failureConds with default := .false }
|
||||
else if conds.isAppOfArity ``ExceptConds.true 1 then
|
||||
failureConds := { failureConds with default := .true }
|
||||
else
|
||||
failureConds := { failureConds with default := .other conds }
|
||||
-- vc.withContext <| logWarning m!"Found failure conds: {failureConds.points.toList}"
|
||||
return (·, ·, ·) <$> prefixPoint? <*> suffixPoint? <*> pure failureConds
|
||||
|
||||
def duplicateMVar (m : MVarId) : MetaM MVarId := do
|
||||
let d ← m.getDecl
|
||||
let e ← mkFreshExprMVarAt d.lctx d.localInstances d.type d.kind d.userName d.numScopeArgs
|
||||
return e.mvarId!
|
||||
|
||||
/-- Remove the macro scopes introduced by quote expansion from the syntax. -/
|
||||
def eraseQuoteMacroScopesFromSyntax : Syntax → Syntax
|
||||
| Syntax.ident info rawVal val preresolved =>
|
||||
if rawVal.contains '@' then
|
||||
-- This was an inaccessible name in the proof state. Its raw val looks like
|
||||
-- "acc._@.external:file:///.../tests/lean/run/mvcgenInvariantsSuggestions.lean.2049968788._hygCtx._hyg.56"
|
||||
-- Keep the macro scopes!
|
||||
Syntax.ident info rawVal val preresolved
|
||||
else
|
||||
-- This was one of the names made inaccessible by quote expansion. Its raw val looks like
|
||||
-- "xs"
|
||||
-- Erase the macro scopes.
|
||||
Syntax.ident info rawVal val.eraseMacroScopes preresolved
|
||||
| Syntax.node info kind args =>
|
||||
Syntax.node info kind (args.map eraseQuoteMacroScopesFromSyntax)
|
||||
| Syntax.atom info val => Syntax.atom info val
|
||||
| Syntax.missing => Syntax.missing
|
||||
|
||||
/-- Remove the macro scopes introduced by quote expansion from the syntax. -/
|
||||
def eraseQuoteMacroScopesFromTSyntax (syn : TSyntax name) : TSyntax name :=
|
||||
⟨eraseQuoteMacroScopesFromSyntax syn.raw⟩
|
||||
|
||||
/--
|
||||
A simple ad-hoc version of `SPred.Tactic.IsPure`, but without producing a proof and without
|
||||
involving the type class machinery.
|
||||
Example: `spred(∀x, ⌜a⌝ → let y := v; ⌜b⌝ ∧ ⌜c⌝ ∨ ⌜d⌝)` becomes `⌜∀x, a → let y := v; b ∧ c ∨ d⌝`.
|
||||
-/
|
||||
partial def tryHoistPure (e : Expr) : Expr :=
|
||||
match go e with
|
||||
| none => e
|
||||
| some (lvl, e) => SPred.mkPure lvl (TypeList.mkNil lvl) e
|
||||
where
|
||||
go (e : Expr) : Option (Level × Expr) := do
|
||||
if e.isAppOfArity ``SPred.pure 2 then
|
||||
return (e.getAppFn.constLevels![0]!, e.getArg! 1)
|
||||
if let some (_, lhs, rhs) := e.app3? ``SPred.and then
|
||||
let (_, lhs) ← go lhs
|
||||
let (lvl, rhs) ← go rhs
|
||||
return (lvl, mkAnd lhs rhs)
|
||||
if let some (_, lhs, rhs) := e.app3? ``SPred.or then
|
||||
let (_, lhs) ← go lhs
|
||||
let (lvl, rhs) ← go rhs
|
||||
return (lvl, mkOr lhs rhs)
|
||||
if let some (_, _, .lam n ty body bi) := e.app3? ``SPred.forall then
|
||||
let (lvl, body) ← go body
|
||||
return (lvl, mkForall n bi ty body)
|
||||
if let .letE n ty val body nondep := e then
|
||||
let (lvl, body) ← go body
|
||||
return (lvl, .letE n ty val body nondep)
|
||||
failure
|
||||
|
||||
/--
|
||||
Based on how a given metavariable `inv` binding a `Std.Do.Invariant` is used in the `vcs`, suggest
|
||||
an initial assignment for `inv` to fill in for the user.
|
||||
-/
|
||||
def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term := do
|
||||
public def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term := do
|
||||
-- We only synthesize suggestions for invariant subgoals
|
||||
let invType ← instantiateMVars (← inv.getType)
|
||||
let_expr _c@Std.Do.Invariant _α _l doStateTupleTy _ps := invType
|
||||
let_expr c@Std.Do.Invariant α l letMutsTy _ps := invType
|
||||
| throwError "Expected invariant type, got {invType}"
|
||||
let us := c.constLevels!
|
||||
|
||||
-- Simplify the VCs a bit using `mleave`. Makes the job of the analysis below simpler.
|
||||
let vcs ← vcs.flatMapM fun vc =>
|
||||
try
|
||||
(·.toArray) <$> evalTacticAt (← `(tactic| mleave)) (← duplicateMVar vc)
|
||||
catch _e =>
|
||||
-- log m!"Failed to simplify {vc}: {_e.toMessageData}"
|
||||
-- logWarning m!"Failed to simplify {vc}: {_e.toMessageData}"
|
||||
pure #[vc]
|
||||
|
||||
inv.withContext do
|
||||
-- When the loop has an early return, we want to suggest an invariant using `Invariant.withEarlyReturn`.
|
||||
if let some (_ρ, _σ) ← hasEarlyReturn vcs inv doStateTupleTy then
|
||||
-- log m!"Found early return for {inv}!"
|
||||
-- I tried to construct the Expr directly below, but elaborating and then delaborating `_` felt
|
||||
-- strange; furthermore calling the delaborator felt wrong. I might resurrect this code once
|
||||
-- the suggested invariants become deeper, though.
|
||||
--let us := c.constLevels!
|
||||
--withLocalDeclsDND #[(`xs, mkApp2 (mkConst ``List.Cursor us) α l), (`acc, σ)] fun _ => _
|
||||
--let onContinue ← withLocalDeclsDND #[(`xs, mkApp2 (mkConst ``List.Cursor us) α l), (`acc, σ)] fun _ => _dunno
|
||||
--let onReturn ← withLocalDeclsDND #[(`r, ρ), (`acc, σ)] fun _ => _dunno
|
||||
--let onExcept := mkConst ``ExceptConds.false us
|
||||
--let e := mkApp8 (mkConst ``Std.Do.Invariant.withEarlyReturn us) ps α l σ ρ onContinue onReturn onExcept
|
||||
-- how to delab `e : Expr` back into a `Term` to show to the user?
|
||||
let t ← ``(Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _))
|
||||
-- log m!"Suggested invariant: {toString t}"
|
||||
-- log m!"Suggested invariant: {toMessageData t}"
|
||||
return eraseMacroScopesFromTSyntax t
|
||||
eraseMacroScopesFromTSyntax <$> `(⇓ ⟨xs, acc⟩ => _)
|
||||
-- Build the success points into self-contained lambdas, to be beta reduced below.
|
||||
let suggestion? ←
|
||||
withLocalDeclD `xs (mkApp2 (mkConst ``List.Cursor us) α l) fun xs =>
|
||||
withLocalDeclD `letMuts letMutsTy fun letMuts => do
|
||||
let some (prefixPoint, suffixPoint, failureConds) ← collectInvariantHints vcs inv xs letMuts | return none
|
||||
let pred := SPredNil.mkOr prefixPoint.lvl prefixPoint.clause suffixPoint.clause
|
||||
let success ← mkLambdaFVars #[xs, letMuts] (tryHoistPure pred)
|
||||
let onReturn ← mkLambdaFVars #[letMuts] (tryHoistPure suffixPoint.letMutsPred)
|
||||
return some (success, onReturn, failureConds)
|
||||
|
||||
-- Quotes introduce macro scopes to any binders. `eraseQuoteMacroScopesFromTSyntax` removes just
|
||||
-- those, and will not remove any inaccessible markers stemming from inaccessible free variables
|
||||
-- in the proof state.
|
||||
eraseQuoteMacroScopesFromTSyntax <$> do
|
||||
--
|
||||
-- Finally, build the syntax for the suggestion. It's a giant configuration space mess, because
|
||||
-- 1. Generally want to suggest something using `⇓ ⟨xs, letMuts⟩ => ...`, i.e. `PostCond.noThrow`.
|
||||
-- 2. However, on early return we want to suggest something using `Invariant.withEarlyReturn`.
|
||||
-- 3. When there are non-`False` failure conditions, we cannot suggest `⇓ ⟨xs, letMuts⟩ => ...`.
|
||||
-- We might be able to suggest `⇓? ⟨xs, letMuts⟩ => ...` (`True` failure condition),
|
||||
-- or `post⟨...⟩` (more than 0 failure handlers, but ending in `()`), and fall back to
|
||||
-- `by exact ⟨...⟩` (not ending in `()`).
|
||||
-- 4. Similarly for the `onExcept` argument of `Invariant.withEarlyReturn`.
|
||||
-- Hence the spaghetti code.
|
||||
--
|
||||
if let some (ρ, σ) ← hasEarlyReturn vcs inv letMutsTy then
|
||||
-- logWarning m!"Found early return for {inv}!"
|
||||
-- Suggest an invariant using `Invariant.withEarlyReturn`.
|
||||
if let some (success, onReturn, failureConds) := suggestion? then
|
||||
-- First construct `onContinue` and `onReturn` clause and simplify them according to the
|
||||
-- definition of `Invariant.withEarlyReturn`.
|
||||
let (onContinue, onReturn) ← withLocalDeclD `xs (mkApp2 (mkConst ``List.Cursor us) α l) fun xs =>
|
||||
withLocalDeclD `r ρ fun r =>
|
||||
withLocalDeclD `letMuts σ fun letMuts => do
|
||||
let onContinue := success.beta #[xs, ← mkAppM ``MProd.mk #[← mkNone ρ, letMuts]]
|
||||
let onReturn := onReturn.beta #[← mkAppM ``MProd.mk #[← mkSome ρ r, letMuts]]
|
||||
let ctx ← Simp.mkContext
|
||||
(config := {})
|
||||
(simpTheorems := #[(← Meta.getSimpTheorems)])
|
||||
(congrTheorems := (← Meta.getSimpCongrTheorems))
|
||||
let simprocs ← ({} : Simp.SimprocsArray).add `reduceCtorEq false
|
||||
let (res1, _) ← Lean.Meta.simp onContinue ctx simprocs
|
||||
let (res2, _) ← Lean.Meta.simp onReturn ctx simprocs
|
||||
return (← Lean.PrettyPrinter.delab res1.expr, ← Lean.PrettyPrinter.delab res2.expr)
|
||||
-- Now the configuration mess.
|
||||
if failureConds.points.isEmpty then
|
||||
match failureConds.default with
|
||||
| .false | .unit =>
|
||||
`(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue))
|
||||
-- we handle the following two cases here rather than through
|
||||
-- `postCondWithMultipleConditions` below because that would insert a superfluous `by exact _`.
|
||||
| .true =>
|
||||
`(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue (onExcept := ExceptConds.true)))
|
||||
| .other e =>
|
||||
`(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue (onExcept := $(← Lean.PrettyPrinter.delab e))))
|
||||
else -- need the postcondition long form as `onExcept` arg
|
||||
let mut terms : Array Term := #[]
|
||||
for point in failureConds.points do
|
||||
terms := terms.push (← Lean.PrettyPrinter.delab point)
|
||||
let onExcept ← postCondWithMultipleConditions terms failureConds.default
|
||||
`(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue) (onExcept := $onExcept))
|
||||
else -- No suggestion. Just fill in `_`.
|
||||
`(Invariant.withEarlyReturn (onReturn := fun r letMuts => _) (onContinue := fun xs letMuts => _))
|
||||
else if let some (success, _, failureConds) := suggestion? then
|
||||
-- No early return, but we do have a suggestion.
|
||||
withLocalDeclD `xs (mkApp2 (mkConst ``List.Cursor us) α l) fun xs =>
|
||||
withLocalDeclD `letMuts letMutsTy fun letMuts => do
|
||||
let successBody ← Lean.PrettyPrinter.delab (success.beta #[xs, letMuts])
|
||||
-- Configuration mess
|
||||
if failureConds.points.isEmpty && not (failureConds.default matches .other _) then
|
||||
if (failureConds.default matches .true) then
|
||||
`(⇓? ⟨xs, letMuts⟩ => $successBody)
|
||||
else
|
||||
`(⇓ ⟨xs, letMuts⟩ => $successBody)
|
||||
else -- need the long form
|
||||
let mut terms : Array Term := #[← `(fun ⟨xs, letMuts⟩ => $successBody)]
|
||||
for point in failureConds.points do
|
||||
terms := terms.push (← Lean.PrettyPrinter.delab point)
|
||||
postCondWithMultipleConditions terms failureConds.default
|
||||
else
|
||||
-- No early return and no suggestion. Just suggest _something_.
|
||||
-- `PostCond.noThrow` is the most common case.
|
||||
`(⇓ ⟨xs, letMuts⟩ => _)
|
||||
where
|
||||
postCondWithMultipleConditions (handlers : Array Term) (default : ExceptCondsDefault) : MetaM Term := do
|
||||
let handlers := Syntax.TSepArray.ofElems (sep := ",") handlers
|
||||
match default with
|
||||
| .unit => `(post⟨$handlers,*⟩)
|
||||
-- See the comment in `post⟨_⟩` syntax for why we emit `by exact` here.
|
||||
| .false => `(by exact ⟨$handlers,*, ExceptConds.false⟩)
|
||||
| .true => `(by exact ⟨$handlers,*, ExceptConds.true⟩)
|
||||
| .other e => `(by exact ⟨$handlers,*, $(← Lean.PrettyPrinter.delab e)⟩)
|
||||
|
|
|
|||
|
|
@ -359,16 +359,3 @@ syntax vcAlts := "with " (ppSpace colGt tactic)? withPosition((colGe vcAlt)*)
|
|||
syntax (name := mvcgen) "mvcgen" optConfig
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
|
||||
(invariantAlts)? (vcAlts)? : 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
|
||||
|
|
|
|||
|
|
@ -5,6 +5,8 @@ open Std Do
|
|||
|
||||
set_option grind.warning false
|
||||
set_option mvcgen.warning false
|
||||
set_option pp.rawOnError true
|
||||
set_option warn.sorry false
|
||||
|
||||
def mySum (l : List Nat) : Nat := Id.run do
|
||||
let mut acc := 0
|
||||
|
|
@ -15,7 +17,7 @@ def mySum (l : List Nat) : Nat := Id.run do
|
|||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· ⇓⟨xs, acc⟩ => _
|
||||
· ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
|
||||
|
|
@ -24,6 +26,49 @@ theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
|
|||
mvcgen invariants?
|
||||
all_goals admit
|
||||
|
||||
def mySum2 (l : List Nat) : Nat := Id.run do
|
||||
let mut acc := 0
|
||||
let mut acc2 := 0
|
||||
for x in l do
|
||||
acc := acc + x
|
||||
acc2 := acc2 + x
|
||||
return acc
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = ⟨0, 0⟩ ∨ xs.suffix = [] ∧ letMuts.fst = l.sum⌝
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem mySum2_suggest_invariant (l : List Nat) : mySum2 l = l.sum := by
|
||||
generalize h : mySum2 l = r
|
||||
apply Id.of_wp_run_eq h
|
||||
mvcgen invariants?
|
||||
all_goals admit
|
||||
|
||||
def copy (l : List Nat) : Id (Array Nat) := do
|
||||
let mut acc := #[]
|
||||
for x in l do
|
||||
acc := acc.push x
|
||||
return acc
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = acc✝ ∨ xs.suffix = [] ∧ letMuts = l.toArray⌝
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem copy_suggest_invariant (l : List Nat) : ⦃⌜True⌝⦄ copy l ⦃⇓ r => ⌜r = l.toArray⌝⦄ := by
|
||||
mvcgen [copy] invariants?
|
||||
/-
|
||||
case inv1
|
||||
l : List Nat
|
||||
acc✝ : Array Nat := #[]
|
||||
⊢ Invariant l (Array Nat) PostShape.pure
|
||||
...
|
||||
-/
|
||||
all_goals admit
|
||||
|
||||
def nodup (l : List Int) : Bool := Id.run do
|
||||
let mut seen : HashSet Int := ∅
|
||||
for x in l do
|
||||
|
|
@ -35,7 +80,9 @@ def nodup (l : List Int) : Bool := Id.run do
|
|||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
|
||||
·
|
||||
Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝)
|
||||
(onContinue := fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝)
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem nodup_suggest_invariant (l : List Int) : nodup l ↔ l.Nodup := by
|
||||
|
|
@ -60,8 +107,18 @@ def nodup_twice (l : List Int) : Bool := Id.run do
|
|||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
|
||||
· Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
|
||||
·
|
||||
Invariant.withEarlyReturn (onReturn := fun r letMuts =>
|
||||
spred(Prod.fst ?inv2 ({ «prefix» := [], suffix := l, property := ⋯ }, ⟨none, ∅⟩) ∧
|
||||
{ down := r = true ↔ l.Nodup }))
|
||||
(onContinue := fun xs letMuts =>
|
||||
spred({ down := xs.prefix = [] ∧ letMuts = ∅ } ∨
|
||||
⌜xs.suffix = []⌝ ∧
|
||||
Prod.fst ?inv2 ({ «prefix» := [], suffix := l, property := ⋯ }, ⟨none, ∅⟩) ∧
|
||||
{ down := True }))
|
||||
·
|
||||
Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝)
|
||||
(onContinue := fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝)
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem nodup_twice_suggest_invariant (l : List Int) : nodup_twice l ↔ l.Nodup := by
|
||||
|
|
@ -70,7 +127,6 @@ theorem nodup_twice_suggest_invariant (l : List Int) : nodup_twice l ↔ l.Nodup
|
|||
mvcgen invariants?
|
||||
all_goals admit
|
||||
|
||||
|
||||
structure Supply where
|
||||
counter : Nat
|
||||
|
||||
|
|
@ -89,10 +145,11 @@ def mkFreshN (n : Nat) : AppM (List Nat) := do
|
|||
acc := acc.push n
|
||||
return acc.toList
|
||||
|
||||
-- In the following, we suggest an inaccessible variable `acc` in the invariant. Unfortunate.
|
||||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· ⇓⟨xs, acc⟩ => _
|
||||
· ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = acc✝ ∨ xs.suffix = [] ∧ letMuts.toList.Nodup⌝
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem mkFreshN_suggest_invariant (n : Nat) : ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by
|
||||
|
|
@ -110,7 +167,10 @@ def mkFreshN_early_return (n : Nat) : AppM (List Nat) := do
|
|||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
|
||||
·
|
||||
Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜letMuts.toList.Nodup ∧ r.Nodup⌝)
|
||||
(onContinue := fun xs letMuts =>
|
||||
⌜xs.prefix = [] ∧ letMuts = acc✝ ∨ xs.suffix = [] ∧ letMuts.toList.Nodup⌝)
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem mkFreshN_early_return_suggest_invariant (n : Nat) : ⦃⌜True⌝⦄ mkFreshN_early_return n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by
|
||||
|
|
@ -125,7 +185,9 @@ def earlyReturnWithoutLetMut (l : List Int) : Bool := Id.run do
|
|||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _)
|
||||
·
|
||||
Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜r = true⌝) (onContinue :=
|
||||
fun xs letMuts => ⌜xs.prefix = [] ∨ xs.suffix = []⌝)
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem earlyReturnWithoutLetMut_suggest_invariant (l : List Int) : earlyReturnWithoutLetMut l := by
|
||||
|
|
@ -147,7 +209,8 @@ def notQuiteEarlyReturn (l : List Nat) : Option Nat := Id.run do
|
|||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· ⇓⟨xs, acc⟩ => _
|
||||
· ⇓⟨xs, letMuts⟩ =>
|
||||
⌜xs.prefix = [] ∧ letMuts = ⟨none, ()⟩ ∨ xs.suffix = [] ∧ letMuts.fst = l.getLast?⌝
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem notQuiteEarlyReturn_suggest_invariant (l : List Nat) : notQuiteEarlyReturn l = l.getLast? := by
|
||||
|
|
@ -156,23 +219,124 @@ theorem notQuiteEarlyReturn_suggest_invariant (l : List Nat) : notQuiteEarlyRetu
|
|||
mvcgen invariants?
|
||||
all_goals admit
|
||||
|
||||
def polyMonad [Monad m] (l : List Nat) : m (Option Nat) := do
|
||||
-- The idea here is that the type of the state tuple *looks* like it's an early return, but `last`
|
||||
-- is not used as if it is an early return variable. Specifically, `last` is set without breaking
|
||||
-- out of the loop.
|
||||
let mut last : Option Nat := none
|
||||
let mut mdummy : Unit := () -- m* is important because let mut vars are sorted alphabetically
|
||||
def polySum [Monad m] (l : List Nat) : m Nat := do
|
||||
let mut acc := 0
|
||||
let mut acc2 := 0
|
||||
for x in l do
|
||||
last := some x
|
||||
mdummy := ()
|
||||
return last
|
||||
acc := acc + x
|
||||
acc2 := acc2 + x
|
||||
return acc
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· ⇓⟨xs, acc⟩ => _
|
||||
· ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = ⟨0, 0⟩ ∨ xs.suffix = [] ∧ letMuts.fst = l.sum⌝
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem polyMonad_suggest_invariant [Monad m] [WPMonad m ps] (l : List Nat) : ⦃⌜True⌝⦄ @polyMonad m _ l ⦃⇓ r => ⌜True⌝⦄ := by
|
||||
mvcgen [polyMonad] invariants?
|
||||
theorem polySum_suggest_invariant [Monad m] [WPMonad m ps] (l : List Nat) : ⦃⌜True⌝⦄ @polySum m _ l ⦃⇓ r => ⌜r = l.sum⌝⦄ := by
|
||||
mvcgen [polySum] invariants?
|
||||
all_goals admit
|
||||
|
||||
def polyNodup [Monad m] (l : List Int) : m Bool := do
|
||||
let mut seen : HashSet Int := ∅
|
||||
for x in l do
|
||||
if x ∈ seen then
|
||||
return false
|
||||
seen := seen.insert x
|
||||
return true
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
·
|
||||
Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝)
|
||||
(onContinue := fun xs letMuts =>
|
||||
⌜xs.prefix = [] ∧ letMuts = seen✝ ∨ xs.suffix = [] ∧ l.Nodup⌝)
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem polyNodup_suggest_invariant [Monad m] [WPMonad m ps] (l : List Int) : ⦃⌜True⌝⦄ @polyNodup m _ l ⦃⇓r => ⌜r ↔ l.Nodup⌝⦄ := by
|
||||
mvcgen [polyNodup] invariants?
|
||||
all_goals admit
|
||||
|
||||
def fast_expo (x n : Nat) : Nat := Id.run do
|
||||
let mut x := x
|
||||
let mut y := 1
|
||||
let mut e := n
|
||||
for _ in [:n] do -- simulating a while loop running at most n times
|
||||
if e = 0 then break
|
||||
if e % 2 = 1 then
|
||||
y := x * y
|
||||
e := e - 1
|
||||
else
|
||||
x := x*x
|
||||
e := e/2
|
||||
|
||||
return y
|
||||
|
||||
open Std.Do
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
· ⇓⟨xs, letMuts⟩ =>
|
||||
⌜xs.prefix = [] ∧ letMuts = ⟨n, x, 1⟩ ∨ xs.suffix = [] ∧ letMuts.2.snd = x ^ n⌝
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
|
||||
generalize h : fast_expo x n = r
|
||||
apply Id.of_wp_run_eq h
|
||||
mvcgen invariants?
|
||||
all_goals admit
|
||||
|
||||
namespace FreshBounded
|
||||
|
||||
structure Supply where
|
||||
counter : Nat
|
||||
limit : Nat
|
||||
property : counter ≤ limit
|
||||
|
||||
def mkFresh : EStateM String Supply Nat := do
|
||||
let supply ← get
|
||||
if h : supply.counter = supply.limit then
|
||||
throw s!"Supply exhausted: {supply.counter} = {supply.limit}"
|
||||
else
|
||||
let n := supply.counter
|
||||
have := supply.property
|
||||
set {supply with counter := n + 1, property := by omega}
|
||||
pure n
|
||||
|
||||
def mkFreshN (n : Nat) : ExceptT Char (EStateM String Supply) (List Nat) := do
|
||||
let mut acc := #[]
|
||||
for _ in [:n] do
|
||||
acc := acc.push (← mkFresh)
|
||||
pure acc.toList
|
||||
|
||||
@[spec]
|
||||
theorem mkFresh_spec (c : Nat) :
|
||||
⦃fun state => ⌜state.counter = c⌝⦄
|
||||
mkFresh
|
||||
⦃post⟨fun r state => ⌜r = c ∧ c < state.counter⌝, fun _msg state => ⌜c = state.counter ∧ c = state.limit⌝⟩⦄ := by
|
||||
mvcgen [mkFresh]
|
||||
all_goals grind
|
||||
|
||||
/--
|
||||
info: Try this:
|
||||
invariants
|
||||
·
|
||||
post⟨fun ⟨xs, letMuts⟩ =>
|
||||
⌜xs.prefix = [] ∧ letMuts = acc✝ ∨ xs.suffix = [] ∧ letMuts.toList.Nodup⌝, fun x => ⌜False⌝,
|
||||
fun _msg state => ⌜state.counter = state.limit⌝⟩
|
||||
-/
|
||||
#guard_msgs (info) in
|
||||
theorem mkFreshN_spec (n : Nat) :
|
||||
⦃⌜True⌝⦄
|
||||
mkFreshN n
|
||||
⦃post⟨fun r => ⌜r.Nodup⌝, fun _ => ⌜False⌝, fun _msg state => ⌜state.counter = state.limit⌝⟩⦄ := by
|
||||
mvcgen [mkFreshN] invariants?
|
||||
-- The full invariant is:
|
||||
-- · post⟨fun ⟨xs, acc⟩ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝,
|
||||
-- fun _ => ⌜False⌝,
|
||||
-- fun _msg state => ⌜state.counter = state.limit⌝⟩
|
||||
all_goals admit
|
||||
|
||||
end FreshBounded
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue