# paterson: Equivalence of two flowchart schemes, due to Paterson

cf. "Mathematical theory of computation", Manna, 1974 cf. "Kleene algebra with tests and program schematology", A. Angus and D. Kozen, 2001

From RelationAlgebra Require Import kat normalisation rewriting move kat_tac comparisons rel.
Set Implicit Arguments.

# Memory model

we need only five memory locations: the y_i are temporary variables and io is used for input and output
Inductive loc := y1 | y2 | y3 | y4 | io.
Record state := { v1: nat; v2: nat; v3: nat; v4: nat; vio: nat }.

getting the content of a memory cell
Definition get x := match x with y1v1 | y2v2 | y3v3 | y4v4 | iovio end.

setting the content of a memory cell
Definition set x n m :=
match x with
| y1 ⇒ {| v1:=n; v2:=v2 m; v3:=v3 m; v4:=v4 m; vio:=vio m |}
| y2 ⇒ {| v1:=v1 m; v2:=n; v3:=v3 m; v4:=v4 m; vio:=vio m |}
| y3 ⇒ {| v1:=v1 m; v2:=v2 m; v3:=n; v4:=v4 m; vio:=vio m |}
| y4 ⇒ {| v1:=v1 m; v2:=v2 m; v3:=v3 m; v4:=n; vio:=vio m |}
| io ⇒ {| v1:=v1 m; v2:=v2 m; v3:=v3 m; v4:=v4 m; vio:=n |}
end.

basic properties of get and set
Lemma get_set x v m: get x (set x v m) = v.
Proof. now destruct x. Qed.

Lemma get_set' x y v m: xy get x (set y v m) = get x m.
Proof. destruct y; destruct x; simpl; trivial; congruence. Qed.

Lemma set_set x v v' m: set x v (set x v' m) = set x v m.
Proof. now destruct x. Qed.

