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 <sg@lean-fro.org>
This commit is contained in:
Sebastian Graf
GitHub
parent
98e4b2882f
commit
0c5946ab3f
41 changed files with 603 additions and 531 deletions
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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`.
|
||||
|
|
|
|||
|
|
@ -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}"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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!]
|
||||
|
|
|
|||
|
|
@ -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}'"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 =>
|
||||
|
|
|
|||
|
|
@ -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 α) :
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 ()
|
||||
|
||||
|
|
|
|||
|
|
@ -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, *]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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])
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue