wp.lean

namespace design_1

structure wp_state (σ : Type) (α : Type) :=
/- wp is a function that converts a postcondition into a predcondition. -/
(wp     : (α × σ → Prop) → σ → Prop)
(action : σ → α × σ)
(valid  : ∀ (post : α × σ → Prop) (s : σ), (wp post) s → post (action s))


namespace wp_state

def return {σ : Type} {α : Type} (a : α) : wp_state σ α :=
{ wp     := λ post s₀, post (a, s₀),
  action := λ s, (a, s),
  valid  := begin intros, assumption end }

def bind {σ α β : Type} (m₁ : wp_state σ α) (m₂ : α → wp_state σ β) : wp_state σ β :=
{ wp     := λ post s₀, m₁.wp (λ r, (m₂ r.1).wp post r.2) s₀,
  action := λ s₀ : σ, let r := m₁.action s₀ in (m₂ r.1).action r.2,
  valid  :=
  begin
     intros post s hp,
     apply (m₂ ((m₁.action s).fst)).valid post ((m₁.action s).snd),
     apply m₁.valid (λ r, (m₂ r.1).wp post r.2) s hp
  end }

def read {σ : Type} : wp_state σ σ :=
{ wp     := λ post s₀, post (s₀, s₀),
  action := λ s, (s, s),
  valid  := begin intros, assumption end }

def write {σ : Type} (s : σ) : wp_state σ unit :=
{ wp     := λ post s₀, post ((), s),
  action := λ s₀, ((), s),
  valid  := begin intros, assumption end }

def assert {σ : Type} (p : σ → Prop) : wp_state σ unit :=
{ wp     := λ post s₀, p s₀ ∧  post ((), s₀),
  action := λ s, ((), s),
  valid  := begin intros post s h, exact h.2 end }

lemma read_read_eq_read {σ : Type} : (bind (@read σ) (λ _, read)) = read :=
rfl

lemma read_write_eq_write {σ : Type} (s : σ) : (bind read (λ _, write s)) = write s :=
rfl

lemma write_write_eq_write {σ : Type} (s₁ s₂ : σ) : (bind (write s₁) (λ _, write s₂)) = write s₂ :=
rfl

lemma read_write_eq_return {σ : Type} : (bind (@read σ) write) = return () :=
rfl

end wp_state

end design_1


namespace design_2

/-
We can combine `action` and `valid` fields.
action : Π (s : σ), { r : α × σ // ∀ post, (wp post) s → post r }
-/

structure wp_state (σ : Type) (α : Type) :=
(wp     : (α × σ → Prop) → σ → Prop)
(action : Π (s : σ), { r : α × σ // ∀ post, (wp post) s → post r })

namespace wp_state

def return {σ : Type} {α : Type} (a : α) : wp_state σ α :=
{ wp     := λ post s₀, post (a, s₀),
  action := λ s, ⟨(a, s), begin intros, assumption end⟩ }

def bind {σ α β : Type} (m₁ : wp_state σ α) (m₂ : α → wp_state σ β) : wp_state σ β :=
{ wp     := λ post s₀, m₁.wp (λ r, (m₂ r.1).wp post r.2) s₀,
  action := λ s : σ,
   let r := m₁.action s in
   ⟨ (m₂ r.val.1).action r.val.2,
     begin
       intros post h,
       apply ((m₂ r.val.1).action r.val.2).2 post,
       apply r.2 _ h,
     end⟩ }

def read {σ : Type} : wp_state σ σ :=
{ wp     := λ post s₀, post (s₀, s₀),
  action := λ s, ⟨(s, s), begin intros, assumption end⟩ }

def write {σ : Type} (s : σ) : wp_state σ unit :=
{ wp     := λ post s₀, post ((), s),
  action := λ s₀, ⟨((), s), begin intros, assumption end⟩ }

def assert {σ : Type} (p : σ → Prop) : wp_state σ unit :=
{ wp     := λ post s₀, p s₀ ∧  post ((), s₀),
  action := λ s, ⟨((), s), begin intros _ h, exact h.2 end⟩ }

lemma read_read_eq_read {σ : Type} : (bind (@read σ) (λ _, read)) = read :=
rfl

lemma read_write_eq_write {σ : Type} (s : σ) : (bind read (λ _, write s)) = write s :=
rfl

lemma write_write_eq_write {σ : Type} (s₁ s₂ : σ) : (bind (write s₁) (λ _, write s₂)) = write s₂ :=
rfl

lemma read_write_eq_return {σ : Type} : (bind (@read σ) write) = return () :=
rfl

end wp_state

end design_2