Lemma set_set' x y v v' m: xy set x v (set y v' m) = set y v' (set x v m).
Proof. destruct y; destruct x; simpl; trivial; congruence. Qed.

comparing locations
Definition eqb x y :=
match x,y with
| y1,y1 | y2,y2 | y3,y3 | y4,y4 | io,iotrue
| _,_false
end.
Lemma eqb_spec: x y, reflect (x=y) (eqb x y).
Proof. destruct x; destruct y; simpl; try constructor; congruence. Qed.
Lemma eqb_false x y: xy eqb x y = false.
Proof. case eqb_spec; congruence. Qed.
Lemma neqb_spec x y: negb (eqb x y) xy.
Proof. case eqb_spec; intuition; congruence. Qed.

# Arithmetic and Boolean expressions

Section s.

we assume arbitrary functions to interpret symbols f, g, and p
Variable ff: nat nat.
Variable gg: nat nat nat.
Variable pp: nat bool.

we use a single inductive to represent Arithmetic and Boolean expressions: this allows us to share code about evaluation, free variables and so on, through polymorphism

## evaluation of expressions

Fixpoint eval A (e: expr A) (m: state): A :=
match e with
| e_var xget x m
| O ⇒ 0%nat
| f' eff (eval e m)
| g' e fgg (eval e m) (eval f m)
| p' epp (eval e m)
| e_cap e feval e m &&& eval f m
| e_cup e feval e m ||| eval f m
| e_neg enegb (eval e m)
| e_botfalse
| e_toptrue
end.

## Free variables

Fixpoint free y A (e: expr A): bool :=
match e with
| e_var xnegb (eqb x y)
| f' e | p' e | e_neg efree y e
| g' e f | e_cap e f | e_cup e ffree y e &&& free y f
| _true
end.

## Substitution

Fixpoint subst x v A (f: expr A): expr A :=
match f with
| e_var yif eqb x y then v else e_var y
| OO
| f' ef' (subst x v e)
| p' ep' (subst x v e)
| g' e fg' (subst x v e) (subst x v f)
| e_cup e fe_cup (subst x v e) (subst x v f)
| e_cap e fe_cap (subst x v e) (subst x v f)
| e_neg ee_neg (subst x v e)
| e_bote_bot
| e_tope_top
end.

Lemma subst_free x v A (e: expr A): free x e subst x v e = e.
Proof.
induction e; simpl; trivial.
rewrite neqb_spec. case eqb_spec; congruence.
intro. now rewrite IHe.
rewrite landb_spec. intros [? ?]. now rewrite IHe1, IHe2.
intro. now rewrite IHe.
rewrite landb_spec. intros [? ?]. now rewrite IHe1, IHe2.
rewrite landb_spec. intros [? ?]. now rewrite IHe1, IHe2.
intro. now rewrite IHe.
Qed.

Lemma free_subst x e A (f: expr A): free x e free x (subst x e f).
Proof.
intro. induction f; simpl; rewrite ?IHf1; auto.
case eqb_spec; trivial. simpl. rewrite neqb_spec. congruence.
Qed.

# Programs

We just use KAT expressions, since any gflowchat scheme can be encoded as such an expression
Inductive prog :=
| p_tst(t: expr bool)
| p_aff(x: loc)(e: expr nat)
| p_str(p: prog)
| p_dot(p q: prog)
| p_pls(p q: prog).

# Bigstep semantics

updating the memory, according to the assignment x<-e
Definition update x e m := set x (eval e m) m.
relational counterpart of this function
Notation upd x e := (frel (update x e)).

Bigstep semantics, as a fixpoint
Fixpoint bstep (p: prog): hrel state state :=
match p with
| p_tst p[eval p: dset state]
| p_aff x eupd x e
| p_str p(bstep p)^*
| p_dot p qbstep p bstep q
| p_pls p qbstep p + bstep q
end.

auxiliary lemma relating the evaluation of expressions, the assignments to the memory, and subsitution of expressions
Lemma eval_update x v A (e: expr A) m: eval e (update x v m) = eval (subst x v e) m.
Proof.
induction e; simpl; try congruence.
unfold update. case eqb_spec. intros <-. apply get_set.
intro. apply get_set'. congruence.
now rewrite IHe1, IHe2.
now rewrite IHe1, IHe2.
Qed.

Now we make the set of programs a Kleene algebra with tests: we declare canonical structures for Boolean expressions (tests), programs (Kleene elements), and the natural injection of the former into the latter

Canonical Structure expr_lattice_ops: lattice.ops := {|
car := expr bool;
leq := fun x yeval x eval y;
weq := fun x yeval x eval y;
cup := e_cup;
cap := e_cap;
bot := e_bot;
top := e_top;
neg := e_neg
|}.

Canonical Structure prog_lattice_ops: lattice.ops := {|
car := prog;
leq := fun x ybstep x bstep y;
weq := fun x ybstep x bstep y;
cup := p_pls;
cap := assert_false p_pls;
bot := p_tst e_bot;
top := assert_false (p_tst e_bot);
neg := assert_false id
|}.

Canonical Structure prog_monoid_ops: monoid.ops := {|
ob := unit;
mor n m := prog_lattice_ops;
dot n m p := p_dot;
one n := p_tst e_top;
itr n := (fun xp_dot x (p_str x));
str n := p_str;
cnv n m := assert_false id;
ldv n m p := assert_false (fun _id);
rdv n m p := assert_false (fun _id)
|}.

Canonical Structure prog_kat_ops: kat.ops := {|
kar := prog_monoid_ops;
tst n := expr_lattice_ops;
inj n := p_tst
|}.

Notation prog' := (prog_kat_ops tt tt).
Notation test := (@tst prog_kat_ops tt).

proving that the laws of KAT are satisfied is almost trivial, since the model faithfully embeds in the relational model

Instance expr_lattice_laws: lattice.laws BL expr_lattice_ops.
Proof.
apply laws_of_injective_morphism with (@eval bool: expr bool dset state); trivial.
split; simpl; tauto.
Qed.

Instance prog_monoid_laws: monoid.laws BKA prog_monoid_ops.
Proof.
apply laws_of_faithful_functor with (fun _state) (fun _ _: unitbstep); trivial.
split; simpl; try discriminate; try tauto. 2: firstorder.
split; simpl; try discriminate; try tauto. firstorder auto with bool.
Qed.
Instance prog_lattice_laws: lattice.laws BKA prog_lattice_ops := lattice_laws tt tt.

Instance prog_kat_laws: kat.laws prog_kat_ops.
Proof.
constructor; simpl; eauto with typeclass_instances. 2: tauto.
split; try discriminate; try (simpl; tauto).
intros x y H. apply inj_leq. intro m. apply H.
intros x y H. apply inj_weq. intro m. apply H.
intros _ x y. apply (inj_cup (X:=hrel_kat_ops)).
intros _ x y. apply (inj_cap (X:=hrel_kat_ops)).
Qed.

## variables read by a program

Fixpoint dont_read y (p: prog'): bool :=
match p with
| p_dot p q | p_pls p qdont_read y p &&& dont_read y q
| p_aff x efree y e
| p_tst tfree y t
end.

Infix " ;" := (dot _ _ _) (left associativity, at level 40): ra_terms.
Definition aff x e: prog' := p_aff x e.
Notation "x <- e" := (aff x e) (at level 30).
Notation del y := (y<-O).

# Laws of schematic KAT

Arguments hrel_monoid_ops : simpl never.
Arguments hrel_lattice_ops : simpl never.

(the numbering corresponds to Angus and Kozen's paper)
Lemma eq_6 (x y: loc) (s t: expr nat):
negb (eqb x y) &&& free y s x<-s;y<-t y<-subst x s t; x<-s.
Proof.
rewrite landb_spec, neqb_spec. intros [D H]. cbn.
rewrite 2frel_comp. apply frel_weq. intro m.
unfold update at 1 2 3. rewrite set_set' by congruence. f_equal.
now rewrite eval_update, subst_free.
unfold update. now rewrite <-eval_update.
Qed.

Lemma eq_7 (x y: loc) (s t: expr nat):
negb (eqb x y) &&& free x s x<-s;y<-t x<-s;y<-subst x s t.
Proof.
rewrite landb_spec, neqb_spec. intros [D H]. cbn.
rewrite 2frel_comp. apply frel_weq. intro m.
unfold update at 1 3. f_equal.
rewrite 2eval_update. symmetry. rewrite subst_free. reflexivity.
now apply free_subst.
Qed.

Lemma eq_8 (x: loc) (s t: expr nat): x<-s;x<-t x<-subst x s t.
Proof.
cbn. rewrite frel_comp. apply frel_weq. intro m.
unfold update. rewrite set_set. f_equal. apply eval_update.
Qed.

Lemma eq_9 (x: loc) (t: expr nat) (phi: test): [subst x t phi: test];x<-t x<-t;[phi].
Proof.
Transparent hrel_lattice_ops. intros m m'. split. Opaque hrel_lattice_ops.
intros [m0 [<- H] ->]. eexists. reflexivity. split; trivial. now rewrite eval_update.
intros [m0 → [<- H]]. eexists. 2: reflexivity. split; trivial. now rewrite <-eval_update.
Qed.

Lemma eq_6' (x y: loc) (s t: expr nat): free x t &&& negb (eqb x y) &&& free y s
x<-s;y<-t y<-t; x<-s.
Proof. rewrite landb_spec. intros [? ?]. now rewrite eq_6, subst_free. Qed.

Lemma eq_9' (x: loc) (t: expr nat) (phi: test): free x phi [phi];x<-t x<-t;[phi].
Proof. intro. now rewrite <-eq_9, subst_free. Qed.

Transparent hrel_lattice_ops.
Arguments hrel_lattice_ops : simpl never.

Lemma same_value (f: state state) (p: prog') (a b: test):
bstep p frel f ( m, eval a (f m) = eval b (f m))
p;[a !b !a b] 0.
Proof.
intros Hp H. cbn. rewrite Hp.
intros m m' [? → [<- E]].
exfalso. rewrite lorb_spec, 2landb_spec, 2negb_spec, H in E. intuition congruence.
Qed.

# Garbage-collecting assignments to unread variables

(i.e., Lemma 4.5 in Angus and Kozen's paper)
Fixpoint gc y (p: prog'): prog' :=
match p with
| p_str p(gc y p)^*
| p_tst _p
| p_aff x eif eqb x y then 1 else x<-e
| p_dot p qgc y p ; gc y q
| p_pls p qgc y p + gc y q
end.

Arguments prog_monoid_ops : simpl never.
Arguments prog_lattice_ops : simpl never.
Arguments prog_kat_ops : simpl never.

Lemma gc_correct y p: dont_read y p gc y p; del y p; del y.
Proof.
intro H. transitivity (del y; gc y p).
induction p; cbn.
now apply eq_9'.
case eqb_spec. ra. intro. apply eq_6'. now rewrite eqb_false.
symmetry. apply str_move. symmetry. now auto.
apply landb_spec in H as [? ?]. mrewrite IHp2. 2: assumption. now mrewrite IHp1.
apply landb_spec in H as [? ?]. ra_normalise. now apply cup_weq; auto.
symmetry. induction p; cbn.
now apply eq_9'.
case eqb_spec. intros <-. rewrite eq_8. ra. intro D. apply eq_6'. now rewrite eqb_false.
symmetry. apply str_move. symmetry. now auto.
apply landb_spec in H as [? ?]. mrewrite IHp2. 2: assumption. now mrewrite IHp1.
apply landb_spec in H as [? ?]. ra_normalise. now apply cup_weq; auto.
Qed.

Ltac solve_rmov ::=
first
[ eassumption
| symmetry; eassumption
| eapply rmov_x_dot
| apply rmov_x_pls
| apply rmov_x_str
| apply rmov_x_itr
| apply rmov_x_cap
| apply rmov_x_cup
| apply rmov_x_neg
| apply rmov_inj
| apply rmov_x_1
| apply rmov_x_0 ];
match goal with |- ?x ?ysolve_rmov end.

# Paterson's equivalence

Theorem Paterson:
let a1 := p' y1: test in
let a2 := p' y2: test in
let a3 := p' y3: test in
let a4 := p' y4: test in
let clr := del y1; del y2; del y3; del y4 in
let x1 := y1<-io in
let s1 := y1<-f' io in
let s2 := y2<-f' io in
let z1 := io<-y1; clr in
let z2 := io<-y2; clr in
let p11 := y1<-f' y1 in
let p13 := y1<-f' y3 in
let p22 := y2<-f' y2 in
let p41 := y4<-f' y1 in
let q222 := y2<-g' y2 y2 in
let q214 := y2<-g' y1 y4 in
let q211 := y2<-g' y1 y1 in
let q311 := y3<-g' y1 y1 in
let r11 := y1<-f' (f' y1) in
let r12 := y1<-f' (f' y2) in
let r13 := y1<-f' (f' y3) in
let r22 := y2<-f' (f' y2) in
let rhs := s2;[a2];q222;([!a2];r22;[a2];q222)^*;[a2];z2 in
x1;p41;p11;q214;q311;([!a1];p11;q214;q311)^*;[a1];p13;
(([!a4]+[a4];([!a2];p22)^*;[a2 !a3];p41;p11);q214;q311;([!a1];p11;q214;q311)^*;[a1];p13)^*;
[a4];([!a2];p22)^*;[a2 a3];z2 rhs.
Proof.
intros.
simple commutation hypotheses, to be exploited by hkat
assert (a1p22: [a1];p22 p22;[a1]) by now apply eq_9'.
assert (a1q214: [a1];q214 q214;[a1]) by now apply eq_9'.
assert (a1q211: [a1];q211 q211;[a1]) by now apply eq_9'.
assert (a1q311: [a1];q311 q311;[a1]) by now apply eq_9'.
assert (a2p13: [a2];p13 p13;[a2]) by now apply eq_9'.
assert (a2r12: [a2];r12 r12;[a2]) by now apply eq_9'.
assert (a2r13: [a2];r13 r13;[a2]) by now apply eq_9'.
assert (a3p13: [a3];p13 p13;[a3]) by now apply eq_9'.
assert (a3p22: [a3];p22 p22;[a3]) by now apply eq_9'.
assert (a3r12: [a3];r12 r12;[a3]) by now apply eq_9'.
assert (a3r13: [a3];r13 r13;[a3]) by now apply eq_9'.
assert (a4p13: [a4];p13 p13;[a4]) by now apply eq_9'.
assert (a4p11: [a4];p11 p11;[a4]) by now apply eq_9'.
assert (a4p22: [a4];p22 p22;[a4]) by now apply eq_9'.
assert (a4q214: [a4];q214 q214;[a4]) by now apply eq_9'.
assert (a4q211: [a4];q211 q211;[a4]) by now apply eq_9'.
assert (a4q311: [a4];q311 q311;[a4]) by now apply eq_9'.
assert (p41p11: p41;p11;[a1 !a4 !a1 a4] 0).
eapply same_value. apply frel_comp. reflexivity.
assert (q211q311: q211;q311;[a2 !a3 !a2 a3] 0).
eapply same_value. apply frel_comp. reflexivity.
assert (r12p22: r12;p22;p22;[a1 !a2 !a1 a2] 0).
eapply same_value. simpl bstep. rewrite 2frel_comp. reflexivity. reflexivity.
this one cannot be used by hkat, it's used by rmov1
assert (p13p22: p13;p22 p22;p13) by now apply eq_6'.

here starts the proof; the numbers in the comments refer to the equation numbers in Angus and Kozen's paper proof
(19)
transitivity (
x1;p41;p11;q214;q311;
([!a1 !a4];p11;q214;q311 +
[!a1 a4];p11;q214;q311 +
[ a1 !a4];p13;[!a4];q214;q311 +
[a1 a4];p13;([!a2];p22)^*;[a2 !a3];p41;p11;q214;q311)^*;
[a1];p13;([!a2];p22)^*;[a2 a3 a4];z2).
clear -a4p13 a4p22. hkat.
do 2 rmov1 p13.
(23+)
transitivity (
x1;p41;p11;q214;q311;
([!a1 !a4];p11;q214;q311 +
[!a1 a4];p11;q214;q311 +
[ a1 !a4];p13;[!a4];q214;q311 +
[a1 a4];p13;([!a2];p22)^*;[a2 !a3];p41;p11;q214;q311)^*;
([!a2];p22)^*;[a1 a2 a3 a4];(p13;z2)).
clear -a1p22; hkat.
setoid_replace (p13;z2) with z2
by (unfold z2, clr; mrewrite <-(gc_correct y1); [ simpl gc; kat | reflexivity ]).
(24)
transitivity (x1;p41;p11;q214;q311;
([a1 a4];p13;([!a2];p22)^*;[a2 !a3];p41;p11;q214;q311)^*;
([!a2];p22)^*;[a1 a2 a3 a4];z2).
clear -p41p11 a1p22 a1q214 a1q311 a4p11 a4p13 a4p22 a4q214 a4q311; hkat.
big simplification w.r.t the paper proof here...
(27)
assert (p41p11q214: p41;p11;q214 p41;p11;q211).
change (upd y4 (f' y1) ; upd y1 (f' y1) ; upd y2 (g' y1 y4) upd y4 (f' y1) ; upd y1 (f' y1) ; upd y2 (g' y1 y1)).
now rewrite 3frel_comp.
do 2 mrewrite p41p11q214. clear p41p11q214.
(29)
transitivity (x1;(p41;(p11;q211;q311;[a1];p13;([!a2];p22)^*;[a2 !a3]))^*;
p41;p11;q211;q311;([!a2];p22)^*;[a1 a2 a3];z2).
clear -p41p11 a1p22 a1q211 a1q311 a4p22 a4q211 a4q311; hkat.
(31)
transitivity (x1;(p11;q211;q311;[a1];p13;([!a2];p22)^*;[a2 !a3])^*;
p11;q211;q311;([!a2];p22)^*;[a1 a2 a3];z2).
unfold z2, clr. mrewrite <-(gc_correct y4). 2: reflexivity. simpl gc. kat.
(32)
rmov1 p13.
transitivity ((x1;p11);(q211;q311;([!a2];p22)^*;[a1 a2 !a3];(p13;p11))^*;
q211;q311;([!a2];p22)^*;[a1 a2 a3];z2).
clear -a1p22 a2p13 a3p13; hkat.
big simplification w.r.t the paper proof here...
(33)
setoid_replace (x1;p11) with s1 by apply eq_8.
setoid_replace (p13;p11) with r13 by apply eq_8.
(34)
transitivity (s1;(q211;q311;(([!a2];p22)^*;([a1];r13));[a2 !a3])^*;
q211;q311;([!a2];p22)^*;[a1 a2 a3];z2).
clear -a2r13 a3r13; hkat.
setoid_replace (([!a2];p22)^*;([a1];r13)) with ([a1];r13;([!a2];p22)^*)
by (assert (r13;p22 p22;r13) by (now apply eq_6'); rmov1 r13; clear -a1p22; hkat).
transitivity (s1;([a1];(q211;q311;r13);([!a2];p22)^*;[a2 !a3])^*;
q211;q311;([!a2];p22)^*;[a1 a2 a3];z2).
clear -a1q311 a1q211; hkat.
(35)
setoid_replace (q211;q311;r13) with (q211;q311;r12).
2: change (upd y2 (g' y1 y1) ; upd y3 (g' y1 y1) ; upd y1 (f' (f' y3)) upd y2 (g' y1 y1) ; upd y3 (g' y1 y1) ; upd y1 (f' (f' y2))); now rewrite 3frel_comp.
(36)
transitivity (s1;([a1];(q211;q311);[!a2];r12;([!a2];p22)^*;[a2])^*;
(q211;q311);[a2];([!a2];p22)^*;[a1 a2];z2).
clear -a3p22 a3r12 q211q311. hkat.
(37)
transitivity (s1;([a1];q211;[!a2];r12;([!a2];p22)^*;[a2])^*;
q211;[a2];([!a2];p22)^*;[a1 a2];z2).
unfold z2, clr. mrewrite <-(gc_correct y3). 2: reflexivity. simpl gc. kat.
(38)
transitivity (s1;[a1];q211;([!a2];r12;[a1];p22;[a2];q211 +
[!a2];r12;[a1];p22;[!a2];(p22;q211))^*;[a2];z2).
clear -a1p22 a1q211 a2r12 r12p22 a1p22. hkat.
big simplification w.r.t the paper proof here...
(43)
assert (p22q211: p22;q211 q211) by apply eq_8. rewrite p22q211.
transitivity (s1;[a1];q211;([!a2];r12;[a1];(p22;q211))^*;[a2];z2). kat.
rewrite p22q211. clear p22q211.
(44)
unfold s1, a1, q211, r12, a2. rewrite <-eq_9. mrewrite eq_7. 2: reflexivity.
mrewrite <-eq_9. mrewrite (eq_7 y1 y2 (f' (f' y2))). 2: reflexivity.
unfold z2, clr. mrewrite <-(gc_correct y1). 2: reflexivity.
unfold rhs, z2, clr, s2, a2. rewrite <-eq_9.
unfold q222. mrewrite eq_7. 2: reflexivity.
unfold r22. mrewrite <-eq_9. do 2 mrewrite eq_8.
simpl gc. kat.
(47)
Qed.

End s.