From 0c5946ab3ffbcd156f8e022ce8abc6a7c52cb324 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 7 Jul 2025 15:11:41 +0200 Subject: [PATCH] feat: Make `Std.Do` universe polymorphic (#9194) This PR makes the logic and tactics of `Std.Do` universe polymorphic, at the cost of a few definitional properties arising from the switch from `Prop` to `ULift Prop` in the base case `SPred []`. Co-authored-by: Sebastian Graf --- src/Init/Prelude.lean | 3 + src/Init/Tactics.lean | 2 +- src/Lean/Elab/Tactic/Do/Attr.lean | 4 +- .../Elab/Tactic/Do/ProofMode/Assumption.lean | 14 +- src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean | 13 +- src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean | 90 ++++----- src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean | 2 +- .../Elab/Tactic/Do/ProofMode/Constructor.lean | 4 +- src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean | 13 +- src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean | 8 +- .../Elab/Tactic/Do/ProofMode/Exfalso.lean | 8 +- src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean | 28 +-- src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean | 12 +- src/Lean/Elab/Tactic/Do/ProofMode/Have.lean | 16 +- src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean | 8 +- .../Elab/Tactic/Do/ProofMode/LeftRight.lean | 4 +- src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean | 50 ++--- src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean | 7 +- src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean | 6 +- src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean | 4 +- .../Elab/Tactic/Do/ProofMode/Specialize.lean | 70 +++---- src/Lean/Elab/Tactic/Do/Spec.lean | 61 +++--- src/Lean/Elab/Tactic/Do/Syntax.lean | 17 +- src/Lean/Elab/Tactic/Do/VCGen.lean | 3 +- src/Std/Do/PostCond.lean | 48 ++--- src/Std/Do/PredTrans.lean | 40 ++-- src/Std/Do/SPred/DerivedLaws.lean | 92 ++++----- src/Std/Do/SPred/Laws.lean | 82 +++++--- src/Std/Do/SPred/Notation.lean | 4 +- src/Std/Do/SPred/SPred.lean | 99 +++++----- src/Std/Do/SPred/SVal.lean | 36 ++-- src/Std/Do/Triple/Basic.lean | 10 +- src/Std/Do/Triple/SpecLemmas.lean | 33 ++-- src/Std/Do/WP/Basic.lean | 23 +-- src/Std/Do/WP/Monad.lean | 6 +- src/Std/Do/WP/SimpLemmas.lean | 14 +- src/Std/Tactic/Do/ProofMode.lean | 2 +- src/Std/Tactic/Do/Syntax.lean | 1 + tests/lean/run/bhaviksSampler.lean | 2 +- tests/lean/run/doLogicTests.lean | 185 ++++++++++-------- tests/lean/run/spredNotation.lean | 10 +- 41 files changed, 603 insertions(+), 531 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 783c6a6dc0..68e7b9003e 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -886,6 +886,9 @@ theorem ULift.up_down {α : Type u} (b : ULift.{v} α) : Eq (up (down b)) b := r /-- Bijection between `α` and `ULift.{v} α` -/ theorem ULift.down_up {α : Type u} (a : α) : Eq (down (up.{v} a)) a := rfl +instance [Inhabited α] : Inhabited (ULift α) where + default := ULift.up default + /-- Either a proof that `p` is true or a proof that `p` is false. This is equivalent to a `Bool` paired with a proof that the `Bool` is `true` if and only if `p` is true. diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 1fcee5e811..09edb46fc5 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -2117,7 +2117,7 @@ the verification conditions `?pre : H ⊢ₛ P` and `?post : Q ⊢ₚ Q'`. success and failure continuations. * `?pre` and `?post.*` goals introduce their stateful hypothesis as `h`. * Any uninstantiated MVar arising from instantiation of `foo_spec` becomes a new subgoal. -* If the goal looks like `fun s => _ ⊢ₛ _` then `mspec` will first `mintro ∀s`. +* If the target of the stateful goal looks like `fun s => _` then `mspec` will first `mintro ∀s`. * If `P` has schematic variables that can be instantiated by doing `mintro ∀s`, for example `foo_spec : ∀(n:Nat), ⦃⌜n = ‹Nat›ₛ⌝⦄ foo ⦃Q⦄`, then `mspec` will do `mintro ∀s` first to instantiate `n = s`. diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean index b6aab84c90..daeb71b199 100644 --- a/src/Lean/Elab/Tactic/Do/Attr.lean +++ b/src/Lean/Elab/Tactic/Do/Attr.lean @@ -162,12 +162,12 @@ private def mkSpecTheorem (type : Expr) (proof : SpecProof) (prio : Nat) : MetaM withNewMCtxDepth do let (xs, _, type) ← withSimpGlobalConfig (forallMetaTelescopeReducing type) let type ← whnfR type - let_expr Triple _m ps _inst _α prog P _Q := type + let_expr c@Triple _m ps _inst _α prog P _Q := type | throwError "unexpected kind of spec theorem; not a triple{indentExpr type}" let keys ← DiscrTree.mkPath prog (noIndexAtArgs := false) -- beta potential of `P` describes how many times we want to `mintro ∀s`, that is, -- *eta*-expand the goal. - let σs := mkApp (mkConst ``PostShape.args) ps + let σs := mkApp (mkConst ``PostShape.args [c.constLevels![0]!]) ps let etaPotential ← computeMVarBetaPotentialForSPred xs σs P -- logInfo m!"Beta potential {etaPotential} for {P}" -- logInfo m!"mkSpecTheorem: {keys}, proof: {proof}" diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean index cea24e78dc..56c2ca202f 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Assumption.lean @@ -18,20 +18,20 @@ partial def MGoal.assumption (goal : MGoal) : OptionT MetaM Expr := do failure if let some hyp := parseHyp? goal.hyps then guard (← isDefEq hyp.p goal.target) - return mkApp2 (mkConst ``SPred.entails.refl) goal.σs hyp.p - if let some (σs, lhs, rhs) := parseAnd? goal.hyps then + return mkApp2 (mkConst ``SPred.entails.refl [goal.u]) goal.σs hyp.p + if let some (u, σs, lhs, rhs) := parseAnd? goal.hyps then -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Display). - mkApp5 (mkConst ``Assumption.right) σs lhs rhs goal.target <$> assumption { goal with hyps := rhs } + mkApp5 (mkConst ``Assumption.right [u]) σs lhs rhs goal.target <$> assumption { goal with hyps := rhs } <|> - mkApp5 (mkConst ``Assumption.left) σs lhs rhs goal.target <$> assumption { goal with hyps := lhs } + mkApp5 (mkConst ``Assumption.left [u]) σs lhs rhs goal.target <$> assumption { goal with hyps := lhs } else panic! s!"assumption: hypothesis without proper metadata: {goal.hyps}" def MGoal.assumptionPure (goal : MGoal) : OptionT MetaM Expr := do - let φ := mkApp2 (mkConst ``tautological) goal.σs goal.target + let φ := mkApp2 (mkConst ``tautological [goal.u]) goal.σs goal.target let fvarId ← OptionT.mk (findLocalDeclWithType? φ) - let inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ goal.σs goal.target) - return mkApp6 (mkConst ``Exact.from_tautology) φ goal.σs goal.hyps goal.target inst (.fvar fvarId) + let inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology [goal.u]) φ goal.σs goal.target) + return mkApp6 (mkConst ``Exact.from_tautology [goal.u]) goal.σs φ goal.hyps goal.target inst (.fvar fvarId) @[builtin_tactic Lean.Parser.Tactic.massumption] def elabMAssumption : Tactic | _ => do diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean index af281fe93e..6db7085a59 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean @@ -21,12 +21,13 @@ def mStart (goal : Expr) : MetaM MStartResult := do if let some mgoal := parseMGoal? goal then return { goal := mgoal } - let listType := mkApp (mkConst ``List [.succ .zero]) (mkSort (.succ .zero)) - let σs ← mkFreshExprMVar listType - let P ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs) - let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology) goal σs P) - let prf := mkApp4 (mkConst ``ProofMode.start_entails) σs P goal inst - let goal : MGoal := { σs, hyps := emptyHyp σs, target := ← instantiateMVars P } + let u ← mkFreshLevelMVar + let σs ← mkFreshExprMVar (σs.mkType u) + let P ← mkFreshExprMVar (mkApp (mkConst ``SPred [u]) σs) + let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology [u]) goal σs P) + let u ← instantiateLevelMVars u + let prf := mkApp4 (mkConst ``ProofMode.start_entails [u]) σs P goal inst + let goal : MGoal := { u, σs, hyps := emptyHyp u σs, target := ← instantiateMVars P } return { goal, proof? := some prf } def mStartMVar (mvar : MVarId) : MetaM (MVarId × MGoal) := mvar.withContext do diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean index 50d521af72..e18af97b1a 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean @@ -17,30 +17,30 @@ open Lean Elab Tactic Meta initialize registerTraceClass `Meta.Tactic.Do.cases -- Given σs and H, produces H₁, H₂ and a proof that H₁ ∧ H₂ ⊣⊢ₛ H. -def synthIsAnd (σs H : Expr) : OptionT MetaM (Expr × Expr × Expr) := do - if let some (_σs, H₁, H₂) := parseAnd? H.consumeMData then - return (H₁, H₂, mkApp2 (mkConst ``SPred.bientails.refl) σs H) +def synthIsAnd (u : Level) (σs H : Expr) : OptionT MetaM (Expr × Expr × Expr) := do + if let some (_u, _σs, H₁, H₂) := parseAnd? H.consumeMData then + return (H₁, H₂, mkApp2 (mkConst ``SPred.bientails.refl [u]) σs H) try - let H₁ ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs) - let H₂ ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs) - let inst ← synthInstance (mkApp4 (mkConst ``IsAnd) σs H H₁ H₂) - return (H₁, H₂, mkApp5 (mkConst ``IsAnd.to_and) σs H H₁ H₂ inst) + let H₁ ← mkFreshExprMVar (mkApp (mkConst ``SPred [u]) σs) + let H₂ ← mkFreshExprMVar (mkApp (mkConst ``SPred [u]) σs) + let inst ← synthInstance (mkApp4 (mkConst ``IsAnd [u]) σs H H₁ H₂) + return (H₁, H₂, mkApp5 (mkConst ``IsAnd.to_and [u]) σs H H₁ H₂ inst) catch _ => failure -- Produce a proof for Q ∧ H ⊢ₛ T by opening a new goal P ⊢ₛ T, where P ⊣⊢ₛ Q ∧ H. -def mCasesAddGoal (goals : IO.Ref (Array MVarId)) (σs : Expr) (T : Expr) (Q : Expr) (H : Expr) : MetaM (Unit × MGoal × Expr) := do - let (P, hand) := mkAnd σs Q H +def mCasesAddGoal (u : Level) (goals : IO.Ref (Array MVarId)) (σs : Expr) (T : Expr) (Q : Expr) (H : Expr) : MetaM (Unit × MGoal × Expr) := do + let (P, hand) := mkAnd u σs Q H -- hand : Q ∧ H ⊣⊢ₛ P -- Need to produce a proof that P ⊢ₛ T and return res - let goal : MGoal := { σs := σs, hyps := P, target := T } + let goal : MGoal := { u := u, σs := σs, hyps := P, target := T } let m ← mkFreshExprSyntheticOpaqueMVar goal.toExpr goals.modify (·.push m.mvarId!) - let prf := mkApp7 (mkConst ``SCases.add_goal) σs P Q H T hand m - let goal := { goal with hyps := mkAnd! σs Q H } + let prf := mkApp7 (mkConst ``Cases.add_goal [u]) σs P Q H T hand m + let goal := { goal with hyps := mkAnd! u σs Q H } return ((), goal, prf) private def getQH (goal : MGoal) : MetaM (Expr × Expr) := do - let some (_, Q, H) := parseAnd? goal.hyps | throwError m!"Internal error: Hypotheses not a conjunction {goal.hyps}" + let some (_, _, Q, H) := parseAnd? goal.hyps | throwError m!"Internal error: Hypotheses not a conjunction {goal.hyps}" return (Q, H) -- Pretty much like sPureCore, but for existential quantifiers. @@ -57,8 +57,8 @@ def mCasesExists (H : Expr) (name : TSyntax ``binderIdent) let (r, goal, prf /- : goal.toExpr -/) ← k x let (Q, _) ← getQH goal let u ← getLevel α - let prf := mkApp6 (mkConst ``SCases.exists [u]) α σs Q ψ goal.target (← mkLambdaFVars #[x] prf) - let goal := { goal with hyps := mkAnd! σs Q H } + let prf := mkApp6 (mkConst ``Cases.exists [goal.u, u]) σs α Q ψ goal.target (← mkLambdaFVars #[x] prf) + let goal := { goal with hyps := mkAnd! goal.u σs Q H } return (r, goal, prf) -- goal is P ⊢ₛ T @@ -71,16 +71,16 @@ def mCasesExists (H : Expr) (name : TSyntax ``binderIdent) -- and finally the caller builds the proof for -- P ⊢ₛ Q ∧ H ⊢ₛ T -- by unfocussing. -partial def mCasesCore (σs : Expr) (H : Expr) (pat : MCasesPat) (k : Expr → MetaM (α × MGoal × Expr)): MetaM (α × MGoal × Expr) := +partial def mCasesCore (u : Level) (σs : Expr) (H : Expr) (pat : MCasesPat) (k : Expr → MetaM (α × MGoal × Expr)): MetaM (α × MGoal × Expr) := match pat with | .clear => do - let H' := emptyHyp σs -- H' = ⌜True⌝ + let H' := emptyHyp u σs -- H' = ⌜True⌝ let (a, goal, prf) ← k H' let (Q, _H) ← getQH goal -- prf : Q ∧ ⌜True⌝ ⊢ₛ T -- Then Q ∧ H ⊢ₛ Q ∧ ⌜True⌝ ⊢ₛ T - let prf := mkApp5 (mkConst ``SCases.clear) σs Q H goal.target prf - let goal := { goal with hyps := mkAnd! σs Q H } + let prf := mkApp5 (mkConst ``Cases.clear [u]) σs Q H goal.target prf + let goal := { goal with hyps := mkAnd! u σs Q H } return (a, goal, prf) | .stateful name => do let (name, ref) ← getFreshHypName name @@ -92,12 +92,12 @@ partial def mCasesCore (σs : Expr) (H : Expr) (pat : MCasesPat) (k : Expr → M mPureCore σs H name fun _ _hφ => do -- This case is very similar to the clear case, but we need to -- return Q ⊢ₛ T, not Q ∧ H ⊢ₛ T. - let H' := emptyHyp σs -- H' = ⌜True⌝ + let H' := emptyHyp u σs -- H' = ⌜True⌝ let (a, goal, prf) ← k H' let (Q, _H) ← getQH goal -- prf : Q ∧ ⌜True⌝ ⊢ₛ T -- Then Q ⊢ₛ Q ∧ ⌜True⌝ ⊢ₛ T - let prf := mkApp4 (mkConst ``SCases.pure) σs Q goal.target prf + let prf := mkApp4 (mkConst ``Cases.pure [u]) σs Q goal.target prf let goal := { goal with hyps := Q } return (a, goal, prf) -- Now prf : Q ∧ H ⊢ₛ T (where H is ⌜φ⌝). Exactly what is needed. @@ -105,15 +105,15 @@ partial def mCasesCore (σs : Expr) (H : Expr) (pat : MCasesPat) (k : Expr → M try -- First try to see if H can be introduced as a pure hypothesis let φ ← mkFreshExprMVar (mkSort .zero) - let _ ← synthInstance (mkApp3 (mkConst ``IsPure) σs H φ) - mCasesCore σs H (.pure name) k + let _ ← synthInstance (mkApp3 (mkConst ``IsPure [u]) σs H φ) + mCasesCore u σs H (.pure name) k catch _ => -- Otherwise introduce it as a stateful hypothesis. - mCasesCore σs H (.stateful name) k - | .tuple [] => mCasesCore σs H .clear k - | .tuple [p] => mCasesCore σs H p k + mCasesCore u σs H (.stateful name) k + | .tuple [] => mCasesCore u σs H .clear k + | .tuple [p] => mCasesCore u σs H p k | .tuple (p :: ps) => do - if let some (H₁, H₂, hand) ← synthIsAnd σs H then + if let some (H₁, H₂, hand) ← synthIsAnd u σs H then -- goal is Q ∧ H ⊢ₛ T, where `hand : H ⊣⊢ₛ H₁ ∧ H₂`. Plan: -- 1. Recurse on H₁ and H₂. -- 2. The inner callback sees H₁' and H₂' and calls k on H₁₂', where H₁₂' = mkAnd H₁' H₂' @@ -123,29 +123,29 @@ partial def mCasesCore (σs : Expr) (H : Expr) (pat : MCasesPat) (k : Expr → M -- 6. The outer callback reassociates and returns (Q ∧ H₂) ∧ H₁' ⊢ₛ T -- 7. The top-level receives (Q ∧ H₂) ∧ H₁ ⊢ₛ T -- 8. Reassociate to Q ∧ (H₁ ∧ H₂) ⊢ₛ T, rebuild Q ∧ H ⊢ₛ T and return it. - let ((a, Q), goal, prf) ← mCasesCore σs H₁ p fun H₁' => do - let ((a, Q), goal, prf) ← mCasesCore σs H₂ (.tuple ps) fun H₂' => do - let (H₁₂', hand') := mkAnd σs H₁' H₂' + let ((a, Q), goal, prf) ← mCasesCore u σs H₁ p fun H₁' => do + let ((a, Q), goal, prf) ← mCasesCore u σs H₂ (.tuple ps) fun H₂' => do + let (H₁₂', hand') := mkAnd u σs H₁' H₂' let (a, goal, prf) ← k H₁₂' -- (2) -- (3) prf : Q ∧ H₁₂' ⊢ₛ T -- (4) refocus to (Q ∧ H₁') ∧ H₂' let (Q, _H) ← getQH goal let T := goal.target - let prf := mkApp8 (mkConst ``SCases.and_1) σs Q H₁' H₂' H₁₂' T hand' prf + let prf := mkApp8 (mkConst ``Cases.and_1 [u]) σs Q H₁' H₂' H₁₂' T hand' prf -- check prf - let QH₁' := mkAnd! σs Q H₁' - let goal := { goal with hyps := mkAnd! σs QH₁' H₂' } + let QH₁' := mkAnd! u σs Q H₁' + let goal := { goal with hyps := mkAnd! u σs QH₁' H₂' } return ((a, Q), goal, prf) -- (5) prf : (Q ∧ H₁') ∧ H₂ ⊢ₛ T -- (6) refocus to prf : (Q ∧ H₂) ∧ H₁' ⊢ₛ T - let prf := mkApp6 (mkConst ``SCases.and_2) σs Q H₁' H₂ goal.target prf - let QH₂ := mkAnd! σs Q H₂ - let goal := { goal with hyps := mkAnd! σs QH₂ H₁' } + let prf := mkApp6 (mkConst ``Cases.and_2 [u]) σs Q H₁' H₂ goal.target prf + let QH₂ := mkAnd! u σs Q H₂ + let goal := { goal with hyps := mkAnd! u σs QH₂ H₁' } return ((a, Q), goal, prf) -- (7) prf : (Q ∧ H₂) ∧ H₁ ⊢ₛ T -- (8) rearrange to Q ∧ H ⊢ₛ T - let prf := mkApp8 (mkConst ``SCases.and_3) σs Q H₁ H₂ H goal.target hand prf - let goal := { goal with hyps := mkAnd! σs Q H } + let prf := mkApp8 (mkConst ``Cases.and_3 [u]) σs Q H₁ H₂ H goal.target hand prf + let goal := { goal with hyps := mkAnd! u σs Q H } return (a, goal, prf) else if let some (_α, σs, ψ) := H.consumeMData.app3? ``SPred.exists then let .one n := p @@ -154,21 +154,21 @@ partial def mCasesCore (σs : Expr) (H : Expr) (pat : MCasesPat) (k : Expr → M -- 1. Recurse on ψ n where (n : α) is named according to the head pattern p. -- 2. Receive a proof for Q ∧ ψ n ⊢ₛ T. -- 3. Build a proof for Q ∧ (∃ x, ψ x) ⊢ₛ T from it (in sCasesExists). - mCasesExists H n fun x => mCasesCore σs (ψ.betaRev #[x]) (.alts ps) k + mCasesExists H n fun x => mCasesCore u σs (ψ.betaRev #[x]) (.alts ps) k else throwError "Neither a conjunction nor an existential quantifier {H}" | .alts [] => throwUnsupportedSyntax - | .alts [p] => mCasesCore σs H p k + | .alts [p] => mCasesCore u σs H p k | .alts (p :: ps) => do let some (σs, H₁, H₂) := H.consumeMData.app3? ``SPred.or | throwError "Not a disjunction {H}" -- goal is Q ∧ (H₁ ∨ H₂) ⊢ₛ T. Plan: -- 1. Recurse on H₁ and H₂ with the same k. -- 2. Receive proofs for Q ∧ H₁ ⊢ₛ T and Q ∧ H₂ ⊢ₛ T. -- 3. Build a proof for Q ∧ (H₁ ∨ H₂) ⊢ₛ T from them. - let (_a, goal₁, prf₁) ← mCasesCore σs H₁ p k - let (a, _goal₂, prf₂) ← mCasesCore σs H₂ (.alts ps) k + let (_a, goal₁, prf₁) ← mCasesCore u σs H₁ p k + let (a, _goal₂, prf₂) ← mCasesCore u σs H₂ (.alts ps) k let (Q, _H₁) ← getQH goal₁ - let goal := { goal₁ with hyps := mkAnd! σs Q (mkApp3 (mkConst ``SPred.or) σs H₁ H₂) } - let prf := mkApp7 (mkConst ``SPred.and_or_elim_r) σs Q H₁ H₂ goal.target prf₁ prf₂ + let goal := { goal₁ with hyps := mkAnd! u σs Q (mkApp3 (mkConst ``SPred.or [u]) σs H₁ H₂) } + let prf := mkApp7 (mkConst ``SPred.and_or_elim_r [u]) σs Q H₁ H₂ goal.target prf₁ prf₂ return (a, goal, prf) private theorem assembled_proof {σs} {P P' Q H H' T : SPred σs} @@ -196,7 +196,7 @@ def elabMCases : Tactic let Q := focus.restHyps let H := focus.focusHyp let goals ← IO.mkRef #[] - let (_, _new_goal, prf) ← mCasesCore goal.σs H pat (mCasesAddGoal goals goal.σs goal.target Q) + let (_, _new_goal, prf) ← mCasesCore goal.u goal.σs H pat (mCasesAddGoal goal.u goals goal.σs goal.target Q) -- Now prf : Q ∧ H ⊢ₛ T. Prepend hfocus.mp, done. let prf := focus.rewriteHyps goal prf diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean index d60c576af3..31dea56e16 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Clear.lean @@ -22,7 +22,7 @@ def elabMClear : Tactic let res ← goal.focusHypWithInfo hyp let m ← mkFreshExprSyntheticOpaqueMVar (res.restGoal goal).toExpr - mvar.assign (mkApp7 (mkConst ``Clear.clear) goal.σs goal.hyps + mvar.assign (mkApp7 (mkConst ``Clear.clear [goal.u]) goal.σs goal.hyps res.restHyps res.focusHyp goal.target res.proof m) replaceMainGoal [m.mvarId!] | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Constructor.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Constructor.lean index 4a6fb1d183..d7fe93618e 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Constructor.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Constructor.lean @@ -15,11 +15,11 @@ def mConstructorCore (mvar : MVarId) : MetaM (MVarId × MVarId) := do let g ← instantiateMVars <| ← mvar.getType let some goal := parseMGoal? g | throwError "not in proof mode" - let mkApp3 (.const ``SPred.and []) σs L R := goal.target | throwError "target is not SPred.and" + let mkApp3 (.const ``SPred.and _) σs L R := goal.target | throwError "target is not SPred.and" let leftGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := L}.toExpr let rightGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := R}.toExpr - mvar.assign (mkApp6 (mkConst ``SPred.and_intro) σs goal.hyps L R leftGoal rightGoal) + mvar.assign (mkApp6 (mkConst ``SPred.and_intro [goal.u]) σs goal.hyps L R leftGoal rightGoal) return (leftGoal.mvarId!, rightGoal.mvarId!) @[builtin_tactic Lean.Parser.Tactic.mconstructor] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean index a220826dd0..b1f0b3b821 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean @@ -13,19 +13,14 @@ open Lean Expr Meta PrettyPrinter Delaborator SubExpr @[builtin_delab app.Std.Tactic.Do.MGoalEntails] private partial def delabMGoal : Delab := do - let expr ← instantiateMVars <| ← getExpr - - -- extract environment - let some goal := parseMGoal? expr | failure - -- delaborate - let (_, hyps) ← withAppFn ∘ withAppArg <| delabHypotheses goal.σs ({}, #[]) + let (_, hyps) ← withAppFn ∘ withAppArg <| delabHypotheses ({}, #[]) let target ← SPred.Notation.unpack (← withAppArg <| delab) -- build syntax return ⟨← `(Std.Tactic.Do.mgoalStx| $hyps.reverse* ⊢ₛ $target:term)⟩ where - delabHypotheses (σs : Expr) + delabHypotheses (acc : NameMap Nat × Array (TSyntax ``mgoalHyp)) : DelabM (NameMap Nat × Array (TSyntax ``mgoalHyp)) := do let hyps ← getExpr @@ -42,8 +37,8 @@ where let stx ← `(Std.Tactic.Do.mgoalHyp| $name' : $(← SPred.Notation.unpack (← withMDataExpr <| delab))) return (map.insert hyp.name idx, lines.push stx) if (parseAnd? hyps).isSome then - let acc_rhs ← withAppArg <| delabHypotheses σs acc - let acc_lhs ← withAppFn ∘ withAppArg <| delabHypotheses σs acc_rhs + let acc_rhs ← withAppArg <| delabHypotheses acc + let acc_lhs ← withAppFn ∘ withAppArg <| delabHypotheses acc_rhs return acc_lhs else failure diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean index 09cd5d998d..01dd1650d5 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean @@ -16,7 +16,7 @@ def _root_.Lean.Elab.Tactic.Do.ProofMode.MGoal.exact (goal : MGoal) (hyp : Synta if goal.findHyp? hyp.getId |>.isNone then failure let focusRes ← goal.focusHypWithInfo ⟨hyp⟩ OptionT.mk do - let proof := mkApp5 (mkConst ``Exact.assumption) goal.σs goal.hyps focusRes.restHyps goal.target focusRes.proof + let proof := mkApp5 (mkConst ``Exact.assumption [goal.u]) goal.σs goal.hyps focusRes.restHyps goal.target focusRes.proof unless ← isDefEq focusRes.focusHyp goal.target do throwError "mexact tactic failed, hypothesis {hyp} is not definitionally equal to {goal.target}" return proof @@ -24,10 +24,10 @@ def _root_.Lean.Elab.Tactic.Do.ProofMode.MGoal.exact (goal : MGoal) (hyp : Synta def _root_.Lean.Elab.Tactic.Do.ProofMode.MGoal.exactPure (goal : MGoal) (hyp : Syntax) : TacticM Expr := do let φ ← mkFreshExprMVar (mkSort .zero) let h ← elabTermEnsuringType hyp φ - let P ← mkFreshExprMVar (mkApp (mkConst ``SPred) goal.σs) - let some inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ goal.σs P) + let P ← mkFreshExprMVar (mkApp (mkConst ``SPred [goal.u]) goal.σs) + let some inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology [goal.u]) φ goal.σs P) | throwError "mexact tactic failed, {hyp} is not an SPred tautology" - return mkApp6 (mkConst ``Exact.from_tautology) φ goal.σs goal.hyps goal.target inst h + return mkApp6 (mkConst ``Exact.from_tautology [goal.u]) goal.σs φ goal.hyps goal.target inst h @[builtin_tactic Lean.Parser.Tactic.mexact] def elabMExact : Tactic diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean index 6d4b5391b9..9e83844f4e 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Exfalso.lean @@ -15,8 +15,8 @@ open Lean Elab Tactic Meta -- set_option pp.all true in -- #check ⌜False⌝ -private def falseProp (σs : Expr) : Expr := -- ⌜False⌝ standing in for an empty conjunction of hypotheses - mkApp3 (mkConst ``SVal.curry) (.sort .zero) σs <| mkLambda `escape .default (mkApp (mkConst ``SVal.StateTuple) σs) (mkConst ``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)) @[builtin_tactic Lean.Parser.Tactic.mexfalso] def elabMExfalso : Tactic | _ => do @@ -24,8 +24,8 @@ def elabMExfalso : Tactic | _ => do mvar.withContext do let g ← instantiateMVars <| ← mvar.getType let some goal := parseMGoal? g | throwError "not in proof mode" - let newGoal := { goal with target := falseProp goal.σs } + let newGoal := { goal with target := falseProp goal.u goal.σs } let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr - let prf := mkApp4 (mkConst ``SPred.exfalso) goal.σs goal.hyps goal.target m + let prf := mkApp4 (mkConst ``SPred.exfalso [goal.u]) goal.σs goal.hyps goal.target m mvar.assign prf replaceMainGoal [m.mvarId!] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean index f7dd15e0f7..0534e1cfd0 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean @@ -21,43 +21,43 @@ structure FocusResult where proof : Expr deriving Inhabited -partial def focusHyp (σs : Expr) (e : Expr) (name : Name) : Option FocusResult := do +partial def focusHyp (u : Level) (σs : Expr) (e : Expr) (name : Name) : Option FocusResult := do if let some hyp := parseHyp? e then if hyp.name = name then - return ⟨e, emptyHyp σs, mkApp2 (mkConst ``Focus.this) σs e⟩ + return ⟨e, emptyHyp u σs, mkApp2 (mkConst ``Focus.this [u]) σs e⟩ else none - else if let some (σs, lhs, rhs) := parseAnd? e then + else if let some (u, σs, lhs, rhs) := parseAnd? e then try -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Delab). - let ⟨focus, rhs', h₁⟩ ← focusHyp σs rhs name - let ⟨C, h₂⟩ := mkAnd σs lhs rhs' - return ⟨focus, C, mkApp8 (mkConst ``Focus.right) σs lhs rhs rhs' C focus h₁ h₂⟩ + let ⟨focus, rhs', h₁⟩ ← focusHyp u σs rhs name + let ⟨C, h₂⟩ := mkAnd u σs lhs rhs' + return ⟨focus, C, mkApp8 (mkConst ``Focus.right [u]) σs lhs rhs rhs' C focus h₁ h₂⟩ catch _ => - let ⟨focus, lhs', h₁⟩ ← focusHyp σs lhs name - let ⟨C, h₂⟩ := mkAnd σs lhs' rhs - return ⟨focus, C, mkApp8 (mkConst ``Focus.left) σs lhs lhs' rhs C focus h₁ h₂⟩ + let ⟨focus, lhs', h₁⟩ ← focusHyp u σs lhs name + let ⟨C, h₂⟩ := mkAnd u σs lhs' rhs + return ⟨focus, C, mkApp8 (mkConst ``Focus.left [u]) σs lhs lhs' rhs C focus h₁ h₂⟩ else if let some _ := parseEmptyHyp? e then none else panic! s!"focusHyp: hypothesis without proper metadata: {e}" def MGoal.focusHyp (goal : MGoal) (name : Name) : Option FocusResult := - Lean.Elab.Tactic.Do.ProofMode.focusHyp goal.σs goal.hyps name + Lean.Elab.Tactic.Do.ProofMode.focusHyp goal.u goal.σs goal.hyps name -def FocusResult.refl (σs : Expr) (restHyps : Expr) (focusHyp : Expr) : FocusResult := - let proof := mkApp2 (mkConst ``SPred.bientails.refl) σs (mkAnd! σs restHyps focusHyp) +def FocusResult.refl (u : Level) (σs : Expr) (restHyps : Expr) (focusHyp : Expr) : FocusResult := + let proof := mkApp2 (mkConst ``SPred.bientails.refl [u]) σs (mkAnd! u σs restHyps focusHyp) { restHyps, focusHyp, proof } def FocusResult.restGoal (res : FocusResult) (goal : MGoal) : MGoal := { goal with hyps := res.restHyps } def FocusResult.recombineGoal (res : FocusResult) (goal : MGoal) : MGoal := - { goal with hyps := mkAnd! goal.σs res.restHyps res.focusHyp } + { goal with hyps := mkAnd! goal.u goal.σs res.restHyps res.focusHyp } /-- Turn a proof for `(res.recombineGoal goal).toExpr` into one for `goal.toExpr`. -/ def FocusResult.rewriteHyps (res : FocusResult) (goal : MGoal) : Expr → Expr := - mkApp6 (mkConst ``Focus.rewrite_hyps) goal.σs goal.hyps (mkAnd! goal.σs res.restHyps res.focusHyp) goal.target res.proof + mkApp6 (mkConst ``Focus.rewrite_hyps [goal.u]) goal.σs goal.hyps (mkAnd! goal.u goal.σs res.restHyps res.focusHyp) goal.target res.proof def MGoal.focusHypWithInfo (goal : MGoal) (name : Ident) : MetaM FocusResult := do let some res := goal.focusHyp name.getId | throwError "unknown hypothesis '{name}'" diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean index bc059c2511..c0619be6e0 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Frame.lean @@ -21,7 +21,7 @@ partial def transferHypNames (P P' : Expr) : MetaM Expr := (·.snd) <$> label (c collectHyps (P : Expr) (acc : List Hyp := []) : List Hyp := if let some hyp := parseHyp? P then hyp :: acc - else if let some (_, L, R) := parseAnd? P then + else if let some (_, _, L, R) := parseAnd? P then collectHyps L (collectHyps R acc) else acc @@ -30,10 +30,10 @@ partial def transferHypNames (P P' : Expr) : MetaM Expr := (·.snd) <$> label (c let P' ← instantiateMVarsIfMVarApp P' if let some _ := parseEmptyHyp? P' then return (Ps, P') - if let some (σs, L, R) := parseAnd? P' then + if let some (u, σs, L, R) := parseAnd? P' then let (Ps, L') ← label Ps L let (Ps, R') ← label Ps R - return (Ps, mkAnd! σs L' R') + return (Ps, mkAnd! u σs L' R') else let mut Ps' := Ps repeat @@ -50,8 +50,8 @@ def mFrameCore [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (kFail : m (α × Expr)) (kSuccess : Expr /-φ:Prop-/ → Expr /-h:φ-/ → MGoal → m (α × Expr)) : m (α × Expr) := do let P := goal.hyps let φ ← mkFreshExprMVar (mkSort .zero) - let P' ← mkFreshExprMVar (mkApp (mkConst ``SPred) goal.σs) - if let some inst ← synthInstance? (mkApp4 (mkConst ``HasFrame) goal.σs P P' φ) then + let P' ← mkFreshExprMVar (mkApp (mkConst ``SPred [goal.u]) goal.σs) + if let some inst ← synthInstance? (mkApp4 (mkConst ``HasFrame [goal.u]) goal.σs P P' φ) then if ← isDefEq (mkConst ``True) φ then return (← kFail) -- copy the name of P to P' if it is a named hypothesis let P' ← transferHypNames P P' @@ -59,7 +59,7 @@ def mFrameCore [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] withLocalDeclD `h φ fun hφ => do let (a, prf) ← kSuccess φ hφ goal let prf ← mkLambdaFVars #[hφ] prf - let prf := mkApp7 (mkConst ``Frame.frame) goal.σs P P' goal.target φ inst prf + let prf := mkApp7 (mkConst ``Frame.frame [goal.u]) goal.σs P P' goal.target φ inst prf return (a, prf) else kFail diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Have.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Have.lean index e96ecec14f..0f4fe4bd5f 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Have.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Have.lean @@ -26,9 +26,9 @@ def elabMDup : Tactic addHypInfo h goal.σs hyp (isBinder := true) let H' := hyp.toExpr let T := goal.target - let newGoal := { goal with hyps := mkAnd! goal.σs P H' } + let newGoal := { goal with hyps := mkAnd! goal.u goal.σs P H' } let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr - mvar.assign (mkApp7 (mkConst ``Have.dup) goal.σs P Q H T res.proof m) + mvar.assign (mkApp7 (mkConst ``Have.dup [goal.u]) goal.σs P Q H T res.proof m) replaceMainGoal [m.mvarId!] | _ => throwUnsupportedSyntax @@ -39,7 +39,7 @@ def elabMHave : Tactic mvar.withContext do -- build goal `P ⊢ₛ T` from `P ⊢ₛ H` and residual goal `P ∧ H ⊢ₛ T` let P := goal.hyps - let spred := mkApp (mkConst ``SPred) goal.σs + let spred := mkApp (mkConst ``SPred [goal.u]) goal.σs let H ← match ty? with | some ty => elabTerm ty spred | _ => mkFreshExprMVar spred @@ -48,12 +48,12 @@ def elabMHave : Tactic addHypInfo h goal.σs hyp (isBinder := true) let H := hyp.toExpr let T := goal.target - let (PH, hand) := mkAnd goal.σs P H + let (PH, hand) := mkAnd goal.u goal.σs P H let haveGoal := { goal with target := H } let hhave ← elabTermEnsuringType rhs haveGoal.toExpr let newGoal := { goal with hyps := PH } let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr - mvar.assign (mkApp8 (mkConst ``Have.have) goal.σs P H PH T hand hhave m) + mvar.assign (mkApp8 (mkConst ``Have.have [goal.u]) goal.σs P H PH T hand hhave m) replaceMainGoal [m.mvarId!] | _ => throwUnsupportedSyntax @@ -67,7 +67,7 @@ def elabMReplace : Tactic let some res := goal.focusHyp h.raw.getId | throwError m!"Hypothesis {h} not found" let P := res.restHyps let H := res.focusHyp - let spred := mkApp (mkConst ``SPred) goal.σs + let spred := mkApp (mkConst ``SPred [goal.u]) goal.σs let H' ← match ty? with | some ty => elabTerm ty spred | _ => mkFreshExprMVar spred @@ -78,10 +78,10 @@ def elabMReplace : Tactic let haveGoal := { goal with target := H' } let hhave ← elabTermEnsuringType rhs haveGoal.toExpr let T := goal.target - let (PH', hand) := mkAnd goal.σs P H' + let (PH', hand) := mkAnd goal.u goal.σs P H' let newGoal := { goal with hyps := PH' } let m ← mkFreshExprSyntheticOpaqueMVar newGoal.toExpr - let prf := mkApp (mkApp10 (mkConst ``Have.replace) goal.σs P H H' PH PH' T res.proof hand hhave) m + let prf := mkApp (mkApp10 (mkConst ``Have.replace [goal.u]) goal.σs P H H' PH PH' T res.proof hand hhave) m mvar.assign prf replaceMainGoal [m.mvarId!] | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean index e48e911c83..7d2b512d72 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean @@ -20,10 +20,10 @@ partial def mIntro [Monad m] [MonadControlT MetaM m] (goal : MGoal) (ident : TSy addHypInfo ref σs hyp (isBinder := true) let Q := goal.hyps let H := hyp.toExpr - let (P, hand) := mkAnd goal.σs goal.hyps H + let (P, hand) := mkAnd goal.u goal.σs goal.hyps H map do let (a, prf) ← k { goal with hyps := P, target := T } - let prf := mkApp7 (mkConst ``Intro.intro) σs P Q H T hand prf + let prf := mkApp7 (mkConst ``Intro.intro [goal.u]) σs P Q H T hand prf return (a, prf) -- This is regular MVar.intro, but it takes care not to leave the proof mode by preserving metadata @@ -38,9 +38,9 @@ partial def mIntroForall [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] let H := betaRevPreservingHypNames σs' goal.hyps #[s] let T := goal.target.betaRev #[s] map do - let (a, prf) ← k { σs:=σs', hyps:=H, target:=T } + let (a, prf) ← k { u := goal.u, σs:=σs', hyps:=H, target:=T } let prf ← mkLambdaFVars #[s] prf - return (a, mkApp5 (mkConst ``SPred.entails_cons_intro) σ σs' goal.hyps goal.target prf) + return (a, mkApp5 (mkConst ``SPred.entails_cons_intro [goal.u]) σs' σ goal.hyps goal.target prf) def mIntroForallN [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (n : Nat) (k : MGoal → m (α × Expr)) : m (α × Expr) := match n with diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean b/src/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean index 3a887846bc..f4c2978588 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/LeftRight.lean @@ -15,12 +15,12 @@ def mLeftRightCore (right : Bool) (mvar : MVarId) : MetaM MVarId := do let g ← instantiateMVars <| ← mvar.getType let some goal := parseMGoal? g | throwError "not in proof mode" - let mkApp3 (.const ``SPred.or []) σs L R := goal.target | throwError "target is not SPred.or" + let mkApp3 (.const ``SPred.or _) σs L R := goal.target | throwError "target is not SPred.or" let (thm, keep) := if right then (``SPred.or_intro_r', R) else (``SPred.or_intro_l', L) let newGoal ← mkFreshExprSyntheticOpaqueMVar {goal with target := keep}.toExpr - mvar.assign (mkApp5 (mkConst thm) σs goal.hyps L R newGoal) + mvar.assign (mkApp5 (mkConst thm [goal.u]) σs goal.hyps L R newGoal) return newGoal.mvarId! @[builtin_tactic Lean.Parser.Tactic.mleft] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean index 5bd491c9a5..8207f2a122 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean @@ -31,10 +31,10 @@ def Hyp.toExpr (hyp : Hyp) : Expr := -- set_option pp.all true in -- #check ⌜True⌝ -def emptyHyp (σs : Expr) : Expr := -- ⌜True⌝ standing in for an empty conjunction of hypotheses - mkApp3 (mkConst ``SVal.curry) (.sort .zero) σs <| mkLambda `escape .default (mkApp (mkConst ``SVal.StateTuple) σs) (mkConst ``True) -def parseEmptyHyp? : Expr → Option Expr - | mkApp3 (.const ``SVal.curry _) (.sort .zero) σs (.lam _ _ (.const ``True _) _) => some σs +def emptyHyp (u : Level) (σs : Expr) : Expr := -- ⌜True⌝ 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 ``True)) +def parseEmptyHyp? : Expr → Option (Level × Expr) + | mkApp3 (.const ``SVal.curry [u]) (mkApp (.const ``ULift _) (.sort .zero)) σs (.lam _ _ (mkApp2 (.const ``ULift.up _) _ (.const ``True _)) _) => some (u, σs) | _ => none def pushLeftConjunct (pos : SubExpr.Pos) : SubExpr.Pos := @@ -45,27 +45,29 @@ def pushRightConjunct (pos : SubExpr.Pos) : SubExpr.Pos := /-- Combine two hypotheses into a conjunction. Precondition: Neither `lhs` nor `rhs` is empty (`parseEmptyHyp?`). -/ -def mkAnd! (σs lhs rhs : Expr) : Expr := - mkApp3 (mkConst ``SPred.and) σs lhs rhs +def mkAnd! (u : Level) (σs lhs rhs : Expr) : Expr := + mkApp3 (mkConst ``SPred.and [u]) σs lhs rhs /-- Smart constructor that cancels away empty hypotheses, along with a proof that `lhs ∧ rhs ⊣⊢ₛ result`. -/ -def mkAnd (σs lhs rhs : Expr) : Expr × Expr := +def mkAnd (u : Level) (σs lhs rhs : Expr) : Expr × Expr := if let some _ := parseEmptyHyp? lhs then - (rhs, mkApp2 (mkConst ``SPred.true_and) σs rhs) + (rhs, mkApp2 (mkConst ``SPred.true_and [u]) σs rhs) else if let some _ := parseEmptyHyp? rhs then - (lhs, mkApp2 (mkConst ``SPred.and_true) σs lhs) + (lhs, mkApp2 (mkConst ``SPred.and_true [u]) σs lhs) else - let result := mkAnd! σs lhs rhs - (result, mkApp2 (mkConst ``SPred.bientails.refl) σs result) + let result := mkAnd! u σs lhs rhs + (result, mkApp2 (mkConst ``SPred.bientails.refl [u]) σs result) -def σs.mkType : Expr := mkApp (mkConst ``List [.succ .zero]) (mkSort (.succ .zero)) -def σs.mkNil : Expr := mkApp (mkConst ``List.nil [.succ .zero]) (mkSort (.succ .zero)) +def σs.mkType (u : Level) : Expr := mkApp (mkConst ``List [.succ u]) (mkSort (.succ u)) +def σs.mkNil (u : Level) : Expr := mkApp (mkConst ``List.nil [.succ u]) (mkSort (.succ u)) -def parseAnd? (e : Expr) : Option (Expr × Expr × Expr) := - e.app3? ``SPred.and <|> (σs.mkNil, ·) <$> e.app2? ``And +def parseAnd? (e : Expr) : Option (Level × Expr × Expr × Expr) := + (e.getAppFn.constLevels![0]!, ·) <$> e.app3? ``SPred.and + <|> (0, σs.mkNil 0, ·) <$> e.app2? ``And structure MGoal where + u : Level σs : Expr -- Q(List Type) hyps : Expr -- A conjunction of hypotheses in `SPred σs`, each carrying a name and uniq as metadata (`parseHyp?`) target : Expr -- Q(SPred $σs) @@ -73,7 +75,7 @@ structure MGoal where def parseMGoal? (expr : Expr) : Option MGoal := do let some (σs, hyps, target) := expr.consumeMData.app3? ``MGoalEntails | none - some { σs, hyps, target } + some { u := expr.getAppFn'.constLevels![0]!, σs, hyps, target } open Tactic in def ensureMGoal : TacticM (MVarId × MGoal) := do @@ -85,11 +87,11 @@ def ensureMGoal : TacticM (MVarId × MGoal) := do throwError "Not in proof mode" def MGoal.strip (goal : MGoal) : Expr := -- omits the .mdata wrapper - mkApp3 (mkConst ``SPred.entails) goal.σs goal.hyps goal.target + mkApp3 (mkConst ``SPred.entails [goal.u]) goal.σs goal.hyps goal.target /-- Roundtrips with `parseMGoal?`. -/ def MGoal.toExpr (goal : MGoal) : Expr := - mkApp3 (mkConst ``MGoalEntails) goal.σs goal.hyps goal.target + mkApp3 (mkConst ``MGoalEntails [goal.u]) goal.σs goal.hyps goal.target partial def MGoal.findHyp? (goal : MGoal) (name : Name) : Option (SubExpr.Pos × Hyp) := go goal.hyps SubExpr.Pos.root where @@ -99,7 +101,7 @@ partial def MGoal.findHyp? (goal : MGoal) (name : Name) : Option (SubExpr.Pos × return (p, hyp) else none - else if let some (_, lhs, rhs) := parseAnd? e then + else if let some (_, _, lhs, rhs) := parseAnd? e then -- NB: Need to prefer rhs over lhs, like the goal view (Lean.Elab.Tactic.Do.ProofMode.Delab). go rhs (pushLeftConjunct p) <|> go lhs (pushRightConjunct p) else if let some _ := parseEmptyHyp? e then @@ -120,13 +122,13 @@ def getFreshHypName : TSyntax ``binderIdent → CoreM (Name × Syntax) | stx => return (← mkFreshUserName `h, stx) partial def betaRevPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr := - if let some _σs := parseEmptyHyp? e then - emptyHyp σs' + if let some (u, _) := parseEmptyHyp? e then + emptyHyp u σs' else if let some hyp := parseHyp? e then { hyp with p := hyp.p.betaRev args }.toExpr - else if let some (_σs, lhs, rhs) := parseAnd? e then + else if let some (u, _σs, lhs, rhs) := parseAnd? e then -- _σs = σ :: σs' - mkAnd! σs' (betaRevPreservingHypNames σs' lhs args) (betaRevPreservingHypNames σs' rhs args) + mkAnd! u σs' (betaRevPreservingHypNames σs' lhs args) (betaRevPreservingHypNames σs' rhs args) else e.betaRev args @@ -150,5 +152,5 @@ def addLocalVarInfo (stx : Syntax) (lctx : LocalContext) def addHypInfo (stx : Syntax) (σs : Expr) (hyp : Hyp) (isBinder := false) : MetaM Unit := do let lctx ← getLCtx - let ty := mkApp2 (mkConst ``MGoalHypMarker) σs hyp.p + let ty := mkApp2 (← mkConstWithFreshMVarLevels ``MGoalHypMarker) σs hyp.p addLocalVarInfo stx (lctx.mkLocalDecl ⟨hyp.uniq⟩ hyp.name ty) (.fvar ⟨hyp.uniq⟩) ty isBinder diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean index 3e5e86936b..081857410b 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean @@ -19,15 +19,16 @@ open Lean Elab Tactic Meta -- It calls `k` with the φ in H = ⌜φ⌝ and a proof `h : φ` thereof. def mPureCore (σs : Expr) (hyp : Expr) (name : TSyntax ``binderIdent) (k : Expr /-φ:Prop-/ → Expr /-h:φ-/ → MetaM (α × MGoal × Expr)) : MetaM (α × MGoal × Expr) := do + let u ← mkFreshLevelMVar let φ ← mkFreshExprMVar (mkSort .zero) - let inst ← synthInstance (mkApp3 (mkConst ``IsPure) σs hyp φ) + let inst ← synthInstance (mkApp3 (mkConst ``IsPure [u]) σs hyp φ) let (name, ref) ← getFreshHypName name withLocalDeclD name φ fun h => do addLocalVarInfo ref (← getLCtx) h φ let (a, goal, prf /- : goal.toExpr -/) ← k φ h let prf ← mkLambdaFVars #[h] prf - let prf := mkApp7 (mkConst ``Pure.thm) σs goal.hyps hyp goal.target φ inst prf - let goal := { goal with hyps := mkAnd! σs goal.hyps hyp } + let prf := mkApp7 (mkConst ``Pure.thm [u]) σs goal.hyps hyp goal.target φ inst prf + let goal := { goal with hyps := mkAnd! u σs goal.hyps hyp } return (a, goal, prf) @[builtin_tactic Lean.Parser.Tactic.mpure] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean index 1bfa0cfba4..c64fdaae9e 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean @@ -44,15 +44,15 @@ partial def mRefineCore (goal : MGoal) (pat : MRefinePat) (k : MGoal → TSyntax | .tuple [p] => mRefineCore goal p k | .tuple (p::ps) => do let T ← whnfR goal.target - if let some (σs, T₁, T₂) := parseAnd? T.consumeMData then + if let some (u, σs, T₁, T₂) := parseAnd? T.consumeMData then let prf₁ ← mRefineCore { goal with target := T₁ } p k let prf₂ ← mRefineCore { goal with target := T₂ } (.tuple ps) k - return mkApp6 (mkConst ``SPred.and_intro) σs goal.hyps T₁ T₂ prf₁ prf₂ + return mkApp6 (mkConst ``SPred.and_intro [u]) σs goal.hyps T₁ T₂ prf₁ prf₂ else if let some (α, σs, ψ) := T.app3? ``SPred.exists then let some witness ← patAsTerm p (some α) | throwError "pattern does not elaborate to a term to instantiate ψ" let prf ← mRefineCore { goal with target := ψ.betaRev #[witness] } (.tuple ps) k let u ← getLevel α - return mkApp6 (mkConst ``SPred.exists_intro' [u]) α σs goal.hyps ψ witness prf + return mkApp6 (mkConst ``SPred.exists_intro' [u, goal.u]) α σs goal.hyps ψ witness prf else throwError "Neither a conjunction nor an existential quantifier {goal.target}" @[builtin_tactic Lean.Parser.Tactic.mrefine] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean index 125c014935..9e73298af8 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean @@ -18,8 +18,8 @@ partial def mRevertStep (goal : MGoal) (ref : TSyntax `ident) (k : MGoal → Met let Q := res.restHyps let H := res.focusHyp let T := goal.target - let prf ← k { goal with hyps := Q, target := mkApp3 (mkConst ``SPred.imp) goal.σs H T } - let prf := mkApp7 (mkConst ``Revert.revert) goal.σs P Q H T res.proof prf + let prf ← k { goal with hyps := Q, target := mkApp3 (mkConst ``SPred.imp [goal.u]) goal.σs H T } + let prf := mkApp7 (mkConst ``Revert.revert [goal.u]) goal.σs P Q H T res.proof prf return prf @[builtin_tactic Lean.Parser.Tactic.mrevert] diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean index 3baac03e5d..735031e8bf 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean @@ -16,31 +16,31 @@ open Lean Elab Tactic Meta initialize registerTraceClass `Meta.Tactic.Do.specialize -def mSpecializeImpStateful (σs : Expr) (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do +def mSpecializeImpStateful (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do guard (arg.raw.isIdent) - let some argRes := focusHyp σs (mkAnd! σs P QR) arg.raw.getId | failure + let some specHyp := parseHyp? QR | failure + let mkApp3 (.const ``SPred.imp [u]) σs Q' R := specHyp.p | failure + let some argRes := focusHyp u σs (mkAnd! u σs P QR) arg.raw.getId | failure let some hyp := parseHyp? argRes.focusHyp | failure addHypInfo arg σs hyp OptionT.mk do -- no OptionT failure after this point -- The goal is P ∧ (Q → R) -- argRes.proof : P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q -- we want to return (R, (proof : P ∧ (Q → R) ⊢ₛ P ∧ R)) - let some specHyp := parseHyp? QR | panic! "Precondition of specializeImpStateful violated" let P' := argRes.restHyps let Q := argRes.focusHyp let hrefocus := argRes.proof -- P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q - let mkApp3 (.const ``SPred.imp []) σs Q' R := specHyp.p | throwError "Expected implication {QR}" - let proof := mkApp6 (mkConst ``Specialize.imp_stateful) σs P P' Q R hrefocus + let proof := mkApp6 (mkConst ``Specialize.imp_stateful [u]) σs P P' Q R hrefocus -- check proof - trace[Meta.Tactic.Do.specialize] "Statefully specialize {specHyp.p} with {Q}. New Goal: {mkAnd! σs P R}" + trace[Meta.Tactic.Do.specialize] "Statefully specialize {specHyp.p} with {Q}. New Goal: {mkAnd! u σs P R}" unless ← isDefEq Q Q' do throwError "failed to specialize {specHyp.p} with {Q}" return ({ specHyp with p := R }.toExpr, proof) -def mSpecializeImpPure (_σs : Expr) (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do +def mSpecializeImpPure (P : Expr) (QR : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do let some specHyp := parseHyp? QR | panic! "Precondition of specializeImpPure violated" - let mkApp3 (.const ``SPred.imp []) σs Q R := specHyp.p | failure + let mkApp3 (.const ``SPred.imp [u]) σs Q R := specHyp.p | failure let mut φ ← mkFreshExprMVar (mkSort .zero) let mut (hφ, mvarIds) ← try elabTermWithHoles arg.raw φ `specialize (allowNaturalHoles := true) @@ -49,35 +49,35 @@ def mSpecializeImpPure (_σs : Expr) (P : Expr) (QR : Expr) (arg : TSyntax `term -- so that we can infer an instance of `PropAsSPredTautology`. -- NB: PropAsSPredTautology φ ⌜φ⌝ is unfortunately impossible because ⊢ₛ ⌜φ⌝ does not imply φ. -- Hence this additional (lossy) conversion. - if let some inst ← synthInstance? (mkApp3 (mkConst ``IsPure) σs Q φ) then - hφ := mkApp5 (mkConst ``Specialize.pure_taut) σs φ Q inst hφ - φ := mkApp2 (mkConst ``tautological) σs Q + if let some inst ← synthInstance? (mkApp3 (mkConst ``IsPure [u]) σs Q φ) then + hφ := mkApp5 (mkConst ``Specialize.pure_taut [u]) σs φ Q inst hφ + φ := mkApp2 (mkConst ``tautological [u]) σs Q - let some inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology) φ σs Q) + let some inst ← synthInstance? (mkApp3 (mkConst ``PropAsSPredTautology [u]) φ σs Q) | failure OptionT.mk do -- no OptionT failure after this point -- The goal is P ∧ (Q → R) -- we want to return (R, (proof : P ∧ (Q → R) ⊢ₛ P ∧ R)) pushGoals mvarIds - let proof := mkApp7 (mkConst ``Specialize.imp_pure) σs φ P Q R inst hφ + let proof := mkApp7 (mkConst ``Specialize.imp_pure [u]) σs φ P Q R inst hφ -- check proof - trace[Meta.Tactic.Do.specialize] "Purely specialize {specHyp.p} with {Q}. New Goal: {mkAnd! σs P R}" + trace[Meta.Tactic.Do.specialize] "Purely specialize {specHyp.p} with {Q}. New Goal: {mkAnd! u σs P R}" -- logInfo m!"proof: {← inferType proof}" return ({ specHyp with p := R }.toExpr, proof) -def mSpecializeForall (_σs : Expr) (P : Expr) (Ψ : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do +def mSpecializeForall (P : Expr) (Ψ : Expr) (arg : TSyntax `term) : OptionT TacticM (Expr × Expr) := do let some specHyp := parseHyp? Ψ | panic! "Precondition of specializeForall violated" - let mkApp3 (.const ``SPred.forall [u]) α σs αR := specHyp.p | failure + let mkApp3 (.const ``SPred.forall [u, v]) α σs αR := specHyp.p | failure let (a, mvarIds) ← try elabTermWithHoles arg.raw α `specialize (allowNaturalHoles := true) catch _ => failure OptionT.mk do -- no OptionT failure after this point pushGoals mvarIds - let proof := mkApp5 (mkConst ``Specialize.forall [u]) σs α P αR a + let proof := mkApp5 (mkConst ``Specialize.forall [u, v]) σs α P αR a let R := αR.beta #[a] -- check proof - trace[Meta.Tactic.Do.specialize] "Instantiate {specHyp.p} with {a}. New Goal: {mkAnd! σs P R}" + trace[Meta.Tactic.Do.specialize] "Instantiate {specHyp.p} with {a}. New Goal: {mkAnd! u σs P R}" return ({ specHyp with p := R }.toExpr, proof) @[builtin_tactic Lean.Parser.Tactic.mspecialize] @@ -95,6 +95,7 @@ def elabMSpecialize : Tactic -- 3. Recombine with mkAnd (NB: P' might be empty), compose with P' ∧ H' ⊣⊢ₛ mkAnd P' H'. -- 4. Make a new MVar for goal `mkAnd P' H' ⊢ T` and assign the transitive chain. let some specFocus := goal.focusHyp hyp.getId | throwError "unknown identifier '{hyp}'" + let u := goal.u let σs := goal.σs let P := specFocus.restHyps let mut H := specFocus.focusHyp @@ -102,22 +103,22 @@ def elabMSpecialize : Tactic addHypInfo hyp σs hyp' -- invariant: proof (_ : { goal with hyps := mkAnd! σs P H }.toExpr) fills the mvar let mut proof : Expr → Expr := - mkApp7 (mkConst ``Specialize.focus) σs goal.hyps P H goal.target specFocus.proof + mkApp7 (mkConst ``Specialize.focus [u]) σs goal.hyps P H goal.target specFocus.proof for arg in args do let res? ← OptionT.run - (mSpecializeImpStateful σs P H arg - <|> mSpecializeImpPure σs P H arg - <|> mSpecializeForall σs P H arg) + (mSpecializeImpStateful P H arg + <|> mSpecializeImpPure P H arg + <|> mSpecializeForall P H arg) match res? with | some (H', H2H') => -- logInfo m!"H: {H}, proof: {← inferType H2H'}" - proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans) σs (mkAnd! σs P H) (mkAnd! σs P H') goal.target H2H' hgoal) + proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans [u]) σs (mkAnd! u σs P H) (mkAnd! u σs P H') goal.target H2H' hgoal) H := H' | none => throwError "Could not specialize {H} with {arg}" - let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! σs P H }.toExpr + let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! u σs P H }.toExpr mvar.assign (proof newMVar) replaceMainGoal [newMVar.mvarId!] @@ -139,30 +140,31 @@ def elabMspecializePure : Tactic -- One for each arg; end up with goal P ∧ H' ⊢ₛ T -- 3. Recombine with mkAnd (NB: P' might be empty), compose with P' ∧ H' ⊣⊢ₛ mkAnd P' H'. -- 4. Make a new MVar for goal `mkAnd P' H' ⊢ T` and assign the transitive chain. + let u := goal.u let σs := goal.σs let P := goal.hyps let T := goal.target let hφ ← elabTerm head none let φ ← inferType hφ - let H ← mkFreshExprMVar (mkApp (mkConst ``SPred) σs) - let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology) φ σs H) + let H ← mkFreshExprMVar (mkApp (mkConst ``SPred [u]) σs) + let inst ← synthInstance (mkApp3 (mkConst ``PropAsSPredTautology [u]) φ σs H) let uniq ← mkFreshId let mut H := (Hyp.mk hyp.getId uniq (← instantiateMVars H)).toExpr - let goal : MGoal := { goal with hyps := mkAnd! σs P H } - -- invariant: proof (_ : { goal with hyps := mkAnd! σs P H }.toExpr) fills the mvar + let goal : MGoal := { goal with hyps := mkAnd! u σs P H } + -- invariant: proof (_ : { goal with hyps := mkAnd! u σs P H }.toExpr) fills the mvar let mut proof : Expr → Expr := - mkApp8 (mkConst ``Specialize.pure_start) σs φ H P T inst hφ + mkApp8 (mkConst ``Specialize.pure_start [u]) σs φ H P T inst hφ for arg in args do let res? ← OptionT.run - (mSpecializeImpStateful σs P H ⟨arg⟩ - <|> mSpecializeImpPure σs P H ⟨arg⟩ - <|> mSpecializeForall σs P H ⟨arg⟩) + (mSpecializeImpStateful P H ⟨arg⟩ + <|> mSpecializeImpPure P H ⟨arg⟩ + <|> mSpecializeForall P H ⟨arg⟩) match res? with | some (H', H2H') => -- logInfo m!"H: {H}, proof: {← inferType H2H'}" - proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans) σs (mkAnd! σs P H) (mkAnd! σs P H') goal.target H2H' hgoal) + proof := fun hgoal => proof (mkApp6 (mkConst ``SPred.entails.trans [u]) σs (mkAnd! u σs P H) (mkAnd! u σs P H') goal.target H2H' hgoal) H := H' | none => throwError "Could not specialize {H} with {arg}" @@ -170,7 +172,7 @@ def elabMspecializePure : Tactic let some hyp' := parseHyp? H | panic! "Invariant of specialize_pure violated" addHypInfo hyp σs hyp' - let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! σs P H }.toExpr + let newMVar ← mkFreshExprSyntheticOpaqueMVar { goal with hyps := mkAnd! u σs P H }.toExpr mvar.assign (proof newMVar) replaceMainGoal [newMVar.mvarId!] | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean index 88576a23fd..8ee186bb1c 100644 --- a/src/Lean/Elab/Tactic/Do/Spec.lean +++ b/src/Lean/Elab/Tactic/Do/Spec.lean @@ -19,7 +19,7 @@ open Std.Do Do.SpecAttr Do.ProofMode builtin_initialize registerTraceClass `Elab.Tactic.Do.spec def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem := do - let_expr WP.wp _m _ps _instWP _α prog := wp | throwError "target not a wp application {wp}" + let_expr c@WP.wp _m _ps _instWP _α prog := wp | throwError "target not a wp application {wp}" let prog ← instantiateMVarsIfMVarApp prog let prog := prog.headBeta let candidates ← database.specs.getMatch prog @@ -30,7 +30,7 @@ def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem := do let (_, _, _, type) ← spec.proof.instantiate trace[Elab.Tactic.Do.spec] "{spec.proof} instantiates to {type}" let_expr Triple m ps instWP α specProg _P _Q := type | throwError "Not a triple: {type}" - isDefEq wp (mkApp5 (← mkConstWithFreshMVarLevels ``WP.wp) m ps instWP α specProg) + isDefEq wp (mkApp5 (mkConst ``WP.wp c.constLevels!) m ps instWP α specProg) trace[Elab.Tactic.Do.spec] "Specs for {prog}: {specs.map (·.proof)}" if specs.isEmpty then throwError m!"No specs found for {indentExpr prog}\nCandidates: {candidates.map (·.proof)}" return specs[0]! @@ -50,8 +50,9 @@ def elabTermIntoSpecTheorem (stx : TSyntax `term) (expectedTy : Expr) : TacticM def elabSpec (stx? : Option (TSyntax `term)) (wp : Expr) : TacticM SpecTheorem := do let_expr f@WP.wp m ps instWP α prog := wp | throwError "target not a wp application {wp}" - let P ← mkFreshExprMVar (mkApp (mkConst ``Assertion) ps) (userName := `P) - let Q ← mkFreshExprMVar (mkApp2 (mkConst ``PostCond) α ps) (userName := `Q) + let u := f.constLevels![0]! + let P ← mkFreshExprMVar (mkApp (mkConst ``Assertion [u]) ps) (userName := `P) + let Q ← mkFreshExprMVar (mkApp2 (mkConst ``PostCond [u]) α ps) (userName := `Q) let expectedTy := mkApp7 (mkConst ``Triple f.constLevels!) m ps instWP α prog P Q trace[Elab.Tactic.Do.spec] "spec syntax: {stx?}" trace[Elab.Tactic.Do.spec] "expected type: {← instantiateMVars expectedTy}" @@ -67,59 +68,62 @@ private def mkProj' (n : Name) (i : Nat) (Q : Expr) : MetaM Expr := do mutual partial def dischargePostEntails (α : Expr) (ps : Expr) (Q : Expr) (Q' : Expr) (goalTag : Name) : n Expr := do -- Often, Q' is fully instantiated while Q contains metavariables. Try refl + let u ← liftMetaM <| getLevel α >>= decLevel if (← isDefEq Q Q') then - return mkApp3 (mkConst ``PostCond.entails.refl) α ps Q' + return mkApp3 (mkConst ``PostCond.entails.refl [u]) α ps Q' let Q ← whnfR Q let Q' ← whnfR Q' -- If Q (postcond of the spec) is just an fvar, we do not decompose further if let some _fvarId := Q.fvarId? then - return ← mkFreshExprSyntheticOpaqueMVar (mkApp4 (mkConst ``PostCond.entails) α ps Q Q') (goalTag ++ `post) + return ← mkFreshExprSyntheticOpaqueMVar (mkApp4 (mkConst ``PostCond.entails [u]) α ps Q Q') (goalTag ++ `post) -- Otherwise decompose the conjunction let prf₁ ← withLocalDeclD (← liftMetaM <| mkFreshUserName `r) α fun a => do let Q1a := (← mkProj' ``Prod 0 Q).betaRev #[a] let Q'1a := (← mkProj' ``Prod 0 Q').betaRev #[a] - let σs := mkApp (mkConst ``PostShape.args) ps + let σs := mkApp (mkConst ``PostShape.args [u]) ps let uniq ← liftMetaM mkFreshId - let goal := MGoal.mk σs (Hyp.mk `h uniq Q1a).toExpr Q'1a + let goal := MGoal.mk u σs (Hyp.mk `h uniq Q1a).toExpr Q'1a mkLambdaFVars #[a] (← mkFreshExprSyntheticOpaqueMVar goal.toExpr (goalTag ++ `success)) - let prf₂ ← dischargeFailEntails ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except) - mkAppM ``And.intro #[prf₁, prf₂] -- This is just a bit too painful to construct by hand + let prf₂ ← dischargeFailEntails u ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except) + mkAppM ``And.intro #[prf₁, prf₂] -partial def dischargeFailEntails (ps : Expr) (Q : Expr) (Q' : Expr) (goalTag : Name) : n Expr := do +partial def dischargeFailEntails (u : Level) (ps : Expr) (Q : Expr) (Q' : Expr) (goalTag : Name) : n Expr := do if ps.isAppOf ``PostShape.pure then return mkConst ``True.intro if ← isDefEq Q Q' then - return mkApp2 (mkConst ``FailConds.entails.refl) ps Q - if ← isDefEq Q (mkApp (mkConst ``FailConds.false) ps) then - return mkApp2 (mkConst ``FailConds.entails_false) ps Q' - if ← isDefEq Q' (mkApp (mkConst ``FailConds.true) ps) then - return mkApp2 (mkConst ``FailConds.entails_true) ps Q + return mkApp2 (mkConst ``FailConds.entails.refl [u]) ps Q + if ← isDefEq Q (mkApp (mkConst ``FailConds.false [u]) ps) then + return mkApp2 (mkConst ``FailConds.entails_false [u]) ps Q' + if ← isDefEq Q' (mkApp (mkConst ``FailConds.true [u]) ps) then + return mkApp2 (mkConst ``FailConds.entails_true [u]) ps Q -- the remaining cases are recursive. if let some (_σ, ps) := ps.app2? ``PostShape.arg then - return ← dischargeFailEntails ps Q Q' goalTag + return ← dischargeFailEntails u ps Q Q' goalTag if let some (ε, ps) := ps.app2? ``PostShape.except then let Q ← whnfR Q let Q' ← whnfR Q' let prf₁ ← withLocalDeclD (← liftMetaM <| mkFreshUserName `e) ε fun e => do let Q1e := (← mkProj' ``Prod 0 Q).betaRev #[e] let Q'1e := (← mkProj' ``Prod 0 Q').betaRev #[e] - let σs := mkApp (mkConst ``PostShape.args) ps + let σs := mkApp (mkConst ``PostShape.args [u]) ps let uniq ← liftMetaM mkFreshId - let goal := MGoal.mk σs (Hyp.mk `h uniq Q1e).toExpr Q'1e + let goal := MGoal.mk u σs (Hyp.mk `h uniq Q1e).toExpr Q'1e mkLambdaFVars #[e] (← mkFreshExprSyntheticOpaqueMVar goal.toExpr (goalTag ++ `handle)) - let prf₂ ← dischargeFailEntails ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except) + let prf₂ ← dischargeFailEntails u ps (← mkProj' ``Prod 1 Q) (← mkProj' ``Prod 1 Q') (goalTag ++ `except) return ← mkAppM ``And.intro #[prf₁, prf₂] -- This is just a bit too painful to construct by hand -- This case happens when decomposing with unknown `ps : PostShape` - mkFreshExprSyntheticOpaqueMVar (mkApp3 (mkConst ``FailConds.entails) ps Q Q') goalTag + mkFreshExprSyntheticOpaqueMVar (mkApp3 (mkConst ``FailConds.entails [u]) ps Q Q') goalTag end def dischargeMGoal (goal : MGoal) (goalTag : Name) : n Expr := do - liftMetaM <| do trace[Elab.Tactic.Do.spec] "dischargeMGoal: {(← reduceProj? goal.target).getD goal.target}" + 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 -- semi-reducible.) - let some prf ← liftMetaM goal.assumption | mkFreshExprSyntheticOpaqueMVar goal.toExpr goalTag + let some prf ← liftMetaM (withDefault <| goal.assumption <|> goal.assumptionPure) + | mkFreshExprSyntheticOpaqueMVar goal.toExpr goalTag + liftMetaM <| do trace[Elab.Tactic.Do.spec] "proof: {prf}" return prf def mkPreTag (goalTag : Name) : Name := Id.run do @@ -175,6 +179,7 @@ def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name let P := P.betaRev excessArgs let spec := spec.betaRev excessArgs + let u := goal.u -- Often P or Q are schematic (i.e. an MVar app). Try to solve by rfl. -- We do `fullApproxDefEq` here so that `constApprox` is active; this is useful in @@ -189,19 +194,19 @@ def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name -- Try to avoid creating a longer name if the postcondition does not need to create a goal let tag := if !QQ'Rfl then mkPreTag goalTag else goalTag let HPPrf ← dischargeMGoal { goal with target := P } tag - prePrf := mkApp6 (mkConst ``SPred.entails.trans) goal.σs goal.hyps P goal.target HPPrf + prePrf := mkApp6 (mkConst ``SPred.entails.trans [u]) goal.σs goal.hyps P goal.target HPPrf -- Discharge the entailment on postconditions if not rfl let mut postPrf : Expr → Expr := id if !QQ'Rfl then -- Try to avoid creating a longer name if the precondition does not need to create a goal let tag := if !HPRfl then goalTag ++ `post else goalTag - let wpApplyQ := mkApp4 (mkConst ``PredTrans.apply) ps α wp Q -- wp⟦x⟧.apply Q; that is, T without excess args - let wpApplyQ' := mkApp4 (mkConst ``PredTrans.apply) ps α wp Q' -- wp⟦x⟧.apply Q' + let wpApplyQ := mkApp4 (mkConst ``PredTrans.apply [u]) ps α wp Q -- wp⟦x⟧.apply Q; that is, T without excess args + let wpApplyQ' := mkApp4 (mkConst ``PredTrans.apply [u]) ps α wp Q' -- wp⟦x⟧.apply Q' let QQ' ← dischargePostEntails α ps Q Q' tag - let QQ'mono := mkApp6 (mkConst ``PredTrans.mono) ps α wp Q Q' QQ' + let QQ'mono := mkApp6 (mkConst ``PredTrans.mono [u]) ps α wp Q Q' QQ' postPrf := fun h => - mkApp6 (mkConst ``SPred.entails.trans) goal.σs P (wpApplyQ.betaRev excessArgs) (wpApplyQ'.betaRev excessArgs) + mkApp6 (mkConst ``SPred.entails.trans [u]) goal.σs P (wpApplyQ.betaRev excessArgs) (wpApplyQ'.betaRev excessArgs) h (QQ'mono.betaRev excessArgs) -- finally build the proof; HPPrf.trans (spec.trans QQ'mono) diff --git a/src/Lean/Elab/Tactic/Do/Syntax.lean b/src/Lean/Elab/Tactic/Do/Syntax.lean index 08c8732eeb..0c234300c6 100644 --- a/src/Lean/Elab/Tactic/Do/Syntax.lean +++ b/src/Lean/Elab/Tactic/Do/Syntax.lean @@ -32,17 +32,18 @@ private meta def elabTriple : TermElab -- then `Triple x P _` will not elaborate because `σ → Assertion ps =?= Assertion ?ps` fails. -- We must first instantiate `?ps` to `.arg σ ps` through the `outParam` of `WP`, hence this elaborator. -- This is tracked in #8766, and #8074 might be a fix. - let (u, m, α, ps, inst, x) ← withRef x do + let (u, v, m, α, ps, inst, x) ← withRef x do let x ← elabTerm x none let ty ← inferType x tryPostponeIfMVar ty let ty ← instantiateMVars ty let .app m α := ty.consumeMData | throwError "Type of {x} is not a type application: {ty}" - let some u ← Level.dec <$> getLevel ty | throwError "Wrong level 0 {ty}" - let ps ← mkFreshExprMVar (mkConst ``PostShape) - let inst ← synthInstance (mkApp2 (mkConst ``WP [u]) m ps) - return (u, m, α, ps, inst, x) - let P ← elabTerm (← `(spred($P))) (mkApp (mkConst ``Assertion) ps) - let Q ← elabTerm (← `(spred($Q))) (mkApp2 (mkConst ``PostCond) α ps) - return mkApp7 (mkConst ``Triple [u]) m ps inst α x P Q + let some u ← Level.dec <$> getLevel α | throwError "Wrong level 0 {ty}" + let some v ← Level.dec <$> getLevel ty | throwError "Wrong level 0 {ty}" + let ps ← mkFreshExprMVar (mkConst ``PostShape [u]) + let inst ← synthInstance (mkApp2 (mkConst ``WP [u, v]) m ps) + return (u, v, m, α, ps, inst, x) + let P ← elabTerm (← `(spred($P))) (mkApp (mkConst ``Assertion [u]) ps) + let Q ← elabTerm Q (mkApp2 (mkConst ``PostCond [u]) α ps) + return mkApp7 (mkConst ``Triple [u, v]) m ps inst α x P Q | _, _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 5c90dacc48..1eb9f7a5e7 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen.lean @@ -291,11 +291,12 @@ where | c@WP.wp m ps instWP α e => let e ← instantiateMVarsIfMVarApp e let e := e.headBeta + let [u, _] := c.constLevels! | panic! "PredTrans.apply has wrong number of levels" trace[Elab.Tactic.Do.vcgen] "Target: {e}" let goalWithNewProg e' := let wp' := mkApp5 c m ps instWP α e' let args' := args.set! 2 wp' - { goal with target := mkAppN (mkConst ``PredTrans.apply) args' } + { goal with target := mkAppN (mkConst ``PredTrans.apply [u]) args' } -- lambda-expressions if e.getAppFn'.isLambda && false then diff --git a/src/Std/Do/PostCond.lean b/src/Std/Do/PostCond.lean index b960f261df..cd46e2731e 100644 --- a/src/Std/Do/PostCond.lean +++ b/src/Std/Do/PostCond.lean @@ -38,12 +38,16 @@ via `PostShape.args`. namespace Std.Do -inductive PostShape : Type 1 where - | pure : PostShape - | arg : (σ : Type) → PostShape → PostShape - | except : (ε : Type) → PostShape → PostShape +universe u -abbrev PostShape.args : PostShape → List Type +inductive PostShape : Type (u+1) where + | pure : PostShape + | arg : (σ : Type u) → PostShape → PostShape + | except : (ε : Type u) → PostShape → PostShape + +variable {ps : PostShape.{u}} {α σ ε : Type u} + +abbrev PostShape.args : PostShape.{u} → List (Type u) | .pure => [] | .arg σ s => σ :: PostShape.args s | .except _ s => PostShape.args s @@ -51,33 +55,33 @@ abbrev PostShape.args : PostShape → List Type /-- An assertion on the `.arg`s in the given predicate shape. ``` - example : Assertion (.arg ρ .pure) = (ρ → Prop) := rfl - example : Assertion (.except ε .pure) = Prop := rfl - example : Assertion (.arg σ (.except ε .pure)) = (σ → Prop) := rfl - example : Assertion (.except ε (.arg σ .pure)) = (σ → Prop) := rfl + example : Assertion (.arg ρ .pure) = (ρ → ULift Prop) := rfl + example : Assertion (.except ε .pure) = ULift Prop := rfl + example : Assertion (.arg σ (.except ε .pure)) = (σ → ULift Prop) := rfl + example : Assertion (.except ε (.arg σ .pure)) = (σ → ULift Prop) := rfl ``` This is an abbreviation for `SPred` under the hood, so all theorems about `SPred` apply. -/ -abbrev Assertion (ps : PostShape) : Type := +abbrev Assertion (ps : PostShape.{u}) : Type u := SPred (PostShape.args ps) /-- Encodes one continuation barrel for each `PostShape.except` in the given predicate shape. ``` example : FailConds (.pure) = Unit := rfl - example : FailConds (.except ε .pure) = ((ε → Prop) × Unit) := rfl - example : FailConds (.arg σ (.except ε .pure)) = ((ε → Prop) × Unit) := rfl - example : FailConds (.except ε (.arg σ .pure)) = ((ε → σ → Prop) × Unit) := rfl + example : FailConds (.except ε .pure) = ((ε → ULift Prop) × Unit) := rfl + example : FailConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Unit) := rfl + example : FailConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl ``` -/ -def FailConds : PostShape → Type - | .pure => Unit +def FailConds : PostShape.{u} → Type u + | .pure => PUnit | .arg _ ps => FailConds ps | .except ε ps => (ε → Assertion ps) × FailConds ps @[simp] -def FailConds.const {ps : PostShape} (p : Prop) : FailConds ps := match ps with - | .pure => () +def FailConds.const {ps : PostShape.{u}} (p : Prop) : FailConds ps := match ps with + | .pure => ⟨⟩ | .arg _ ps => @FailConds.const ps p | .except _ ps => (fun _ε => spred(⌜p⌝), @FailConds.const ps p) @@ -90,7 +94,7 @@ def FailConds.false : FailConds ps := FailConds.const False instance : Inhabited (FailConds ps) where default := FailConds.true -def FailConds.entails {ps : PostShape} (x y : FailConds ps) : Prop := +def FailConds.entails {ps : PostShape.{u}} (x y : FailConds ps) : Prop := match ps with | .pure => True | .arg _ ps => @entails ps x y @@ -119,9 +123,9 @@ theorem FailConds.entails_true {x : FailConds ps} : x ⊢ₑ FailConds.true := b induction ps <;> simp_all [true, const, entails] @[simp] -def FailConds.and {ps : PostShape} (x : FailConds ps) (y : FailConds ps) : FailConds ps := +def FailConds.and {ps : PostShape.{u}} (x : FailConds ps) (y : FailConds ps) : FailConds ps := match ps with - | .pure => () + | .pure => ⟨⟩ | .arg _ ps => @FailConds.and ps x y | .except _ _ => (fun e => SPred.and (x.1 e) (y.1 e), FailConds.and x.2 y.2) @@ -179,8 +183,8 @@ theorem FailConds.and_eq_left {ps : PostShape} {p q : FailConds ps} (h : p ⊢ example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → Prop) × (ε → σ → Prop) × Unit) := rfl ``` -/ -abbrev PostCond (α : Type) (s : PostShape) : Type := - (α → Assertion s) × FailConds s +abbrev PostCond (α : Type u) (ps : PostShape.{u}) : Type u := + (α → Assertion ps) × FailConds ps @[inherit_doc PostCond] scoped macro:max "post⟨" handlers:term,+,? "⟩" : term => diff --git a/src/Std/Do/PredTrans.lean b/src/Std/Do/PredTrans.lean index 7858e3315d..5c7af5aacd 100644 --- a/src/Std/Do/PredTrans.lean +++ b/src/Std/Do/PredTrans.lean @@ -28,18 +28,20 @@ This module defines interpretations of common monadic operations, such as `get`, namespace Std.Do +universe u +variable {ps : PostShape.{u}} {α : Type u} + /-- The stronger the postcondition, the stronger the transformed precondition. -/ -def PredTrans.Monotonic {ps : PostShape} {α : Type} (t : PostCond α ps → Assertion ps) : Prop := +def PredTrans.Monotonic (t : PostCond α ps → Assertion ps) : Prop := ∀ Q₁ Q₂, (Q₁ ⊢ₚ Q₂) → (t Q₁) ⊢ₛ (t Q₂) /-- Transforming a conjunction of postconditions is the same as the conjunction of transformed postconditions. -/ -def PredTrans.Conjunctive {ps : PostShape} {α : Type} (t : PostCond α ps → Assertion ps) : Prop := +def PredTrans.Conjunctive (t : PostCond α ps → Assertion ps) : Prop := ∀ Q₁ Q₂, t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂ /-- Any predicate transformer that is conjunctive is also monotonic. -/ -def PredTrans.Conjunctive.mono {ps : PostShape} {α : Type} - (t : PostCond α ps → Assertion ps) (h : PredTrans.Conjunctive t) : PredTrans.Monotonic t := by +def PredTrans.Conjunctive.mono (t : PostCond α ps → Assertion ps) (h : PredTrans.Conjunctive t) : PredTrans.Monotonic t := by intro Q₁ Q₂ hq replace hq : Q₁ = (Q₁ ∧ₚ Q₂) := PostCond.and_eq_left hq rw [hq, (h Q₁ Q₂).to_eq] @@ -53,27 +55,27 @@ def PredTrans.Conjunctive.mono {ps : PostShape} {α : Type} `Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂`. -/ @[ext] -structure PredTrans (ps : PostShape) (α : Type) : Type where +structure PredTrans (ps : PostShape) (α : Type u) : Type u where apply : PostCond α ps → Assertion ps conjunctive : PredTrans.Conjunctive apply namespace PredTrans -theorem mono {ps : PostShape} {α : Type} (t : PredTrans ps α) : Monotonic t.apply := +theorem mono (t : PredTrans ps α) : Monotonic t.apply := Conjunctive.mono t.apply t.conjunctive /-- Given a fixed postcondition, the *stronger* predicate transformer will yield a *weaker* precondition. -/ -def le {ps : PostShape} {α : Type} (x y : PredTrans ps α) : Prop := +def le (x y : PredTrans ps α) : Prop := ∀ Q, y.apply Q ⊢ₛ x.apply Q -- the weaker the precondition, the smaller the PredTrans instance : LE (PredTrans ps α) := ⟨le⟩ -def pure {ps : PostShape} {α : Type} (a : α) : PredTrans ps α := +def pure (a : α) : PredTrans ps α := { apply := fun Q => Q.1 a, conjunctive := by intro _ _; simp } -def bind {ps : PostShape} {α β : Type} (x : PredTrans ps α) (f : α → PredTrans ps β) : PredTrans ps β := +def bind (x : PredTrans ps α) (f : α → PredTrans ps β) : PredTrans ps β := { apply := fun Q => x.apply (fun a => (f a).apply Q, Q.2), conjunctive := by intro Q₁ Q₂ @@ -83,7 +85,7 @@ def bind {ps : PostShape} {α β : Type} (x : PredTrans ps α) (f : α → PredT conv in (f _).apply _ => rw [((f _).conjunctive _ _).to_eq] } -def const {ps : PostShape} {α : Type} (p : Assertion ps) : PredTrans ps α := +def const (p : Assertion ps) : PredTrans ps α := { apply := fun Q => p, conjunctive := by intro _ _; simp [SPred.and_self.to_eq] } instance : Monad (PredTrans ps) where @@ -91,26 +93,26 @@ instance : Monad (PredTrans ps) where bind := bind @[simp] -theorem pure_apply {ps : PostShape} {α : Type} (a : α) (Q : PostCond α ps) : +theorem pure_apply (a : α) (Q : PostCond α ps) : (PredTrans.pure a : PredTrans ps α).apply Q = Q.1 a := by rfl @[simp] -theorem Pure_pure_apply {ps : PostShape} {α : Type} (a : α) (Q : PostCond α ps) : +theorem Pure_pure_apply (a : α) (Q : PostCond α ps) : (Pure.pure a : PredTrans ps α).apply Q = Q.1 a := by rfl @[simp] -theorem map_apply {ps : PostShape} {α β : Type} (f : α → β) (x : PredTrans ps α) (Q : PostCond β ps) : +theorem map_apply (f : α → β) (x : PredTrans ps α) (Q : PostCond β ps) : (f <$> x).apply Q = x.apply (fun a => Q.1 (f a), Q.2) := by rfl @[simp] -theorem bind_apply {ps : PostShape} {α β : Type} (x : PredTrans ps α) (f : α → PredTrans ps β) (Q : PostCond β ps) : +theorem bind_apply (x : PredTrans ps α) (f : α → PredTrans ps β) (Q : PostCond β ps) : (x >>= f).apply Q = x.apply (fun a => (f a).apply Q, Q.2) := by rfl @[simp] -theorem seq_apply {ps : PostShape} {α β : Type} (f : PredTrans ps (α → β)) (x : PredTrans ps α) (Q : PostCond β ps) : +theorem seq_apply (f : PredTrans ps (α → β)) (x : PredTrans ps α) (Q : PostCond β ps) : (f <*> x).apply Q = f.apply (fun g => x.apply (fun a => Q.1 (g a), Q.2), Q.2) := by rfl -theorem bind_mono {ps : PostShape} {α β : Type} {x y : PredTrans ps α} {f : α → PredTrans ps β} +theorem bind_mono {x y : PredTrans ps α} {f : α → PredTrans ps β} (h : x ≤ y) : x >>= f ≤ y >>= f := by intro Q; exact (h (_, Q.2)) instance instLawfulMonad : LawfulMonad (PredTrans ps) := @@ -121,7 +123,7 @@ instance instLawfulMonad : LawfulMonad (PredTrans ps) := -- The interpretation of `StateT σ (PredTrans ps) α` into `PredTrans (.arg σ ps) α`. -- Think: modifyGetM -def pushArg {ps : PostShape} {σ : Type} {α : Type} (x : StateT σ (PredTrans ps) α) : PredTrans (.arg σ ps) α := +def pushArg {σ : Type u} (x : StateT σ (PredTrans ps) α) : PredTrans (.arg σ ps) α := { apply := fun Q s => (x s).apply (fun (a, s) => Q.1 a s, Q.2), conjunctive := by intro Q₁ Q₂ @@ -180,11 +182,11 @@ instance instMonadFunctorExcept : MonadFunctor (PredTrans m) (PredTrans (.except monadMap f x := pushExcept (f x.popExcept) @[simp] -def pushArg_apply {ps} {α : Type} {σ : Type} {Q : PostCond α (.arg σ ps)} (f : σ → PredTrans ps (α × σ)) : +def pushArg_apply {ps} {α σ : Type u} {Q : PostCond α (.arg σ ps)} (f : σ → PredTrans ps (α × σ)) : (pushArg f).apply Q = fun s => (f s).apply (fun ⟨a, s⟩ => Q.1 a s, Q.2) := rfl @[simp] -def pushExcept_apply {ps} {α ε} {Q : PostCond α (.except ε ps)} (x : PredTrans ps (Except ε α)) : +def pushExcept_apply {ps} {α ε : Type u} {Q : PostCond α (.except ε ps)} (x : PredTrans ps (Except ε α)) : (pushExcept x).apply Q = x.apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := rfl def dite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : c → PredTrans ps α) (e : ¬ c → PredTrans ps α) : diff --git a/src/Std/Do/SPred/DerivedLaws.lean b/src/Std/Do/SPred/DerivedLaws.lean index 2b0c13bdec..dcace3dd69 100644 --- a/src/Std/Do/SPred/DerivedLaws.lean +++ b/src/Std/Do/SPred/DerivedLaws.lean @@ -16,15 +16,16 @@ the laws in `Std.Do.Laws`. namespace Std.Do.SPred -variable {σs : List Type} {P P' Q Q' R R' : SPred σs} {φ φ₁ φ₂ : Prop} +universe u +variable {σs : List (Type u)} {P P' Q Q' R R' : SPred σs} {φ φ₁ φ₂ : Prop} -theorem entails.rfl {σs : List Type} {P : SPred σs} : P ⊢ₛ P := entails.refl P +theorem entails.rfl : P ⊢ₛ P := entails.refl P -theorem bientails.rfl {σs : List Type} {P : SPred σs} : P ⊣⊢ₛ P := bientails.refl P -theorem bientails.of_eq {σs : List Type} {P Q : SPred σs} (h : P = Q) : P ⊣⊢ₛ Q := h ▸ .rfl +theorem bientails.rfl {P : SPred σs} : P ⊣⊢ₛ P := bientails.refl P +theorem bientails.of_eq {P Q : SPred σs} (h : P = Q) : P ⊣⊢ₛ Q := h ▸ .rfl -theorem bientails.mp {σs : List Type} {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (P ⊢ₛ Q) := fun h => (bientails.iff.mp h).1 -theorem bientails.mpr {σs : List Type} {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊢ₛ P) := fun h => (bientails.iff.mp h).2 +theorem bientails.mp {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (P ⊢ₛ Q) := fun h => (bientails.iff.mp h).1 +theorem bientails.mpr {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊢ₛ P) := fun h => (bientails.iff.mp h).2 /-! # Connectives -/ @@ -145,7 +146,7 @@ theorem pure_forall {φ : α → Prop} : (∀ x, (⌜φ x⌝ : SPred σs)) ⊣ theorem pure_exists {φ : α → Prop} : (∃ x, ⌜φ x⌝ : SPred σs) ⊣⊢ₛ ⌜∃ x, φ x⌝ := bientails.iff.mpr ⟨exists_elim fun a => pure_mono (⟨a, ·⟩), pure_elim' fun ⟨x, h⟩ => (pure_intro h).trans (exists_intro' x .rfl)⟩ @[simp] theorem true_intro_simp : (Q ⊢ₛ ⌜True⌝) ↔ True := iff_true_intro true_intro -@[simp] theorem true_intro_simp_nil {Q : SPred []} : (Q ⊢ₛ True) ↔ True := true_intro_simp +@[simp] theorem true_intro_simp_nil {Q : SPred []} : (Q ⊢ₛ ⌜True⌝) ↔ True := true_intro_simp /-! # Miscellaneous -/ @@ -154,27 +155,27 @@ theorem and_right_comm : (P ∧ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∧ Q := and_assoc. /-! # Working with entailment -/ -theorem entails_pure_intro {σs : List Type} (P Q : Prop) (h : P → Q) : entails ⌜P⌝ (σs := σs) ⌜Q⌝ := pure_elim' fun hp => pure_intro (h hp) +theorem entails_pure_intro (P Q : Prop) (h : P → Q) : entails ⌜P⌝ (σs := σs) ⌜Q⌝ := pure_elim' fun hp => pure_intro (h hp) -@[simp] theorem entails_elim_nil (P Q : SPred []) : entails P Q ↔ P → Q := iff_of_eq rfl -theorem entails_elim_cons {σ : Type} {σs : List Type} (P Q : SPred (σ::σs)) : P ⊢ₛ Q ↔ ∀ s, (P s ⊢ₛ Q s) := by simp only [entails] -@[simp] theorem entails_pure_elim_cons {σ : Type} {σs : List Type} [Inhabited σ] (P Q : Prop) : entails ⌜P⌝ (σs := σ::σs) ⌜Q⌝ ↔ entails ⌜P⌝ (σs := σs) ⌜Q⌝:= by simp [entails] -@[simp] theorem entails_true_intro {σs : List Type} (P Q : SPred σs) : ⊢ₛ P → Q ↔ P ⊢ₛ Q := Iff.intro (fun h => (and_intro true_intro .rfl).trans (imp_elim h)) (fun h => imp_intro (and_elim_r.trans h)) +@[simp] theorem entails_elim_nil (P Q : SPred []) : entails P Q ↔ P.down → Q.down := iff_of_eq rfl +theorem entails_elim_cons {σ : Type u} (P Q : SPred (σ::σs)) : P ⊢ₛ Q ↔ ∀ s, (P s ⊢ₛ Q s) := by simp only [entails] +@[simp] theorem entails_pure_elim_cons {σ : Type u} [Inhabited σ] (P Q : Prop) : entails ⌜P⌝ (σs := σ::σs) ⌜Q⌝ ↔ entails ⌜P⌝ (σs := σs) ⌜Q⌝:= by simp [entails] +@[simp] theorem entails_true_intro (P Q : SPred σs) : ⊢ₛ P → Q ↔ P ⊢ₛ Q := Iff.intro (fun h => (and_intro true_intro .rfl).trans (imp_elim h)) (fun h => imp_intro (and_elim_r.trans h)) /-! # Tactic support -/ namespace Tactic /-- Tautology in `SPred` as a quotable definition. -/ -abbrev tautological {σs : List Type} (Q : SPred σs) : Prop := ⊢ₛ Q +abbrev tautological (Q : SPred σs) : Prop := ⊢ₛ Q -class PropAsSPredTautology (φ : Prop) {σs : outParam (List Type)} (P : outParam (SPred σs)) : Prop where +class PropAsSPredTautology (φ : Prop) {σs : outParam (List (Type u))} (P : outParam (SPred σs)) : Prop where iff : φ ↔ ⊢ₛ P -instance : PropAsSPredTautology (σs := []) φ φ where iff := true_imp_iff.symm +instance {φ : ULift Prop} : PropAsSPredTautology.{0} (σs := []) φ.down φ where iff := true_imp_iff.symm instance : PropAsSPredTautology (P ⊢ₛ Q) spred(P → Q) where iff := (entails_true_intro P Q).symm instance : PropAsSPredTautology (⊢ₛ P) P where iff := Iff.rfl -class IsPure {σs : List Type} (P : SPred σs) (φ : outParam Prop) where to_pure : P ⊣⊢ₛ ⌜φ⌝ +class IsPure (P : SPred σs) (φ : outParam Prop) where to_pure : P ⊣⊢ₛ ⌜φ⌝ instance (σs) : IsPure (σs:=σs) ⌜φ⌝ φ where to_pure := .rfl instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ → ⌜ψ⌝) (φ → ψ) where to_pure := pure_imp instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ ∧ ⌜ψ⌝) (φ ∧ ψ) where to_pure := pure_and @@ -182,9 +183,10 @@ 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 (P : Prop) : IsPure (σs:=[]) P P where to_pure := Iff.rfl +instance (φ : Prop) : IsPure (σs:=[]) ⌜φ⌝ φ where to_pure := Iff.rfl +instance (P : SPred []) : IsPure (σs:=[]) P P.down where to_pure := Iff.rfl -class IsAnd {σs : List Type} (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) where +class IsAnd (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) where to_and : P ⊣⊢ₛ Q₁ ∧ Q₂ instance (σs) (Q₁ Q₂ : SPred σs) : IsAnd (σs:=σs) spred(Q₁ ∧ Q₂) Q₁ Q₂ where to_and := .rfl instance (σs) : IsAnd (σs:=σs) ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝ where to_and := pure_and.symm @@ -193,34 +195,34 @@ instance (σs) (P Q₁ Q₂ : σ → SPred σs) [base : ∀ s, IsAnd (P s) (Q₁ theorem ProofMode.start_entails {φ : Prop} [PropAsSPredTautology φ P] : (⊢ₛ P) → φ := PropAsSPredTautology.iff.mpr theorem ProofMode.elim_entails {φ : Prop} [PropAsSPredTautology φ P] : φ → (⊢ₛ P) := PropAsSPredTautology.iff.mp -theorem Assumption.left {σs : List Type} {P Q R : SPred σs} (h : P ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_l.trans h -theorem Assumption.right {σs : List Type} {P Q R : SPred σs} (h : Q ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_r.trans h -theorem SCases.add_goal {σs} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (hgoal : P ⊢ₛ T) : Q ∧ H ⊢ₛ T := hand.mp.trans hgoal -theorem SCases.clear {σs} {Q H T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ∧ H ⊢ₛ T := (and_mono_r true_intro).trans hgoal -theorem SCases.pure {σs} {Q T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ⊢ₛ T := (and_intro .rfl true_intro).trans hgoal -theorem SCases.and_1 {σs} {Q H₁' H₂' H₁₂' T : SPred σs} (hand : H₁' ∧ H₂' ⊣⊢ₛ H₁₂') (hgoal : Q ∧ H₁₂' ⊢ₛ T) : (Q ∧ H₁') ∧ H₂' ⊢ₛ T := ((and_congr_r hand.symm).trans and_assoc.symm).mpr.trans hgoal -theorem SCases.and_2 {σs} {Q H₁' H₂ T : SPred σs} (hgoal : (Q ∧ H₁') ∧ H₂ ⊢ₛ T) : (Q ∧ H₂) ∧ H₁' ⊢ₛ T := and_right_comm.mp.trans hgoal -theorem SCases.and_3 {σs} {Q H₁ H₂ H T : SPred σs} (hand : H ⊣⊢ₛ H₁ ∧ H₂) (hgoal : (Q ∧ H₂) ∧ H₁ ⊢ₛ T) : Q ∧ H ⊢ₛ T := (and_congr_r hand).mp.trans (and_assoc.mpr.trans (and_right_comm.mp.trans hgoal)) -theorem SCases.exists {σs : List Type} {Q : SPred σs} {ψ : α → SPred σs} {T : SPred σs} (h : ∀ a, Q ∧ ψ a ⊢ₛ T) : Q ∧ (∃ a, ψ a) ⊢ₛ T := imp_elim' (exists_elim fun a => imp_intro (entails.trans and_symm (h a))) -theorem Clear.clear {σs : List Type} {P P' A Q : SPred σs} (hfocus : P ⊣⊢ₛ P' ∧ A) (h : P' ⊢ₛ Q) : P ⊢ₛ Q := hfocus.mp.trans <| (and_mono_l h).trans and_elim_l -theorem Exact.assumption {σs : List Type} {P P' A : SPred σs} (h : P ⊣⊢ₛ P' ∧ A) : P ⊢ₛ A := h.mp.trans and_elim_r -theorem Exact.from_tautology {σs : List Type} {P T : SPred σs} [PropAsSPredTautology φ T] (h : φ) : P ⊢ₛ T := true_intro.trans (PropAsSPredTautology.iff.mp h) -theorem Focus.this {σs : List Type} {P : SPred σs} : P ⊣⊢ₛ ⌜True⌝ ∧ P := true_and.symm -theorem Focus.left {σs : List Type} {P P' Q C R : SPred σs} (h₁ : P ⊣⊢ₛ P' ∧ R) (h₂ : P' ∧ Q ⊣⊢ₛ C) : P ∧ Q ⊣⊢ₛ C ∧ R := (and_congr_l h₁).trans (and_right_comm.trans (and_congr_l h₂)) -theorem Focus.right {σs : List Type} {P Q Q' C R : SPred σs} (h₁ : Q ⊣⊢ₛ Q' ∧ R) (h₂ : P ∧ Q' ⊣⊢ₛ C) : P ∧ Q ⊣⊢ₛ C ∧ R := (and_congr_r h₁).trans (and_assoc.symm.trans (and_congr_l h₂)) +theorem Assumption.left {P Q R : SPred σs} (h : P ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_l.trans h +theorem Assumption.right {P Q R : SPred σs} (h : Q ⊢ₛ R) : P ∧ Q ⊢ₛ R := and_elim_r.trans h +theorem Cases.add_goal {σs} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (hgoal : P ⊢ₛ T) : Q ∧ H ⊢ₛ T := hand.mp.trans hgoal +theorem Cases.clear {σs} {Q H T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ∧ H ⊢ₛ T := (and_mono_r true_intro).trans hgoal +theorem Cases.pure {σs} {Q T : SPred σs} (hgoal : Q ∧ ⌜True⌝ ⊢ₛ T) : Q ⊢ₛ T := (and_intro .rfl true_intro).trans hgoal +theorem Cases.and_1 {σs} {Q H₁' H₂' H₁₂' T : SPred σs} (hand : H₁' ∧ H₂' ⊣⊢ₛ H₁₂') (hgoal : Q ∧ H₁₂' ⊢ₛ T) : (Q ∧ H₁') ∧ H₂' ⊢ₛ T := ((and_congr_r hand.symm).trans and_assoc.symm).mpr.trans hgoal +theorem Cases.and_2 {σs} {Q H₁' H₂ T : SPred σs} (hgoal : (Q ∧ H₁') ∧ H₂ ⊢ₛ T) : (Q ∧ H₂) ∧ H₁' ⊢ₛ T := and_right_comm.mp.trans hgoal +theorem Cases.and_3 {σs} {Q H₁ H₂ H T : SPred σs} (hand : H ⊣⊢ₛ H₁ ∧ H₂) (hgoal : (Q ∧ H₂) ∧ H₁ ⊢ₛ T) : Q ∧ H ⊢ₛ T := (and_congr_r hand).mp.trans (and_assoc.mpr.trans (and_right_comm.mp.trans hgoal)) +theorem Cases.exists {Q : SPred σs} {ψ : α → SPred σs} {T : SPred σs} (h : ∀ a, Q ∧ ψ a ⊢ₛ T) : Q ∧ (∃ a, ψ a) ⊢ₛ T := imp_elim' (exists_elim fun a => imp_intro (entails.trans and_symm (h a))) +theorem Clear.clear {P P' A Q : SPred σs} (hfocus : P ⊣⊢ₛ P' ∧ A) (h : P' ⊢ₛ Q) : P ⊢ₛ Q := hfocus.mp.trans <| (and_mono_l h).trans and_elim_l +theorem Exact.assumption {P P' A : SPred σs} (h : P ⊣⊢ₛ P' ∧ A) : P ⊢ₛ A := h.mp.trans and_elim_r +theorem Exact.from_tautology {P T : SPred σs} [PropAsSPredTautology φ T] (h : φ) : P ⊢ₛ T := true_intro.trans (PropAsSPredTautology.iff.mp h) +theorem Focus.this {P : SPred σs} : P ⊣⊢ₛ ⌜True⌝ ∧ P := true_and.symm +theorem Focus.left {P P' Q C R : SPred σs} (h₁ : P ⊣⊢ₛ P' ∧ R) (h₂ : P' ∧ Q ⊣⊢ₛ C) : P ∧ Q ⊣⊢ₛ C ∧ R := (and_congr_l h₁).trans (and_right_comm.trans (and_congr_l h₂)) +theorem Focus.right {P Q Q' C R : SPred σs} (h₁ : Q ⊣⊢ₛ Q' ∧ R) (h₂ : P ∧ Q' ⊣⊢ₛ C) : P ∧ Q ⊣⊢ₛ C ∧ R := (and_congr_r h₁).trans (and_assoc.symm.trans (and_congr_l h₂)) theorem Focus.rewrite_hyps {σs} {P Q R : SPred σs} (hrw : P ⊣⊢ₛ Q) (hgoal : Q ⊢ₛ R) : P ⊢ₛ R := hrw.mp.trans hgoal -theorem Have.dup {σs : List Type} {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (hgoal : P ∧ H ⊢ₛ T) : P ⊢ₛ T := (and_intro .rfl (hfoc.mp.trans and_elim_r)).trans hgoal -theorem Have.have {σs : List Type} {P H PH T : SPred σs} (hand : P ∧ H ⊣⊢ₛ PH) (hhave : P ⊢ₛ H) (hgoal : PH ⊢ₛ T) : P ⊢ₛ T := (and_intro .rfl hhave).trans (hand.mp.trans hgoal) -theorem Have.replace {σs : List Type} {P H H' PH PH' T : SPred σs} (hfoc : PH ⊣⊢ₛ P ∧ H ) (hand : P ∧ H' ⊣⊢ₛ PH') (hhave : PH ⊢ₛ H') (hgoal : PH' ⊢ₛ T) : PH ⊢ₛ T := (and_intro (hfoc.mp.trans and_elim_l) hhave).trans (hand.mp.trans hgoal) -theorem Intro.intro {σs : List Type} {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (h : P ⊢ₛ T) : Q ⊢ₛ H → T := imp_intro (hand.mp.trans h) -theorem Pure.thm {σs : List Type} {P Q T : SPred σs} {φ : Prop} [IsPure Q φ] (h : φ → P ⊢ₛ T) : P ∧ Q ⊢ₛ T := by +theorem Have.dup {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (hgoal : P ∧ H ⊢ₛ T) : P ⊢ₛ T := (and_intro .rfl (hfoc.mp.trans and_elim_r)).trans hgoal +theorem Have.have {P H PH T : SPred σs} (hand : P ∧ H ⊣⊢ₛ PH) (hhave : P ⊢ₛ H) (hgoal : PH ⊢ₛ T) : P ⊢ₛ T := (and_intro .rfl hhave).trans (hand.mp.trans hgoal) +theorem Have.replace {P H H' PH PH' T : SPred σs} (hfoc : PH ⊣⊢ₛ P ∧ H ) (hand : P ∧ H' ⊣⊢ₛ PH') (hhave : PH ⊢ₛ H') (hgoal : PH' ⊢ₛ T) : PH ⊢ₛ T := (and_intro (hfoc.mp.trans and_elim_l) hhave).trans (hand.mp.trans hgoal) +theorem Intro.intro {P Q H T : SPred σs} (hand : Q ∧ H ⊣⊢ₛ P) (h : P ⊢ₛ T) : Q ⊢ₛ H → T := imp_intro (hand.mp.trans h) +theorem Pure.thm {P Q T : SPred σs} {φ : Prop} [IsPure Q φ] (h : φ → P ⊢ₛ T) : P ∧ Q ⊢ₛ T := by apply pure_elim · exact and_elim_r.trans IsPure.to_pure.mp · intro hp exact and_elim_l.trans (h hp) /-- A generalization of `pure_intro` exploiting `IsPure`. -/ -theorem Pure.intro {σs : List Type} {P Q : SPred σs} {φ : Prop} [IsPure Q φ] (hp : φ) : P ⊢ₛ Q := (pure_intro hp).trans IsPure.to_pure.mpr -theorem Revert.revert {σs : List Type} {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (h : Q ⊢ₛ H → T) : P ⊢ₛ T := hfoc.mp.trans (imp_elim h) +theorem Pure.intro {P Q : SPred σs} {φ : Prop} [IsPure Q φ] (hp : φ) : P ⊢ₛ Q := (pure_intro hp).trans IsPure.to_pure.mpr +theorem Revert.revert {P Q H T : SPred σs} (hfoc : P ⊣⊢ₛ Q ∧ H) (h : Q ⊢ₛ H → T) : P ⊢ₛ T := hfoc.mp.trans (imp_elim h) theorem Specialize.imp_stateful {P P' Q R : SPred σs} (hrefocus : P ∧ (Q → R) ⊣⊢ₛ P' ∧ Q) : P ∧ (Q → R) ⊢ₛ P ∧ R := by calc spred(P ∧ (Q → R)) @@ -241,17 +243,18 @@ theorem Specialize.pure_start {φ : Prop} {H P T : SPred σs} [PropAsSPredTautol theorem Specialize.pure_taut {σs} {φ} {P : SPred σs} [IsPure P φ] (h : φ) : ⊢ₛ P := (pure_intro h).trans IsPure.to_pure.mpr theorem Specialize.focus {P P' Q R : SPred σs} (hfocus : P ⊣⊢ₛ P' ∧ Q) (hnew : P' ∧ Q ⊢ₛ R) : P ⊢ₛ R := hfocus.mp.trans hnew -class SimpAnd {σs : List Type} (P Q : SPred σs) (PQ : outParam (SPred σs)) : Prop where +class SimpAnd (P Q : SPred σs) (PQ : outParam (SPred σs)) : Prop where simp_and : P ∧ Q ⊣⊢ₛ PQ instance (σs) (P Q : SPred σs) : SimpAnd P Q (spred(P ∧ Q)) where simp_and := .rfl instance (σs) (P : SPred σs) : SimpAnd P ⌜True⌝ P where simp_and := and_true instance (σs) (P : SPred σs) : SimpAnd ⌜True⌝ P P where simp_and := true_and -class HasFrame {σs : List Type} (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) : Prop where +class HasFrame (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) : Prop where reassoc : P ⊣⊢ₛ P' ∧ ⌜φ⌝ instance (σs) : HasFrame (σs:=σs) ⌜φ⌝ ⌜True⌝ φ where reassoc := true_and.symm 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' : 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 instance (σs) (P P' Q Q' QQ : SPred σs) [HasFrame P Q φ] [HasFrame P' Q' ψ] [SimpAnd Q Q' QQ]: HasFrame (σs:=σs) spred(P ∧ P') QQ (φ ∧ ψ) where @@ -277,9 +280,10 @@ instance (σs) (P Q : SPred σs) [HasFrame P Q ψ] : HasFrame (σs:=σs) spred(P <| and_congr_r (and_comm.trans pure_and) -- The following instance comes last so that it gets the highest priority. -- It's the most efficient and best solution if valid -instance {P : Prop} : HasFrame (σs:=[]) P ⌜True⌝ P where reassoc := true_and.symm +instance {φ : Prop} : HasFrame (σs:=[]) ⌜φ⌝ ⌜True⌝ φ where reassoc := true_and.symm +instance {P : SPred []} : HasFrame (σs:=[]) P ⌜True⌝ P.down where reassoc := true_and.symm -theorem Frame.frame {σs : List Type} {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ] +theorem Frame.frame {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ] (h : φ → Q ⊢ₛ T) : P ⊢ₛ T := by apply SPred.pure_elim · exact HasFrame.reassoc.mp.trans SPred.and_elim_r diff --git a/src/Std/Do/SPred/Laws.lean b/src/Std/Do/SPred/Laws.lean index ac6d6ed774..16e1678d6e 100644 --- a/src/Std/Do/SPred/Laws.lean +++ b/src/Std/Do/SPred/Laws.lean @@ -18,25 +18,28 @@ be derived without doing so. `Std.Do.SPred.DerivedLaws` has some more laws that are derivative of what follows. -/ +universe u +variable {σs : List (Type u)} + /-! # Entailment -/ @[refl, simp] -theorem entails.refl {σs : List Type} (P : SPred σs) : P ⊢ₛ P := by - match σs with - | [] => simp [entails] - | σ :: _ => intro s; exact entails.refl (P s) +theorem entails.refl (P : SPred σs) : P ⊢ₛ P := by + induction σs with + | nil => simp [entails] + | cons σ _ ih => intro s; exact ih (P s) -theorem entails.trans {σs : List Type} {P Q R : SPred σs} : (P ⊢ₛ Q) → (Q ⊢ₛ R) → (P ⊢ₛ R) := by - match σs with - | [] => intro h₁ h₂; exact h₂ ∘ h₁ - | σ :: _ => intro h₁ h₂; intro s; exact entails.trans (h₁ s) (h₂ s) +theorem entails.trans {P Q R : SPred σs} : (P ⊢ₛ Q) → (Q ⊢ₛ R) → (P ⊢ₛ R) := by + induction σs with + | nil => intro h₁ h₂; exact h₂ ∘ h₁ + | cons σ _ ih => intro h₁ h₂; intro s; exact ih (h₁ s) (h₂ s) -instance {σs : List Type} : Trans (@entails σs) entails entails where +instance : Trans (@entails σs) entails entails where trans := entails.trans /-! # Bientailment -/ -theorem bientails.iff {σs : List Type} {P Q : SPred σs} : P ⊣⊢ₛ Q ↔ (P ⊢ₛ Q) ∧ (Q ⊢ₛ P) := by +theorem bientails.iff {P Q : SPred σs} : P ⊣⊢ₛ Q ↔ (P ⊢ₛ Q) ∧ (Q ⊢ₛ P) := by induction σs with | nil => exact Iff.intro (fun h => ⟨h.mp, h.mpr⟩) (fun h => ⟨h.1, h.2⟩) | cons σ σs ih => @@ -45,43 +48,43 @@ theorem bientails.iff {σs : List Type} {P Q : SPred σs} : P ⊣⊢ₛ Q ↔ (P · intro h s; exact ih.mpr ⟨h.1 s, h.2 s⟩ @[refl, simp] -theorem bientails.refl {σs : List Type} (P : SPred σs) : P ⊣⊢ₛ P := by +theorem bientails.refl (P : SPred σs) : P ⊣⊢ₛ P := by induction σs <;> simp [bientails, *] -theorem bientails.trans {σs : List Type} {P Q R : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ R) → (P ⊣⊢ₛ R) := by +theorem bientails.trans {P Q R : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ R) → (P ⊣⊢ₛ R) := by induction σs case nil => simp +contextual only [bientails, implies_true] case cons σ σs ih => intro hpq hqr s; exact ih (hpq s) (hqr s) -instance {σs : List Type} : Trans (@bientails σs) bientails bientails where +instance : Trans (@bientails σs) bientails bientails where trans := bientails.trans -theorem bientails.symm {σs : List Type} {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ P) := by +theorem bientails.symm {P Q : SPred σs} : (P ⊣⊢ₛ Q) → (Q ⊣⊢ₛ P) := by induction σs case nil => exact Iff.symm case cons σ σs ih => intro h s; exact ih (h s) -theorem bientails.to_eq {σs : List Type} {P Q : SPred σs} (h : P ⊣⊢ₛ Q) : P = Q := by +theorem bientails.to_eq {P Q : SPred σs} (h : P ⊣⊢ₛ Q) : P = Q := by induction σs - case nil => rw[iff_iff_eq.mp h] + case nil => ext; rw [iff_iff_eq.mp h] case cons σ σs ih => ext s; rw[ih (h s)] /-! # Pure -/ -theorem pure_intro {σs : List Type} {φ : Prop} {P : SPred σs} : φ → P ⊢ₛ ⌜φ⌝ := by - induction σs <;> simp_all [entails] +theorem pure_intro {φ : Prop} {P : SPred σs} : φ → P ⊢ₛ ⌜φ⌝ := by + induction σs <;> simp_all [entails, SVal.curry] -theorem pure_elim' {σs : List Type} {φ : Prop} {P : SPred σs} : (φ → ⌜True⌝ ⊢ₛ P) → ⌜φ⌝ ⊢ₛ P := by - induction σs <;> simp_all [entails] +theorem pure_elim' {φ : Prop} {P : SPred σs} : (φ → ⌜True⌝ ⊢ₛ P) → ⌜φ⌝ ⊢ₛ P := by + induction σs <;> simp_all [entails, SVal.curry] -- Ideally, we'd like to prove the following theorem: --- theorem pure_elim' {σs : List Type} {φ : Prop} : SPred.entails (σs:=σs) ⌜True⌝ ⌜φ⌝ → φ +-- theorem pure_elim' {φ : Prop} : SPred.entails (σs:=σs) ⌜True⌝ ⌜φ⌝ → φ -- Unfortunately, this is only true if all `σs` are Inhabited. /-! # Conjunction -/ -theorem and_intro {σs : List Type} {P Q R : SPred σs} (h1 : P ⊢ₛ Q) (h2 : P ⊢ₛ R) : P ⊢ₛ Q ∧ R := by +theorem and_intro {P Q R : SPred σs} (h1 : P ⊢ₛ Q) (h2 : P ⊢ₛ R) : P ⊢ₛ Q ∧ R := by induction σs <;> simp_all [entails] theorem and_elim_l {P Q : SPred σs} : P ∧ Q ⊢ₛ P := by @@ -92,39 +95,56 @@ theorem and_elim_r {P Q : SPred σs} : P ∧ Q ⊢ₛ Q := by /-! # Disjunction -/ -theorem or_intro_l {σs : List Type} {P Q : SPred σs} : P ⊢ₛ P ∨ Q := by +theorem or_intro_l {P Q : SPred σs} : P ⊢ₛ P ∨ Q := by induction σs <;> simp_all [entails] -theorem or_intro_r {σs : List Type} {P Q : SPred σs} : Q ⊢ₛ P ∨ Q := by +theorem or_intro_r {P Q : SPred σs} : Q ⊢ₛ P ∨ Q := by induction σs <;> simp_all [entails] -theorem or_elim {σs : List Type} {P Q R : SPred σs} (h1 : P ⊢ₛ R) (h2 : Q ⊢ₛ R) : P ∨ Q ⊢ₛ R := by +theorem or_elim {P Q R : SPred σs} (h1 : P ⊢ₛ R) (h2 : Q ⊢ₛ R) : P ∨ Q ⊢ₛ R := by induction σs case nil => exact (Or.elim · h1 h2) case cons => simp_all [entails] /-! # Implication -/ -theorem imp_intro {σs : List Type} {P Q R : SPred σs} (h : P ∧ Q ⊢ₛ R) : P ⊢ₛ Q → R := by +theorem imp_intro {P Q R : SPred σs} (h : P ∧ Q ⊢ₛ R) : P ⊢ₛ Q → R := by induction σs <;> simp_all [entails] -theorem imp_elim {σs : List Type} {P Q R : SPred σs} (h : P ⊢ₛ Q → R) : P ∧ Q ⊢ₛ R := by +theorem imp_elim {P Q R : SPred σs} (h : P ⊢ₛ Q → R) : P ∧ Q ⊢ₛ R := by induction σs <;> simp_all [entails] /-! # Quantifiers -/ -theorem forall_intro {σs : List Type} {P : SPred σs} {Ψ : α → SPred σs} (h : ∀ a, P ⊢ₛ Ψ a) : P ⊢ₛ ∀ a, Ψ a := by +theorem forall_intro {P : SPred σs} {Ψ : α → SPred σs} (h : ∀ a, P ⊢ₛ Ψ a) : P ⊢ₛ ∀ a, Ψ a := by induction σs <;> simp_all [entails] -theorem forall_elim {σs : List Type} {Ψ : α → SPred σs} (a : α) : (∀ a, Ψ a) ⊢ₛ Ψ a := by +theorem forall_elim {Ψ : α → SPred σs} (a : α) : (∀ a, Ψ a) ⊢ₛ Ψ a := by induction σs <;> simp_all [entails] -theorem exists_intro {σs : List Type} {Ψ : α → SPred σs} (a : α) : Ψ a ⊢ₛ ∃ a, Ψ a := by +theorem exists_intro {Ψ : α → SPred σs} (a : α) : Ψ a ⊢ₛ ∃ a, Ψ a := by induction σs case nil => intro _; exists a case cons σ σs ih => intro s; exact @ih (fun a => Ψ a s) -theorem exists_elim {σs : List Type} {Φ : α → SPred σs} {Q : SPred σs} (h : ∀ a, Φ a ⊢ₛ Q) : (∃ a, Φ a) ⊢ₛ Q := by +theorem exists_elim {Φ : α → SPred σs} {Q : SPred σs} (h : ∀ a, Φ a ⊢ₛ Q) : (∃ a, Φ a) ⊢ₛ Q := by induction σs case nil => intro ⟨a, ha⟩; exact h a ha case cons σ σs ih => intro s; exact ih (fun a => h a s) + +/-! # Curry -/ + +theorem and_curry {P Q : SVal.StateTuple σs → Prop} : SVal.curry (fun t => ⟨P t⟩) ∧ SVal.curry (fun t => ⟨Q t⟩) ⊣⊢ₛ (SVal.curry fun t => ⟨P t ∧ Q t⟩) := by + induction σs + case nil => rfl + case cons σ σs ih => intro s; simp only [and_cons, SVal.curry_cons]; exact ih + +theorem or_curry {P Q : SVal.StateTuple σs → Prop} : SVal.curry (fun t => ⟨P t⟩) ∨ SVal.curry (fun t => ⟨Q t⟩) ⊣⊢ₛ (SVal.curry fun t => ⟨P t ∨ Q t⟩) := by + induction σs + case nil => rfl + case cons σ σs ih => intro s; simp only [or_cons, SVal.curry_cons]; exact ih + +theorem imp_curry {P Q : SVal.StateTuple σs → Prop} : (SVal.curry (fun t => ⟨P t⟩) → SVal.curry (fun t => ⟨Q t⟩)) ⊣⊢ₛ (SVal.curry fun t => ⟨P t → Q t⟩) := by + induction σs + case nil => rfl + case cons σ σs ih => intro s; simp only [imp_cons, SVal.curry_cons]; exact ih diff --git a/src/Std/Do/SPred/Notation.lean b/src/Std/Do/SPred/Notation.lean index 5643dd26db..f0a3855dbc 100644 --- a/src/Std/Do/SPred/Notation.lean +++ b/src/Std/Do/SPred/Notation.lean @@ -64,7 +64,7 @@ scoped syntax:25 "⊢ₛ " term:25 : term scoped syntax:25 term:25 " ⊣⊢ₛ " term:25 : term macro_rules - | `(⌜$t⌝) => ``(SVal.curry (fun tuple => $t)) + | `(⌜$t⌝) => ``(SVal.curry (fun tuple => ULift.up $t)) | `(#$t) => `(SVal.uncurry $t (by assumption)) | `(‹$t›ₛ) => `(#(SVal.getThe $t)) | `($P ⊢ₛ $Q) => ``(SPred.entails spred($P) spred($Q)) @@ -93,7 +93,7 @@ namespace SPred.Notation private def unexpandCurry : Unexpander | `($_ $t $ts*) => do match t with - | `(fun $_ => $e) => if ts.isEmpty then ``(⌜$e⌝) else ``(⌜$e⌝ $ts*) + | `(fun $_ => { down := $e }) => if ts.isEmpty then ``(⌜$e⌝) else ``(⌜$e⌝ $ts*) | _ => throw () | _ => throw () diff --git a/src/Std/Do/SPred/SPred.lean b/src/Std/Do/SPred/SPred.lean index efda94e974..4b8cd775ac 100644 --- a/src/Std/Do/SPred/SPred.lean +++ b/src/Std/Do/SPred/SPred.lean @@ -19,91 +19,98 @@ namespace Std.Do /-- A predicate indexed by a list of states. ``` - example : SPred [Nat, Bool] = (Nat → Bool → Prop) := rfl + example : SPred [Nat, Bool] = (Nat → Bool → ULift Prop) := rfl ``` -/ -abbrev SPred (σs : List Type) : Type := SVal σs Prop +abbrev SPred (σs : List (Type u)) : Type u := SVal σs (ULift Prop) 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⌝. -/ -private abbrev pure {σs : List Type} (P : Prop) : SPred σs := SVal.curry (fun _ => P) +private abbrev pure (P : Prop) : SPred σs := SVal.curry (fun _ => ⟨P⟩) @[ext] -theorem ext {σs : List Type} {P Q : SPred (σ::σs)} : (∀ s, P s = Q s) → P = Q := funext +theorem ext_nil {P Q : SPred []} (h : P.down ↔ Q.down) : P = Q := by + cases P; cases Q; simp_all + +@[ext] +theorem ext_cons {P Q : SPred (σ::σs)} : (∀ s, P s = Q s) → P = Q := funext /-- Entailment in `SPred`. -/ -def entails {σs : List Type} (P Q : SPred σs) : Prop := match σs with - | [] => P → Q +def entails {σs : List (Type u)} (P Q : SPred σs) : Prop := match σs with + | [] => P.down → Q.down | σ :: _ => ∀ (s : σ), entails (P s) (Q s) -@[simp] theorem entails_nil {P Q : SPred []} : entails P Q = (P → Q) := rfl -theorem entails_cons {σs : List Type} {P Q : SPred (σ::σs)} : entails P Q = (∀ s, entails (P s) (Q s)) := rfl -theorem entails_cons_intro {σs : List Type} {P Q : SPred (σ::σs)} : (∀ s, entails (P s) (Q s)) → entails P Q := by simp only [entails, imp_self] +@[simp] theorem entails_nil {P Q : SPred []} : entails P Q = (P.down → Q.down) := rfl +theorem entails_cons {P Q : SPred (σ::σs)} : entails P Q = (∀ s, entails (P s) (Q s)) := rfl +theorem entails_cons_intro {P Q : SPred (σ::σs)} : (∀ s, entails (P s) (Q s)) → entails P Q := by simp only [entails, imp_self] -- Reducibility of entails must be semi-reducible so that entails_refl is useful for rfl /-- Equivalence relation on `SPred`. Convert to `Eq` via `bientails.to_eq`. -/ -def bientails {σs : List Type} (P Q : SPred σs) : Prop := match σs with - | [] => P ↔ Q +def bientails {σs : List (Type u)} (P Q : SPred σs) : Prop := match σs with + | [] => P.down ↔ Q.down | σ :: _ => ∀ (s : σ), bientails (P s) (Q s) -@[simp] theorem bientails_nil {P Q : SPred []} : bientails P Q = (P ↔ Q) := rfl -theorem bientails_cons {σs : List Type} {P Q : SPred (σ::σs)} : bientails P Q = (∀ s, bientails (P s) (Q s)) := rfl -theorem bientails_cons_intro {σs : List Type} {P Q : SPred (σ::σs)} : (∀ s, bientails (P s) (Q s)) → bientails P Q := by simp only [bientails, imp_self] +@[simp] theorem bientails_nil {P Q : SPred []} : bientails P Q = (P.down ↔ Q.down) := rfl +theorem bientails_cons {P Q : SPred (σ::σs)} : bientails P Q = (∀ s, bientails (P s) (Q s)) := rfl +theorem bientails_cons_intro {P Q : SPred (σ::σs)} : (∀ s, bientails (P s) (Q s)) → bientails P Q := by simp only [bientails, imp_self] /-- Conjunction in `SPred`. -/ -def and {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with - | [] => P ∧ Q +def and {σs : List (Type u)} (P Q : SPred σs) : SPred σs := match σs with + | [] => ⟨P.down ∧ Q.down⟩ | σ :: _ => fun (s : σ) => and (P s) (Q s) -@[simp] theorem and_nil {P Q : SPred []} : and P Q = (P ∧ Q) := rfl -@[simp] theorem and_cons {σs : List Type} {P Q : SPred (σ::σs)} : and P Q s = and (P s) (Q s) := rfl +@[simp] theorem and_nil {P Q : SPred []} : and P Q = ⟨P.down ∧ Q.down⟩ := rfl +@[simp] theorem and_cons {P Q : SPred (σ::σs)} : and P Q s = and (P s) (Q s) := rfl /-- Disjunction in `SPred`. -/ -def or {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with - | [] => P ∨ Q +def or {σs : List (Type u)} (P Q : SPred σs) : SPred σs := match σs with + | [] => ⟨P.down ∨ Q.down⟩ | σ :: _ => fun (s : σ) => or (P s) (Q s) -@[simp] theorem or_nil {P Q : SPred []} : or P Q = (P ∨ Q) := rfl -@[simp] theorem or_cons {σs : List Type} {P Q : SPred (σ::σs)} : or P Q s = or (P s) (Q s) := rfl +@[simp] theorem or_nil {P Q : SPred []} : or P Q = ⟨P.down ∨ Q.down⟩ := rfl +@[simp] theorem or_cons {P Q : SPred (σ::σs)} : or P Q s = or (P s) (Q s) := rfl /-- Negation in `SPred`. -/ -def not {σs : List Type} (P : SPred σs) : SPred σs := match σs with - | [] => ¬ P +def not {σs : List (Type u)} (P : SPred σs) : SPred σs := match σs with + | [] => ⟨¬ P.down⟩ | σ :: _ => fun (s : σ) => not (P s) -@[simp] theorem not_nil {P : SPred []} : not P = (¬ P) := rfl -@[simp] theorem not_cons {σs : List Type} {P : SPred (σ::σs)} : not P s = not (P s) := rfl +@[simp] theorem not_nil {P : SPred []} : not P = ⟨¬ P.down⟩ := rfl +@[simp] theorem not_cons {P : SPred (σ::σs)} : not P s = not (P s) := rfl /-- Implication in `SPred`. -/ -def imp {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with - | [] => P → Q +def imp {σs : List (Type u)} (P Q : SPred σs) : SPred σs := match σs with + | [] => ⟨P.down → Q.down⟩ | σ :: _ => fun (s : σ) => imp (P s) (Q s) -@[simp] theorem imp_nil {P Q : SPred []} : imp P Q = (P → Q) := rfl -@[simp] theorem imp_cons {σs : List Type} {P Q : SPred (σ::σs)} : imp P Q s = imp (P s) (Q s) := rfl +@[simp] theorem imp_nil {P Q : SPred []} : imp P Q = ⟨P.down → Q.down⟩ := rfl +@[simp] theorem imp_cons {P Q : SPred (σ::σs)} : imp P Q s = imp (P s) (Q s) := rfl /-- Biconditional in `SPred`. -/ -def iff {σs : List Type} (P Q : SPred σs) : SPred σs := match σs with - | [] => P ↔ Q +def iff {σs : List (Type u)} (P Q : SPred σs) : SPred σs := match σs with + | [] => ⟨P.down ↔ Q.down⟩ | σ :: _ => fun (s : σ) => iff (P s) (Q s) -@[simp] theorem iff_nil {P Q : SPred []} : iff P Q = (P ↔ Q) := rfl -@[simp] theorem iff_cons {σs : List Type} {P Q : SPred (σ::σs)} : iff P Q s = iff (P s) (Q s) := rfl +@[simp] theorem iff_nil {P Q : SPred []} : iff P Q = ⟨P.down ↔ Q.down⟩ := rfl +@[simp] theorem iff_cons {P Q : SPred (σ::σs)} : iff P Q s = iff (P s) (Q s) := rfl /-- Existential quantifier in `SPred`. -/ -def «exists» {α} {σs : List Type} (P : α → SPred σs) : SPred σs := match σs with - | [] => ∃ a, P a +def «exists» {α} {σs : List (Type u)} (P : α → SPred σs) : SPred σs := match σs with + | [] => ⟨∃ a, (P a).down⟩ | σ :: _ => fun (s : σ) => «exists» (fun a => P a s) -@[simp] theorem exists_nil {α} {P : α → SPred []} : «exists» P = (∃ a, P a) := rfl -@[simp] theorem exists_cons {σs : List Type} {α} {P : α → SPred (σ::σs)} : «exists» P s = «exists» (fun a => P a s) := rfl +@[simp] theorem exists_nil {α} {P : α → SPred []} : «exists» P = ⟨∃ a, (P a).down⟩ := rfl +@[simp] theorem exists_cons {α} {P : α → SPred (σ::σs)} : «exists» P s = «exists» (fun a => P a s) := rfl /-- Universal quantifier in `SPred`. -/ -def «forall» {α} {σs : List Type} (P : α → SPred σs) : SPred σs := match σs with - | [] => ∀ a, P a +def «forall» {α} {σs : List (Type u)} (P : α → SPred σs) : SPred σs := match σs with + | [] => ⟨∀ a, (P a).down⟩ | σ :: _ => fun (s : σ) => «forall» (fun a => P a s) -@[simp] theorem forall_nil {α} {P : α → SPred []} : «forall» P = (∀ a, P a) := rfl -@[simp] theorem forall_cons {σs : List Type} {α} {P : α → SPred (σ::σs)} : «forall» P s = «forall» (fun a => P a s) := rfl +@[simp] theorem forall_nil {α} {P : α → SPred []} : «forall» P = ⟨∀ a, (P a).down⟩ := rfl +@[simp] theorem forall_cons {α} {P : α → SPred (σ::σs)} : «forall» P s = «forall» (fun a => P a s) := rfl /-- Conjunction of a list of `SPred`. -/ -def conjunction {σs : List Type} (env : List (SPred σs)) : SPred σs := match env with +def conjunction {σs : List (Type u)} (env : List (SPred σs)) : SPred σs := match env with | [] => pure True | P::env => P.and (conjunction env) -@[simp] theorem conjunction_nil {σs : List Type} : conjunction ([] : List (SPred σs)) = pure True := rfl -@[simp] theorem conjunction_cons {σs : List Type} {P : SPred σs} {env : List (SPred σs)} : conjunction (P::env) = P.and (conjunction env) := rfl -@[simp] theorem conjunction_apply {σs : List Type} {env : List (SPred (σ::σs))} : conjunction env s = conjunction (env.map (· s)) := by +@[simp] theorem conjunction_nil : conjunction ([] : List (SPred σs)) = pure True := rfl +@[simp] theorem conjunction_cons {P : SPred σs} {env : List (SPred σs)} : conjunction (P::env) = P.and (conjunction env) := rfl +@[simp] theorem conjunction_apply {env : List (SPred (σ::σs))} : conjunction env s = conjunction (env.map (· s)) := by induction env <;> simp [conjunction, *] diff --git a/src/Std/Do/SPred/SVal.lean b/src/Std/Do/SPred/SVal.lean index 1047ef097b..bc6473404c 100644 --- a/src/Std/Do/SPred/SVal.lean +++ b/src/Std/Do/SPred/SVal.lean @@ -16,19 +16,19 @@ namespace Std.Do example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl ``` -/ -abbrev SVal (σs : List Type) (α : Type) := match σs with +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.) +(Begs for investigation. #8074.) -/ namespace SVal /-- A tuple capturing the whole state of an `SVal`. -/ -def StateTuple (σs : List Type) := match σs with - | [] => Unit +def StateTuple (σs : List (Type u)) : Type u := match σs with + | [] => PUnit | σ :: σs => σ × StateTuple σs instance : Inhabited (StateTuple []) where @@ -38,29 +38,29 @@ instance [Inhabited σ] [Inhabited (StateTuple σs)] : Inhabited (StateTuple (σ default := (default, default) /-- Curry a function taking a `StateTuple` into an `SVal`. -/ -def curry {σs : List Type} (f : StateTuple σs → α) : SVal σs α := match σs with - | [] => f () +def curry {σs : List (Type u)} (f : StateTuple σs → α) : SVal σs α := match σs with + | [] => f ⟨⟩ | _ :: _ => fun s => curry (fun s' => f (s, s')) -@[simp] theorem curry_nil {f : StateTuple [] → α} : curry f = f () := rfl -@[simp] theorem curry_cons {σ : Type} {σs : List Type} {f : StateTuple (σ::σs) → α} {s : σ} : curry f s = curry (fun s' => f (s, s')) := rfl +@[simp] theorem curry_nil {f : StateTuple [] → α} : curry f = f ⟨⟩ := rfl +@[simp] theorem curry_cons {σ : Type u} {σs : List (Type u)} {f : StateTuple (σ::σs) → α} {s : σ} : curry f s = curry (fun s' => f (s, s')) := rfl /-- Uncurry an `SVal` into a function taking a `StateTuple`. -/ -def uncurry {σs : List Type} (f : SVal σs α) : StateTuple σs → α := match σs with +def uncurry {σs : List (Type u)} (f : SVal σs α) : StateTuple σs → α := match σs with | [] => fun _ => f | _ :: _ => fun (s, t) => uncurry (f s) t -@[simp] theorem uncurry_nil {σ : Type} {s : σ} : uncurry (σs:=[]) s = fun _ => s := rfl -@[simp] theorem uncurry_cons {σ : Type} {σs : List Type} {f : SVal (σ::σs) α} {s : σ} {t : StateTuple σs} : uncurry f (s, t) = uncurry (f s) t := rfl +@[simp] theorem uncurry_nil {σ : Type u} {s : σ} : uncurry (σs:=[]) s = fun _ => s := rfl +@[simp] theorem uncurry_cons {σ : Type u} {σs : List (Type u)} {f : SVal (σ::σs) α} {s : σ} {t : StateTuple σs} : uncurry f (s, t) = uncurry (f s) t := rfl -@[simp] theorem uncurry_curry {σs : List Type} {f : StateTuple σs → α} : uncurry (σs:=σs) (curry f) = f := by induction σs <;> (simp[uncurry, curry, *]; rfl) -@[simp] theorem curry_uncurry {σs : List Type} {f : SVal σs α} : curry (σs:=σs) (uncurry f) = f := by induction σs <;> simp[uncurry, curry, *] +@[simp] theorem uncurry_curry {σs : List (Type u)} {f : StateTuple σs → α} : uncurry (σs:=σs) (curry f) = f := by induction σs <;> (simp[uncurry, curry, *]; rfl) +@[simp] 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} (a : α) : SVal σs α := curry (fun _ => a) +abbrev pure {σs : List (Type u)} (a : α) : SVal σs α := curry (fun _ => a) instance [Inhabited α] : Inhabited (SVal σs α) where default := pure default -class GetTy (σ : Type) (σs : List Type) where +class GetTy (σ : Type u) (σs : List (Type u)) where get : SVal σs σ instance : GetTy σ (σ :: σs) where @@ -70,6 +70,6 @@ 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} (σ : Type) [GetTy σ σs] : SVal σs σ := GetTy.get -@[simp] theorem getThe_here {σs : List Type} (σ : Type) (s : σ) : getThe (σs := σ::σs) σ s = pure s := rfl -@[simp] theorem getThe_there {σs : List Type} [GetTy σ σs] (σ' : Type) (s : σ') : getThe (σs := σ'::σs) σ s = getThe (σs := σs) σ := rfl +def getThe {σs : List (Type u)} (σ : Type u) [GetTy σ σs] : SVal σs σ := GetTy.get +@[simp] theorem getThe_here {σs : List (Type u)} (σ : Type u) (s : σ) : getThe (σs := σ::σs) σ s = pure s := rfl +@[simp] 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/Do/Triple/Basic.lean b/src/Std/Do/Triple/Basic.lean index 0dcd8661d4..dbede852d5 100644 --- a/src/Std/Do/Triple/Basic.lean +++ b/src/Std/Do/Triple/Basic.lean @@ -19,8 +19,8 @@ It is thus defined in terms of an instance `WP m ps`. namespace Std.Do -universe u -variable {m : Type → Type u} {ps : PostShape} +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} /-- A Hoare triple for reasoning about monadic programs. @@ -29,7 +29,7 @@ variable {m : Type → Type u} {ps : PostShape} `⦃P⦄ x ⦃Q⦄` is convenient syntax for `Triple x P Q`. -/ -def Triple [WP m ps] {α} (x : m α) (P : Assertion ps) (Q : PostCond α ps) : Prop := +def Triple [WP m ps] {α : Type u} (x : m α) (P : Assertion ps) (Q : PostCond α ps) : Prop := P ⊢ₛ wp⟦x⟧ Q @[inherit_doc Std.Do.Triple] @@ -46,10 +46,10 @@ namespace Triple instance [WP m ps] (x : m α) : SPred.Tactic.PropAsSPredTautology (Triple x P Q) spred(P → wp⟦x⟧ Q) where iff := (SPred.entails_true_intro P (wp⟦x⟧ Q)).symm -theorem pure [Monad m] [WPMonad m ps] {α} {Q : PostCond α ps} (a : α) (himp : P ⊢ₛ Q.1 a) : +theorem pure [Monad m] [WPMonad m ps] {α : Type u} {Q : PostCond α ps} (a : α) (himp : P ⊢ₛ Q.1 a) : Triple (pure (f:=m) a) P Q := himp.trans (by simp) -theorem bind [Monad m] [WPMonad m ps] {α β} {P : Assertion ps} {Q : α → Assertion ps} {R : PostCond β ps} (x : m α) (f : α → m β) +theorem bind [Monad m] [WPMonad m ps] {α β : Type u} {P : Assertion ps} {Q : α → Assertion ps} {R : PostCond β ps} (x : m α) (f : α → m β) (hx : Triple x P (Q, R.2)) (hf : ∀ b, Triple (f b) (Q b) R) : Triple (x >>= f) P R := by diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index a30d802c94..805a212856 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/src/Std/Do/Triple/SpecLemmas.lean @@ -51,15 +51,15 @@ local notation:lead (priority := high) "⦃" P "⦄ " x:lead " ⦃" Q "⦄" => T /-! # `Monad` -/ -universe u -variable {m : Type → Type u} {ps : PostShape} +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} theorem Spec.pure' [Monad m] [WPMonad m ps] {P : Assertion ps} {Q : PostCond α ps} (h : P ⊢ₛ Q.1 a) : ⦃P⦄ Pure.pure (f:=m) a ⦃Q⦄ := Triple.pure a h @[spec] -theorem Spec.pure {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α} {a : α} {Q : PostCond α ps} : +theorem Spec.pure [Monad m] [WPMonad m ps] {α} {a : α} {Q : PostCond α ps} : ⦃Q.1 a⦄ Pure.pure (f:=m) a ⦃Q⦄ := Spec.pure' .rfl theorem Spec.bind' [Monad m] [WPMonad m ps] {x : m α} {f : α → m β} {P : Assertion ps} {Q : PostCond β ps} @@ -67,15 +67,15 @@ theorem Spec.bind' [Monad m] [WPMonad m ps] {x : m α} {f : α → m β} {P : As ⦃P⦄ (x >>= f) ⦃Q⦄ := Triple.bind x f h (fun _ => .rfl) @[spec] -theorem Spec.bind {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → m β} {Q : PostCond β ps} : +theorem Spec.bind [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → m β} {Q : PostCond β ps} : ⦃wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2)⦄ (x >>= f) ⦃Q⦄ := Spec.bind' .rfl @[spec] -theorem Spec.map {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → β} {Q : PostCond β ps} : +theorem Spec.map [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → β} {Q : PostCond β ps} : ⦃wp⟦x⟧ (fun a => Q.1 (f a), Q.2)⦄ (f <$> x) ⦃Q⦄ := by simp [Triple, SPred.entails.refl] @[spec] -theorem Spec.seq {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α β} {x : m (α → β)} {y : m α} {Q : PostCond β ps} : +theorem Spec.seq [Monad m] [WPMonad m ps] {α β} {x : m (α → β)} {y : m α} {Q : PostCond β ps} : ⦃wp⟦x⟧ (fun f => wp⟦y⟧ (fun a => Q.1 (f a), Q.2), Q.2)⦄ (x <*> y) ⦃Q⦄ := by simp [Triple, SPred.entails.refl] /-! # `MonadLift` -/ @@ -156,7 +156,7 @@ theorem Spec.get_StateT [Monad m] [WPMonad m psm] : @[spec] theorem Spec.set_StateT [Monad m] [WPMonad m psm] : - ⦃fun _ => Q.1 () s⦄ (MonadStateOf.set s : StateT σ m PUnit) ⦃Q⦄ := by simp [Triple] + ⦃fun _ => Q.1 ⟨⟩ s⦄ (MonadStateOf.set s : StateT σ m PUnit) ⦃Q⦄ := by simp [Triple] @[spec] theorem Spec.modifyGet_StateT [Monad m] [WPMonad m ps] : @@ -288,7 +288,7 @@ theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : /-! # `ForIn` -/ @[spec] -theorem Spec.forIn'_list {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape} +theorem Spec.forIn'_list {α β : Type u} [Monad m] [WPMonad m ps] {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs) ps) @@ -322,7 +322,7 @@ theorem Spec.forIn'_list {α : Type} {β : Type} {m : Type → Type v} {ps : Pos exact this -- using the postcondition as a constant invariant: -theorem Spec.forIn'_list_const_inv {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape} +theorem Spec.forIn'_list_const_inv {α β : Type u} [Monad m] [WPMonad m ps] {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} {inv : PostCond β ps} @@ -333,8 +333,9 @@ theorem Spec.forIn'_list_const_inv {α : Type} {β : Type} {m : Type → Type v} ⦃inv.1 init⦄ forIn' xs init f ⦃inv⦄ := Spec.forIn'_list (fun p => inv.1 p.1, inv.2) (fun b _ x hx _ _ => step x hx b) +set_option pp.universes true in @[spec] -theorem Spec.forIn_list {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape} +theorem Spec.forIn_list {α β : Type u} [Monad m] [WPMonad m ps] {xs : List α} {init : β} {f : α → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs) ps) @@ -349,7 +350,7 @@ theorem Spec.forIn_list {α : Type} {β : Type} {m : Type → Type v} {ps : Post exact Spec.forIn'_list inv (fun b rpref x _ suff h => step b rpref x suff h) -- using the postcondition as a constant invariant: -theorem Spec.forIn_list_const_inv {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape} +theorem Spec.forIn_list_const_inv {α β : Type u} [Monad m] [WPMonad m ps] {xs : List α} {init : β} {f : α → β → m (ForInStep β)} {inv : PostCond β ps} @@ -361,7 +362,7 @@ theorem Spec.forIn_list_const_inv {α : Type} {β : Type} {m : Type → Type v} Spec.forIn_list (fun p => inv.1 p.1, inv.2) (fun b _ hd _ _ => step hd b) @[spec] -theorem Spec.foldlM_list {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape} +theorem Spec.foldlM_list {α β : Type u} [Monad m] [WPMonad m ps] {xs : List α} {init : β} {f : β → α → m β} (inv : PostCond (β × List.Zipper xs) ps) @@ -378,7 +379,7 @@ theorem Spec.foldlM_list {α : Type} {β : Type} {m : Type → Type v} {ps : Pos exact step -- using the postcondition as a constant invariant: -theorem Spec.foldlM_list_const_inv {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape} +theorem Spec.foldlM_list_const_inv {α β : Type u} [Monad m] [WPMonad m ps] {xs : List α} {init : β} {f : β → α → m β} {inv : PostCond β ps} @@ -420,7 +421,7 @@ theorem Spec.forIn_range {β : Type} {m : Type → Type v} {ps : PostShape} apply Spec.forIn_list inv step @[spec] -theorem Spec.forIn'_array {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape} +theorem Spec.forIn'_array {α β : Type u} [Monad m] [WPMonad m ps] {xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs.toList) ps) @@ -436,7 +437,7 @@ theorem Spec.forIn'_array {α : Type} {β : Type} {m : Type → Type v} {ps : Po apply Spec.forIn'_list inv (fun b rpref x hx suff h => step b rpref x (by simp[hx]) suff h) @[spec] -theorem Spec.forIn_array {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape} +theorem Spec.forIn_array {α β : Type u} [Monad m] [WPMonad m ps] {xs : Array α} {init : β} {f : α → β → m (ForInStep β)} (inv : PostCond (β × List.Zipper xs.toList) ps) @@ -452,7 +453,7 @@ theorem Spec.forIn_array {α : Type} {β : Type} {m : Type → Type v} {ps : Pos apply Spec.forIn_list inv step @[spec] -theorem Spec.foldlM_array {α : Type} {β : Type} {m : Type → Type v} {ps : PostShape} +theorem Spec.foldlM_array {α β : Type u} [Monad m] [WPMonad m ps] {xs : Array α} {init : β} {f : β → α → m β} (inv : PostCond (β × List.Zipper xs.toList) ps) diff --git a/src/Std/Do/WP/Basic.lean b/src/Std/Do/WP/Basic.lean index 4e6142390b..545c241105 100644 --- a/src/Std/Do/WP/Basic.lean +++ b/src/Std/Do/WP/Basic.lean @@ -36,15 +36,15 @@ by the subclass `WPMonad`. namespace Std.Do -universe u -variable {m : Type → Type u} +universe u v +variable {m : Type u → Type v} /-- A weakest precondition interpretation of a monadic program `x : m α` in terms of a predicate transformer `PredTrans ps α`. The monad `m` determines `ps : PostShape`. See the module comment for more details. -/ -class WP (m : Type → Type u) (ps : outParam PostShape) where +class WP (m : Type u → Type v) (ps : outParam PostShape.{u}) where wp {α} (x : m α) : PredTrans ps α export WP (wp) @@ -93,19 +93,16 @@ instance Reader.instWP : WP (ReaderM ρ) (.arg ρ .pure) := instance Except.instWP : WP (Except ε) (.except ε .pure) := inferInstanceAs (WP (ExceptT ε Id) (.except ε .pure)) -theorem Id.by_wp {α} {x : α} {prog : Id α} (h : Id.run prog = x) (P : α → Prop) : - wp⟦prog⟧ (PostCond.total P) → P x := h ▸ id +theorem Id.by_wp {α : Type u} {x : α} {prog : Id α} (h : Id.run prog = x) (P : α → Prop) : + (⊢ₛ wp⟦prog⟧ (PostCond.total (fun a => ⟨P a⟩))) → P x := h ▸ (· True.intro) theorem StateM.by_wp {α} {x : α × σ} {prog : StateM σ α} (h : StateT.run prog s = x) (P : α × σ → Prop) : - wp⟦prog⟧ (PostCond.total (fun a s' => P (a, s'))) s → P x := by - intro hspec - simp only [wp, PredTrans.pure, PredTrans.pushArg_apply] at hspec - exact h ▸ hspec + (⊢ₛ wp⟦prog⟧ (PostCond.total (fun a s' => ⟨P (a, s')⟩)) s) → P x := h ▸ (· True.intro) theorem EStateM.by_wp {α} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α} (h : EStateM.run prog s = x) (P : EStateM.Result ε σ α → Prop) : - wp⟦prog⟧ (PostCond.total (fun a s' => P (EStateM.Result.ok a s'))) s → P x := by + (⊢ₛ wp⟦prog⟧ (PostCond.total (fun a s' => ⟨P (EStateM.Result.ok a s')⟩)) s) → P x := by intro hspec - simp only [wp, FailConds.false, FailConds.const, SVal.curry_cons, SVal.curry_nil] at hspec + simp only [wp, FailConds.false, FailConds.const, SVal.curry_cons] at hspec split at hspec - case h_1 a s' heq => rw[← heq] at hspec; exact h ▸ hspec - case h_2 => contradiction + case h_1 a s' heq => rw[← heq] at hspec; exact h ▸ hspec True.intro + case h_2 => exfalso; exact hspec True.intro diff --git a/src/Std/Do/WP/Monad.lean b/src/Std/Do/WP/Monad.lean index e74670a6ed..165f6b3d91 100644 --- a/src/Std/Do/WP/Monad.lean +++ b/src/Std/Do/WP/Monad.lean @@ -15,13 +15,13 @@ it preserves `pure` and `bind`. namespace Std.Do -universe u -variable {m : Type → Type u} {ps : PostShape} +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} /-- A `WP` that is also a monad morphism, preserving `pure` and `bind`. (They all are.) -/ -class WPMonad (m : Type → Type u) (ps : outParam PostShape) [Monad m] +class WPMonad (m : Type u → Type v) (ps : outParam PostShape.{u}) [Monad m] extends LawfulMonad m, WP m ps where wp_pure : ∀ {α} (a : α), wp (pure a) = pure a wp_bind : ∀ {α β} (x : m α) (f : α → m β), wp (do let a ← x; f a) = do let a ← wp x; wp (f a) diff --git a/src/Std/Do/WP/SimpLemmas.lean b/src/Std/Do/WP/SimpLemmas.lean index 346e31fb98..71609be562 100644 --- a/src/Std/Do/WP/SimpLemmas.lean +++ b/src/Std/Do/WP/SimpLemmas.lean @@ -20,8 +20,8 @@ namespace Std.Do.WP open WPMonad -universe u -variable {m : Type → Type u} {ps : PostShape} +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} /-! ## `WP` -/ @@ -149,11 +149,11 @@ theorem modifyGetThe_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → α @[simp] theorem modify_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → σ) : - wp⟦modify f : m PUnit⟧ Q = wp⟦MonadStateOf.modifyGet fun s => ((), f s) : m PUnit⟧ Q := rfl + wp⟦modify f : m PUnit⟧ Q = wp⟦MonadStateOf.modifyGet fun s => (⟨⟩, f s) : m PUnit⟧ Q := rfl @[simp] theorem modifyThe_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → σ) : - wp⟦modifyThe σ f : m PUnit⟧ Q = wp⟦MonadStateOf.modifyGet fun s => ((), f s) : m PUnit⟧ Q := rfl + wp⟦modifyThe σ f : m PUnit⟧ Q = wp⟦MonadStateOf.modifyGet fun s => (⟨⟩, f s) : m PUnit⟧ Q := rfl -- instances @@ -210,19 +210,19 @@ open MonadFunctor renaming monadMap → mmap -- that enjoys quite a tricky definition. -- However, we found that relying on specialised lemmas is both much simpler and more reliable. @[simp] -theorem monadMap_StateT (m : Type → Type u) [Monad m] [WP m ps] +theorem monadMap_StateT [Monad m] [WP m ps] (f : ∀{β}, m β → m β) {α} (x : StateT σ m α) (Q : PostCond α (.arg σ ps)) : wp⟦mmap (m:=m) f x⟧ Q = fun s => wp⟦f (x.run s)⟧ (fun (a, s) => Q.1 a s, Q.2) := by simp [wp, MonadFunctor.monadMap, StateT.run] @[simp] -theorem monadMap_ReaderT (m : Type → Type u) [Monad m] [WP m ps] +theorem monadMap_ReaderT [Monad m] [WP m ps] (f : ∀{β}, m β → m β) {α} (x : ReaderT ρ m α) (Q : PostCond α (.arg ρ ps)) : wp⟦mmap (m:=m) f x⟧ Q = fun s => wp⟦f (x.run s)⟧ (fun a => Q.1 a s, Q.2) := by simp [wp, MonadFunctor.monadMap, ReaderT.run] @[simp] -theorem monadMap_ExceptT (m : Type → Type u) [Monad m] [WP m ps] +theorem monadMap_ExceptT [Monad m] [WP m ps] (f : ∀{β}, m β → m β) {α} (x : ExceptT ε m α) (Q : PostCond α (.except ε ps)) : wp⟦mmap (m:=m) f x⟧ Q = wp⟦f x.run⟧ (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := by simp [wp, MonadFunctor.monadMap, ExceptT.run] diff --git a/src/Std/Tactic/Do/ProofMode.lean b/src/Std/Tactic/Do/ProofMode.lean index 137cae127c..b32db6a430 100644 --- a/src/Std/Tactic/Do/ProofMode.lean +++ b/src/Std/Tactic/Do/ProofMode.lean @@ -21,6 +21,6 @@ abbrev MGoalEntails := @SPred.entails /-- This is only used for delaboration purposes, so that we can render context variables that appear to have type `A : PROP` even though `PROP` is not a type. -/ -def MGoalHypMarker {σs : List Type} (_A : SPred σs) : Prop := True +def MGoalHypMarker {σs : List (Type u)} (_A : SPred σs) : Prop := True end Std.Tactic.Do diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean index 6dc9f426fe..e6b22a04df 100644 --- a/src/Std/Tactic/Do/Syntax.lean +++ b/src/Std/Tactic/Do/Syntax.lean @@ -214,6 +214,7 @@ macro (name := mspec) "mspec" spec:(ppSpace colGt term)? : tactic => $(mkIdent ``Std.Do.SPred.true_intro_simp):term, $(mkIdent ``Std.Do.SPred.true_intro_simp_nil):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]) diff --git a/tests/lean/run/bhaviksSampler.lean b/tests/lean/run/bhaviksSampler.lean index d156a2b8d6..d363c4f60f 100644 --- a/tests/lean/run/bhaviksSampler.lean +++ b/tests/lean/run/bhaviksSampler.lean @@ -155,7 +155,7 @@ theorem sampler_correct {m : Type → Type u} {k h} [Monad m] [WPMonad m ps] : case inv => exact (⇓ (midway, xs) => ⌜Midway.valid midway xs.rpref.length⌝) -- case step => simp_all case post.success => - simp_all + dsimp mpure h mpure_intro have h := h.nodup_take diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean index c9b5520b66..f0cea14a3b 100644 --- a/tests/lean/run/doLogicTests.lean +++ b/tests/lean/run/doLogicTests.lean @@ -6,6 +6,7 @@ Authors: Sebastian Graf import Std.Tactic.Do import Std.Tactic.Do.Syntax +import Std open Std.Do @@ -85,13 +86,13 @@ open Code open Lean.Parser.Tactic theorem sum_loop_spec : - ⦃True⦄ + ⦃⌜True⌝⦄ sum_loop - ⦃⇓r => r < 30⦄ := by + ⦃⇓r => ⌜r < 30⌝⦄ := by mintro - unfold sum_loop mspec - case inv => exact (⇓ (r, xs) => (∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25) + case inv => exact (⇓ (r, xs) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝) all_goals simp_all +decide; try omega intros mintro _ @@ -151,25 +152,22 @@ theorem mkFreshPair_spec_no_eta : intro _; simp_all example : PostCond (Nat × Std.List.Zipper (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) := - ⟨fun (r, xs) s => r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4, fun e s => e = 42 ∧ s = 4, ()⟩ + ⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝, ()⟩ example : PostCond (Nat × Std.List.Zipper (List.range' 1 3 1)) (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) := - post⟨fun (r, xs) s => r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4, fun e s => e = 42 ∧ s = 4⟩ - -example : (Nat × Std.List.Zipper (List.range' 1 3 1)) → Assertion (PostShape.except Nat (PostShape.arg Nat PostShape.pure)) := - let x := ⟨fun (r, xs) s => r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4, fun e s => e = 42 ∧ s = 4⟩; Prod.fst x + post⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩ theorem throwing_loop_spec : - ⦃fun s => s = 4⦄ + ⦃fun s => ⌜s = 4⌝⦄ throwing_loop - ⦃post⟨fun _ _ => False, - fun e s => e = 42 ∧ s = 4⟩⦄ := by + ⦃post⟨fun _ _ => ⌜False⌝, + fun e s => ⌜e = 42 ∧ s = 4⌝⟩⦄ := by mintro hs dsimp only [throwing_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift] mspec mspec mspec - case inv => exact post⟨fun (r, xs) s => r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4, fun e s => e = 42 ∧ s = 4⟩ + case inv => exact post⟨fun (r, xs) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝, fun e s => ⌜e = 42 ∧ s = 4⌝⟩ case post.success => mspec mspec @@ -194,13 +192,14 @@ theorem beaking_loop_spec : dsimp only [breaking_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift] mspec mspec - case inv => exact (⇓ (r, xs) s => (r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42) + case inv => exact (⇓ (r, xs) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝) all_goals simp_all case post => intro _ h conv at h in (List.sum _) => whnf simp at h - omega + simp + grind case step => intros mintro _ @@ -209,14 +208,14 @@ theorem beaking_loop_spec : case isFalse => intro _; mintro _; mspec; simp_all; omega theorem returning_loop_spec : - ⦃fun s => s = 4⦄ + ⦃fun s => ⌜s = 4⌝⦄ returning_loop - ⦃⇓ r s => r = 42 ∧ s = 4⦄ := by + ⦃⇓ r s => ⌜r = 42 ∧ s = 4⌝⦄ := by mintro hs dsimp only [returning_loop, get, getThe, instMonadStateOfOfMonadLift, liftM, monadLift] mspec mspec - case inv => exact (⇓ (r, xs) s => (r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4) + case inv => exact (⇓ (r, xs) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝) all_goals simp_all case post => split @@ -265,25 +264,24 @@ abbrev fib_spec : Nat → Nat -- simp only [h, reduceIte] -- mspec -- mspec_no_bind Spec.bind --- set_option trace.mpl.tactics.spec true in --- mspec_no_bind Spec.forIn_list (⇓ (⟨a, b⟩, xs) => a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)) ?step +-- set_option trace.Elab.Tactic.Do.spec true in +-- mspec_no_bind Spec.forIn_list ?inv ?step -- -- case step => dsimp; intros; mintro _; simp_all -- simp_all [Nat.sub_one_add_one] -theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => r = fib_spec n⦄ := by +theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by unfold fib_impl dsimp mintro _ if h : n = 0 then simp [h] else simp only [h, reduceIte] mspec -- Spec.pure - mspec Spec.forIn_range (⇓ (⟨a, b⟩, xs) => a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)) ?step + mspec Spec.forIn_range (⇓ (⟨a, b⟩, xs) => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step case step => dsimp; intros; mintro _; simp_all simp_all [Nat.sub_one_add_one] -#check fib_impl.fun_cases -theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => r = fib_spec n⦄ := by +theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by apply fib_impl.fun_cases n _ ?case1 ?case2 case case1 => rintro rfl; mintro -; simp only [fib_impl, ↓reduceIte]; mspec case case2 => @@ -291,7 +289,7 @@ theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => r = fib_spec mintro - simp only [fib_impl, h, reduceIte] mspec - mspec Spec.forIn_range (⇓ (⟨a, b⟩, xs) => a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)) ?step + mspec Spec.forIn_range (⇓ (⟨a, b⟩, xs) => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) ?step case step => dsimp; intros; mintro _; mspec; mspec; simp_all simp_all [Nat.sub_one_add_one] @@ -299,12 +297,12 @@ theorem fib_impl_vcs (Q : Nat → PostCond Nat PostShape.pure) (I : (n : Nat) → (_ : ¬n = 0) → PostCond (MProd Nat Nat × Std.List.Zipper [1:n].toList) PostShape.pure) - (ret : (Q 0).1 0) - (loop_pre : ∀ n (hn : ¬n = 0), (I n hn).1 (⟨0, 1⟩, Std.List.Zipper.begin _)) + (ret : ⊢ₛ (Q 0).1 0) + (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 (⟨0, 1⟩, Std.List.Zipper.begin _)) (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 (r, Std.List.Zipper.end _) ⊢ₛ (Q n).1 r.snd) (loop_step : ∀ n (hn : ¬n = 0) r rpref x suff (h : [1:n].toList = rpref.reverse ++ x :: suff), (I n hn).1 (r, ⟨rpref, x::suff, by simp[h]⟩) ⊢ₛ (I n hn).1 (⟨r.2, r.1+r.2⟩, ⟨x::rpref, suff, by simp[h]⟩)) - : wp⟦fib_impl n⟧ (Q n) := by + : ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by apply fib_impl.fun_cases n _ ?case1 ?case2 case case1 => intro h; simp only [fib_impl, h, ↓reduceIte]; mstart; mspec case case2 => @@ -313,7 +311,7 @@ theorem fib_impl_vcs mstart mspec mspec - case pre1 => mpure_intro; exact loop_pre n hn + case pre1 => exact loop_pre n hn case post.success => mspec; mpure_intro; apply_rules [loop_post] case step => intro _ _ _ _ h; @@ -323,19 +321,18 @@ theorem fib_impl_vcs mpure_intro apply_rules [loop_step] -theorem fib_triple_vcs : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => r = fib_spec n⦄ := by - intro _ +theorem fib_triple_vcs : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by apply fib_impl_vcs - case I => intro n hn; exact (⇓ (⟨a, b⟩, xs) => a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)) - case ret => rfl - case loop_pre => intros; trivial - case loop_post => simp_all[Nat.sub_one_add_one] + case I => intro n hn; exact (⇓ (⟨a, b⟩, xs) => ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝) + case ret => mpure_intro; rfl + case loop_pre => intros; mpure_intro; trivial + case loop_post => simp_all [Nat.sub_one_add_one] case loop_step => simp_all theorem fib_correct {n} : (fib_impl n).run = fib_spec n := by generalize h : (fib_impl n).run = x apply Id.by_wp h - apply fib_triple True.intro + apply fib_triple end fib @@ -355,11 +352,11 @@ def program (n : Nat) (k : Nat) : IO Nat := do open scoped Std.Do.IO.Bare -axiom IO.rand_spec {n : Nat} : ⦃True⦄ (IO.rand 0 n : IO Nat) ⦃⇓r => r < n⦄ +axiom IO.rand_spec {n : Nat} : ⦃⌜True⌝⦄ (IO.rand 0 n : IO Nat) ⦃⇓r => ⌜r < n⌝⦄ /-- The result has the same parity as the input. -/ @[spec] -theorem addRandomEvens_spec (n k) : ⦃True⦄ (addRandomEvens n k) ⦃⇓r => r % 2 = k % 2⦄ := by +theorem addRandomEvens_spec (n k) : ⦃⌜True⌝⦄ (addRandomEvens n k) ⦃⇓r => ⌜r % 2 = k % 2⌝⦄ := by unfold addRandomEvens mintro - mspec Spec.forIn_list_const_inv @@ -370,7 +367,7 @@ theorem addRandomEvens_spec (n k) : ⦃True⦄ (addRandomEvens n k) ⦃⇓r => r /-- Since we're adding even numbers to our number twice, and summing, the entire result is even. -/ -theorem program_spec (n k) : ⦃True⦄ program n k ⦃⇓r => r % 2 = 0⦄ := by +theorem program_spec (n k) : ⦃⌜True⌝⦄ program n k ⦃⇓r => ⌜r % 2 = 0⌝⦄ := by unfold program mintro - mspec (addRandomEvens_spec n k) @@ -397,7 +394,7 @@ noncomputable def prog (n : Nat) : M Nat := do let c ← op b return (a + b + c) -axiom isValid : Nat → Char → Bool → String → Prop +axiom isValid : Nat → Char → Bool → String → ULift Prop axiom op.spec {n} : ⦃isValid⦄ op n ⦃⇓r => ⌜r > 42⌝ ∧ isValid⦄ @@ -435,26 +432,26 @@ namespace Automated open Code -theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => r = fib_spec n⦄ := by +theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by unfold fib_impl mvcgen case inv => exact ⇓ (⟨a, b⟩, xs) => - a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1) + ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝ all_goals simp_all +zetaDelta [Nat.sub_one_add_one] -theorem fib_triple_step : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => r = fib_spec n⦄ := by +theorem fib_triple_step : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by unfold fib_impl mvcgen_step 14 -- 13 still has a wp⟦·⟧ case inv => exact ⇓ (⟨a, b⟩, xs) => - a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1) + ⌜a = fib_spec xs.rpref.length ∧ b = fib_spec (xs.rpref.length + 1)⌝ all_goals simp_all +zetaDelta [Nat.sub_one_add_one] attribute [local spec] fib_triple in -theorem fib_triple_attr : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => r = fib_spec n⦄ := by +theorem fib_triple_attr : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by mvcgen attribute [local spec] fib_triple in -theorem fib_triple_erase : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => r = fib_spec n⦄ := by +theorem fib_triple_erase : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by mvcgen [-fib_triple] -- should not make any progress fail_if_success done admit @@ -463,16 +460,16 @@ theorem fib_impl_vcs (Q : Nat → PostCond Nat PostShape.pure) (I : (n : Nat) → (_ : ¬n = 0) → PostCond (MProd Nat Nat × Std.List.Zipper [1:n].toList) PostShape.pure) - (ret : (Q 0).1 0) - (loop_pre : ∀ n (hn : ¬n = 0), (I n hn).1 (⟨0, 1⟩, Std.List.Zipper.begin _)) + (ret : ⊢ₛ (Q 0).1 0) + (loop_pre : ∀ n (hn : ¬n = 0), ⊢ₛ (I n hn).1 (⟨0, 1⟩, Std.List.Zipper.begin _)) (loop_post : ∀ n (hn : ¬n = 0) r, (I n hn).1 (r, Std.List.Zipper.end _) ⊢ₛ (Q n).1 r.snd) (loop_step : ∀ n (hn : ¬n = 0) r rpref x suff (h : [1:n].toList = rpref.reverse ++ x :: suff), (I n hn).1 (r, ⟨rpref, x::suff, by simp[h]⟩) ⊢ₛ (I n hn).1 (⟨r.2, r.1+r.2⟩, ⟨x::rpref, suff, by simp[h]⟩)) - : wp⟦fib_impl n⟧ (Q n) := by + : ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by unfold fib_impl mvcgen case inv h => exact I n h - case isTrue h => subst h; mpure_intro; exact ret + case isTrue h => subst h; exact ret case isFalse h => mpure_intro; apply_rules [loop_pre] case step => mpure_intro; apply_rules [loop_step] case post.success => mpure_intro; apply_rules [loop_post] @@ -514,58 +511,58 @@ theorem mkFreshPair_triple : ⦃⌜True⌝⦄ mkFreshPair ⦃⇓ (a, b) => ⌜a simp_all [SPred.entails_elim_cons] theorem sum_loop_spec : - ⦃True⦄ + ⦃⌜True⌝⦄ sum_loop - ⦃⇓r => r < 30⦄ := by + ⦃⇓r => ⌜r < 30⌝⦄ := by -- cf. `ByHand.sum_loop_spec` mintro - mvcgen [sum_loop] - case inv => exact (⇓ (r, xs) => (∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25) - all_goals simp_all +decide; try omega + case inv => exact (⇓ (r, xs) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝) + all_goals simp_all +decide; try grind theorem throwing_loop_spec : - ⦃fun s => s = 4⦄ + ⦃fun s => ⌜s = 4⌝⦄ throwing_loop - ⦃post⟨fun _ _ => False, - fun e s => e = 42 ∧ s = 4⟩⦄ := by + ⦃post⟨fun _ _ => ⌜False⌝, + fun e s => ⌜e = 42 ∧ s = 4⌝⟩⦄ := by mvcgen [throwing_loop] - case inv => exact post⟨fun (r, xs) s => r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4, - fun e s => e = 42 ∧ s = 4⟩ - all_goals (try simp_all; done) + case inv => exact post⟨fun (r, xs) 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, SPred.entails_nil]; decide - case post.success => grind + case post.success => simp_all only [SVal.curry_nil, SPred.entails_nil]; grind + case post.except => simp_all case isTrue => intro _; simp_all - case isFalse => intro _; simp_all only [SPred.entails_nil]; grind + case isFalse => intro _; simp_all only [SVal.curry_nil, SPred.entails_nil]; grind theorem test_loop_break : ⦃⌜‹Nat›ₛ = 42⌝⦄ breaking_loop ⦃⇓ r => ⌜r > 4 ∧ ‹Nat›ₛ = 1⌝⦄ := by mvcgen [breaking_loop] - case inv => exact (⇓ (r, xs) s => (r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42) + case inv => exact (⇓ (r, xs) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝) + case pre1 => simp_all case isTrue => intro _; simp_all - case isFalse => intro _; simp_all; omega + case isFalse => intro _; simp_all only [SVal.curry_nil, SPred.entails_nil]; grind case post.success => simp_all conv at h in (List.sum _) => whnf simp at h - omega - simp_all + grind theorem test_loop_early_return : - ⦃fun s => s = 4⦄ + ⦃fun s => ⌜s = 4⌝⦄ returning_loop - ⦃⇓ r s => r = 42 ∧ s = 4⦄ := by + ⦃⇓ r s => ⌜r = 42 ∧ s = 4⌝⦄ := by mvcgen [returning_loop] - case inv => exact (⇓ (r, xs) s => (r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4) + case inv => exact (⇓ (r, xs) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝) case isTrue => intro _; simp_all - case isFalse => intro _; simp_all; omega + case isFalse => intro _; simp_all only [SVal.curry_nil, SPred.entails_nil]; grind case pre1 => simp_all case h_1 => simp_all conv at h in (List.sum _) => whnf simp at h - omega + grind case h_2 => simp_all theorem unfold_to_expose_match_spec : @@ -586,15 +583,15 @@ theorem test_match_splitting {m : Option Nat} (h : m = some 4) : simp_all theorem test_sum : - ⦃True⦄ + ⦃⌜True⌝⦄ do let mut x := 0 for i in [1:5] do x := x + i pure (f := Id) x - ⦃⇓r => r < 30⦄ := by + ⦃⇓r => ⌜r < 30⌝⦄ := by mvcgen - case inv => exact (⇓ (r, xs) => (∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25) + case inv => exact (⇓ (r, xs) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝) case step => simp_all omega @@ -641,7 +638,7 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) : · intro h apply Id.by_wp (P := (· = true)) rfl mvcgen - case inv => exact (⇓ (r, xs) => r.1 = none ∧ ∀ x, x ∈ xs.suff → p x) + case inv => exact (⇓ (r, xs) => ⌜r.1 = none ∧ ∀ x, x ∈ xs.suff → p x⌝) case pre1 => simp; intro a ha; apply h a ha.upper all_goals simp_all · intro ht i hin @@ -653,8 +650,8 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) : mvcgen case inv => exact (⇓ (r, xs) => match r.1 with - | none => i ∈ xs.suff - | some b => b = false ∧ xs.suff = []) + | none => ⌜i ∈ xs.suff⌝ + | some b => ⌜b = false ∧ xs.suff = []⌝) all_goals simp_all; try grind simp [ht] at hf @@ -796,9 +793,9 @@ def max_and_sum (xs : Array Nat) : Id (Nat × Nat) := do return (max, sum) theorem max_and_sum_spec (xs : Array Nat) : - ⦃⌜∀ i, (h : i < xs.size) → xs[i] ≥ 0⌝⦄ max_and_sum xs ⦃⇓ (m, s) => s ≤ m * xs.size ⦄ := by + ⦃⌜∀ i, (h : i < xs.size) → xs[i] ≥ 0⌝⦄ max_and_sum xs ⦃⇓ (m, s) => ⌜s ≤ m * xs.size⌝⦄ := by mvcgen [max_and_sum] - case inv => exact (⇓ (⟨m, s⟩, xs) => s ≤ m * xs.rpref.length) + case inv => exact (⇓ (⟨m, s⟩, xs) => ⌜s ≤ m * xs.rpref.length⌝) all_goals simp_all · rw [Nat.left_distrib] simp @@ -824,7 +821,7 @@ theorem Spec.get_StateT' [Monad m] [WPMonad m psm] : pure () theorem need_const_approx : - ⦃fun x => x = ()⦄ + ⦃fun x => ⌜x = ()⌝⦄ test ⦃⇓ _ => ⌜True⌝⦄ := by unfold test @@ -833,7 +830,7 @@ theorem need_const_approx : split <;> mspec theorem need_const_approx' : - ⦃fun x => x = ()⦄ + ⦃fun x => ⌜x = ()⌝⦄ test ⦃⇓ _ => ⌜True⌝⦄ := by mvcgen [test] @@ -889,3 +886,31 @@ theorem ex': ⦃⌜True⌝⦄ test_ite ⦃Q⦄ := by split <;> mspec end RishsTailContextBug + +namespace KimsUnivPolyUseCase + +open Std + +variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] + +def mergeWithAll (m₁ m₂ : ExtTreeMap α β cmp) (f : α → Option β → Option β → Option β) : ExtTreeMap α β cmp := + Id.run do + let mut r := ∅ + for (a, b₁) in m₁ do + if let some b := f a (some b₁) m₂[a]? then + r := r.insert a b + for (a, b₂) in m₂ do + if a ∉ m₁ then + if let some b := f a none (some b₂) then + r := r.insert a b + return r + +theorem mem_mergeWithAll [LawfulEqCmp cmp] {m₁ m₂ : ExtTreeMap α β cmp} {f : α → Option β → Option β → Option β} {a : α} : + a ∈ mergeWithAll m₁ m₂ f ↔ (a ∈ m₁ ∨ a ∈ m₂) ∧ (f a m₁[a]? m₂[a]?).isSome := by + generalize h : mergeWithAll m₁ m₂ f = x + apply Id.by_wp h + mvcgen + -- this was only to demonstrate that `Id.by_wp` and `mvcgen` applies here despite the universe polymorphism + admit + +end KimsUnivPolyUseCase diff --git a/tests/lean/run/spredNotation.lean b/tests/lean/run/spredNotation.lean index a62b595d4f..e05674e872 100644 --- a/tests/lean/run/spredNotation.lean +++ b/tests/lean/run/spredNotation.lean @@ -26,19 +26,19 @@ variable #check P ⊣⊢ₛ Q -/-- info: ⌜φ⌝ : SVal [Nat, Char, Bool] Prop -/ +/-- info: ⌜φ⌝ : SVal [Nat, Char, Bool] (ULift Prop) -/ #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] Prop +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] Prop -/ +/-- info: ⌜#theChar tuple = 'a'⌝ : SVal [Nat, Char, Bool] (ULift Prop) -/ #guard_msgs in #check ⌜#theChar = 'a'⌝ @@ -144,7 +144,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] Prop +else ⌜False⌝ : SVal [Nat, Char, Bool] (ULift Prop) -/ #guard_msgs in #check spred(if true then term(match (1,2) with | (x,y) => Φ x y) else ⌜False⌝) @@ -173,4 +173,4 @@ info: ∀ (a b n o : Nat) (s : Nat × Nat), ⌜a = n ∧ b = o⌝ ⊢ₛ ⌜s.fs -/ #guard_msgs in set_option linter.unusedVariables false in -#check ∀ (a b n o : Nat) (s : Nat × Nat), (SVal.curry fun f => a = n ∧ b = o) ⊢ₛ SVal.curry fun f => s.1 = n ∧ a = n + 1 ∧ b = o +#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)