Hoare triples for OracleComp and extensions

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

@[reducible, inline]

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

@[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

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

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

Post-conditions are partially ordered by reverse inclusion

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

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

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₃

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

def OracleComp.StateM.HoareState.get {σ : Type u_1} : HoareState (PreCondition.top σ) σ fun (s x s' : σ) => s = s' ∧ x = 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'

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

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

@[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)

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

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

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

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

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

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

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

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' ℕ × ℕ

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

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

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

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