Library semantics3
Definition of the semantics as trajectories (traj_prog).
Definition of the projections of the trajectories (proj_traj_prog).
Require Export prog.
Require Export set.
Require Export set_prog.
Require Import List. Import ListNotations.
Require Export prefix.
Require Import quotient.
Require Import seq.
Require Import control.
Require Import data.
Require Import assert.
Require Import set_relation.
Require Import set_deps.
Require Import set2.
Require Import last_state.
Require Import FunctionalExtensionality.
Definition state := id → nat.
Definition state_eps := option state.
Definition traj := list (label × state_eps).
Definition empty_state : state :=
fun _ ⇒ 0.
Global Opaque empty_state.
Definition update (st : state) (x : id) (n : nat) : state :=
fun x' ⇒ if eq_id_dec x x' then n else st x'.
Theorem update_eq : ∀ n x st,
(update st x n) x = n.
Proof.
intros.
unfold update.
destruct (eq_id_dec x x). reflexivity. contradiction n0; reflexivity.
Qed.
Theorem update_neq : ∀ x2 x1 n st,
x2 ≠ x1 →
(update st x2 n) x1 = (st x1).
Proof.
intros. unfold update.
destruct (eq_id_dec x2 x1).
contradiction.
reflexivity.
Qed.
Theorem update_shadow : ∀ n1 n2 x1 x2 (st : state),
(update (update st x2 n1) x2 n2) x1 = (update st x2 n2) x1.
Proof.
intros.
destruct (eq_id_dec x2 x1).
subst. rewrite update_eq. rewrite update_eq. reflexivity.
rewrite 3!update_neq; try reflexivity; try apply n.
Qed.
Theorem update_same : ∀ n1 x1 x2 (st : state),
st x1 = n1 →
(update st x1 n1) x2 = st x2.
Proof.
intros.
unfold update.
destruct (eq_id_dec x1 x2).
symmetry. rewrite <- e. exact H.
reflexivity.
Qed.
Global Opaque update.
Theorem update_permute : ∀ n1 n2 x1 x2 x3 st,
x2 ≠ x1 →
(update (update st x2 n1) x1 n2) x3 = (update (update st x1 n2) x2 n1) x3.
Proof.
intros.
destruct (eq_id_dec x2 x3).
rewrite e.
rewrite update_neq. rewrite update_eq.
rewrite update_eq. reflexivity.
rewrite <- e. apply not_eq_sym. exact H.
destruct (eq_id_dec x1 x3).
rewrite e. rewrite update_eq.
rewrite update_neq. rewrite update_eq. reflexivity.
exact n.
rewrite 4!update_neq. reflexivity.
exact n0. exact n. exact n. exact n0.
Qed.
Fixpoint aeval (st : state) (a : aexp) : nat :=
match a with
| A_num n ⇒ n
| A_id x ⇒ st x
| A_plus a1 a2 ⇒ (aeval st a1) + (aeval st a2)
| A_minus a1 a2 ⇒ (aeval st a1) - (aeval st a2)
| A_mult a1 a2 ⇒ (aeval st a1) × (aeval st a2)
end.
Fixpoint beval (st : state) (b : bexp) : bool :=
match b with
| B_true ⇒ true
| B_false ⇒ false
| B_eq a1 a2 ⇒ Nat.eqb (aeval st a1) (aeval st a2)
| B_le a1 a2 ⇒ Nat.leb (aeval st a1) (aeval st a2)
| B_not b1 ⇒ negb (beval st b1)
| B_and b1 b2 ⇒ andb (beval st b1) (beval st b2)
end.
Fixpoint traj_prog n ste p :=
match n with
| 0 ⇒ []
| S n' ⇒
match ste with
| Some st ⇒
match p with
| {{}} ⇒ []
| s;;q ⇒
match s with
| SKIP << l >> ⇒ (l, Some st) :: traj_prog n' (Some st) q
| i::=a << l >> ⇒ (l, Some (update st i (aeval st a))) ::
traj_prog n' (Some (update st i (aeval st a))) q
| IFB << l >> b THEN p1 ELSE p2 FI ⇒ (l, Some st) ::
if (beval st b) then traj_prog n' (Some st) (p1+;+q)
else traj_prog n' (Some st) (p2+;+q)
| WHILE << l >> b DO p END ⇒ (l, Some st) ::
if (beval st b) then
traj_prog n' (Some st) (p+;+(WHILE << l >> b DO p END;;q))
else traj_prog n' (Some st) q
| ASSERT << l >> b =>> l' ⇒
if (beval st b) then (l, Some st)::traj_prog n' (Some st) q
else [(l, None)]
end
end
| None ⇒ []
end
end.
Functional Scheme traj_prog_ind :=
Induction for traj_prog Sort Prop.
Lemma traj_prog_length : ∀ n ste p,
length (traj_prog n ste p) ≤ n.
Proof.
intros.
functional induction (traj_prog n ste p); simpl;
try (apply le_n_S; try assumption);
try (apply le_0_n).
Qed.
Lemma traj_prog_prefix : ∀ m ste p n, m ≤ n →
prefix (traj_prog m ste p) (traj_prog n ste p).
Proof.
intros m ste p.
functional induction (traj_prog m ste p); intros;
try (destruct n; [ inversion H |]; simpl; try rewrite e3;
apply prefix_single; try (apply IHl;
apply le_S_n in H; assumption));
try (apply PR_nil).
Qed.
Lemma traj_prog_less_than_length : ∀ n ste p m,
length (traj_prog n ste p) = m →
∀ l, l ≤ m → length (traj_prog l ste p) = l.
Proof.
apply (traj_prog_ind
(fun n ste p tr ⇒ ∀ m, length tr = m → ∀ l, l ≤ m →
length (traj_prog l ste p) = l)); intros;
try (destruct l0; [reflexivity |]; simpl; try rewrite e3; simpl; apply eq_S;
destruct m; [inversion H1 |]; apply H with (m:=m);
[simpl in H0; apply eq_add_S; assumption | apply le_S_n; assumption]).
- simpl in H. subst m. inversion H0. reflexivity.
- simpl in H. subst m. inversion H0. reflexivity.
- destruct l0.
+ reflexivity.
+ simpl in H. subst m. apply le_S_n in H0. inversion H0.
simpl. rewrite e3. reflexivity.
- simpl in H. subst m. inversion H0. reflexivity.
Qed.
Lemma traj_prog_length_not_reached : ∀ m ste p,
length (traj_prog m ste p) < m →
∀ n, m ≤ n → traj_prog n ste p = traj_prog m ste p.
Proof.
intros m ste p H. functional induction (traj_prog m ste p); intros; simpl;
try (destruct n; [ inversion H0 |]; simpl; try rewrite e3;
simpl in H; apply le_S_n in H; apply le_S_n in H0;
try rewrite IHl by assumption; reflexivity).
- inversion H.
Qed.
Lemma traj_prog_app : ∀ n ste p q,
let tr:=traj_prog n ste p in
let ste':=last_state tr ste in
let len:=length tr in
traj_prog n ste (p+;+q) = tr ++
traj_prog (n-len) ste' q.
Proof.
intros n ste p. functional induction (traj_prog n ste p);
intros; try (rewrite last_state_cons_change_default; simpl;
try rewrite e3;
try (specialize (IHl q0); try rewrite <- seq_assoc in IHl; simpl in IHl;
rewrite IHl));
try reflexivity.
- destruct n'; reflexivity.
Qed.
Lemma traj_prog_app_saturate : ∀ n ste p,
length (traj_prog n ste p) = n →
∀ q, traj_prog n ste (p+;+q) = traj_prog n ste p.
Proof.
intros.
rewrite traj_prog_app.
rewrite H. rewrite Nat.sub_diag. simpl. rewrite app_nil_r. reflexivity.
Qed.
Lemma traj_prog_app_last_none : ∀ n ste p,
last_state (traj_prog n ste p) ste = None →
∀ q, traj_prog n ste (p+;+q) = traj_prog n ste p.
Proof.
intros. rewrite traj_prog_app.
rewrite H. destruct (n - _); rewrite app_nil_r; reflexivity.
Qed.
Definition partial_state := id → option nat.
Definition partial_state_eps := option partial_state.
Definition proj_state (st:state) (V:set id) : partial_state :=
fun i ⇒ if set_mem i V then Some (st i) else None.
Definition proj_state_eps (ste:state_eps) V : partial_state_eps :=
match ste with
| Some st ⇒ Some (proj_state st V)
| None ⇒ None
end.
Definition partial_traj := list (label × partial_state_eps).
Fixpoint proj_traj_prog n ste p L : partial_traj :=
match n with
| 0 ⇒ []
| S n' ⇒
match ste with
| Some st ⇒
match p with
| {{}} ⇒ []
| s;;q ⇒
match s with
| SKIP << l >> ⇒
if set_mem l L then (l, Some (proj_state st \emptyset)) ::
proj_traj_prog n' (Some st) q L
else
proj_traj_prog n' (Some st) q L
| i::=a << l >> ⇒
if set_mem l L then
(l, Some (proj_state (update st i (aeval st a))
(set_add i (set_of_id_aexp a)))) ::
proj_traj_prog n' (Some (update st i (aeval st a))) q L
else
proj_traj_prog n' (Some (update st i (aeval st a))) q L
| IFB << l >> b THEN p1 ELSE p2 FI ⇒
if (beval st b) then
if set_mem l L then
(l, Some (proj_state st (set_of_id_bexp b))) ::
proj_traj_prog n' (Some st) (p1+;+q) L
else
proj_traj_prog n' (Some st) (p1+;+q) L
else
if set_mem l L then
(l, Some (proj_state st (set_of_id_bexp b))) ::
proj_traj_prog n' (Some st) (p2+;+q) L
else
proj_traj_prog n' (Some st) (p2+;+q) L
| WHILE << l >> b DO p END ⇒
if (beval st b) then
if set_mem l L then
(l, Some (proj_state st (set_of_id_bexp b))) ::
proj_traj_prog n' (Some st)
(p+;+(WHILE << l >> b DO p END;;q)) L
else
proj_traj_prog n' (Some st)
(p+;+(WHILE << l >> b DO p END;;q)) L
else
if set_mem l L then
(l, Some (proj_state st (set_of_id_bexp b))) ::
proj_traj_prog n' (Some st) q L
else
proj_traj_prog n' (Some st) q L
| ASSERT << l >> b =>> l' ⇒
if (beval st b) then
if set_mem l L then
(l, Some (proj_state st (set_of_id_bexp b))) ::
proj_traj_prog n' (Some st) q L
else
proj_traj_prog n' (Some st) q L
else if set_mem l L then [(l, None)] else []
end
end
| None ⇒ []
end
end.
Functional Scheme proj_traj_prog_ind :=
Induction for proj_traj_prog Sort Prop.
Lemma proj_traj_prog_prefix : ∀ m ste p L n, m ≤ n →
prefix (proj_traj_prog m ste p L)
(proj_traj_prog n ste p L).
Proof.
intros m ste p L.
functional induction (proj_traj_prog m ste p L); intros;
try (destruct n; [ inversion H |]; simpl; rewrite e3; try rewrite e4;
try (apply prefix_single);
try (apply IHp0; apply le_S_n in H; assumption));
try (apply PR_nil).
Qed.
Lemma proj_traj_prog_length : ∀ n ste p L,
length (proj_traj_prog n ste p L) ≤ n.
Proof.
intros. functional induction (proj_traj_prog n ste p L);
try (simpl; try (apply le_n_S); try (apply le_S); try assumption);
try (apply le_0_n).
Qed.
Lemma proj_traj_prog_app : ∀ n ste p L q,
let tr:=traj_prog n ste p in
let ste':=last_state tr ste in
let len:=length tr in
proj_traj_prog n ste (p+;+q) L =
proj_traj_prog n ste p L ++
proj_traj_prog (n-len) ste' q L.
Proof.
intros n ste p L. functional induction (proj_traj_prog n ste p L);
intros; try (rewrite app_prog_cons;
rewrite proj_traj_prog_equation;
try (rewrite <- app_comm_cons);
rewrite (traj_prog_equation _ _ (_;;_));
rewrite e3;
try rewrite e4;
simpl minus; rewrite last_state_cons_change_default;
try (specialize (IHp0 q0); try rewrite <- seq_assoc in IHp0; simpl in IHp0;
rewrite IHp0)); try reflexivity.
- destruct n'; reflexivity.
- destruct n'; reflexivity.
Qed.
Fixpoint flat_state_prog n ste p :=
match n with
| 0 ⇒ {{}}
| S n' ⇒
match ste with
| Some st ⇒
match p with
| {{}} ⇒ {{}}
| s;;q ⇒
match s with
| SKIP << l >> ⇒ SKIP << l >>;; flat_state_prog n' (Some st) q
| i::=a << l >> ⇒ i ::= a << l >>;;
flat_state_prog n' (Some (update st i (aeval st a))) q
| IFB << l >> b THEN p1 ELSE p2 FI ⇒
if (beval st b) then
(ASSERT << l >> b =>> l);;
flat_state_prog n' (Some st) (p1+;+q)
else
(ASSERT << l >> B_not b =>> l);;
flat_state_prog n' (Some st) (p2+;+q)
| WHILE << l >> b DO p END ⇒
if (beval st b) then
(ASSERT << l >> b =>> l);;
flat_state_prog n' (Some st) (p+;+(WHILE << l >> b DO p END;;q))
else
(ASSERT << l >> B_not b =>> l);;
flat_state_prog n' (Some st) q
| ASSERT << l >> b =>> l' ⇒
(ASSERT << l >> b =>> l');;
if (beval st b) then flat_state_prog n' (Some st) q
else {{}}
end
end
| None ⇒ {{}}
end
end.
Functional Scheme flat_state_prog_ind :=
Induction for flat_state_prog Sort Prop.
Lemma flat_state_prog_is_flatR : ∀ n ste p,
is_flatR_prog (flat_state_prog n ste p).
Proof.
intros.
functional induction (flat_state_prog n ste p);
repeat constructor; assumption.
Qed.
Lemma flat_state_prog_traj : ∀ n ste p,
traj_prog n ste p = traj_prog n ste (flat_state_prog n ste p).
Proof.
intros. functional induction (flat_state_prog n ste p);
simpl; try rewrite e3; try rewrite IHp0; try reflexivity.
Qed.
Lemma flat_state_prog_num_lab : ∀ n ste p,
num_lab_prog (flat_state_prog n ste p) ≤ n.
Proof.
intros.
functional induction (flat_state_prog n ste p);
simpl; try (apply le_n_S); try (assumption); try apply le_0_n.
Qed.
Lemma is_flatR_of_prog_one_step : ∀ q p,
(∀ l, is_flatR_of_prog q p →
is_flatR_of_prog (SKIP << l >>;; q) (SKIP << l >>;; p)) ∧
(∀ i a l, is_flatR_of_prog q p →
is_flatR_of_prog (i ::= a << l >>;; q) (i::= a << l >>;; p)) ∧
(∀ l b p1 p2,
is_flatR_of_prog q (p1+;+p) →
is_flatR_of_prog ((ASSERT << l >> b =>> l);; q)
(IFB << l >> b THEN p1 ELSE p2 FI;; p)) ∧
(∀ l b p1 p2,
is_flatR_of_prog q (p2+;+p) →
is_flatR_of_prog ((ASSERT << l >> B_not b =>> l);; q)
(IFB << l >> b THEN p1 ELSE p2 FI;; p)) ∧
(∀ l b p1,
is_flatR_of_prog q (p1+;+(WHILE << l >> b DO p1 END);;p) →
is_flatR_of_prog ((ASSERT << l >> b =>> l);; q)
(WHILE << l >> b DO p1 END;; p)) ∧
(∀ l b p1,
is_flatR_of_prog q p →
is_flatR_of_prog ((ASSERT << l >> B_not b =>> l);; q)
(WHILE << l >> b DO p1 END;; p)) ∧
(∀ l b l',
is_flatR_of_prog q p →
is_flatR_of_prog ((ASSERT << l >> b =>> l');; q)
((ASSERT << l >> b =>> l');; p)).
Proof.
repeat split; intros.
- replace (SKIP << l >>;;q) with ({{SKIP << l >>}}+;+q) by reflexivity.
apply IFOP_cons. constructor. assumption.
- replace (i::= a << l >>;;q) with ({{i ::= a << l >>}}+;+q) by reflexivity.
apply IFOP_cons. constructor. assumption.
- apply is_flatR_of_prog_intro in H. inversion H as [q1 [q2 [H0 [H1 H2]]]].
rewrite H0.
replace ((ASSERT << l >> b =>> l);;q1 +;+ q2)
with (((ASSERT << l >> b =>> l);;q1) +;+ q2) by reflexivity.
apply IFOP_cons. apply IFOS_ifb_l. assumption. assumption.
- apply is_flatR_of_prog_intro in H. inversion H as [q1 [q2 [H0 [H1 H2]]]].
rewrite H0.
replace ((ASSERT << l >> B_not b =>> l);;q1 +;+ q2)
with (((ASSERT << l >> B_not b =>> l);;q1) +;+ q2) by reflexivity.
apply IFOP_cons. apply IFOS_ifb_r. assumption. assumption.
- apply is_flatR_of_prog_intro in H. inversion H as [q1 [q2 [H0 [H1 H2]]]].
inversion H2.
rewrite H0. rewrite <- H5.
replace ((ASSERT << l >> b =>> l);;q1 +;+ p0 +;+ p2)
with (((ASSERT << l >> b =>> l);;q1 +;+ p0) +;+ p2)
by (simpl; rewrite <- seq_assoc; reflexivity).
apply IFOP_cons. apply IFOS_while_loop; assumption. assumption.
- replace ((ASSERT << l >> B_not b =>> l);;q)
with (({{ASSERT << l >> B_not b =>> l}}+;+q)) by reflexivity.
apply IFOP_cons. apply IFOS_while_end. assumption.
- replace ((ASSERT << l >> b =>> l');;q)
with (({{ASSERT << l >> b =>> l'}}+;+q)) by reflexivity.
apply IFOP_cons. apply IFOS_assert. assumption.
Qed.
Lemma flat_state_prog_is_flatR_of_if_terminating_no_error : ∀ n ste p,
length (traj_prog n ste p) < n →
last_state (traj_prog n ste p) ste ≠ None →
is_flatR_of_prog (flat_state_prog n ste p) p.
Proof.
intros. functional induction (traj_prog n ste p);
try (simpl; try rewrite e3; apply is_flatR_of_prog_one_step;
simpl in H; try rewrite e3 in H; apply le_S_n in H;
rewrite last_state_cons_change_default in H0;
apply IHl; assumption).
- inversion H.
- constructor.
- simpl in H0. contradiction H0; reflexivity.
- simpl in H0. contradiction H0. reflexivity.
Qed.
Lemma flat_state_prog_traj_length : ∀ n ste p,
length (traj_prog n ste p) = num_lab_prog (flat_state_prog n ste p).
Proof.
intros. functional induction (flat_state_prog n ste p); simpl;
try rewrite e3; simpl; try (apply f_equal); try assumption; try reflexivity.
Qed.
Lemma flat_state_prog_prefix : ∀ m ste p n, m ≤ n →
prefix_prog (flat_state_prog m ste p) (flat_state_prog n ste p).
Proof.
intros m ste p.
functional induction (flat_state_prog m ste p); intros;
(destruct n; [ inversion H |]); simpl; try rewrite e3;
try apply prefix_prog_single; try (apply IHp0;
apply le_S_n in H; assumption); try apply PP_nil.
Qed.
Lemma flat_state_prog_prefix_is_flatR_of : ∀ n ste p,
∃ q, is_flatR_of_prog q p ∧ prefix_prog (flat_state_prog n ste p) q.
Proof.
intros.
functional induction (flat_state_prog n ste p).
- ∃ (flat_l_prog p). split. apply flat_l_prog_correct. apply PP_nil.
- ∃ {{}}. split; constructor.
- inversion IHp0 as [q0 [H H0]]. ∃ (SKIP << l >>;; q0).
split.
+ replace (SKIP << l >>;; q0)
with ({{SKIP << l >>}} +;+ q0) at 1 by reflexivity. apply IFOP_cons.
constructor. assumption.
+ apply prefix_prog_single. assumption.
- inversion IHp0 as [q0 [H H0]]. ∃ (i ::= a << l >>;; q0).
split.
+ replace (i ::= a << l >>;; q0)
with ({{i ::= a << l >>}} +;+ q0) at 1 by reflexivity. apply IFOP_cons.
constructor. assumption.
+ apply prefix_prog_single. assumption.
- inversion IHp0 as [q0 [H H0]]. ∃ ((ASSERT << l >> b =>> l);; q0).
apply is_flatR_of_prog_intro in H.
inversion H as [q1 [q2 [H1 [H2 H3]]]].
split.
+ rewrite H1. replace ((ASSERT << l >> b =>> l);; q1 +;+ q2)
with (((ASSERT << l >> b =>> l);; q1) +;+ q2) at 1 by reflexivity.
apply IFOP_cons; try constructor; assumption.
+ apply prefix_prog_single. assumption.
- inversion IHp0 as [q0 [H H0]]. ∃ ((ASSERT << l >> B_not b =>> l);; q0).
apply is_flatR_of_prog_intro in H.
inversion H as [q1 [q2 [H1 [H2 H3]]]].
split.
+ rewrite H1. replace ((ASSERT << l >> B_not b =>> l);; q1 +;+ q2)
with (((ASSERT << l >> B_not b =>> l);; q1) +;+ q2) at 1 by reflexivity.
apply IFOP_cons; try constructor; assumption.
+ apply prefix_prog_single. assumption.
- inversion IHp0 as [q0 [H H0]]. ∃ ((ASSERT << l >> b =>> l);; q0).
apply is_flatR_of_prog_intro in H.
inversion H as [q1 [q2 [H1 [H2 H3]]]].
inversion H3.
split.
+ rewrite H1. rewrite <- H6.
replace ((ASSERT << l >> b =>> l);; q1 +;+ p +;+ p1)
with ((((ASSERT << l >> b =>> l);; q1) +;+ p) +;+ p1) at 1.
apply IFOP_cons; try constructor; assumption.
rewrite <- seq_assoc. reflexivity.
+ apply prefix_prog_single. assumption.
- inversion IHp0 as [q0 [H H0]]. ∃ ((ASSERT << l >> B_not b =>> l);; q0).
split.
+ replace ((ASSERT << l >> B_not b =>> l);; q0)
with ({{ASSERT << l >> B_not b =>> l}} +;+ q0) at 1 by reflexivity.
apply IFOP_cons; try constructor; assumption.
+ apply prefix_prog_single. assumption.
- inversion IHp0 as [q0 [H H0]]. ∃ ((ASSERT << l >> b =>> l');; q0).
split.
+ replace ((ASSERT << l >> b =>> l');; q0)
with ({{ASSERT << l >> b =>> l'}} +;+ q0) at 1 by reflexivity.
apply IFOP_cons; try constructor; assumption.
+ apply prefix_prog_single. assumption.
- ∃ ({{ASSERT << l >> b =>> l'}}+;+(flat_l_prog q)). split.
+ apply IFOP_cons. apply IFOS_assert. apply flat_l_prog_correct.
+ simpl. apply PP_after. apply PP_nil.
- ∃ (flat_l_prog p).
split.
+ apply flat_l_prog_correct.
+ apply PP_nil.
Qed.
Lemma is_flatR_prog_traj_length : ∀ n ste p,
is_flatR_prog p →
length (traj_prog n ste p) ≤ num_lab_prog p.
Proof.
intros n ste p H. revert n ste.
induction H; intros; simpl.
- destruct n; destruct ste; apply le_n.
- destruct n.
+ apply le_0_n.
+ destruct ste as [ st |].
× inversion H; simpl; try (destruct (beval st b)); apply le_n_S;
try apply IHis_flatR_prog; try apply le_0_n.
× apply le_0_n.
Qed.
Lemma is_flatR_prog_num_lab_not_reached : ∀ ste p,
is_flatR_prog p →
length (traj_prog (num_lab_prog p) ste p) < num_lab_prog p →
last_state (traj_prog (num_lab_prog p) ste p) ste = None.
Proof.
intros ste p H. revert ste. induction H; intros.
- inversion H.
- inversion H; subst; simpl num_lab_prog;
destruct ste as [ st |]; simpl traj_prog;
simpl in H1; apply le_S_n in H1;
try (destruct (beval st b)); try reflexivity;
rewrite last_state_cons_change_default; apply IHis_flatR_prog; assumption.
Qed.
Lemma traj_prog_three_cases : ∀ n ste p,
length (traj_prog n ste p) = n ∨
length (traj_prog n ste p) < n ∧ last_state (traj_prog n ste p) ste ≠ None ∨
length (traj_prog n ste p) < n ∧ last_state (traj_prog n ste p) ste = None.
Proof.
intros. destruct (Nat.lt_ge_cases (length (traj_prog n ste p)) n).
- right. destruct (last_state (traj_prog n ste p) ste).
+ left. split. assumption. discriminate.
+ right. split. assumption. reflexivity.
- left. apply le_antisym. apply traj_prog_length. assumption.
Qed.
Lemma traj_prog_is_flatR_of : ∀ n ste p,
∃ q, is_flatR_of_prog q p ∧
traj_prog n ste p = traj_prog n ste q.
Proof.
intros. pose proof (flat_state_prog_prefix_is_flatR_of n ste p).
inversion H as [q [H0 H1]].
destruct (traj_prog_three_cases n ste p) as [H2 | [[H2 H3] | [H2 H3]] ].
- ∃ q. split.
+ assumption.
+ apply prefix_prog_intro in H1. inversion H1 as [r H3].
rewrite H3. rewrite traj_prog_app_saturate;
rewrite <- flat_state_prog_traj.
× reflexivity.
× assumption.
- ∃ (flat_state_prog n ste p). split.
+ apply flat_state_prog_is_flatR_of_if_terminating_no_error; assumption.
+ rewrite <- flat_state_prog_traj. reflexivity.
- ∃ q. split.
+ assumption.
+ apply prefix_prog_intro in H1. inversion H1 as [r H4].
rewrite H4. rewrite traj_prog_app_last_none;
rewrite <- flat_state_prog_traj.
× reflexivity.
× assumption.
Qed.
Lemma flat_data_depsR_prog_unrel :
∀ (s : stmt) (i : id) (s' : stmt),
stmt_is_assR_id s i →
¬ stmt_is_assR_id s' i →
∀ (p : prog) (l l' : label),
flat_data_depsR_prog (s;; p) l l' →
flat_data_depsR_prog (s;; s';; p) l l'.
Proof.
intros.
inversion H1; subst.
+ apply FDP_unrel with (i:=i); assumption.
+ apply FDP_unrel with (i:=i); assumption.
+ do 2 apply FDP_after. assumption.
Qed.
Lemma not_id_inR_aexp_update_same_aeval : ∀ a i,
¬ id_inR_aexp a i → ∀ st n,
aeval (update st i n) a = aeval st a.
Proof.
intros.
induction a; simpl.
- reflexivity.
- destruct (eq_id_dec i i0).
+ subst. contradiction H. constructor.
+ rewrite update_neq. reflexivity. assumption.
- rewrite IHa1, IHa2. reflexivity.
intros contra. apply H. apply IIA_plus_r. assumption.
intros contra. apply H. apply IIA_plus_l. assumption.
- rewrite IHa1, IHa2. reflexivity.
intros contra. apply H. apply IIA_minus_r. assumption.
intros contra. apply H. apply IIA_minus_l. assumption.
- rewrite IHa1, IHa2. reflexivity.
intros contra. apply H. apply IIA_mult_r. assumption.
intros contra. apply H. apply IIA_mult_l. assumption.
Qed.
Lemma not_id_inR_bexp_update_same_beval : ∀ b i,
¬ id_inR_bexp b i → ∀ st n,
beval (update st i n) b = beval st b.
Proof.
intros.
induction b; simpl.
- reflexivity.
- reflexivity.
- rewrite 2!not_id_inR_aexp_update_same_aeval. reflexivity.
intros contra. apply H. apply IIB_eq_r. assumption.
intros contra. apply H. apply IIB_eq_l. assumption.
- rewrite 2!not_id_inR_aexp_update_same_aeval. reflexivity.
intros contra. apply H. apply IIB_le_r. assumption.
intros contra. apply H. apply IIB_le_l. assumption.
- rewrite IHb. reflexivity.
intros contra. apply H. apply IIB_not. assumption.
- rewrite IHb1, IHb2. reflexivity.
intros contra. apply H. apply IIB_and_r. assumption.
intros contra. apply H. apply IIB_and_l. assumption.
Qed.
Lemma update_shadow_fun : ∀ n1 n2 st x,
update (update st x n1) x n2 = update st x n2.
Proof.
intros. apply functional_extensionality; intros x'.
rewrite update_shadow. reflexivity.
Qed.
Lemma update_permute_fun : ∀ n1 n2 st x1 x2,
x1 ≠ x2 → update (update st x1 n1) x2 n2 = update (update st x2 n2) x1 n1.
Proof.
intros. apply functional_extensionality; intros x'.
rewrite update_permute by assumption. reflexivity.
Qed.
Lemma proj_state_update_not_in_L_fun : ∀ st i k L,
¬ set_In i L →
proj_state (update st i k) L = proj_state st L.
Proof.
intros. apply functional_extensionality; intros i'.
apply set_mem_complete2 in H.
unfold proj_state.
destruct (set_mem i' L) eqn:Heqmem.
- rewrite update_neq. reflexivity. intros contra; subst. rewrite Heqmem in H.
discriminate H.
- reflexivity.
Qed.
Lemma flat_data_depsR_prog_stable_after : ∀ s p L,
set_stable (flat_data_depsR_prog (s;;p)) L →
set_stable (flat_data_depsR_prog p) L.
Proof.
intros.
unfold set_stable; intros. apply H with (l':=l'); try assumption.
apply FDP_after. assumption.
Qed.
Lemma flat_data_depsR_prog_stable_unrel : ∀ s s' i,
stmt_is_assR_id s i →
¬ stmt_is_assR_id s' i →
∀ (p : prog) L,
set_stable (flat_data_depsR_prog (s;;s';;p)) L →
set_stable (flat_data_depsR_prog (s;;p)) L.
Proof.
intros.
unfold set_stable; intros. apply H1 with (l':=l'); try assumption.
apply flat_data_depsR_prog_unrel with (i:=i); assumption.
Qed.
Lemma ass_not_preserved_proj_equal : ∀ p,
is_flatR_prog p → ∀ i a l L,
set_stable (flat_data_depsR_prog ((i ::= a << l >>);; p)) L →
set_mem l L = false →
∀ n k st,
proj_traj_prog n (Some (update st i k)) (keep_L_prog p L) L =
proj_traj_prog n (Some st) (keep_L_prog p L) L.
Proof.
intros p H. induction H; intros.
- destruct n; reflexivity.
- destruct n.
+ reflexivity.
+ inversion H.
× simpl keep_L_prog. { destruct (set_mem l0 L) eqn:Heqmem.
- simpl. rewrite Heqmem.
rewrite IHis_flatR_prog with (a:=a) (l:=l); try assumption.
reflexivity.
apply flat_data_depsR_prog_stable_unrel with (i:=i) in H1.
assumption. constructor. intros contra; subst s; inversion contra.
- rewrite IHis_flatR_prog with (a:=a) (l:=l); try assumption.
reflexivity.
apply flat_data_depsR_prog_stable_unrel with (i:=i) in H1.
assumption. constructor. intros contra; subst s; inversion contra. }
× simpl keep_L_prog. { destruct (set_mem l0 L) eqn:Heqmem.
- simpl. rewrite Heqmem.
assert (¬ id_inR_aexp a0 i).
{ intros contra. pose proof H1. unfold set_stable in H4.
specialize (H4 l0 (set_mem_correct1 _ _ Heqmem) l).
apply not_true_iff_false in H2. apply H2. apply set_mem_correct2.
apply H4. subst s. apply FDP_here with (i:=i). constructor.
constructor. assumption.
}
rewrite not_id_inR_aexp_update_same_aeval by assumption.
destruct (eq_id_dec i i0).
+ subst i0. rewrite update_shadow_fun. reflexivity.
+ rewrite update_permute_fun by assumption. apply f_equal2.
× do 2 apply f_equal. rewrite proj_state_update_not_in_L_fun.
reflexivity. intros contra. apply set_add_elim in contra.
destruct contra; [| apply set_of_id_aexp_correct in H5];
contradiction.
× rewrite IHis_flatR_prog with (a:=a) (l:=l); try assumption.
reflexivity.
unfold set_stable; intros. apply H1 with (l':=l'); try assumption.
apply flat_data_depsR_prog_unrel with (i:=i). constructor.
intros contra; subst s; inversion contra.
symmetry in H3; contradiction.
assumption.
- destruct (eq_id_dec i i0).
+ subst i0.
rewrite IHis_flatR_prog with (a:=a0) (l:=l0).
reflexivity.
apply flat_data_depsR_prog_stable_after in H1. subst s; assumption.
assumption.
+ rewrite IHis_flatR_prog with (a:=a) (l:=l); try assumption.
reflexivity.
apply flat_data_depsR_prog_stable_unrel with (i:=i) in H1.
assumption. constructor. intros contra; subst s; inversion contra.
symmetry in H3; contradiction. }
× simpl keep_L_prog. { destruct (set_mem l0 L) eqn:Heqmem.
- simpl. rewrite Heqmem.
assert (¬ id_inR_bexp b i).
{ intros contra. pose proof H1. unfold set_stable in H4.
specialize (H4 l0 (set_mem_correct1 _ _ Heqmem) l).
apply not_true_iff_false in H2. apply H2. apply set_mem_correct2.
apply H4. subst s. apply FDP_here with (i:=i). constructor.
constructor. assumption.
}
rewrite not_id_inR_bexp_update_same_beval by assumption.
destruct (beval st b) eqn:Heqbeval.
+ rewrite proj_state_update_not_in_L_fun
by (rewrite set_of_id_bexp_correct; assumption).
rewrite IHis_flatR_prog with (a:=a) (l:=l); try assumption.
reflexivity.
apply flat_data_depsR_prog_stable_unrel with (i:=i) in H1.
assumption. constructor. intros contra; subst s; inversion contra.
+ reflexivity.
- rewrite IHis_flatR_prog with (a:=a) (l:=l); try assumption.
reflexivity.
apply flat_data_depsR_prog_stable_unrel with (i:=i) in H1.
assumption. constructor. intros contra; subst s; inversion contra. }
Qed.
Lemma assert_depsR_prog_stable_after : ∀ s p L,
set_stable (assert_depsR_prog (s;;p)) L →
set_stable (assert_depsR_prog p) L.
Proof.
intros.
unfold set_stable; intros. apply H with (l':=l'); try assumption.
apply ADP_after. assumption.
Qed.
Lemma is_flatR_prog_proj_traj_keep_L_prefix :
∀ p,
is_flatR_prog p → ∀ (L:set label),
set_stable (flat_data_depsR_prog p) L →
∀ n ste q, q = keep_L_prog p L →
prefix (proj_traj_prog n ste p L) (proj_traj_prog n ste q L).
Proof.
intros p H. induction H; intros.
- destruct n; destruct ste; apply PR_nil.
- inversion H; subst.
+ destruct n.
× simpl. apply PR_nil.
× { destruct ste as [ st |].
- destruct (set_mem l L) eqn:Heqmem;
[| apply prefix_trans
with (l2:=(proj_traj_prog n (Some st) (keep_L_prog p L) L));
[| simpl keep_L_prog; rewrite Heqmem; apply proj_traj_prog_prefix;
apply le_S; apply le_n ] ];
simpl; rewrite 2?Heqmem; try apply prefix_single;
(apply IHis_flatR_prog; try reflexivity;
try apply flat_data_depsR_prog_stable_after in H1; assumption).
- apply PR_nil. }
+ destruct n.
× simpl. apply PR_nil.
× { destruct ste as [ st |].
- destruct (set_mem l L) eqn:Heqmem.
+ simpl; rewrite 2!Heqmem. apply prefix_single.
apply IHis_flatR_prog; try reflexivity.
× apply flat_data_depsR_prog_stable_after in H1; assumption.
+ simpl proj_traj_prog at 1. simpl keep_L_prog. rewrite Heqmem.
apply prefix_trans
with (l2:=(proj_traj_prog n (Some (update st i (aeval st a)))
(keep_L_prog p L) L)).
apply IHis_flatR_prog; try reflexivity.
× apply flat_data_depsR_prog_stable_after in H1. assumption.
× rewrite ass_not_preserved_proj_equal with (a:=a) (l:=l)
by assumption.
apply proj_traj_prog_prefix. apply le_S; apply le_n.
- apply PR_nil. }
+ destruct n.
× simpl. apply PR_nil.
× { destruct ste as [ st |].
- destruct (set_mem l L) eqn:Heqmem.
+ simpl; rewrite 2!Heqmem.
destruct (beval st b).
× apply prefix_single. { apply IHis_flatR_prog; try reflexivity.
- apply flat_data_depsR_prog_stable_after in H1; assumption. }
× apply prefix_refl.
+ simpl proj_traj_prog at 1. simpl keep_L_prog.
rewrite Heqmem.
destruct (beval st b).
× { apply prefix_trans
with (l2:=(proj_traj_prog n (Some st) (keep_L_prog p L) L)).
- apply IHis_flatR_prog; try reflexivity.
+ apply flat_data_depsR_prog_stable_after in H1. assumption.
- apply proj_traj_prog_prefix. apply le_S; apply le_n. }
× apply PR_nil.
- apply PR_nil. }
Qed.
Lemma flat_state_prog_proj_traj :
∀ (n : nat) (ste : option state) (p : prog) L,
proj_traj_prog n ste p L = proj_traj_prog n ste (flat_state_prog n ste p) L.
Proof.
intros. functional induction (proj_traj_prog n ste p L);
repeat (simpl || rewrite e3 || rewrite e4 || rewrite IHp0); reflexivity.
Qed.
Lemma flat_data_depsR_prog_prefix :
∀ p q, prefix_prog p q →
∀ l l', flat_data_depsR_prog p l l' → flat_data_depsR_prog q l l'.
Proof.
intros p q Hprefix. intros. revert q Hprefix.
induction H; intros; apply prefix_prog_intro in Hprefix;
inversion Hprefix as [r Hprefix']; rewrite Hprefix'; simpl in ×.
- apply FDP_here with (i:=i); assumption.
- apply FDP_unrel with (i:=i); try assumption.
apply IHflat_data_depsR_prog. apply prefix_prog_single.
apply prefix_prog_app.
- apply FDP_after. apply IHflat_data_depsR_prog. apply prefix_prog_app.
Qed.
Lemma flat_data_depsR_prog_stable_prefix :
∀ p q, prefix_prog p q →
∀ L,
set_stable (flat_data_depsR_prog q) L →
set_stable (flat_data_depsR_prog p) L.
Proof.
intros. unfold set_stable; intros. apply H0 with (l':=l'); try assumption.
apply flat_data_depsR_prog_prefix with (p:=p); assumption.
Qed.
Lemma keep_L_prog_app : ∀ q1 q2 L,
keep_L_prog (q1+;+q2) L = (keep_L_prog q1 L) +;+ (keep_L_prog q2 L).
Proof.
intros. induction q1.
- simpl. reflexivity.
- simpl. destruct (set_mem (stmt_get_label s) L).
+ simpl. rewrite IHq1. reflexivity.
+ assumption.
Qed.
Lemma stable_inclusion_stable : ∀ `{DS:DecidableType}
(d1 d2:relation A) (x:set A),
inclusion A d1 d2 → set_stable d2 x → set_stable d1 x.
Proof.
intros.
unfold set_stable; intros.
apply H0 in H1. apply H1. apply H. assumption.
Qed.
Lemma label_first_inR_prog_quotient_include : ∀ p q,
is_quotientR_prog p q → ∀ l,
label_first_inR_prog q l → label_first_inR_prog p l.
Proof.
intros. induction H.
- inversion H0.
- apply LFP_after. apply IHis_quotientR_prog; assumption.
- inversion H0.
+ inversion H1; subst; simpl; apply LFP_here.
+ apply LFP_after. apply IHis_quotientR_prog; assumption.
Qed.
Lemma control_depsR_prog_quotient_include : ∀ p q,
is_quotientR_prog p q →
inclusion label (control_depsR_prog q) (control_depsR_prog p).
Proof.
intros. unfold inclusion. revert p q H.
apply (is_quotientR_prog_mutual_ind
(fun p q H ⇒ ∀ x y, control_depsR_prog q x y →
control_depsR_prog p x y)
(fun s t H ⇒ ∀ x y, control_depsR_stmt t x y →
control_depsR_stmt s x y)); intros.
- inversion H.
- apply CDP_after. apply H; assumption.
- inversion H1.
+ apply CDP_here. apply H0; assumption.
+ apply CDP_after. apply H; assumption.
- assumption.
- assumption.
- inversion H1; subst.
+ apply CDS_ifb_l. apply H; assumption.
+ apply CDS_ifb_r. apply H0; assumption.
+ apply CDS_ifb_cond_l.
apply label_first_inR_prog_quotient_include with (q:=q1); assumption.
+ apply CDS_ifb_cond_r.
apply label_first_inR_prog_quotient_include with (q:=q2); assumption.
- inversion H0; subst.
+ apply CDS_while. apply H; assumption.
+ apply CDS_while_cond.
apply label_first_inR_prog_quotient_include with (q:=q); assumption.
- assumption.
Qed.
Lemma control_depsR_prog_stable_quotient : ∀ p q,
is_quotientR_prog p q → ∀ L,
set_stable (control_depsR_prog p) L →
set_stable (control_depsR_prog q) L.
Proof.
intros.
apply stable_inclusion_stable with (d2:=control_depsR_prog p).
apply control_depsR_prog_quotient_include. assumption. assumption.
Qed.
Lemma control_depsR_prog_stable_unrel : ∀ p s s' L,
set_stable (control_depsR_prog (s;;s';;p)) L →
set_stable (control_depsR_prog (s;;p)) L.
Proof.
intros. apply control_depsR_prog_stable_quotient with (p:=s;;s';;p).
apply IQP_stmt. apply IQP_remove. apply is_quotientR_refl.
apply is_quotientR_prog_single. apply is_quotientR_refl.
assumption.
Qed.
Lemma control_depsR_prog_stable_cons : ∀ s q L,
set_stable (control_depsR_prog (s;; q)) L →
set_stable (control_depsR_stmt s) L ∧
set_stable (control_depsR_prog q) L.
Proof.
unfold set_stable; split; intros;
(apply H with (l':=l'); [assumption|]).
- apply CDP_here. assumption.
- apply CDP_after. assumption.
Qed.
Lemma control_depsR_prog_stable_cons_reverse : ∀ s q L,
set_stable (control_depsR_stmt s) L ∧
set_stable (control_depsR_prog q) L →
set_stable (control_depsR_prog (s;; q)) L.
Proof.
unfold set_stable; intros.
inversion H1; apply H in H6; assumption.
Qed.
Lemma control_depsR_prog_stable_app : ∀ q1 q2 L,
set_stable (control_depsR_prog (q1+;+q2)) L ↔
set_stable (control_depsR_prog q1) L ∧
set_stable (control_depsR_prog q2) L.
Proof.
intros. induction q1; split; simpl; intros.
- split.
+ unfold set_stable. intros. inversion H1.
+ assumption.
- apply H.
- split.
+ apply control_depsR_prog_stable_cons_reverse.
apply control_depsR_prog_stable_cons in H.
split.
× apply H.
× apply IHq1; apply H.
+ apply control_depsR_prog_stable_cons in H.
apply IHq1; apply H.
- destruct H.
apply control_depsR_prog_stable_cons_reverse.
apply control_depsR_prog_stable_cons in H.
split.
+ apply H.
+ apply IHq1. split. apply H. apply H0.
Qed.
Lemma assert_depsR_prog_stable_cons : ∀ s q L,
set_stable (assert_depsR_prog (s;;q)) L ↔
set_stable (assert_depsR_stmt s) L ∧
set_stable (assert_depsR_prog q) L.
Proof.
split; intros.
- split; unfold set_stable in *; intros.
+ apply H with (l':=l'). assumption. apply ADP_here. assumption.
+ apply H with (l':=l'). assumption. apply ADP_after. assumption.
- destruct H. unfold set_stable in *; intros.
inversion H2.
+ apply H with (l':=l'); assumption.
+ apply H0 with (l':=l'); assumption.
Qed.
Lemma assert_depsR_prog_stable_app : ∀ q1 q2 L,
set_stable (assert_depsR_prog (q1+;+q2)) L ↔
set_stable (assert_depsR_prog q1) L ∧
set_stable (assert_depsR_prog q2) L.
Proof.
split; intros.
- induction q1.
+ simpl in H. split.
× unfold set_stable; intros. inversion H1.
× assumption.
+ simpl in H. apply assert_depsR_prog_stable_cons in H. split.
× apply assert_depsR_prog_stable_cons.
split; [apply H | apply IHq1; apply H].
× apply IHq1; apply H.
- induction q1.
+ simpl. apply H.
+ destruct H. apply assert_depsR_prog_stable_cons in H.
simpl. apply assert_depsR_prog_stable_cons.
split.
× apply H.
× apply IHq1. split; [apply H | apply H0].
Qed.
Lemma stmt_is_assR_id_in : ∀ s i,
stmt_is_assR_id s i → ass_inR_stmt s i.
Proof.
intros. inversion H.
constructor.
Qed.
Lemma flat_data_depsR_prog_app_unrel :
∀ (s : stmt) (i : id) (q : prog),
stmt_is_assR_id s i →
¬ ass_inR_prog q i →
∀ (p : prog) (l l' : label),
flat_data_depsR_prog (s;; p) l l' →
flat_data_depsR_prog (s;;q+;+ p) l l'.
Proof.
intros.
induction q.
- assumption.
- simpl. apply flat_data_depsR_prog_unrel with (i:=i).
× assumption.
× intros contra. apply H0. apply AIP_here.
apply stmt_is_assR_id_in. assumption.
× apply IHq. intros contra. apply H0. apply AIP_after. assumption.
Qed.
Lemma ass_inR_prog_app : ∀ p1 p2 i,
ass_inR_prog (p1+;+p2) i ↔ ass_inR_prog p1 i ∨ ass_inR_prog p2 i.
Proof.
split; intros.
- induction p1.
+ right; assumption.
+ inversion H.
× left. apply AIP_here; assumption.
× apply IHp1 in H3. { destruct H3.
- left. apply AIP_after; assumption.
- right. assumption. }
- induction p1.
+ destruct H.
× inversion H.
× assumption.
+ destruct H.
× { inversion H.
- apply AIP_here. assumption.
- simpl. apply AIP_after. apply IHp1. left; assumption. }
× simpl. apply AIP_after. apply IHp1. right; assumption.
Qed.
Lemma ass_inR_prog_single : ∀ s i,
ass_inR_prog {{s}} i ↔ ass_inR_stmt s i.
Proof.
split; intros.
- inversion H.
× assumption.
× inversion H3.
- apply AIP_here. assumption.
Qed.
Lemma ass_not_inR_prog_is_flat_of : ∀ q p,
is_flatR_of_prog q p →
∀ i, ¬ ass_inR_prog p i →
¬ ass_inR_prog q i.
Proof.
apply (is_flatR_of_prog_mutual_ind
(fun q p H ⇒ ∀ i, ¬ ass_inR_prog p i →
¬ ass_inR_prog q i)
(fun q s H ⇒ ∀ i, ¬ ass_inR_stmt s i →
¬ ass_inR_prog q i)); intros.
- assumption.
- intros contra. apply ass_inR_prog_app in contra.
assert (¬ ass_inR_stmt s i1).
{ intros contra2. apply H1. apply AIP_here; assumption. }
assert (¬ ass_inR_prog p1' i1).
{ intros contra2. apply H1. apply AIP_after; assumption. }
specialize (H i1 H2).
specialize (H0 i1 H3).
destruct contra; contradiction.
- rewrite ass_inR_prog_single. assumption.
- rewrite ass_inR_prog_single. assumption.
- intros contra.
inversion contra. inversion H4.
assert (¬ ass_inR_prog p1 i0).
{ intros contra2. apply H0. apply AIS_ifb_l. assumption. }
apply H in H5. contradiction.
- intros contra.
inversion contra. inversion H4.
assert (¬ ass_inR_prog p2 i0).
{ intros contra2. apply H0. apply AIS_ifb_r. assumption. }
apply H in H5. contradiction.
- intros contra.
inversion contra. inversion H5.
assert (¬ ass_inR_prog p i1).
{ intros contra2. apply H1. apply AIS_while. assumption. }
apply H0 in H6. apply H in H1.
apply ass_inR_prog_app in H5. destruct H5; contradiction.
- rewrite ass_inR_prog_single. intros contra. inversion contra.
- rewrite ass_inR_prog_single. assumption.
Qed.
Lemma data_depsR_prog_unrel :
∀ (s : stmt) (i : id) (s' : stmt),
stmt_is_assR_id s i →
¬ ass_inR_stmt s' i →
∀ (p : prog) (l l' : label),
data_depsR_prog (s;; p) l l' →
data_depsR_prog (s;; s';; p) l l'.
Proof.
intros. inversion H1.
inversion H2. subst p0.
inversion H; subst. inversion H10; subst.
apply DDP_flat with (p:=(i::=a <<l1>>);;(flat_l_stmt s')+;+p2).
apply is_flatR_of_prog_one_step.
apply IFOP_cons. apply flat_l_stmt_correct. assumption.
apply flat_data_depsR_prog_app_unrel with (i:=i). constructor.
apply ass_not_inR_prog_is_flat_of with (p:={{s'}}).
apply is_flatR_of_prog_single. apply flat_l_stmt_correct.
rewrite ass_inR_prog_single. assumption.
assumption.
Qed.
Lemma data_depsR_prog_stable_unrel : ∀ s s' i,
stmt_is_assR_id s i →
¬ ass_inR_stmt s' i →
∀ (p : prog) L,
set_stable (data_depsR_prog (s;;s';;p)) L →
set_stable (data_depsR_prog (s;;p)) L.
Proof.
intros.
unfold set_stable; intros. apply H1 with (l':=l'); try assumption.
apply data_depsR_prog_unrel with (i:=i); assumption.
Qed.
Lemma data_depsR_prog_stable_after :
∀ (s : stmt) (p : prog) (L : set label),
set_stable (data_depsR_prog (s;; p)) L →
set_stable (data_depsR_prog p) L.
Proof.
intros.
unfold set_stable; intros. apply H with (l':=l'); try assumption.
apply data_depsR_prog_after. assumption.
Qed.
Lemma id_not_in_mayread_prog_update : ∀ p i,
¬ i \in set_map fst (mayread_prog p) →
∀ n st k L,
proj_traj_prog n (Some (update st i k)) p L =
proj_traj_prog n (Some st) p L.
Proof.
intros p i H n st k L. remember (Some st) as ste. revert i H k st Heqste.
functional induction (traj_prog n ste p); intros; inversion Heqste; subst.
- reflexivity.
- reflexivity.
- simpl. rewrite IHl; try reflexivity.
simpl in H. rewrite set2_diff_fst_emptyset_r in H.
rewrite set_same_union_empty_l in H.
assumption.
- simpl.
assert (¬ id_inR_aexp a i0).
{ intros contra. apply H. rewrite set_map_In. ∃ (i0, l).
rewrite mayread_prog_equation.
split; try reflexivity.
rewrite set_union_In. left. simpl.
rewrite set_map_In. ∃ i0.
rewrite set_of_id_aexp_correct. split; try assumption; try reflexivity.
}
rewrite not_id_inR_aexp_update_same_aeval by assumption.
destruct (eq_id_dec i0 i).
+ subst i0. rewrite update_shadow_fun. reflexivity.
+ rewrite update_permute_fun by assumption. rewrite IHl; try reflexivity.
× { rewrite proj_state_update_not_in_L_fun.
- reflexivity.
- intros contra.
apply set_add_elim in contra. rewrite set_of_id_aexp_correct in contra.
destruct contra; contradiction. }
× intros contra. apply H. rewrite set_map_In in contra.
destruct contra as [(i1, l1) [H1 H2]].
rewrite set_map_In. ∃ (i0, l1).
split; try reflexivity.
rewrite mayread_prog_equation. rewrite set_union_In.
right. rewrite set2_diff_fst_In.
split.
simpl in H2; subst i1; assumption.
simpl. rewrite set_singleton_In. assumption.
- simpl.
assert (¬ id_inR_bexp b i).
{ intros contra. apply H. rewrite set_map_In. ∃ (i, l).
rewrite mayread_prog_equation.
split; try reflexivity.
rewrite set_union_In. left. simpl. rewrite set_union_In. left.
rewrite set_map_In. ∃ i. rewrite set_of_id_bexp_correct.
split; try assumption; try reflexivity.
}
rewrite not_id_inR_bexp_update_same_beval by assumption.
rewrite proj_state_update_not_in_L_fun by (rewrite set_of_id_bexp_correct; assumption).
rewrite e3.
rewrite IHl; try reflexivity.
+ intros contra. rewrite mayread_prog_seq in contra.
apply H. rewrite set_map_In in contra.
destruct contra as [(i0, l0) [H1 H2]].
rewrite set_map_In. ∃ (i, l0).
split; try reflexivity.
rewrite mayread_prog_equation. rewrite set_union_In in H1.
simpl in H2; subst i0.
rewrite set_union_In. destruct H1.
× left. simpl. rewrite 2!set_union_In. right; left. assumption.
× right. simpl. rewrite set2_diff_fst_inter_distr_r.
rewrite set_union_In. left; assumption.
- simpl.
assert (¬ id_inR_bexp b i).
{ intros contra. apply H. rewrite set_map_In. ∃ (i, l).
rewrite mayread_prog_equation.
split; try reflexivity.
rewrite set_union_In. left. simpl. rewrite set_union_In. left.
rewrite set_map_In. ∃ i. rewrite set_of_id_bexp_correct.
split; try assumption; try reflexivity.
}
rewrite not_id_inR_bexp_update_same_beval by assumption.
rewrite proj_state_update_not_in_L_fun by (rewrite set_of_id_bexp_correct; assumption).
rewrite e3.
rewrite IHl; try reflexivity.
+ intros contra. rewrite mayread_prog_seq in contra.
apply H. rewrite set_map_In in contra.
destruct contra as [(i0, l0) [H1 H2]].
rewrite set_map_In. ∃ (i, l0).
split; try reflexivity.
rewrite mayread_prog_equation. rewrite set_union_In in H1.
simpl in H2; subst i0.
rewrite set_union_In. destruct H1.
× left. simpl. rewrite 2!set_union_In. right; right. assumption.
× right. simpl. rewrite set2_diff_fst_inter_distr_r.
rewrite set_union_In. right; assumption.
- simpl.
assert (¬ id_inR_bexp b i).
{ intros contra. apply H. rewrite set_map_In. ∃ (i, l).
rewrite mayread_prog_equation.
split; try reflexivity.
rewrite set_union_In. left. simpl. rewrite set_union_In. left.
rewrite set_map_In. ∃ i. rewrite set_of_id_bexp_correct.
split; try assumption; try reflexivity.
}
rewrite not_id_inR_bexp_update_same_beval by assumption.
rewrite proj_state_update_not_in_L_fun by (rewrite set_of_id_bexp_correct; assumption).
rewrite e3.
rewrite IHl; try reflexivity.
+ intros contra. rewrite mayread_prog_seq in contra.
apply H. rewrite set_map_In in contra.
destruct contra as [(i0, l0) [H1 H2]].
rewrite set_map_In. ∃ (i, l0).
split; try reflexivity.
rewrite mayread_prog_equation. simpl mustdef_stmt. rewrite set2_diff_fst_emptyset_r.
simpl in H2; subst i0.
rewrite set_union_In. rewrite set_union_In in H1. destruct H1.
× left. simpl. rewrite set_union_In. right. assumption.
× rewrite mayread_prog_equation in H1. simpl mustdef_stmt in H1.
rewrite set2_diff_fst_emptyset_r in H1.
rewrite set2_diff_fst_union_distr_l in H1.
rewrite set_union_In in H1. rewrite 2!set2_diff_fst_In in H1.
{ destruct H1.
- left; apply H1.
- right; apply H1. }
- simpl.
assert (¬ id_inR_bexp b i).
{ intros contra. apply H. rewrite set_map_In. ∃ (i, l).
rewrite mayread_prog_equation.
split; try reflexivity.
rewrite set_union_In. left. simpl. rewrite set_union_In. left.
rewrite set_map_In. ∃ i. rewrite set_of_id_bexp_correct.
split; try assumption; try reflexivity.
}
rewrite not_id_inR_bexp_update_same_beval by assumption.
rewrite proj_state_update_not_in_L_fun by (rewrite set_of_id_bexp_correct; assumption).
rewrite e3.
rewrite IHl; try reflexivity.
intros contra. apply H. rewrite set_map_In in contra.
destruct contra as [(i0, l0) [H1 H2]].
rewrite set_map_In. ∃ (i, l0).
split; try reflexivity.
rewrite mayread_prog_equation. rewrite set_union_In. right.
simpl. rewrite set2_diff_fst_emptyset_r. simpl in H2; subst i0. assumption.
- simpl.
assert (¬ id_inR_bexp b i).
{ intros contra. apply H. rewrite set_map_In. ∃ (i, l).
rewrite mayread_prog_equation.
split; try reflexivity.
rewrite set_union_In. left. simpl.
rewrite set_map_In. ∃ i. rewrite set_of_id_bexp_correct.
split; try assumption; try reflexivity.
}
rewrite not_id_inR_bexp_update_same_beval by assumption.
rewrite proj_state_update_not_in_L_fun by (rewrite set_of_id_bexp_correct; assumption).
rewrite e3.
rewrite IHl; try reflexivity.
intros contra. apply H. rewrite set_map_In in contra.
destruct contra as [(i0, l0) [H1 H2]].
simpl in H2; subst i0.
rewrite set_map_In. ∃ (i, l0).
split; try reflexivity.
rewrite mayread_prog_equation.
rewrite set_union_In. right. simpl. rewrite set2_diff_fst_emptyset_r.
assumption.
- simpl.
assert (¬ id_inR_bexp b i).
{ intros contra. apply H. rewrite set_map_In. ∃ (i, l).
rewrite mayread_prog_equation.
split; try reflexivity.
rewrite set_union_In. left. simpl.
rewrite set_map_In. ∃ i. rewrite set_of_id_bexp_correct.
split; try assumption; try reflexivity.
}
rewrite not_id_inR_bexp_update_same_beval by assumption.
rewrite proj_state_update_not_in_L_fun by (rewrite set_of_id_bexp_correct; assumption).
rewrite e3. reflexivity.
Qed.
Lemma is_flatR_prog_no_control : ∀ q,
is_flatR_prog q → ∀ l l',
¬ control_depsR_prog q l l'.
Proof.
intros. induction H.
- intros contra; inversion contra.
- intros contra. inversion contra.
+ inversion H; subst; inversion H5.
+ contradiction.
Qed.
Lemma set_of_labels_prog_empty_nil : ∀ p,
set_same (set_of_labels_prog p) empty_set ↔ p = {{}}.
Proof.
split; intros.
- destruct p. reflexivity.
simpl in H.
assert(set_In (stmt_get_label s) (set_union (set_of_labels_stmt s)
(set_of_labels_prog p))).
replace (set_of_labels_stmt s) with (set_of_labels_prog {{s}}) by reflexivity.
apply set_union_intro. left.
apply label_inR_prog_iff_in_set_of_labels.
apply LIP_here. apply stmt_get_label_in_stmt.
apply H in H0. inversion H0.
- subst; simpl. apply set_same_refl.
Qed.
Lemma keep_L_prog_nil_flat_nil : ∀ p L,
set_stable (control_depsR_prog p) L →
keep_L_prog p L = {{ }} →
∀ q, is_flatR_of_prog q p → keep_L_prog q L = {{}}.
Proof.
intros.
assert(set_same (set_of_labels_prog (keep_L_prog q L)) empty_set).
{
rewrite keep_L_prog_label with (d:=control_depsR_prog p).
split.
apply set_incl_trans with (y:=set_inter (set_of_labels_prog p) L).
apply set_incl_inter. apply set_inter_incl.
unfold set_incl; intros. apply label_inR_prog_iff_in_set_of_labels.
apply is_flatR_of_prog_label with (p1:=q). assumption.
apply label_inR_prog_iff_in_set_of_labels. assumption.
rewrite set_inter_comm. apply set_inter_incl. apply set_incl_refl.
rewrite <- keep_L_prog_label with (d:=control_depsR_prog p).
rewrite H0. simpl. apply set_incl_refl.
assumption. unfold inclusion; intros. assumption.
unfold set_incl; intros. inversion H2.
assumption. unfold inclusion; intros. apply is_flatR_prog_no_control in H2.
inversion H2. apply is_flatR_of_prog_is_flatR with (p:=p). assumption.
}
apply set_of_labels_prog_empty_nil in H2. assumption.
Qed.
Lemma ifb_not_preserved_stable_not_preserved_l : ∀ l b p1 p2 L,
set_mem l L = false →
set_stable (control_depsR_stmt (IFB << l >> b THEN p1 ELSE p2 FI)) L →
keep_L_prog p1 L = {{}}.
Proof.
intros.
destruct (keep_L_prog p1 L) eqn:Heqkeep.
+ reflexivity.
+ assert (label_first_inR_prog (keep_L_prog p1 L) (stmt_get_label s)).
{ rewrite Heqkeep. apply LFP_here. }
apply label_first_inR_prog_quotient_include with (p:=p1) in H1.
unfold set_stable in H0.
assert (control_depsR_stmt (IFB << l >> b THEN p1 ELSE p2 FI) l (stmt_get_label s)).
{ apply CDS_ifb_cond_l. assumption. }
apply H0 in H2.
apply set_mem_complete1 in H. contradiction.
assert (set_same (set_of_labels_prog (keep_L_prog p1 L))
(set_inter (set_of_labels_prog p1) L)).
{ apply (keep_L_prog_label p1 L
(control_depsR_prog {{IFB << l >> b THEN p1 ELSE p2 FI}})).
unfold set_stable. intros. apply H0 with (l':=l').
assumption. inversion H4. assumption. inversion H9.
unfold inclusion. intros. apply CDP_here. apply CDS_ifb_l. assumption.
}
apply (set_inter_elim (stmt_get_label s) (set_of_labels_prog p1) L).
apply H3. rewrite Heqkeep. simpl.
apply set_union_intro. left.
replace (set_of_labels_stmt s) with (set_of_labels_prog {{s}}) by reflexivity.
apply label_inR_prog_iff_in_set_of_labels. apply LIP_here. apply stmt_get_label_in_stmt.
apply keep_L_prog_quotient.
Qed.
Lemma ifb_not_preserved_stable_not_preserved_r : ∀ l b p1 p2 L,
set_mem l L = false →
set_stable (control_depsR_stmt (IFB << l >> b THEN p1 ELSE p2 FI)) L →
keep_L_prog p2 L = {{}}.
Proof.
intros.
destruct (keep_L_prog p2 L) eqn:Heqkeep.
+ reflexivity.
+ assert (label_first_inR_prog (keep_L_prog p2 L) (stmt_get_label s)).
{ rewrite Heqkeep. apply LFP_here. }
apply label_first_inR_prog_quotient_include with (p:=p2) in H1.
unfold set_stable in H0.
assert (control_depsR_stmt (IFB << l >> b THEN p1 ELSE p2 FI) l (stmt_get_label s)).
{ apply CDS_ifb_cond_r. assumption. }
apply H0 in H2.
apply set_mem_complete1 in H. contradiction.
assert (set_same (set_of_labels_prog (keep_L_prog p2 L))
(set_inter (set_of_labels_prog p2) L)).
{ apply (keep_L_prog_label p2 L
(control_depsR_prog {{IFB << l >> b THEN p1 ELSE p2 FI}})).
unfold set_stable. intros. apply H0 with (l':=l').
assumption. inversion H4. assumption. inversion H9.
unfold inclusion. intros. apply CDP_here. apply CDS_ifb_r. assumption.
}
apply (set_inter_elim (stmt_get_label s) (set_of_labels_prog p2) L).
apply H3. rewrite Heqkeep. simpl.
apply set_union_intro. left.
replace (set_of_labels_stmt s) with (set_of_labels_prog {{s}}) by reflexivity.
apply label_inR_prog_iff_in_set_of_labels. apply LIP_here. apply stmt_get_label_in_stmt.
apply keep_L_prog_quotient.
Qed.
Lemma while_not_preserved_stable_not_preserved : ∀ l b p L,
set_mem l L = false →
set_stable (control_depsR_stmt (WHILE << l >> b DO p END)) L →
keep_L_prog p L = {{}}.
Proof.
intros.
destruct (keep_L_prog p L) eqn:Heqkeep.
+ reflexivity.
+ assert (label_first_inR_prog (keep_L_prog p L) (stmt_get_label s)).
{ rewrite Heqkeep. apply LFP_here. }
apply label_first_inR_prog_quotient_include with (p:=p) in H1.
unfold set_stable in H0.
assert (control_depsR_stmt (WHILE << l >> b DO p END) l (stmt_get_label s)).
{ apply CDS_while_cond. assumption. }
apply H0 in H2.
apply set_mem_complete1 in H. contradiction.
assert (set_same (set_of_labels_prog (keep_L_prog p L))
(set_inter (set_of_labels_prog p) L)).
{ apply (keep_L_prog_label p L (control_depsR_prog {{WHILE << l >> b DO p END}})).
unfold set_stable. intros. apply H0 with (l':=l').
assumption. inversion H4. assumption. inversion H9.
unfold inclusion. intros. apply CDP_here. apply CDS_while. assumption.
}
apply (set_inter_elim (stmt_get_label s) (set_of_labels_prog p) L).
apply H3. rewrite Heqkeep. simpl.
apply set_union_intro. left.
replace (set_of_labels_stmt s) with (set_of_labels_prog {{s}}) by reflexivity.
apply label_inR_prog_iff_in_set_of_labels. apply LIP_here. apply stmt_get_label_in_stmt.
apply keep_L_prog_quotient.
Qed.
Lemma keep_L_prog_flat : ∀ q p,
is_flatR_of_prog q p →
∀ L,
set_stable (control_depsR_prog p) L →
is_flatR_of_prog (keep_L_prog q L) (keep_L_prog p L).
Proof.
apply (is_flatR_of_prog_mutual_ind
(fun q p H ⇒ ∀ L, set_stable (control_depsR_prog p) L →
is_flatR_of_prog (keep_L_prog q L) (keep_L_prog p L))
(fun q s H ⇒ ∀ L, set_stable (control_depsR_stmt s) L →
is_flatR_of_prog (keep_L_prog q L) (keep_L_prog {{s}} L)));
intros.
- apply IFOP_nil.
- apply control_depsR_prog_stable_cons in H1.
rewrite keep_L_prog_app. simpl.
destruct (set_mem (stmt_get_label s) L) eqn:Heqmem.
+ apply IFOP_cons. apply is_flatR_of_prog_single.
replace {{keep_L_stmt s L}} with (keep_L_prog {{s}} L).
apply H. apply H1. simpl. rewrite Heqmem; reflexivity. apply H0. apply H1.
+ rewrite keep_L_prog_nil_flat_nil with (p:={{s}}).
apply H0. apply H1. apply control_depsR_prog_stable_cons_reverse.
split. apply H1. unfold set_stable. intros. inversion H3.
simpl. rewrite Heqmem. reflexivity. apply is_flatR_of_prog_single.
assumption.
- simpl. destruct (set_mem l L).
+ apply is_flatR_of_prog_single. constructor.
+ constructor.
- simpl. destruct (set_mem l L).
+ apply is_flatR_of_prog_single. constructor.
+ constructor.
- assert (set_stable (control_depsR_prog p1) L).
{ unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
assumption. apply CDS_ifb_l. assumption. }
simpl. destruct (set_mem l L) eqn:Heqmem.
+ apply is_flatR_of_prog_single. constructor. apply H. assumption.
+ rewrite keep_L_prog_nil_flat_nil with (p:=p1).
constructor. assumption.
rewrite ifb_not_preserved_stable_not_preserved_l with (l:=l) (b:=b) (p2:=p2).
reflexivity. assumption. assumption. assumption.
- assert (set_stable (control_depsR_prog p2) L).
{ unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
assumption. apply CDS_ifb_r. assumption. }
simpl. destruct (set_mem l L) eqn:Heqmem.
+ apply is_flatR_of_prog_single. constructor. apply H. assumption.
+ rewrite keep_L_prog_nil_flat_nil with (p:=p2).
constructor. assumption.
rewrite ifb_not_preserved_stable_not_preserved_r with (l:=l) (b:=b) (p1:=p1).
reflexivity. assumption. assumption. assumption.
- assert (set_stable (control_depsR_prog p) L).
{ unfold set_stable. unfold set_stable in H1. intros. apply H1 with (l':=l').
assumption. apply CDS_while. assumption. }
simpl. destruct (set_mem l L) eqn:Heqmem.
+ apply is_flatR_of_prog_single. rewrite keep_L_prog_app.
constructor. pose proof (H L H1).
simpl in H3. rewrite Heqmem in H3. apply is_flatR_of_prog_single. apply H3.
apply H0. assumption.
+ rewrite keep_L_prog_app. rewrite keep_L_prog_nil_flat_nil with (p:=p).
rewrite keep_L_prog_nil_flat_nil with (p:={{WHILE << l >> b DO p END}}).
apply IFOP_nil.
apply control_depsR_prog_stable_cons_reverse.
split. assumption. unfold set_stable. intros. inversion H4.
simpl. rewrite Heqmem. reflexivity.
apply is_flatR_of_prog_single. assumption.
assumption. apply while_not_preserved_stable_not_preserved with (l:=l) (b:=b);
assumption.
assumption.
- simpl. destruct (set_mem l L).
+ apply is_flatR_of_prog_single. apply IFOS_while_end.
+ apply IFOP_nil.
- simpl. destruct (set_mem l L).
+ apply is_flatR_of_prog_single. apply IFOS_assert.
+ apply IFOP_nil.
Qed.
Lemma keep_L_prog_cons_reverse : ∀ p s q L,
keep_L_prog p L = s;;q →
∃ q1 s' q2, p = q1 +;+ s';;q2 ∧ keep_L_prog q1 L = {{}} ∧
set_mem (stmt_get_label s') L = true.
Proof.
intros p. induction p; intros.
- inversion H.
- simpl in H. destruct (set_mem (stmt_get_label s) L) eqn:Heqmem.
+ inversion H. ∃ {{}}. ∃ s. ∃ p.
repeat split. destruct s; simpl; simpl in Heqmem; assumption.
+ apply IHp in H. inversion H as [q1 [s' [q2 [H0 [H1 H2]]]]].
∃ (s;;q1). ∃ (s'). ∃ q2. repeat split.
× simpl. rewrite <- H0. reflexivity.
× simpl. rewrite Heqmem. assumption.
× assumption.
Qed.
Lemma keep_L_prog_app_reverse : ∀ p q1 q2 L,
keep_L_prog p L = q1 +;+ q2 →
∃ p1 p2, p = p1 +;+ p2 ∧ keep_L_prog p1 L = q1 ∧ keep_L_prog p2 L = q2.
Proof.
intros p. induction p; intros.
- simpl in H. destruct q1; destruct q2; inversion H.
∃ {{}}, {{}}. repeat split.
- simpl in H. destruct (stmt_get_label s \in? L) eqn:Heqmem.
+ destruct q1.
× simpl in H. destruct q2; inversion H.
apply IHp with (q1:={{}}) in H2.
decompose_ex H2. decompose [and] H2; clear H2.
inversion H. ∃ {{}}, (s;;p).
repeat split. simpl. rewrite Heqmem. reflexivity.
× inversion H. apply IHp in H2. decompose_ex H2. decompose [and] H2; clear H2.
∃ (s;;p1), p2. repeat split. simpl. rewrite <- H0. reflexivity.
simpl. rewrite Heqmem. rewrite <- H4. reflexivity.
assumption.
+ apply IHp in H. decompose_ex H. decompose [and] H; clear H.
∃ (s;;p1), p2. repeat split.
simpl. rewrite <- H0. reflexivity.
simpl. rewrite Heqmem. assumption. assumption.
Qed.
Lemma keep_L_prog_app_bis_reverse : ∀ p q1 t q2 L,
keep_L_prog p L = q1 +;+ t;; q2 →
∃ p1 s p2, p = p1 +;+ s;; p2 ∧ keep_L_prog p1 L = q1 ∧
keep_L_stmt s L = t ∧ keep_L_prog p2 L = q2.
Proof.
intros p. induction p; intros.
- simpl in H. destruct q1; inversion H.
- simpl in H. destruct (stmt_get_label s \in? L) eqn:Heqmem.
+ destruct q1; inversion H.
× ∃ {{}}, s, p. repeat split.
× apply IHp in H2.
decompose_ex H2. decompose [and] H2; clear H2.
∃ (s;;p1), s1, p2. { repeat split.
- simpl. rewrite <- H0. reflexivity.
- simpl. rewrite Heqmem. rewrite <- H4. reflexivity.
- assumption.
- assumption. }
+ apply IHp in H.
decompose_ex H. decompose [and] H; clear H.
∃ (s;;p1), s0, p2. { repeat split.
- simpl. rewrite <- H0. reflexivity.
- simpl. rewrite Heqmem. assumption.
- assumption.
- assumption. }
Qed.
Lemma keep_L_prog_flat_reverse : ∀ q1 q,
is_flatR_of_prog q1 q →
∀ p L,
q = keep_L_prog p L →
set_stable (control_depsR_prog p) L →
∃ q2, is_flatR_of_prog q2 p ∧ q1 = keep_L_prog q2 L.
Proof.
apply (is_flatR_of_prog_mutual_ind
(fun q1 q H ⇒ ∀ p L,
q = keep_L_prog p L →
set_stable (control_depsR_prog p) L →
∃ q2, is_flatR_of_prog q2 p ∧ q1 = keep_L_prog q2 L)
(fun q1 t H ⇒ ∀ s L,
{{t}} = keep_L_prog {{s}} L →
set_stable (control_depsR_stmt s) L →
∃ q2, is_flatR_of_stmt q2 s ∧ q1 = keep_L_prog q2 L)); intros.
- ∃ (flat_l_prog p). split. apply flat_l_prog_correct.
rewrite keep_L_prog_nil_flat_nil with (p:=p).
reflexivity. assumption. rewrite H; reflexivity. apply flat_l_prog_correct.
- symmetry in H1. pose proof H1. apply keep_L_prog_cons_reverse in H1.
inversion H1 as [q1 [s' [q2 [H4 [H5 H6]]]]].
rewrite H4 in H2. apply control_depsR_prog_stable_app in H2.
destruct H2. apply control_depsR_prog_stable_cons in H7.
destruct H7.
rewrite H4 in H3. rewrite keep_L_prog_app in H3. simpl in H3.
rewrite H5, H6 in H3. inversion H3.
assert({{s}} = keep_L_prog {{s'}} L).
{ simpl. rewrite H6. rewrite H10. reflexivity. }
apply H in H9.
symmetry in H11. apply H0 in H11.
inversion H9 as [q3 [H12 H13]]. inversion H11 as [q4 [H14 H15]].
∃ ((flat_l_prog q1) +;+ q3 +;+ q4).
split. rewrite H4. apply is_flatR_of_prog_intro.
∃ (flat_l_prog q1). ∃ (q3+;+q4).
repeat split. apply flat_l_prog_correct. apply IFOP_cons; assumption.
rewrite 2!keep_L_prog_app. rewrite keep_L_prog_nil_flat_nil with (p:=q1).
rewrite H13. rewrite H15. reflexivity.
assumption. assumption. apply flat_l_prog_correct. assumption. assumption.
- destruct s; simpl in H; destruct (set_mem l0 L) eqn:Heqmem; inversion H; subst.
∃ {{SKIP << l0 >>}}.
split. constructor. simpl. rewrite Heqmem. reflexivity.
- destruct s; simpl in H; destruct (set_mem l0 L) eqn:Heqmem; inversion H; subst.
∃ {{i0 ::= a0 << l0 >>}}.
split. constructor. simpl. rewrite Heqmem. reflexivity.
- destruct s; simpl in H0; destruct (set_mem l0 L) eqn:Heqmem; inversion H0; subst.
assert(set_stable (control_depsR_prog p) L).
{ unfold set_stable. unfold set_stable in H1. intros. apply H1 with (l':=l').
assumption. apply CDS_ifb_l. assumption. }
pose proof (H p L eq_refl H2).
inversion H3 as [q2 [H4 H5]].
∃ ((ASSERT << l0 >> b0 =>> l0);;q2).
split.
constructor. assumption.
simpl. rewrite Heqmem. rewrite H5. reflexivity.
- destruct s; simpl in H0; destruct (set_mem l0 L) eqn:Heqmem; inversion H0; subst.
assert(set_stable (control_depsR_prog p0) L).
{ unfold set_stable. unfold set_stable in H1. intros. apply H1 with (l':=l').
assumption. apply CDS_ifb_r. assumption. }
pose proof (H p0 L eq_refl H2).
inversion H3 as [q2 [H4 H5]].
∃ ((ASSERT << l0 >> B_not b0 =>> l0);;q2).
split.
constructor. assumption.
simpl. rewrite Heqmem. rewrite H5. reflexivity.
- destruct s; simpl in H1; destruct (set_mem l0 L) eqn:Heqmem; inversion H1; subst.
assert(set_stable (control_depsR_prog p0) L).
{ unfold set_stable. unfold set_stable in H1. intros. apply H2 with (l':=l').
assumption. apply CDS_while. assumption. }
pose proof (H0 p0 L eq_refl H3).
assert ({{WHILE << l0 >> b0 DO keep_L_prog p0 L END}} =
keep_L_prog {{WHILE << l0 >> b0 DO p0 END}} L).
{ simpl. rewrite Heqmem. reflexivity. }
pose proof (H (WHILE << l0 >> b0 DO p0 END) L H5 H2).
inversion H4 as [q2 [H7 H8]].
inversion H6 as [q3 [H9 H10]].
∃ ((ASSERT << l0 >> b0 =>> l0);;q2+;+q3).
split.
apply IFOS_while_loop; assumption.
simpl. rewrite Heqmem. rewrite keep_L_prog_app.
rewrite H8, H10. reflexivity.
- destruct s; simpl in H; destruct (set_mem l0 L) eqn:Heqmem; inversion H; subst.
∃ {{ASSERT << l0 >> B_not b0 =>> l0}}.
split. apply IFOS_while_end.
simpl. rewrite Heqmem. reflexivity.
- destruct s; simpl in H; destruct (set_mem l0 L) eqn:Heqmem; inversion H; subst.
∃ {{ASSERT << l0 >> b0 =>> l1}}.
split. apply IFOS_assert.
simpl. rewrite Heqmem. reflexivity.
Qed.
Lemma ass_not_preserved_mayread : ∀ i a l q L,
set_stable (data_depsR_prog ((i ::= a << l >>);; q)) L →
¬ l \in L →
∀ l', l' \in L → ¬ (i, l') \in mayread_prog q.
Proof.
intros. intros contra. apply H0.
apply H with (l':=l'); try assumption.
apply set_data_prog_correct. rewrite set_data_prog_equation.
rewrite set_union_In. left.
rewrite set2_inner_fst_In. ∃ i.
split.
- simpl. apply set_singleton_In. reflexivity.
- assumption.
Qed.
Lemma mustdef_prog_quotient : ∀ p q,
is_quotientR_prog p q → mustdef_prog q \subseteq mustdef_prog p.
Proof.
apply (is_quotientR_prog_mutual_ind
(fun p q H ⇒ mustdef_prog q \subseteq mustdef_prog p)
(fun s t H ⇒ mustdef_stmt t \subseteq mustdef_stmt s)); intros;
try apply set_incl_refl.
- simpl. unfold set_incl; intros. rewrite set_union_In. right; apply H; assumption.
- simpl. unfold set_incl; intros. rewrite set_union_In in H1.
rewrite set_union_In. destruct H1.
+ left; apply H0; assumption.
+ right; apply H; assumption.
- simpl. unfold set_incl; intros. rewrite set_inter_In in H1. rewrite set_inter_In.
destruct H1. apply H in H1. apply H0 in H2. split; assumption.
Qed.
Definition affected_prog p L := set_map fst (set2_inter_snd (mayread_prog p) L).
Lemma affected_prog_In : ∀ p L i,
i \in affected_prog p L ↔ ∃ l, (i, l) \in mayread_prog p ∧ l \in L.
Proof.
intros. unfold affected_prog.
rewrite set_map_In.
split; intros.
- destruct H as [(i0, l0) [H0 H1]]. simpl in H1; subst i0.
rewrite set2_inter_snd_In in H0. destruct H0. ∃ l0. split; assumption.
- destruct H as [l [H H0]].
∃ (i, l).
split; try reflexivity.
rewrite set2_inter_snd_In. split; assumption.
Qed.
Lemma mayread_prog_keep_L_affected : ∀ p L i,
set_stable (control_depsR_prog p) L →
set_stable (data_depsR_prog p) L →
i \in set_map fst (mayread_prog (keep_L_prog p L)) →
i \in affected_prog p L.
Proof.
intros.
rewrite set_map_In in H1. destruct H1 as [(i0, l0) [H1 H2]].
simpl in H2; subst i0.
rewrite affected_prog_In.
apply mayread_flat in H1. decompose_ex H1. decompose [and] H1; clear H1.
pose proof (keep_L_prog_flat_reverse _ _ H6 _ _ eq_refl H).
destruct H1 as [q3 [H7 H8]].
rewrite H2 in H8. symmetry in H8. apply keep_L_prog_app_reverse in H8.
decompose_ex H8. decompose [and] H8; clear H8.
pose proof H10.
apply keep_L_prog_cons_reverse in H10.
decompose_ex H10. decompose [and] H10; clear H10.
rewrite H8 in H5. rewrite keep_L_prog_app in H5. simpl in H5.
rewrite H12, H13 in H5. simpl in H5. inversion H5; clear H5.
rewrite H8 in H1; clear H8.
assert(is_flatR_prog q1 ∧ is_flatR_stmt s ∧ is_flatR_prog q2).
{ repeat split.
- apply is_flatR_prog_app_reverse with (q:=s;;q2).
rewrite <- H2.
apply is_flatR_of_prog_is_flatR with (p:=keep_L_prog p L); assumption.
- apply is_flatR_prog_single.
apply is_flatR_prog_app_reverse with (q:=q2).
apply is_flatR_prog_app_reverse with (p:=q1). simpl.
rewrite <- H2.
apply is_flatR_of_prog_is_flatR with (p:=keep_L_prog p L); assumption.
- apply is_flatR_prog_app_reverse with (p:=q1+;+{{s}}).
rewrite <- seq_assoc. simpl.
rewrite <- H2.
apply is_flatR_of_prog_is_flatR with (p:=keep_L_prog p L); assumption.
}
assert(is_flatR_prog p1 ∧ is_flatR_prog q0 ∧ is_flatR_stmt s' ∧ is_flatR_prog q4).
{ repeat split.
- apply is_flatR_prog_app_reverse with (q:=q0+;+s';;q4). rewrite <- H1.
apply is_flatR_of_prog_is_flatR with (p:=p); assumption.
- apply is_flatR_prog_app_reverse with (q:=s';;q4).
apply is_flatR_prog_app_reverse with (p:=p1).
rewrite <- H1.
apply is_flatR_of_prog_is_flatR with (p:=p); assumption.
- apply is_flatR_prog_single.
apply is_flatR_prog_app_reverse with (q:=q4).
apply is_flatR_prog_app_reverse with (p:=p1+;+q0).
rewrite <- seq_assoc. simpl.
rewrite <- H1.
apply is_flatR_of_prog_is_flatR with (p:=p); assumption.
- apply is_flatR_prog_app_reverse with (p:=p1+;+q0+;+{{s'}}).
rewrite <- 2!seq_assoc. simpl.
rewrite <- H1.
apply is_flatR_of_prog_is_flatR with (p:=p); assumption.
}
assert ((i, l0) \in mayread_stmt s').
{ apply is_flatR_stmt_mayread; try apply H8.
apply is_flatR_stmt_mayread in H4; try apply H5. destruct H4.
assert (is_flatR_stmt s) by apply H5.
assert (is_flatR_stmt s') by apply H8.
inversion H15; subst s; inversion H16; subst s';
simpl in H17; inversion H17; subst; simpl in H4;
split; try assumption; reflexivity.
}
destruct (set_In_dec i (set_map fst (set2_diff_snd (maydef_prog (p1+;+q0)) L))).
- rewrite set_map_In in s0. destruct s0 as [(i1, l1) [H15 H16]].
simpl in H16; subst i1.
rewrite set2_diff_snd_In in H15. destruct H15.
exfalso. apply H16.
apply H0 with (l':=l0).
apply is_flatR_stmt_mayread in H10; try apply H8. destruct H10.
rewrite <- H17. apply set_mem_correct_iff; assumption.
apply set_data_prog_correct.
apply is_flatR_of_prog_set_data_incl with (q:=q3); try assumption.
rewrite H1. rewrite seq_assoc. rewrite set_data_prog_seq.
rewrite set_union_In. left. rewrite set2_inner_fst_In. ∃ i.
split; try assumption. simpl. rewrite set_union_In. left. assumption.
- ∃ l0. rewrite set_map_In in n.
split.
+ apply is_flatR_of_prog_mayread_incl with (q:=q3); try assumption.
rewrite H1. rewrite seq_assoc. rewrite mayread_prog_seq.
rewrite set_union_In. right.
simpl. rewrite set2_diff_fst_union_distr_l.
rewrite set_union_In. left.
rewrite set2_diff_fst_In. split; try assumption.
intros contra. apply mustdef_prog_exists_maydef in contra.
destruct contra as [l H15].
apply n. ∃ (i, l).
split; try reflexivity.
rewrite set2_diff_snd_In.
split; try assumption. intros contra.
apply maydef_flat in H15. decompose_ex H15. decompose [and] H15; clear H15.
apply is_flatR_prog_is_flatR_of_same in H20; try (apply is_flatR_prog_app; apply H8).
subst q5.
apply is_flatR_stmt_maydef in H18.
× destruct H18. inversion H15; subst s0.
simpl in H16. subst i0 l1.
apply H3.
replace q1 with (keep_L_prog (p1+;+q0) L)
by (rewrite keep_L_prog_app; rewrite H12; rewrite seq_nil_r ; assumption).
rewrite <- H20.
rewrite keep_L_prog_app. simpl.
rewrite (set_mem_correct2 _ _ contra).
rewrite mustdef_prog_seq. rewrite set_union_In. right. simpl.
rewrite set_union_In. left. rewrite set_singleton_In. reflexivity.
× apply is_flatR_prog_single. apply is_flatR_prog_app_reverse with (q:=q7+;+s';;q4).
apply is_flatR_prog_app_reverse with (p:=q6). simpl.
rewrite <- app_prog_cons. rewrite seq_assoc. rewrite H20. rewrite <- seq_assoc.
rewrite <- H1. apply is_flatR_of_prog_is_flatR with (p:=p). assumption.
+ apply is_flatR_stmt_mayread in H10; try apply H8.
destruct H10. subst l0. apply set_mem_correct_iff. assumption.
Qed.
Lemma ass_not_preserved_proj_equal_ok : ∀ n st i a l q L k,
set_stable (control_depsR_prog ((i ::= a << l >>);; q)) L →
set_stable (data_depsR_prog ((i ::= a << l >>);; q)) L →
¬ l \in L →
proj_traj_prog n (Some (update st i k)) (keep_L_prog q L) L =
proj_traj_prog n (Some st) (keep_L_prog q L) L.
Proof.
intros. apply id_not_in_mayread_prog_update.
intros contra. apply mayread_prog_keep_L_affected in contra.
rewrite affected_prog_In in contra.
destruct contra as [l' [H2 H3]].
apply H1. apply H0 with (l':=l'); try assumption.
apply set_data_prog_correct. rewrite set_data_prog_equation.
rewrite set_union_In. left. rewrite set2_inner_fst_In.
∃ i. split. simpl. apply set_singleton_In. reflexivity.
assumption.
apply control_depsR_prog_stable_cons in H; apply H.
apply data_depsR_prog_stable_after in H0; apply H0.
Qed.
Definition partial_state_proj (ste:state_eps) : partial_state_eps :=
match ste with
| None ⇒ None
| Some st ⇒ Some (fun i ⇒ Some (st i))
end.
Lemma proj_traj_prog_three_cases : ∀ n ste p L,
length (proj_traj_prog n ste p L) = n ∨
length (proj_traj_prog n ste p L) < n ∧
last_state (proj_traj_prog n ste p L) (partial_state_proj ste) ≠ None ∨
length (proj_traj_prog n ste p L) < n ∧
last_state (proj_traj_prog n ste p L) (partial_state_proj ste) = None.
Proof.
intros. destruct (Nat.lt_ge_cases (length (proj_traj_prog n ste p L)) n).
- right. destruct (last_state _ _).
+ left. split. assumption. discriminate.
+ right. split. assumption. reflexivity.
- left. apply le_antisym. apply proj_traj_prog_length. assumption.
Qed.
Lemma is_flatR_prog_unrel :
∀ (s : stmt) (i : id) (s' : stmt),
stmt_is_assR_id s i →
¬ stmt_is_assR_id s' i →
∀ (p : prog) (l l' : label),
flat_data_depsR_prog (s;; p) l l' →
flat_data_depsR_prog (s;; s';; p) l l'.
Proof.
intros.
inversion H1; subst.
+ apply FDP_unrel with (i:=i); assumption.
+ apply FDP_unrel with (i:=i); assumption.
+ do 2 apply FDP_after. assumption.
Qed.
Lemma stmt_get_label_is_quotientR_stmt : ∀ s t,
is_quotientR_stmt s t → stmt_get_label t = stmt_get_label s.
Proof.
intros. inversion H; reflexivity.
Qed.
Lemma keep_L_stmt_quotient : ∀ s L,
is_quotientR_stmt s (keep_L_stmt s L).
Proof.
intros s L. revert s.
prog_cases (apply (stmt_mutual_ind
(fun p ⇒ is_quotientR_prog p (keep_L_prog p L))
(fun s ⇒ is_quotientR_stmt s (keep_L_stmt s L)))) Case; intros;
try now constructor.
- Case "P_cons". simpl. destruct (set_mem (stmt_get_label s) L).
+ apply IQP_stmt; assumption.
+ apply IQP_remove; assumption.
Qed.
Lemma keep_L_prog_involutive_quotient : ∀ p L q,
is_quotientR_prog (keep_L_prog p L) q →
keep_L_prog q L = q.
Proof.
apply (prog_mutual_ind
(fun p ⇒ ∀ (L : set label) (q : prog),
is_quotientR_prog (keep_L_prog p L) q → keep_L_prog q L = q)
(fun s ⇒ ∀ (L : set label) (t : stmt),
is_quotientR_stmt (keep_L_stmt s L) t → keep_L_stmt t L = t)); intros.
- simpl in H. inversion H. reflexivity.
- simpl in H1. destruct (set_mem (stmt_get_label s) L) eqn:Heqmem.
+ inversion H1.
× apply H0. assumption.
× simpl. rewrite stmt_get_label_is_quotientR_stmt with (s:=s).
rewrite Heqmem. rewrite H by assumption. rewrite H0 by assumption.
reflexivity. apply is_quotientR_prog_single;
apply is_quotientR_trans with (q:={{keep_L_stmt s L}});
apply is_quotientR_prog_single.
apply keep_L_stmt_quotient.
assumption.
+ apply H0; assumption.
- simpl in H. inversion H. reflexivity.
- simpl in H. inversion H. reflexivity.
- simpl in H1. inversion H1. subst.
simpl. rewrite H by assumption. rewrite H0 by assumption.
reflexivity.
- simpl in H0. inversion H0. simpl. rewrite H by assumption.
reflexivity.
- simpl in H. inversion H. reflexivity.
Qed.
Lemma flat_l_prog_label : ∀ p,
set_of_labels_prog (flat_l_prog p) \subseteq set_of_labels_prog p.
Proof.
intros. unfold set_incl; intros.
apply label_inR_prog_iff_in_set_of_labels in H.
apply label_inR_prog_iff_in_set_of_labels.
apply is_flatR_of_prog_label with (p1:=flat_l_prog p).
apply flat_l_prog_correct.
assumption.
Qed.
Lemma prefix_prog_app_same : ∀ p p1 p2,
prefix_prog p1 p2 → prefix_prog (p+;+p1) (p+;+p2).
Proof.
intros p.
induction p; intros.
- simpl; assumption.
- simpl. apply PP_after. apply IHp; assumption.
Qed.
Lemma is_flatR_stmt_num_lab : ∀ s, is_flatR_stmt s →
num_lab_stmt s = 1.
Proof.
intros. inversion H; reflexivity.
Qed.
Lemma prefix_prog_traj : ∀ p q,
prefix_prog p q → ∀ n ste,
traj_prog (length (traj_prog n ste p)) ste p =
traj_prog (length (traj_prog n ste p)) ste q.
Proof.
intros p q H n ste. revert n ste p q H.
apply (traj_prog_ind
(fun n ste p tr ⇒ ∀ q, prefix_prog p q →
traj_prog (length tr) ste p =
traj_prog (length tr) ste q)); intros; simpl;
try reflexivity;
try (inversion H0; try rewrite e3; apply f_equal; apply H;
try apply prefix_prog_app_same; assumption).
- inversion H0. rewrite e3. apply f_equal. apply H. apply prefix_prog_app_same.
apply PP_after. assumption.
- inversion H. rewrite e3. reflexivity.
Qed.
Lemma prefix_saturate : ∀ (A:Type) (l1 l2:list A),
prefix l1 l2 → length l1 = length l2 → l1 = l2.
Proof.
intros. induction H.
- simpl in H0. symmetry in H0. apply length_zero_iff_nil in H0. symmetry.
assumption.
- simpl in H0. apply eq_add_S in H0. apply f_equal. apply IHprefix. assumption.
Qed.
Lemma prefix_prog_traj2 : ∀ p q,
is_flatR_prog p →
prefix_prog p q → ∀ n ste,
n ≤ num_lab_prog p →
traj_prog n ste p =
traj_prog n ste q.
Proof.
intros p q H. revert q. induction H; intros.
- simpl in H0; inversion H0; reflexivity.
- simpl in H2. rewrite is_flatR_stmt_num_lab in H2 by assumption.
inversion H1. destruct n.
+ reflexivity.
+ apply le_S_n in H2. destruct ste; simpl.
× inversion H; try (destruct (beval s1 b); [|reflexivity]); apply f_equal;
apply IHis_flatR_prog; assumption.
× reflexivity.
Qed.
Lemma traj_prog_not_none :
∀ n ste p,
last_state (traj_prog n ste p) ste ≠ None →
Forall (fun x ⇒ snd x ≠ None) (traj_prog n ste p).
Proof.
intros.
functional induction (traj_prog n ste p); try (constructor; fail);
try (constructor; [discriminate|]; apply IHl;
rewrite last_state_cons_change_default in H; assumption).
simpl in H. contradiction H. reflexivity.
Qed.
Lemma traj_prog_not_none_iff :
∀ n ste p, ste ≠ None →
last_state (traj_prog n ste p) ste ≠ None ↔
Forall (fun x ⇒ snd x ≠ None) (traj_prog n ste p).
Proof.
split; intros.
- apply traj_prog_not_none; assumption.
- induction H0.
+ simpl. assumption.
+ destruct l.
× simpl. assumption.
× rewrite 2!last_state_cons_change_default.
rewrite last_state_cons_change_default in IHForall. assumption.
Qed.
Lemma traj_prog_none_end : ∀ n ste p,
last_state (traj_prog n ste p) ste = None →
∀ m, n ≤ m → traj_prog m ste p = traj_prog n ste p.
Proof.
intros n ste p. functional induction (traj_prog n ste p); intros;
try (destruct m; [inversion H0 |]; simpl; try rewrite e3; apply f_equal; apply IHl;
[rewrite last_state_cons_change_default in H; assumption | apply le_S_n in H0; assumption]).
- simpl in H. subst ste. destruct m; reflexivity.
- destruct m. inversion H0. reflexivity.
- destruct m; [inversion H0 |]; simpl; rewrite e3. reflexivity.
- destruct m; reflexivity.
Qed.