From 9a0c1ab2d02140eb537dcb407c52b0dcbf404c28 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 11 Aug 2025 10:32:16 +0200 Subject: [PATCH] feat: Simpler first-order implementation for pure `SPred`s (#9841) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/Lean/Elab/Tactic/Do/Attr.lean | 3 +- .../Elab/Tactic/Do/ProofMode/Exfalso.lean | 2 +- src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean | 7 +-- src/Lean/Elab/Tactic/Do/Spec.lean | 9 ++-- src/Std/Do/SPred/DerivedLaws.lean | 2 + src/Std/Do/SPred/Laws.lean | 22 +++++++- src/Std/Do/SPred/Notation.lean | 28 ++--------- src/Std/Do/SPred/SPred.lean | 15 ++++-- src/Std/Do/SPred/SVal.lean | 12 ++--- src/Std/Tactic/Do/Syntax.lean | 10 ++-- tests/lean/run/9365.lean | 4 +- tests/lean/run/9474.lean | 4 +- tests/lean/run/doLogicTests.lean | 50 ++++++++----------- tests/lean/run/spredNotation.lean | 38 ++------------ 14 files changed, 79 insertions(+), 127 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index 10f5976ba7..7a49f21a81 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -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 diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean index 85126ed5bf..01c1c6a7bf 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean @@ -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 diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean index 215a8c3821..75c73fa94c 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean @@ -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 diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean index bfe8200a71..a38c500652 100644 --- a/src/Lean/Elab/Tactic/Do/Spec.lean +++ b/src/Lean/Elab/Tactic/Do/Spec.lean @@ -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 diff --git a/src/Std/Do/SPred/DerivedLaws.lean b/src/Std/Do/SPred/DerivedLaws.lean index 281961709e..943ebe3ff8 100644 --- a/src/Std/Do/SPred/DerivedLaws.lean +++ b/src/Std/Do/SPred/DerivedLaws.lean @@ -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 diff --git a/src/Std/Do/SPred/Laws.lean b/src/Std/Do/SPred/Laws.lean index 20b32ce1d6..a07165ab7e 100644 --- a/src/Std/Do/SPred/Laws.lean +++ b/src/Std/Do/SPred/Laws.lean @@ -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 diff --git a/src/Std/Do/SPred/Notation.lean b/src/Std/Do/SPred/Notation.lean index d8c7b62f5a..cd76bfd40b 100644 --- a/src/Std/Do/SPred/Notation.lean +++ b/src/Std/Do/SPred/Notation.lean @@ -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] diff --git a/src/Std/Do/SPred/SPred.lean b/src/Std/Do/SPred/SPred.lean index de2d77f328..72eef379bb 100644 --- a/src/Std/Do/SPred/SPred.lean +++ b/src/Std/Do/SPred/SPred.lean @@ -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, *] diff --git a/src/Std/Do/SPred/SVal.lean b/src/Std/Do/SPred/SVal.lean index e6ae6df907..b292de5919 100644 --- a/src/Std/Do/SPred/SVal.lean +++ b/src/Std/Do/SPred/SVal.lean @@ -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 diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean index 7fcc6199f8..92c8ea3258 100644 --- a/src/Std/Tactic/Do/Syntax.lean +++ b/src/Std/Tactic/Do/Syntax.lean @@ -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] diff --git a/tests/lean/run/9365.lean b/tests/lean/run/9365.lean index 7dd70ffe18..a47196d742 100644 --- a/tests/lean/run/9365.lean +++ b/tests/lean/run/9365.lean @@ -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 diff --git a/tests/lean/run/9474.lean b/tests/lean/run/9474.lean index 9a98869c90..f377a1959c 100644 --- a/tests/lean/run/9474.lean +++ b/tests/lean/run/9474.lean @@ -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 diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean index 44c40dfaaa..ada9cd2996 100644 --- a/tests/lean/run/doLogicTests.lean +++ b/tests/lean/run/doLogicTests.lean @@ -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 diff --git a/tests/lean/run/spredNotation.lean b/tests/lean/run/spredNotation.lean index e05674e872..07ac2ebaa6 100644 --- a/tests/lean/run/spredNotation.lean +++ b/tests/lean/run/spredNotation.lean @@ -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))