Hoare triples for OracleComp and extensions

def OracleComp.StateM.PreCondition (σ : Type u_1) : Type u_1

Equations

• OracleComp.StateM.PreCondition σ = (σ → Prop)

@[reducible, inline]

abbrev OracleComp.StateM.PreCondition.top (σ : Type u_1) : PreCondition σ

Equations

• OracleComp.StateM.PreCondition.top σ x✝ = True

@[simp]

theorem OracleComp.StateM.PreCondition.top_def {σ : Type u_1} : top σ = fun (x : σ) => True

instance OracleComp.StateM.instPartialOrderPreCondition {σ : Type u_1} : PartialOrder (PreCondition σ)

Pre-conditions are partially ordered by reverse inclusion

Equations

• OracleComp.StateM.instPartialOrderPreCondition = PartialOrder.mk ⋯

def OracleComp.StateM.PostCondition (σ : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

Equations

• OracleComp.StateM.PostCondition σ α = (σ → α → σ → Prop)

instance OracleComp.StateM.instPartialOrderPostCondition {σ : Type u_1} {α : Type u_2} : PartialOrder (PostCondition σ α)

Post-conditions are partially ordered by reverse inclusion

Equations

• OracleComp.StateM.instPartialOrderPostCondition = PartialOrder.mk ⋯

def OracleComp.StateM.HoareState {σ : Type u_1} (P : PreCondition σ) (α : Type u_4) (Q : PostCondition σ α) : Type (max u_1 u_4)

Equations

• OracleComp.StateM.HoareState P α Q = ((s : { s : σ // P s }) → { result : α × σ // Q (↑s) result.1 result.2 })

def OracleComp.StateM.HoareState.pure {σ : Type u_1} {α : Type u_2} (x : α) : HoareState (PreCondition.top σ) α fun (s : σ) (a : α) (s' : σ) => s = s' ∧ a = x

Equations

• OracleComp.StateM.HoareState.pure x ⟨s, h⟩ = ⟨(x, s), ⋯⟩

def OracleComp.StateM.HoareState.bind {σ : Type u_1} {α : Type u_2} {β : Type u_3} {P₁ : PreCondition σ} {Q₁ : PostCondition σ α} {P₂ : α → PreCondition σ} {Q₂ : α → PostCondition σ β} (m : HoareState P₁ α Q₁) (f : (x : α) → HoareState (P₂ x) β (Q₂ x)) : HoareState (fun (s₁ : σ) => P₁ s₁ ∧ ∀ (x : α) (s₂ : σ), Q₁ s₁ x s₂ → P₂ x s₂) β fun (s₁ : σ) (y : β) (s₃ : σ) => ∃ (x : α) (s₂ : σ), Q₁ s₁ x s₂ ∧ Q₂ x s₂ y s₃

Equations

• (m >>=ₕ f) ⟨s₁, h₁⟩ = match m ⟨s₁, ⋯⟩ with | ⟨(x, s₂), h₂⟩ => match f x ⟨s₂, ⋯⟩ with | ⟨(y, s₃), h₃⟩ => ⟨(y, s₃), ⋯⟩

def OracleComp.StateM.HoareState.«term_>>=ₕ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def OracleComp.StateM.HoareState.get {σ : Type u_1} : HoareState (PreCondition.top σ) σ fun (s x s' : σ) => s = s' ∧ x = s

Equations

• OracleComp.StateM.HoareState.get ⟨s, h⟩ = ⟨(s, s), ⋯⟩

def OracleComp.StateM.HoareState.set {σ : Type u_1} (s : σ) : HoareState (PreCondition.top σ) PUnit.{u_4 + 1} fun (x : σ) (x : PUnit.{u_4 + 1}) (s' : σ) => s = s'

Equations

• OracleComp.StateM.HoareState.set s ⟨s_1, h⟩ = ⟨(PUnit.unit, s), ⋯⟩

def OracleComp.StateM.HoareTriple {σ α : Type u_4} (P : PreCondition σ) (comp : StateM σ α) (Q : PostCondition σ α) : Prop

Equations

• OracleComp.StateM.HoareTriple P comp Q = ∀ (s : σ), P s → Q s (comp s).1 (comp s).2

def OracleComp.StateM.«term⦃_⦄_⦃_⦄» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OracleComp.StateM.HoareTriple.pure_rule {σ α : Type u_4} (x : α) : HoareTriple (PreCondition.top σ) (pure x) fun (s : σ) (a : α) (s' : σ) => s = s' ∧ a = x

theorem OracleComp.StateM.HoareTriple.pure_rule_forward {σ α : Type u_4} {P : PreCondition σ} (x : α) : HoareTriple P (pure x) fun (s : σ) (a : α) (s' : σ) => s = s' ∧ a = x ∧ P s

theorem OracleComp.StateM.HoareTriple.pure_rule_backward {σ α : Type u_4} {Q : PostCondition σ α} (x : α) : HoareTriple (fun (s : σ) => Q s x s) (pure x) Q

theorem OracleComp.StateM.HoareTriple.bind_rule {σ α β : Type u_4} {P₁ : PreCondition σ} {Q₁ : PostCondition σ α} {P₂ : α → PreCondition σ} {Q₂ : α → PostCondition σ β} {comp₁ : StateM σ α} {comp₂ : α → StateM σ β} (h₁ : HoareTriple P₁ comp₁ Q₁) (h₂ : ∀ (x : α), HoareTriple (P₂ x) (comp₂ x) (Q₂ x)) : HoareTriple (fun (s : σ) => P₁ s ∧ ∀ (x : α) (s' : σ), Q₁ s x s' → P₂ x s') (comp₁ >>= comp₂) fun (s : σ) (y : β) (s'' : σ) => ∃ (x : α) (s' : σ), Q₁ s x s' ∧ Q₂ x s' y s''

theorem OracleComp.StateM.HoareTriple.weaken_rule {σ α : Type u_4} {P : PreCondition σ} {Q : PostCondition σ α} {comp : StateM σ α} (h : HoareTriple P comp Q) (P' : PreCondition σ) (h_imp : ∀ (s : σ), P' s → P s) : HoareTriple P' comp Q

theorem OracleComp.StateM.HoareTriple.strengthen_rule {σ α : Type u_4} {P : PreCondition σ} {Q : PostCondition σ α} {comp : StateM σ α} (h : HoareTriple P comp Q) (Q' : PostCondition σ α) (h_imp : ∀ (s : σ) (x : α) (s' : σ), Q s x s' → Q' s x s') : HoareTriple P comp Q'

theorem OracleComp.StateM.HoareTriple.conseq_rule {σ α : Type u_4} {P : PreCondition σ} {Q : PostCondition σ α} {comp : StateM σ α} (h : HoareTriple P comp Q) (P' : PreCondition σ) (Q' : PostCondition σ α) (hP : ∀ (s : σ), P' s → P s) (hQ : ∀ (s : σ) (x : α) (s' : σ), Q s x s' → Q' s x s') : HoareTriple P' comp Q'

Consequence rule: combination of weaken and strengthen

In this form, it's meant to be applied forward, not backward

theorem OracleComp.StateM.HoareTriple.frame_rule {σ α : Type u_4} {P : PreCondition σ} {Q : PostCondition σ α} {comp : StateM σ α} (h : HoareTriple P comp Q) (R : PreCondition σ) : HoareTriple (fun (s : σ) => P s ∧ R s) comp fun (s : σ) (x : α) (s' : σ) => Q s x s' ∧ R s

@[simp]

theorem OracleComp.StateM.HoareTriple.frame_true_pre {σ α : Type u_4} {P : PreCondition σ} {Q : PostCondition σ α} {comp : StateM σ α} (h : HoareTriple P comp Q) : HoareTriple (fun (s : σ) => P s ∧ True) comp Q

@[simp]

theorem OracleComp.StateM.HoareTriple.get_rule_basic {σ : Type u_4} : HoareTriple (fun (x : σ) => True) get fun (s x s' : σ) => s = x ∧ s = s'

@[simp]

theorem OracleComp.StateM.HoareTriple.set_rule_basic {σ : Type} (s' : σ) : HoareTriple (fun (x : σ) => True) (set s') fun (x : σ) (x : PUnit.{1}) (s'' : σ) => s'' = s'

theorem OracleComp.StateM.HoareTriple.get_rule_forward {σ : Type u_4} (P : PreCondition σ) : HoareTriple P get fun (s x s' : σ) => P s ∧ s = x ∧ s = s'

Strongest postcondition for get: After get executes, we know the value read equals the state, and the state hasn't changed

theorem OracleComp.StateM.HoareTriple.set_rule_forward {σ : Type} (P : PreCondition σ) (s' : σ) : HoareTriple P (set s') fun (s : σ) (x : PUnit.{1}) (s'' : σ) => P s ∧ s'' = s'

theorem OracleComp.StateM.HoareTriple.get_rule_backward {σ : Type u_4} (Q : σ → σ → σ → Prop) : HoareTriple (fun (s : σ) => Q s s s) get Q

Weakest precondition for get: To ensure Q holds after get, Q must hold for the state value we read

theorem OracleComp.StateM.HoareTriple.set_rule_backward {σ : Type} (s' : σ) (Q : σ → Unit → σ → Prop) : HoareTriple (fun (s : σ) => Q s () s') (set s') Q

Weakest precondition for set: To ensure Q holds after setting state to s', Q must hold for that new state

theorem OracleComp.StateM.HoareTriple.conj_rule {σ α : Type u_4} {P₁ P₂ : PreCondition σ} {Q₁ Q₂ : PostCondition σ α} {comp : StateM σ α} (h₁ : HoareTriple P₁ comp Q₁) (h₂ : HoareTriple P₂ comp Q₂) : HoareTriple (fun (s : σ) => P₁ s ∧ P₂ s) comp fun (s : σ) (x : α) (s' : σ) => Q₁ s x s' ∧ Q₂ s x s'

class OracleComp.StateM.WeakestPrecondition {σ α : Type u_4} (comp : StateM σ α) (Q : PostCondition σ α) : Type u_4

• P : PreCondition σ
• hP : HoareTriple (P comp Q) comp Q
• hWeak (P' : PreCondition σ) : HoareTriple P' comp Q → P comp Q ≤ P'

class OracleComp.StateM.StrongestPostcondition {σ α : Type u_4} (P : PreCondition σ) (comp : StateM σ α) : Type u_4

• Q : PostCondition σ α
• hQ : HoareTriple P comp (Q P comp)
• hStrong (Q' : PostCondition σ α) : HoareTriple P comp Q' → Q' ≤ Q P comp

instance OracleComp.StateM.instSubsingletonWeakestPrecondition {σ α : Type u_4} {comp : StateM σ α} {Q : PostCondition σ α} : Subsingleton (WeakestPrecondition comp Q)

instance OracleComp.StateM.instSubsingletonStrongestPostcondition {σ α : Type u_4} {P : PreCondition σ} {comp : StateM σ α} : Subsingleton (StrongestPostcondition P comp)

instance OracleComp.StateM.instInhabitedWeakestPreconditionPureStateM {σ α : Type u_4} {Q : PostCondition σ α} {x : α} : Inhabited (WeakestPrecondition (pure x) Q)

Equations

• OracleComp.StateM.instInhabitedWeakestPreconditionPureStateM = { default := { P := fun (s : σ) => Q s x s, hP := ⋯, hWeak := ⋯ } }

instance OracleComp.StateM.instWeakestPreconditionPureStateM {σ : Type u_4} {Q : PostCondition σ σ} {x : σ} : WeakestPrecondition (pure x) Q

Equations

• OracleComp.StateM.instWeakestPreconditionPureStateM = default

instance OracleComp.StateM.instInhabitedStrongestPostconditionPureStateM {σ α : Type u_4} {P : PreCondition σ} {x : α} : Inhabited (StrongestPostcondition P (pure x))

Equations

• OracleComp.StateM.instInhabitedStrongestPostconditionPureStateM = { default := { Q := fun (s : σ) (a : α) (s' : σ) => s = s' ∧ a = x ∧ P s, hQ := ⋯, hStrong := ⋯ } }

instance OracleComp.StateM.instStrongestPostconditionPureStateM {σ α : Type u_4} {P : PreCondition σ} {x : α} : StrongestPostcondition P (pure x)

Equations

• OracleComp.StateM.instStrongestPostconditionPureStateM = default

instance OracleComp.StateM.instInhabitedWeakestPreconditionGetStateM {σ : Type u_4} {Q : PostCondition σ σ} : Inhabited (WeakestPrecondition get Q)

Equations

• OracleComp.StateM.instInhabitedWeakestPreconditionGetStateM = { default := { P := fun (s : σ) => Q s s s, hP := ⋯, hWeak := ⋯ } }

instance OracleComp.StateM.instWeakestPreconditionGetStateM {σ : Type u_4} {Q : PostCondition σ σ} : WeakestPrecondition get Q

Equations

• OracleComp.StateM.instWeakestPreconditionGetStateM = default

instance OracleComp.StateM.instInhabitedStrongestPostconditionPUnitSetStateM {σ : Type} {P : PreCondition σ} {s' : σ} : Inhabited (StrongestPostcondition P (set s'))

Equations

• OracleComp.StateM.instInhabitedStrongestPostconditionPUnitSetStateM = { default := { Q := fun (s : σ) (x : PUnit.{1}) (s'' : σ) => P s ∧ s'' = s', hQ := ⋯, hStrong := ⋯ } }

instance OracleComp.StateM.instStrongestPostconditionPUnitSetStateM {σ : Type} {P : PreCondition σ} {s' : σ} : StrongestPostcondition P (set s')

Equations

• OracleComp.StateM.instStrongestPostconditionPUnitSetStateM = default

inductive OracleComp.Tree' (a : Type u_1) : Type u_1

• leaf {a : Type u_1} : a → Tree' a
• node {a : Type u_1} : Tree' a → Tree' a → Tree' a

def OracleComp.relabel {α : Type u_1} (t : Tree' α) (n : ℕ) : Tree' ℕ × ℕ

Equations

• OracleComp.relabel (OracleComp.Tree'.leaf a) n = (OracleComp.Tree'.leaf n, n + 1)
• OracleComp.relabel (l.node r) n = match OracleComp.relabel l n with | (l', n') => match OracleComp.relabel r n' with | (r', n'') => (l'.node r', n'')

def OracleComp.relabelM {α : Type u_1} (t : Tree' α) : StateM ℕ (Tree' ℕ)

Equations

• OracleComp.relabelM (OracleComp.Tree'.leaf a) = do let n ← get set (n + 1) pure (OracleComp.Tree'.leaf n)
• OracleComp.relabelM (l.node r) = do let l' ← OracleComp.relabelM l let r' ← OracleComp.relabelM r pure (l'.node r')

def OracleComp.flatten {α : Type u_1} (t : Tree' α) : List α

Equations

• OracleComp.flatten (OracleComp.Tree'.leaf a) = [a]
• OracleComp.flatten (l.node r) = OracleComp.flatten l ++ OracleComp.flatten r

def OracleComp.size {α : Type u_1} : Tree' α → ℕ

Equations

• OracleComp.size (OracleComp.Tree'.leaf a) = 1
• OracleComp.size (l.node r) = OracleComp.size l + OracleComp.size r

def OracleComp.Nat.seq : ℕ → ℕ → List ℕ

Equations

• OracleComp.Nat.seq x✝ 0 = []
• OracleComp.Nat.seq x✝ m.succ = x✝ :: OracleComp.Nat.seq (x✝ + 1) m