Theory QHoare

section ‹Very simple Quantum Hoare logic›

theory QHoare
  imports Quantum_Extra
begin

unbundle register_syntax
unbundle cblinfun_syntax
unbundle lattice_syntax
no_notation Order.top ("⊤ı")

locale qhoare =
  fixes memory_type :: "'mem itself"
begin

definition "apply U R = R U" for R :: ‹'a update ⇒ 'mem update›
definition "ifthen R x = R (butterfly (ket x) (ket x))" for R :: ‹'a update ⇒ 'mem update›
definition "program S = fold (o⇩C⇩L) S id_cblinfun" for S :: ‹'mem update list›


definition hoare :: ‹'mem ell2 ccsubspace ⇒ ('mem ell2 ⇒⇩C⇩L 'mem ell2) list ⇒ 'mem ell2 ccsubspace ⇒ bool› where
  "hoare C p D ⟷ (∀ψ∈space_as_set C. program p *⇩V ψ ∈ space_as_set D)" for C p D

definition EQ :: "('a update ⇒ 'mem update) ⇒ 'a ell2 ⇒ 'mem ell2 ccsubspace" (infix "=⇩q" 75) where
  "EQ R ψ = R (selfbutter ψ) *⇩S ⊤"

lemma program_skip[simp]: "program [] = id_cblinfun"
  by (simp add: qhoare.program_def)

lemma program_seq: "program (p1@p2) = program p2 o⇩C⇩L program p1"
  apply (induction p2 rule:rev_induct)
   apply (simp_all add: program_def)
  by (meson cblinfun_assoc_left(1))

lemma hoare_seq[trans]: "hoare C p1 D ⟹ hoare D p2 E ⟹ hoare C (p1@p2) E"
  by (auto simp: program_seq hoare_def)

lemma hoare_weaken_left[trans]: ‹A ≤ B ⟹ hoare B p C ⟹ hoare A p C›
  unfolding hoare_def
  by (meson in_mono less_eq_ccsubspace.rep_eq) 

lemma hoare_weaken_right[trans]: ‹hoare A p B ⟹ B ≤ C ⟹ hoare A p C›
  unfolding hoare_def 
  by (meson in_mono less_eq_ccsubspace.rep_eq) 

lemma hoare_skip: "C ≤ D ⟹ hoare C [] D"
  by (auto simp: program_def hoare_def in_mono less_eq_ccsubspace.rep_eq)

lemma hoare_apply: 
  assumes "R U *⇩S pre ≤ post"
  shows "hoare pre [apply U R] post"
proof -
  from assms have ‹ψ ∈ space_as_set pre ⟹ R U *⇩V ψ ∈ space_as_set post› for ψ
    by (metis (no_types, lifting) cblinfun_image.rep_eq closure_subset imageI less_eq_ccsubspace.rep_eq subsetD)
  then show ?thesis
    by (auto simp: hoare_def program_def apply_def)
qed

lemma hoare_ifthen: 
  fixes R :: ‹'a update ⇒ 'mem update›
  assumes "R (selfbutter (ket x)) *⇩S pre ≤ post"
  shows "hoare pre [ifthen R x] post"
proof -
  from assms have ‹ψ ∈ space_as_set pre ⟹ R (vector_to_cblinfun (ket x) o⇩C⇩L bra x) *⇩V ψ ∈ space_as_set post› for ψ
    by (metis butterfly_def_one_dim cblinfun_apply_in_image' less_eq_ccsubspace.rep_eq subsetD)
  then show ?thesis
    by (auto simp: hoare_def program_def ifthen_def butterfly_def)
qed
end

unbundle no register_syntax
unbundle no cblinfun_syntax
unbundle no lattice_syntax

end