We prove that the proof rules defined in ribbons_graphical are complete with respect to the rules of separation logic defined in ribbons_basic.
theorem completeness: fixes p c q
assumes prov_triple (p,c,q)
shows ∃G P Q. wf_dia G ∧ coms_dia G c ∧ p = ass P ∧ q = ass Q ∧ prov_dia G P Q (is ∃G P Q. ?Φ G P Q)
proof -
let ?V = [v01,v02]
let ?Λ = (λv. Rib Emp) (v01 := Rib p, v02 := Rib q)
let ?E = [([v01], Com c, [v02])]
let ?G = Graph ?V ?Λ ?E
let ?P = Emp_int ⊗ Ribbon p
let ?Q = Emp_int ⊗ Ribbon q
let ?π = [Inl v01, Inr ([v01], Com c, [v02]), Inl v02]
have coms_dia ?G c
proof -
have coms_dia ?G (foldr (op ;;) [Skip, c, Skip] Skip)
proof (rule coms_main [where π = ?π])
have yiecn: distinct [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] by auto
show ?π ∈ lins ?G
proof (unfold lins.simps[of ?V ?Λ ?E], intro CollectI conjI, simp)
show set [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] =
Inl ` set [v01, v02] ∪ Inr ` set [([v01], Com c, [v02])]
by auto
next
show ∀i j v e.
i < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ∧
j < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ∧
[Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! i = Inl v ∧
[Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! j = Inr e ∧
v ∈ set (fst3 e) ⟶ i < j
proof (intro allI impI, elim conjE)
fix i j v e
assume
axvgk: i < length ?π and
snuyc: j < length ?π and
bwrsk: ?π ! i = Inl v and
irnle: ?π ! j = Inr e and
lpfbk: v ∈ set (fst3 e)
from nth_in_set [OF snuyc irnle] have
lsdkf: e = ([v01], Com c, [v02]) by auto
with lpfbk have cxtvo: v = v01 unfolding fst3_def by auto
have i=0
proof (rule ccontr)
assume xiznn: i ≠ 0
have gocuj: 0 < length ?π by auto
from distinct_conv_nth[of ?π] yiecn have
⋀i j.⟦ i<length ?π ; j<length ?π ; i ≠ j ⟧ ⟹ ?π ! i ≠ ?π ! j
by auto
from this[OF axvgk gocuj xiznn] and bwrsk and cxtvo show
False by auto
qed
moreover have j=1
proof (rule ccontr)
assume xiznn: j ≠ 1
have gocuj: 1 < length ?π by auto
from distinct_conv_nth[of ?π] yiecn have
⋀i j.⟦ i<length ?π ; j<length ?π ; i ≠ j ⟧ ⟹ ?π ! i ≠ ?π ! j
by auto
from this[OF snuyc gocuj xiznn] and irnle and lsdkf show
False by auto
qed
ultimately show i < j by auto
qed
next
show ∀j k w e.
j < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ∧
k < length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ∧
[Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! j = Inr e ∧
[Inl v01, Inr ([v01], Com c, [v02]), Inl v02] ! k = Inl w ∧
w ∈ set (thd3 e) ⟶ j < k
proof (intro allI impI, elim conjE)
fix j k w e
assume
snuyc: j < length ?π and
rldms: k < length ?π and
irnle: ?π ! j = Inr e and
nthqn: ?π ! k = Inl w and
hfmli: w ∈ set (thd3 e)
from nth_in_set [OF snuyc irnle] have
lsdkf: e = ([v01], Com c, [v02]) by auto
with hfmli have qtxuv: w = v02 unfolding thd3_def by auto
have j=1
proof (rule ccontr)
assume xiznn: j ≠ 1
have gocuj: 1 < length ?π by auto
from distinct_conv_nth[of ?π] yiecn have
⋀i j.⟦ i<length ?π ; j<length ?π ; i ≠ j ⟧ ⟹ ?π ! i ≠ ?π ! j
by auto
from this[OF snuyc gocuj xiznn] and irnle and lsdkf show
False by auto
qed
moreover have k=2
proof (rule ccontr)
assume xiznn: k ≠ 2
have gocuj: 2 < length ?π by auto
from distinct_conv_nth[of ?π] yiecn have
⋀i j.⟦ i<length ?π ; j<length ?π ; i ≠ j ⟧ ⟹ ?π ! i ≠ ?π ! j
by auto
from this[OF rldms gocuj xiznn] and nthqn and qtxuv show
False by auto
qed
ultimately show j < k by auto
qed
qed
next
show length [Skip, c, Skip] =
length [Inl v01, Inr ([v01], Com c, [v02]), Inl v02]
by auto
next
fix i
assume
ukhof: i < length ?π and
wfzta: ∃v. ?π ! i = Inl v
have i = 0 ∨ i = 2
proof (rule ccontr)
assume ¬ (i = 0 ∨ i = 2)
with ukhof have i=1 by auto
hence ?π ! i = Inr ([v01], Com c, [v02]) by auto
with wfzta show False by auto
qed
hence (?π ! i = Inl v01) ∨ (?π ! i = Inl v02)
and [Skip, c, Skip] ! i = Skip by auto
moreover have coms_ass (Rib p) Skip and
coms_ass (Rib q) Skip using coms_skip by auto
ultimately show
coms_ass (?Λ (Sum_Type.Projl (?π ! i))) ([Skip, c, Skip] ! i)
by auto
next
fix i
assume
ukhof: i < length ?π and
wfzta: ∃e. ?π ! i = Inr e
have i = 1
proof (rule ccontr)
assume ¬ (i = 1)
with ukhof have i=0 ∨ i=2 by auto
hence ?π ! i = Inl v01 ∨ ?π ! i = Inl v02 by auto
with wfzta show False by auto
qed
hence ncdef: ?π ! i = Inr ([v01], Com c, [v02])
and [Skip, c, Skip] ! i = c by auto
moreover have coms_com (Com c) c using coms_basic by auto
ultimately show
coms_com (snd3 (Sum_Type.Projr (?π ! i)))
([Skip, c, Skip] ! i)
unfolding ncdef unfolding snd3_def by auto
qed
moreover have
c = foldr (op ;;) [Skip, c, Skip] Skip
using seq_skip skip_seq by auto
ultimately show coms_dia ?G c by auto
qed
moreover have p = ass ?P and q = ass ?Q
by (auto simp add: emp_star)
moreover have bivui: wf_dia ?G
proof
show acyclicity ?E
by (unfold acyclicity_def, auto simp add: fst3_def thd3_def, unfold acyclic_def, auto)
next
show linearity ?E by (unfold linearity_def, auto)
qed (auto simp add: fst3_def thd3_def)
moreover have prov_dia ?G ?P ?Q
proof -
have ?P = top_dia ?G by (auto simp add: fst3_def thd3_def)
moreover have ?Q = bot_dia ?G by (auto simp add: fst3_def thd3_def)
moreover have prov_dia ?G (top_dia ?G) (bot_dia ?G)
by (rule Main, auto simp add: Skip Basic emp_star assms fst3_def snd3_def thd3_def bivui)
ultimately show prov_dia ?G ?P ?Q by auto
qed
ultimately show ∃G P Q. wf_dia G ∧ coms_dia G c ∧ p = ass P ∧ q = ass Q ∧ prov_dia G P Q
using exI3[of ?Φ ?G ?P ?Q] by auto
qed
end
