feat: Simpler first-order implementation for pure SPreds (#9841)
This PR migrates the ⌜p⌝ notation for embedding pure p : Prop into SPred σs to expand into a simple, first-order expression SPred.pure p that can be supported by e-matching in grind. Doing so deprives ⌜p⌝ notation of its idiom-bracket-like support for #selector and ‹Nat›ₛ syntax which is thus removed.
This commit is contained in:
Sebastian Graf
GitHub
parent
f15d531acb
commit
9a0c1ab2d0
14 changed files with 79 additions and 127 deletions
|
|
@ -147,8 +147,7 @@ partial def computeMVarBetaPotentialForSPred (xs : Array Expr) (σs : Expr) (e :
|
|||
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`.
|
||||
-- In practice we only need to reduce `fun s => ...` and `SPred.pure`.
|
||||
-- We could write a custom function should `simp` become a bottleneck.
|
||||
e := r.expr
|
||||
let count ← countBVarDependentMVars xs e
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ open Lean Elab Tactic Meta
|
|||
-- set_option pp.all true in
|
||||
-- #check ⌜False⌝
|
||||
private def falseProp (u : Level) (σs : Expr) : Expr := -- ⌜False⌝ standing in for an empty conjunction of hypotheses
|
||||
mkApp3 (mkConst ``SVal.curry [u]) (mkApp (mkConst ``ULift [u, 0]) (.sort .zero)) σs <| mkLambda `tuple .default (mkApp (mkConst ``SVal.StateTuple [u]) σs) (mkApp2 (mkConst ``ULift.up [u, 0]) (.sort .zero) (mkConst ``False))
|
||||
SPred.mkPure u σs (mkConst ``False)
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.mexfalso]
|
||||
def elabMExfalso : Tactic | _ => do
|
||||
|
|
|
|||
|
|
@ -41,13 +41,10 @@ def SPred.mkType (u : Level) (σs : Expr) : Expr :=
|
|||
-- set_option pp.all true in
|
||||
-- #check ⌜True⌝
|
||||
def SPred.mkPure (u : Level) (σs : Expr) (p : Expr) : Expr :=
|
||||
mkApp3 (mkConst ``SVal.curry [u]) (mkApp (mkConst ``ULift [u, 0]) (.sort .zero)) σs <|
|
||||
mkLambda `tuple .default (mkApp (mkConst ``SVal.StateTuple [u]) σs) <|
|
||||
mkApp2 (mkConst ``ULift.up [u, 0]) (.sort .zero) (Expr.liftLooseBVars p 0 1)
|
||||
mkApp2 (mkConst ``SPred.pure [u]) σs p
|
||||
|
||||
def SPred.isPure? : Expr → Option (Level × Expr × Expr)
|
||||
| mkApp3 (.const ``SVal.curry [u]) (mkApp (.const ``ULift _) (.sort .zero)) σs <|
|
||||
.lam _ _ (mkApp2 (.const ``ULift.up _) _ p) _ => some (u, σs, (Expr.lowerLooseBVars p 0 1))
|
||||
| mkApp2 (.const ``SPred.pure [u]) σs p => some (u, σs, p)
|
||||
| _ => none
|
||||
|
||||
def emptyHypName := `emptyHyp
|
||||
|
|
|
|||
|
|
@ -124,7 +124,7 @@ def dischargeMGoal (goal : MGoal) (goalTag : Name) : n Expr := do
|
|||
liftMetaM <| do trace[Elab.Tactic.Do.spec] "dischargeMGoal: {goal.target}"
|
||||
-- simply try one of the assumptions for now. Later on we might want to decompose conjunctions etc; full xsimpl
|
||||
-- The `withDefault` ensures that a hyp `⌜s = 4⌝` can be used to discharge `⌜s = 4⌝ s`.
|
||||
-- (Recall that `⌜s = 4⌝ s` is `SVal.curry (σs:=[Nat]) (fun _ => s = 4) s` and `SVal.curry` is
|
||||
-- (Recall that `⌜s = 4⌝ s` is `SPred.pure (σs:=[Nat]) (s = 4) s` and `SPred.pure` is
|
||||
-- semi-reducible.)
|
||||
-- We also try `mpure_intro; trivial` through `goal.triviallyPure` here because later on an
|
||||
-- assignment like `⌜s = ?c⌝` becomes impossible to discharge because `?c` will get abstracted
|
||||
|
|
@ -156,11 +156,8 @@ def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name
|
|||
let wp := T.getArg! 2
|
||||
let specThm ← elabSpecAtWP 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`.
|
||||
-- The precondition of `specThm` might look like `⌜?n = nₛ ∧ ?m = b⌝`, which expands to
|
||||
-- `SPred.pure (?n = n ∧ ?m = b)`.
|
||||
let residualEta := specThm.etaPotential - (T.getAppNumArgs - 4) -- 4 arguments expected for PredTrans.apply
|
||||
mIntroForallN goal residualEta fun goal => do
|
||||
|
||||
|
|
|
|||
|
|
@ -196,6 +196,7 @@ instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ ∨ ⌜ψ⌝) (φ ∨ ψ) wher
|
|||
instance (σs) (P : α → Prop) : IsPure (σs:=σs) spred(∃ x, ⌜P x⌝) (∃ x, P x) where to_pure := pure_exists
|
||||
instance (σs) (P : α → Prop) : IsPure (σs:=σs) spred(∀ x, ⌜P x⌝) (∀ x, P x) where to_pure := pure_forall
|
||||
instance (σs) (P : SPred (σ::σs)) [inst : IsPure P φ] : IsPure (σs:=σs) spred(P s) φ where to_pure := (iff_of_eq bientails_cons).mp inst.to_pure s
|
||||
instance (σs) (P : SPred σs) [inst : IsPure P φ] : IsPure (σs:=σ::σs) (fun _ => P) φ where to_pure := (iff_of_eq bientails_cons).mpr (fun _ => inst.to_pure)
|
||||
instance (φ : Prop) : IsPure (σs:=[]) ⌜φ⌝ φ where to_pure := Iff.rfl
|
||||
instance (P : SPred []) : IsPure (σs:=[]) P P.down where to_pure := Iff.rfl
|
||||
|
||||
|
|
@ -267,6 +268,7 @@ class HasFrame (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop)
|
|||
reassoc : P ⊣⊢ₛ P' ∧ ⌜φ⌝
|
||||
instance (σs) (P P' Q QP : SPred σs) [HasFrame P Q φ] [SimpAnd Q P' QP]: HasFrame (σs:=σs) spred(P ∧ P') QP φ where reassoc := ((and_congr_l HasFrame.reassoc).trans and_right_comm).trans (and_congr_l SimpAnd.simp_and)
|
||||
instance (σs) (P P' Q' PQ : SPred σs) [HasFrame P' Q' φ] [SimpAnd P Q' PQ]: HasFrame (σs:=σs) spred(P ∧ P') PQ φ where reassoc := ((and_congr_r HasFrame.reassoc).trans and_assoc.symm).trans (and_congr_l SimpAnd.simp_and)
|
||||
instance (σs) (P P' : Prop) (Q : SPred σs) [HasFrame spred(⌜P⌝ ∧ ⌜P'⌝) Q φ] : HasFrame (σs:=σs) ⌜P ∧ P'⌝ Q φ where reassoc := and_pure.symm.trans HasFrame.reassoc
|
||||
instance (σs) (P P' : SVal.StateTuple σs → Prop) (Q : SPred σs) [HasFrame spred(SVal.curry (fun t => ⟨P t⟩) ∧ SVal.curry (fun t => ⟨P' t⟩)) Q φ] : HasFrame (σs:=σs) (SVal.curry fun t => ⟨P t ∧ P' t⟩) Q φ where reassoc := and_curry.symm.trans HasFrame.reassoc
|
||||
instance (σs) (P : SPred σs) : HasFrame (σs:=σs) spred(⌜φ⌝ ∧ P) P φ where reassoc := and_comm
|
||||
instance (σs) (P : SPred σs) : HasFrame (σs:=σs) spred(P ∧ ⌜φ⌝) P φ where reassoc := .rfl
|
||||
|
|
|
|||
|
|
@ -76,16 +76,34 @@ theorem bientails.to_eq {P Q : SPred σs} (h : P ⊣⊢ₛ Q) : P = Q := by
|
|||
|
||||
/-! # Pure -/
|
||||
|
||||
@[simp, grind =] theorem down_pure {φ : Prop} : (⌜φ⌝ : SPred []).down = φ := rfl
|
||||
@[simp, grind =] theorem apply_pure {φ : Prop} : (⌜φ⌝ : SPred (σ::σs)) s = ⌜φ⌝ := rfl
|
||||
|
||||
theorem pure_intro {φ : Prop} {P : SPred σs} : φ → P ⊢ₛ ⌜φ⌝ := by
|
||||
induction σs <;> simp_all [entails, SVal.curry]
|
||||
induction σs <;> simp_all [entails]
|
||||
|
||||
theorem pure_elim' {φ : Prop} {P : SPred σs} : (φ → ⌜True⌝ ⊢ₛ P) → ⌜φ⌝ ⊢ₛ P := by
|
||||
induction σs <;> simp_all [entails, SVal.curry]
|
||||
induction σs <;> simp_all [entails]
|
||||
|
||||
-- Ideally, we'd like to prove the following theorem:
|
||||
-- theorem pure_elim' {φ : Prop} : SPred.entails (σs:=σs) ⌜True⌝ ⌜φ⌝ → φ
|
||||
-- Unfortunately, this is only true if all `σs` are Inhabited.
|
||||
|
||||
theorem and_pure {P Q : Prop} : ⌜P⌝ ∧ ⌜Q⌝ ⊣⊢ₛ (⌜P ∧ Q⌝ : SPred σs) := by
|
||||
induction σs
|
||||
case nil => rfl
|
||||
case cons σ σs ih => intro s; simp only [and_cons]; exact ih
|
||||
|
||||
theorem or_pure {P Q : Prop} : ⌜P⌝ ∨ ⌜Q⌝ ⊣⊢ₛ (⌜P ∨ Q⌝ : SPred σs) := by
|
||||
induction σs
|
||||
case nil => rfl
|
||||
case cons σ σs ih => intro s; simp only [or_cons]; exact ih
|
||||
|
||||
theorem imp_pure {P Q : Prop} : (⌜P⌝ → ⌜Q⌝) ⊣⊢ₛ (⌜P → Q⌝ : SPred σs) := by
|
||||
induction σs
|
||||
case nil => rfl
|
||||
case cons σ σs ih => intro s; simp only [imp_cons]; exact ih
|
||||
|
||||
/-! # Conjunction -/
|
||||
|
||||
theorem and_intro {P Q R : SPred σs} (h1 : P ⊢ₛ Q) (h2 : P ⊢ₛ R) : P ⊢ₛ Q ∧ R := by
|
||||
|
|
|
|||
|
|
@ -50,14 +50,8 @@ partial def SPred.Notation.unpack [Monad m] [MonadRef m] [MonadQuotation m] : Te
|
|||
|
||||
/-! # Idiom notation -/
|
||||
|
||||
/-- Embedding of pure Lean values into `SVal`. -/
|
||||
/-- Embedding of pure Lean values into `SVal`. An alias for `SPred.pure`. -/
|
||||
scoped syntax "⌜" term "⌝" : term
|
||||
/-- ‹t› in `SVal` idiom notation. Accesses the state of type `t`. -/
|
||||
scoped syntax "‹" term "›ₛ" : term
|
||||
/--
|
||||
Use getter `t : SVal σs σ` in `SVal` idiom notation; sugar for `SVal.uncurry t (by assumption)`.
|
||||
-/
|
||||
scoped syntax:max "#" term:max : term
|
||||
|
||||
/-! # Sugar for `SPred` -/
|
||||
|
||||
|
|
@ -69,9 +63,7 @@ scoped syntax:25 "⊢ₛ " term:25 : term
|
|||
scoped syntax:25 term:25 " ⊣⊢ₛ " term:25 : term
|
||||
|
||||
macro_rules
|
||||
| `(⌜$t⌝) => ``(SVal.curry (fun tuple => ULift.up $t))
|
||||
| `(#$t) => `(SVal.uncurry $t (by assumption))
|
||||
| `(‹$t›ₛ) => `(#(SVal.getThe $t))
|
||||
| `(⌜$t⌝) => ``(SPred.pure $t)
|
||||
| `($P ⊢ₛ $Q) => ``(SPred.entails spred($P) spred($Q))
|
||||
| `(spred($P ∧ $Q)) => ``(SPred.and spred($P) spred($Q))
|
||||
| `(spred($P ∨ $Q)) => ``(SPred.or spred($P) spred($Q))
|
||||
|
|
@ -94,20 +86,10 @@ macro_rules
|
|||
|
||||
namespace SPred.Notation
|
||||
|
||||
@[app_unexpander SVal.curry]
|
||||
meta def unexpandCurry : Unexpander
|
||||
@[app_unexpander SPred.pure]
|
||||
meta def unexpandPure : Unexpander
|
||||
| `($_ $t $ts*) => do
|
||||
match t with
|
||||
| `(fun $_ => { down := $e }) => if ts.isEmpty then ``(⌜$e⌝) else ``(⌜$e⌝ $ts*)
|
||||
| _ => throw ()
|
||||
| _ => throw ()
|
||||
|
||||
@[app_unexpander SVal.uncurry]
|
||||
meta def unexpandUncurry : Unexpander
|
||||
| `($_ $f $ts*) => do
|
||||
match f with
|
||||
| `(SVal.getThe $t) => if ts.isEmpty then ``(‹$t›ₛ) else ``(‹$t›ₛ $ts*)
|
||||
| `($t) => if ts.isEmpty then ``(#$t) else ``(#$t $ts*)
|
||||
if ts.isEmpty then ``(⌜$t⌝) else ``(⌜$t⌝ $ts*)
|
||||
| _ => throw ()
|
||||
|
||||
@[app_unexpander SPred.entails]
|
||||
|
|
|
|||
|
|
@ -33,9 +33,6 @@ namespace SPred
|
|||
universe u
|
||||
variable {σs : List (Type u)}
|
||||
|
||||
/-- A pure proposition `P : Prop` embedded into `SPred`. For internal use in this module only; prefer to use idiom bracket notation `⌜P⌝. -/
|
||||
abbrev pure (P : Prop) : SPred σs := SVal.curry (fun _ => ⟨P⟩)
|
||||
|
||||
@[ext]
|
||||
theorem ext_nil {P Q : SPred []} (h : P.down ↔ Q.down) : P = Q := by
|
||||
cases P; cases Q; simp_all
|
||||
|
|
@ -43,6 +40,16 @@ theorem ext_nil {P Q : SPred []} (h : P.down ↔ Q.down) : P = Q := by
|
|||
@[ext]
|
||||
theorem ext_cons {P Q : SPred (σ::σs)} : (∀ s, P s = Q s) → P = Q := funext
|
||||
|
||||
/--
|
||||
A pure proposition `P : Prop` embedded into `SPred`.
|
||||
Prefer to use idiom bracket notation `⌜P⌝.
|
||||
-/
|
||||
def pure {σs : List (Type u)} (P : Prop) : SPred σs := match σs with
|
||||
| [] => ULift.up P
|
||||
| _ :: _ => fun _ => pure P
|
||||
theorem pure_nil : pure (σs:=[]) P = ULift.up P := rfl
|
||||
theorem pure_cons : pure (σs:=σ::σs) P = fun _ => pure P := rfl
|
||||
|
||||
/-- Entailment in `SPred`. -/
|
||||
def entails {σs : List (Type u)} (P Q : SPred σs) : Prop := match σs with
|
||||
| [] => P.down → Q.down
|
||||
|
|
@ -119,4 +126,4 @@ def conjunction {σs : List (Type u)} (env : List (SPred σs)) : SPred σs := ma
|
|||
@[simp, grind =] theorem conjunction_nil : conjunction ([] : List (SPred σs)) = pure True := rfl
|
||||
@[simp, grind =] theorem conjunction_cons {P : SPred σs} {env : List (SPred σs)} : conjunction (P::env) = P.and (conjunction env) := rfl
|
||||
@[simp, grind =] theorem conjunction_apply {env : List (SPred (σ::σs))} : conjunction env s = conjunction (env.map (· s)) := by
|
||||
induction env <;> simp [conjunction, *]
|
||||
induction env <;> simp [conjunction, pure_cons, *]
|
||||
|
|
|
|||
|
|
@ -24,9 +24,10 @@ namespace Std.Do
|
|||
abbrev SVal (σs : List (Type u)) (α : Type u) : Type u := match σs with
|
||||
| [] => α
|
||||
| σ :: σs => σ → SVal σs α
|
||||
|
||||
/- Note about the reducibility of SVal:
|
||||
We need SVal to be reducible, otherwise type inference fails for `Triple`.
|
||||
(Begs for investigation. #8074.)
|
||||
This is tracked in #8074. There is a fix in #9015, but it regresses Mathlib.
|
||||
-/
|
||||
|
||||
namespace SVal
|
||||
|
|
@ -59,22 +60,19 @@ def uncurry {σs : List (Type u)} (f : SVal σs α) : StateTuple σs → α := m
|
|||
@[simp, grind =] theorem uncurry_curry {σs : List (Type u)} {f : StateTuple σs → α} : uncurry (σs:=σs) (curry f) = f := by induction σs <;> (simp[uncurry, curry, *]; rfl)
|
||||
@[simp, grind =] theorem curry_uncurry {σs : List (Type u)} {f : SVal σs α} : curry (σs:=σs) (uncurry f) = f := by induction σs <;> simp[uncurry, curry, *]
|
||||
|
||||
/-- Embed a pure value into an `SVal`. -/
|
||||
abbrev pure {σs : List (Type u)} (a : α) : SVal σs α := curry (fun _ => a)
|
||||
|
||||
instance [Inhabited α] : Inhabited (SVal σs α) where
|
||||
default := pure default
|
||||
default := curry fun _ => default
|
||||
|
||||
class GetTy (σ : Type u) (σs : List (Type u)) where
|
||||
get : SVal σs σ
|
||||
|
||||
instance : GetTy σ (σ :: σs) where
|
||||
get := fun s => pure s
|
||||
get := fun s => curry (fun _ => s)
|
||||
|
||||
instance [GetTy σ₁ σs] : GetTy σ₁ (σ₂ :: σs) where
|
||||
get := fun _ => GetTy.get
|
||||
|
||||
/-- Get the top-most state of type `σ` from an `SVal`. -/
|
||||
def getThe {σs : List (Type u)} (σ : Type u) [GetTy σ σs] : SVal σs σ := GetTy.get
|
||||
@[simp, grind =] theorem getThe_here {σs : List (Type u)} (σ : Type u) (s : σ) : getThe (σs := σ::σs) σ s = pure s := rfl
|
||||
@[simp, grind =] theorem getThe_here {σs : List (Type u)} (σ : Type u) (s : σ) : getThe (σs := σ::σs) σ s = curry (fun _ => s) := rfl
|
||||
@[simp, grind =] theorem getThe_there {σs : List (Type u)} [GetTy σ σs] (σ' : Type u) (s : σ') : getThe (σs := σ'::σs) σ s = getThe (σs := σs) σ := rfl
|
||||
|
|
|
|||
|
|
@ -126,6 +126,8 @@ syntax (name := mstop) "mstop" : tactic
|
|||
@[inherit_doc Lean.Parser.Tactic.mleaveMacro]
|
||||
macro (name := mleave) "mleave" : tactic =>
|
||||
`(tactic| (try simp only [
|
||||
$(mkIdent ``Std.Do.SPred.down_pure):term,
|
||||
$(mkIdent ``Std.Do.SPred.apply_pure):term,
|
||||
-- $(mkIdent ``Std.Do.SPred.entails_cons):term, -- Ineffective until #9015 lands
|
||||
$(mkIdent ``Std.Do.SPred.entails_1):term,
|
||||
$(mkIdent ``Std.Do.SPred.entails_2):term,
|
||||
|
|
@ -289,7 +291,7 @@ Like `mspec`, but does not attempt slight simplification and closing of trivial
|
|||
```
|
||||
mspec_no_simp $spec
|
||||
all_goals
|
||||
((try simp only [SPred.true_intro_simp, SVal.curry_cons, SVal.uncurry_nil, SVal.uncurry_cons, SVal.getThe_here, SVal.getThe_there]);
|
||||
((try simp only [SPred.true_intro_simp, SPred.apply_pure]);
|
||||
(try mpure_intro; trivial))
|
||||
```
|
||||
-/
|
||||
|
|
@ -316,11 +318,7 @@ macro (name := mspec) "mspec" spec:(ppSpace colGt term)? : tactic =>
|
|||
`(tactic| (mspec_no_simp $[$spec]?
|
||||
all_goals ((try simp only [
|
||||
$(mkIdent ``Std.Do.SPred.true_intro_simp):term,
|
||||
$(mkIdent ``Std.Do.SVal.curry_cons):term,
|
||||
$(mkIdent ``Std.Do.SVal.uncurry_nil):term,
|
||||
$(mkIdent ``Std.Do.SVal.uncurry_cons):term,
|
||||
$(mkIdent ``Std.Do.SVal.getThe_here):term,
|
||||
$(mkIdent ``Std.Do.SVal.getThe_there):term])
|
||||
$(mkIdent ``Std.Do.SPred.apply_pure):term])
|
||||
(try mpure_intro; trivial))))
|
||||
|
||||
@[inherit_doc Lean.Parser.Tactic.mvcgenMacro]
|
||||
|
|
|
|||
|
|
@ -6,15 +6,13 @@ set_option mvcgen.warning false
|
|||
|
||||
abbrev SM := StateM (Array Nat)
|
||||
|
||||
abbrev gns : SVal ((Array Nat)::[]) (Array Nat) := fun s => SVal.pure s
|
||||
|
||||
noncomputable def setZeroHead : StateM (Array Nat) Unit := do
|
||||
modify fun _ => #[0, 1, 2, 3, 4, 5]
|
||||
|
||||
theorem setZeroHead_spec :
|
||||
⦃⌜True⌝⦄
|
||||
setZeroHead
|
||||
⦃⇓ _ => ⌜∃ ns', (#gns).toList = 0 :: ns'⌝⦄ := by
|
||||
⦃⇓ _ gns => ⌜∃ ns', gns.toList = 0 :: ns'⌝⦄ := by
|
||||
mvcgen [setZeroHead]
|
||||
-- We want to see and name the tuple `t` here in order for us not having to repeat its
|
||||
-- definition in t.2.toList.tail below
|
||||
|
|
|
|||
|
|
@ -4,8 +4,6 @@ open Std.Do
|
|||
|
||||
set_option mvcgen.warning false
|
||||
|
||||
abbrev gns : SVal ((List Nat)::[]) (List Nat) := fun s => SVal.pure s
|
||||
|
||||
noncomputable def setZeroHead : StateM (List Nat) Unit := do
|
||||
modify fun _ => [1, 0, 1, 2, 3, 4, 5]
|
||||
pure ()
|
||||
|
|
@ -15,7 +13,7 @@ noncomputable def setZeroHead : StateM (List Nat) Unit := do
|
|||
theorem setZeroHead_spec :
|
||||
⦃⌜True⌝⦄
|
||||
setZeroHead
|
||||
⦃⇓ _ => ⌜∃ ns', #gns = 0 :: ns'⌝⦄ := by
|
||||
⦃⇓ _ gns => ⌜∃ ns', gns = 0 :: ns'⌝⦄ := by
|
||||
mvcgen [setZeroHead] -- should mintro through let/have bindings
|
||||
mleave
|
||||
rename_i t
|
||||
|
|
|
|||
|
|
@ -95,20 +95,17 @@ theorem sum_loop_spec :
|
|||
simp_all +decide
|
||||
omega
|
||||
|
||||
private abbrev fst : SVal ((Nat × Nat)::σs) Nat := fun s => SVal.pure s.1
|
||||
private abbrev snd : SVal ((Nat × Nat)::σs) Nat := fun s => SVal.pure s.2
|
||||
|
||||
theorem mkFreshNat_spec [Monad m] [WPMonad m sh] :
|
||||
⦃⌜#fst = n ∧ #snd = o⌝⦄
|
||||
⦃fun p => ⌜p.1 = n ∧ p.2 = o⌝⦄
|
||||
(mkFreshNat : StateT (Nat × Nat) m Nat)
|
||||
⦃⇓ r => ⌜r = n ∧ #fst = n + 1 ∧ #snd = o⌝⦄ := by
|
||||
⦃⇓ r p => ⌜r = n ∧ p.1 = n + 1 ∧ p.2 = o⌝⦄ := by
|
||||
mintro _
|
||||
dsimp only [mkFreshNat, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift, modify, modifyGet]
|
||||
mspec
|
||||
mspec
|
||||
mspec
|
||||
mspec
|
||||
simp
|
||||
simp [*]
|
||||
|
||||
attribute [local spec] mkFreshNat_spec
|
||||
|
||||
|
|
@ -160,7 +157,7 @@ theorem throwing_loop_spec :
|
|||
mspec
|
||||
mspec
|
||||
mspec
|
||||
simp_all only [List.sum_nil, Nat.add_zero, gt_iff_lt, SVal.curry_nil, SPred.entails_nil,
|
||||
simp_all only [List.sum_nil, Nat.add_zero, gt_iff_lt, SPred.down_pure, SPred.entails_nil,
|
||||
imp_false, not_true_eq_false]
|
||||
omega
|
||||
case post.except => simp
|
||||
|
|
@ -174,9 +171,9 @@ theorem throwing_loop_spec :
|
|||
case isFalse => intro _; mintro _; mspec; intro _; simp_all +arith
|
||||
|
||||
theorem beaking_loop_spec :
|
||||
⦃⌜‹Nat›ₛ = 42⌝⦄
|
||||
⦃fun s => ⌜s = 42⌝⦄
|
||||
breaking_loop
|
||||
⦃⇓ r => ⌜r > 4 ∧ ‹Nat›ₛ = 1⌝⦄ := by
|
||||
⦃⇓ r s => ⌜r > 4 ∧ s = 1⌝⦄ := by
|
||||
mintro hs
|
||||
dsimp only [breaking_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift]
|
||||
mspec
|
||||
|
|
@ -214,7 +211,7 @@ theorem returning_loop_spec :
|
|||
· mspec
|
||||
intro _ h
|
||||
conv at h in (List.sum _) => whnf
|
||||
simp at h
|
||||
simp at h ⊢
|
||||
grind
|
||||
case step =>
|
||||
intros
|
||||
|
|
@ -348,10 +345,6 @@ end KimsBabySteps
|
|||
|
||||
section WeNeedAProofMode
|
||||
|
||||
private abbrev theNat : SVal [Nat, Bool] Nat := fun n _ => n
|
||||
private def test (P Q : Assertion (.arg Nat (.arg Bool .pure))) : Assertion (.arg Char (.arg Nat (.arg Bool .pure))) :=
|
||||
spred(fun n => ((∀ y, if y = n then ⌜‹Nat›ₛ + #theNat = 4⌝ else Q) ∧ Q) → P → (∃ x, P → if (x : Bool) then Q else P))
|
||||
|
||||
abbrev M := StateT Nat (StateT Char (StateT Bool (StateT String Id)))
|
||||
axiom op : Nat → M Nat
|
||||
noncomputable def prog (n : Nat) : M Nat := do
|
||||
|
|
@ -443,21 +436,18 @@ theorem fib_impl_vcs
|
|||
case step => apply_rules [loop_step]
|
||||
case post.success => apply_rules [loop_post]
|
||||
|
||||
private abbrev fst : SVal (AppState::σs) Nat := fun s => SVal.pure s.1
|
||||
private abbrev snd : SVal (AppState::σs) Nat := fun s => SVal.pure s.2
|
||||
|
||||
@[spec]
|
||||
theorem mkFreshNat_spec [Monad m] [WPMonad m sh] :
|
||||
⦃⌜#fst = n ∧ #snd = o⌝⦄
|
||||
⦃fun s => ⌜s.1 = n ∧ s.2 = o⌝⦄
|
||||
(mkFreshNat : StateT AppState m Nat)
|
||||
⦃⇓ r => ⌜r = n ∧ #fst = n + 1 ∧ #snd = o⌝⦄ := by
|
||||
⦃⇓ r s => ⌜r = n ∧ s.1 = n + 1 ∧ s.2 = o⌝⦄ := by
|
||||
mvcgen [mkFreshNat]
|
||||
simp_all +zetaDelta
|
||||
|
||||
theorem erase_unfold [Monad m] [WPMonad m sh] :
|
||||
⦃⌜#fst = n ∧ #snd = o⌝⦄
|
||||
⦃fun s => ⌜s.1 = n ∧ s.2 = o⌝⦄
|
||||
(mkFreshNat : StateT AppState m Nat)
|
||||
⦃⇓ r => ⌜r = n ∧ #fst = n + 1 ∧ #snd = o⌝⦄ := by
|
||||
⦃⇓ r s => ⌜r = n ∧ s.1 = n + 1 ∧ s.2 = o⌝⦄ := by
|
||||
unfold mkFreshNat
|
||||
mvcgen [-modify]
|
||||
simp_all [-WP.modify_MonadStateOf]
|
||||
|
|
@ -465,9 +455,9 @@ theorem erase_unfold [Monad m] [WPMonad m sh] :
|
|||
admit
|
||||
|
||||
theorem add_unfold [Monad m] [WPMonad m sh] :
|
||||
⦃⌜#fst = n ∧ #snd = o⌝⦄
|
||||
⦃fun s => ⌜s.1 = n ∧ s.2 = o⌝⦄
|
||||
(mkFreshNat : StateT AppState m Nat)
|
||||
⦃⇓ r => ⌜r = n ∧ #fst = n + 1 ∧ #snd = o⌝⦄ := by
|
||||
⦃⇓ r s => ⌜r = n ∧ s.1 = n + 1 ∧ s.2 = o⌝⦄ := by
|
||||
mvcgen [mkFreshNat]
|
||||
|
||||
theorem mkFreshPair_triple : ⦃⌜True⌝⦄ mkFreshPair ⦃⇓ (a, b) => ⌜a ≠ b⌝⦄ := by
|
||||
|
|
@ -492,21 +482,21 @@ theorem throwing_loop_spec :
|
|||
mvcgen [throwing_loop]
|
||||
case inv => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝,
|
||||
fun e s => ⌜e = 42 ∧ s = 4⌝⟩
|
||||
case pre1 => simp_all only [SVal.curry_nil]; decide
|
||||
case post.success => simp_all only [SVal.curry_nil]; grind
|
||||
case pre1 => simp_all only [SPred.down_pure]; decide
|
||||
case post.success => simp_all only [SPred.down_pure]; grind
|
||||
case post.except => simp_all
|
||||
case isTrue => intro _; simp_all
|
||||
case isFalse => intro _; simp_all only [SVal.curry_nil]; grind
|
||||
case isFalse => intro _; simp_all only [SPred.down_pure]; grind
|
||||
|
||||
theorem test_loop_break :
|
||||
⦃⌜‹Nat›ₛ = 42⌝⦄
|
||||
⦃fun s => ⌜s = 42⌝⦄
|
||||
breaking_loop
|
||||
⦃⇓ r => ⌜r > 4 ∧ ‹Nat›ₛ = 1⌝⦄ := by
|
||||
⦃⇓ r s => ⌜r > 4 ∧ s = 1⌝⦄ := by
|
||||
mvcgen [breaking_loop]
|
||||
case inv => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
|
||||
case pre1 => simp_all
|
||||
case isTrue => intro _; mleave; grind
|
||||
case isFalse => intro _; simp_all only [SVal.curry_nil]; grind
|
||||
case isFalse => intro _; simp_all only [SPred.down_pure]; grind
|
||||
case post.success =>
|
||||
simp_all
|
||||
rename_i h
|
||||
|
|
@ -617,7 +607,7 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) :
|
|||
match r.1 with
|
||||
| none => ⌜i ∈ xs.suff⌝
|
||||
| some b => ⌜b = false ∧ xs.suff = []⌝)
|
||||
all_goals simp_all; try grind
|
||||
all_goals simp_all [SPred.pure_nil]; try grind
|
||||
simp [ht] at hf
|
||||
|
||||
end Automated
|
||||
|
|
|
|||
|
|
@ -26,23 +26,10 @@ variable
|
|||
#check P ⊣⊢ₛ Q
|
||||
|
||||
|
||||
/-- info: ⌜φ⌝ : SVal [Nat, Char, Bool] (ULift Prop) -/
|
||||
/-- info: ⌜φ⌝ : SPred [Nat, Char, Bool] -/
|
||||
#guard_msgs in
|
||||
#check (⌜φ⌝ : SPred [Nat,Char,Bool])
|
||||
|
||||
-- TODO: Figure out how to delaborate away tuple below
|
||||
/--
|
||||
info: ⌜7 + ‹Nat›ₛ tuple = if ‹Bool›ₛ tuple = true then 13 else 7⌝ : SVal [Nat, Char, Bool] (ULift Prop)
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check (⌜7 + ‹Nat›ₛ = if ‹Bool›ₛ then 13 else 7⌝ : SPred [Nat,Char,Bool])
|
||||
|
||||
private abbrev theChar : SVal [Nat,Char,Bool] Char := fun _ c _ => c
|
||||
/-- info: ⌜#theChar tuple = 'a'⌝ : SVal [Nat, Char, Bool] (ULift Prop) -/
|
||||
#guard_msgs in
|
||||
#check ⌜#theChar = 'a'⌝
|
||||
|
||||
|
||||
/-- info: spred(P ∧ Q) : SPred [Nat, Char, Bool] -/
|
||||
#guard_msgs in
|
||||
#check spred(P ∧ Q)
|
||||
|
|
@ -144,7 +131,7 @@ private abbrev theChar : SVal [Nat,Char,Bool] Char := fun _ c _ => c
|
|||
info: if true = true then
|
||||
match (1, 2) with
|
||||
| (x, y) => Φ x y
|
||||
else ⌜False⌝ : SVal [Nat, Char, Bool] (ULift Prop)
|
||||
else ⌜False⌝ : SPred [Nat, Char, Bool]
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check spred(if true then term(match (1,2) with | (x,y) => Φ x y) else ⌜False⌝)
|
||||
|
|
@ -153,24 +140,5 @@ else ⌜False⌝ : SVal [Nat, Char, Bool] (ULift Prop)
|
|||
#guard_msgs in
|
||||
#check spred(Ψ (1 + 1))
|
||||
|
||||
|
||||
private abbrev theNat : SVal [Nat, Bool] Nat := fun n _ => n
|
||||
example (P Q : SPred [Nat, Bool]): SPred [Char, Nat, Bool] :=
|
||||
spred(fun c => ((∀ y, if y = 4 then ⌜y = #theNat⌝ ∧ P else Q) ∧ Q) → (∃ x, P → if (x : Bool) then Q else P))
|
||||
|
||||
-- A bigger example testing unexpansion as well: (TODO: Figure out how to delaborate away tuple below)
|
||||
/--
|
||||
info: fun P Q n =>
|
||||
spred((∀ y, if y = n then ⌜‹Nat›ₛ tuple + #theNat tuple = 4⌝ else Q) ∧ Q →
|
||||
P → ∃ x, P → if x = true then Q else P) : SPred [Nat, Bool] → SPred [Nat, Bool] → Char → SPred [Nat, Bool]
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check fun P Q => spred(fun (n : Char) => ((∀ y, if y = n then ⌜‹Nat›ₛ + #theNat = 4⌝ else Q) ∧ Q) → P → (∃ x, P → if (x : Bool) then Q else P))
|
||||
|
||||
-- Unexpansion should work irrespective of binder name for `f`/`escape`:
|
||||
/--
|
||||
info: ∀ (a b n o : Nat) (s : Nat × Nat), ⌜a = n ∧ b = o⌝ ⊢ₛ ⌜s.fst = n ∧ a = n + 1 ∧ b = o⌝ : Prop
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option linter.unusedVariables false in
|
||||
#check ∀ (a b n o : Nat) (s : Nat × Nat), (SVal.curry fun f => ULift.up (a = n ∧ b = o)) ⊢ₛ SVal.curry fun f => ULift.up (s.1 = n ∧ a = n + 1 ∧ b = o)
|
||||
spred(fun _ => ((∀ y, if y = 4 then (fun theNat => ⌜y = theNat⌝) ∧ P else Q) ∧ Q) → (∃ x, P → if (x : Bool) then Q else P))
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue