Library set_deps
Definition of mustdef_prog, maydef_prog and mayread_prog which compute
respectively the set of labels that are surely assigned in a program, the set of labels
that can be assigned in a program and the set of labels that can be read in a program.
Thanks to these three functions, we can define set_data_prog, which computes the data
dependence in a structural way. This function is proved to correctly implement
the inductive relation data_depsR_prog defined in the module data (set_data_prog_correct).
Require Import Relation_Definitions.
Require Export set_prog.
Require Import label.
Require Import set2.
Require Import data.
Require Import decidable.
Require Import set_instance.
Require Import seq.
Inductive is_bounded_flatR_of_prog : prog → prog → Prop :=
| IBFOP_nil : is_bounded_flatR_of_prog {{}} {{}}
| IBFOP_cons : ∀ s p p1 p1', is_bounded_flatR_of_stmt p s →
is_bounded_flatR_of_prog p1 p1' →
is_bounded_flatR_of_prog (p+;+p1) (s;;p1')
with is_bounded_flatR_of_stmt : prog → stmt → Prop :=
| IBFOS_skip : ∀ l, is_bounded_flatR_of_stmt {{SKIP << l >>}} (SKIP << l >>)
| IBFOS_ass : ∀ i a l,
is_bounded_flatR_of_stmt {{i ::= a << l >>}} (i ::= a << l >>)
| IBFOS_ifb_l : ∀ l b p1 p2 q, is_bounded_flatR_of_prog q p1 →
is_bounded_flatR_of_stmt ((ASSERT << l >> b =>> l);;q)
(IFB << l >> b THEN p1 ELSE p2 FI)
| IBFOS_ifb_r : ∀ l b p1 p2 q, is_bounded_flatR_of_prog q p2 →
is_bounded_flatR_of_stmt ((ASSERT << l >> (B_not b) =>> l);;q)
(IFB << l >> b THEN p1 ELSE p2 FI)
| IBFOS_while_loop : ∀ l b p q1 q2,
is_bounded_flatR_of_prog q1 p → is_bounded_flatR_of_prog q2 p →
is_bounded_flatR_of_stmt ((ASSERT << l >> b =>> l);; q1 +;+
(ASSERT << l >> b =>> l);; q2 +;+
{{ASSERT << l >> B_not b =>>l}})
(WHILE << l >> b DO p END)
| IBFOS_while_end : ∀ l b p,
is_bounded_flatR_of_stmt {{ASSERT << l >> (B_not b) =>> l}}
(WHILE << l >> b DO p END)
| IBFOS_assert : ∀ l b l',
is_bounded_flatR_of_stmt {{ASSERT << l >> b =>> l'}} (ASSERT << l >> b =>> l').
Scheme is_bounded_flatR_of_prog_mutual_ind :=
Induction for is_bounded_flatR_of_prog Sort Prop
with is_bounded_flatR_of_stmt_mutual_ind :=
Induction for is_bounded_flatR_of_stmt Sort Prop.
Lemma is_bounded_flatR_of_prog_is_flatR_of : ∀ q p,
is_bounded_flatR_of_prog q p → is_flatR_of_prog q p.
Proof.
apply (is_bounded_flatR_of_prog_mutual_ind
(fun q p H ⇒ is_flatR_of_prog q p)
(fun q s H ⇒ is_flatR_of_stmt q s)); intros; repeat constructor; assumption.
Qed.
Fixpoint mustdef_prog (p:prog) :=
match p with
| {{}} ⇒ empty_set
| s;;q ⇒ set_union (mustdef_stmt s) (mustdef_prog q)
end
with mustdef_stmt (s:stmt) : set id :=
match s with
| SKIP << _ >> ⇒ empty_set
| i::= _ << _ >> ⇒ set_singleton i
| IFB << _ >> _ THEN p1 ELSE p2 FI ⇒ set_inter (mustdef_prog p1) (mustdef_prog p2)
| WHILE << _ >> _ DO p END ⇒ empty_set
| ASSERT << _ >> _ =>> _ ⇒ empty_set
end.
Lemma mustdef_prog_equation : ∀ p, mustdef_prog p =
match p with
| {{}} ⇒ empty_set
| s;;q ⇒ set_union (mustdef_stmt s) (mustdef_prog q)
end.
Proof.
intros. destruct p; reflexivity.
Qed.
Lemma mustdef_stmt_equation : ∀ s, mustdef_stmt s =
match s with
| SKIP << _ >> ⇒ empty_set
| i::= _ << _ >> ⇒ set_singleton i
| IFB << _ >> _ THEN p1 ELSE p2 FI ⇒ set_inter (mustdef_prog p1) (mustdef_prog p2)
| WHILE << _ >> _ DO p END ⇒ empty_set
| ASSERT << _ >> _ =>> _ ⇒ empty_set
end.
Proof.
intros. destruct s; reflexivity.
Qed.
Fixpoint maydef_prog (p:prog) :=
match p with
| {{}} ⇒ empty_set
| s;;q ⇒ (set_union (set2_diff_fst (maydef_stmt s) (mustdef_prog q)) (maydef_prog q))
end
with maydef_stmt (s:stmt) : set (id × label) :=
match s with
| SKIP << _ >> ⇒ empty_set
| i ::= _ << l >> ⇒ set_singleton (i,l)
| IFB << _ >> _ THEN p1 ELSE p2 FI ⇒ set_union (maydef_prog p1) (maydef_prog p2)
| WHILE << _ >> _ DO p END ⇒ maydef_prog p
| ASSERT << _ >> _ =>> _ ⇒ empty_set
end.
Lemma maydef_prog_equation : ∀ p, maydef_prog p =
match p with
| {{}} ⇒ empty_set
| s;;q ⇒ (set_union (set2_diff_fst (maydef_stmt s) (mustdef_prog q)) (maydef_prog q))
end.
Proof.
intros. destruct p; reflexivity.
Qed.
Lemma maydef_stmt_equation : ∀ s, maydef_stmt s =
match s with
| SKIP << _ >> ⇒ empty_set
| i ::= _ << l >> ⇒ set_singleton (i,l)
| IFB << _ >> _ THEN p1 ELSE p2 FI ⇒ set_union (maydef_prog p1) (maydef_prog p2)
| WHILE << _ >> _ DO p END ⇒ maydef_prog p
| ASSERT << _ >> _ =>> _ ⇒ empty_set
end.
Proof.
intros. destruct s; reflexivity.
Qed.
Fixpoint mayread_prog (p:prog) :=
match p with
| {{}} ⇒ empty_set
| s;;q ⇒ set_union (mayread_stmt s) (set2_diff_fst (mayread_prog q) (mustdef_stmt s))
end
with mayread_stmt (s:stmt) : set (id×label) :=
match s with
| SKIP << _ >> ⇒ empty_set
| _::=a << l >> ⇒ set_map (fun i ⇒ (i,l)) (set_of_id_aexp a)
| IFB << l >> b THEN p1 ELSE p2 FI ⇒
set_union (set_map (fun i ⇒ (i,l)) (set_of_id_bexp b))
(set_union (mayread_prog p1) (mayread_prog p2))
| WHILE << l >> b DO p END ⇒
set_union (set_map (fun i ⇒ (i,l)) (set_of_id_bexp b))
(mayread_prog p)
| ASSERT << l >> b =>> _ ⇒ set_map (fun i ⇒ (i,l)) (set_of_id_bexp b)
end.
Lemma mayread_prog_equation : ∀ p, mayread_prog p =
match p with
| {{}} ⇒ empty_set
| s;;q ⇒ set_union (mayread_stmt s) (set2_diff_fst (mayread_prog q) (mustdef_stmt s))
end.
Proof.
intros. destruct p; reflexivity.
Qed.
Lemma mayread_stmt_equation : ∀ s, mayread_stmt s =
match s with
| SKIP << _ >> ⇒ empty_set
| _::=a << l >> ⇒ set_map (fun i ⇒ (i,l)) (set_of_id_aexp a)
| IFB << l >> b THEN p1 ELSE p2 FI ⇒
set_union (set_map (fun i ⇒ (i,l)) (set_of_id_bexp b))
(set_union (mayread_prog p1) (mayread_prog p2))
| WHILE << l >> b DO p END ⇒
set_union (set_map (fun i ⇒ (i,l)) (set_of_id_bexp b))
(mayread_prog p)
| ASSERT << l >> b =>> _ ⇒ set_map (fun i ⇒ (i,l)) (set_of_id_bexp b)
end.
Proof.
intros. destruct s; reflexivity.
Qed.
Lemma mustdef_prog_seq : ∀ p1 p2,
mustdef_prog (p1+;+p2) \equiv (mustdef_prog p1) \cup (mustdef_prog p2).
Proof.
intros.
induction p1.
- simpl. rewrite set_same_union_empty_l. reflexivity.
- simpl. rewrite IHp1. rewrite set_union_assoc. reflexivity.
Qed.
Lemma mustdef_prog_not_flat : ∀ p i,
¬ set_In i (mustdef_prog p) ↔ ∃ q, ¬ set_In i (mustdef_prog q) ∧
is_flatR_of_prog q p.
Proof.
split; revert p i.
- apply (prog_mutual_ind
(fun p ⇒ ∀ i, ¬ set_In i (mustdef_prog p) →
∃ q, ¬ set_In i (mustdef_prog q) ∧
is_flatR_of_prog q p)
(fun s ⇒ ∀ i, ¬ set_In i (mustdef_stmt s) →
∃ q, ¬ set_In i (mustdef_prog q) ∧
is_flatR_of_stmt q s)); intros.
+ ∃ {{}}. split.
× assumption.
× constructor.
+ simpl in H1. rewrite set_union_In in H1.
apply not_or_iff in H1. destruct H1.
apply H in H1. apply H0 in H2.
destruct H1 as [q1 [H3 H4]].
destruct H2 as [q2 [H5 H6]].
∃ (q1+;+q2).
split.
× intros contra. apply mustdef_prog_seq in contra.
apply set_union_In in contra. destruct contra; contradiction.
× constructor; assumption.
+ ∃ ({{SKIP << l >>}}). split.
× assumption.
× constructor.
+ ∃ ({{i::=a<<l>>}}). split.
× assumption.
× constructor.
+ simpl in H1. rewrite set_inter_In in H1.
apply not_and_iff in H1; try (apply dec_is_decidable; apply set_In_dec).
destruct H1.
× apply H in H1. destruct H1 as [q [H2 H3]].
∃ ((ASSERT <<l >> b =>>l);;q). { split.
- simpl. rewrite set_same_union_empty_l. assumption.
- constructor. assumption. }
× apply H0 in H1. destruct H1 as [q [H2 H3]].
∃ ((ASSERT <<l >> B_not b =>>l);;q). { split.
- simpl. rewrite set_same_union_empty_l. assumption.
- constructor. assumption. }
+ ∃ ({{ASSERT << l >> B_not b =>> l}}). split.
× assumption.
× constructor.
+ ∃ ({{ASSERT << l >> b =>> l0}}). split.
× assumption.
× constructor.
- apply (prog_mutual_ind
(fun p ⇒ ∀ i,
(∃ q, ¬ set_In i (mustdef_prog q) ∧
is_flatR_of_prog q p) →
¬ set_In i (mustdef_prog p))
(fun s ⇒ ∀ i,
(∃ q, ¬ set_In i (mustdef_prog q) ∧
is_flatR_of_stmt q s) →
¬ set_In i (mustdef_stmt s))); intros.
+ intros contra. inversion contra.
+ simpl. rewrite set_union_In.
destruct H1 as [q [H2 H3]]. inversion H3. subst q.
rewrite mustdef_prog_seq in H2. rewrite set_union_In in H2.
intros contra. destruct contra.
× { apply H with (i:=i).
- ∃ p0. split.
+ intros contra. apply H2. left; assumption.
+ assumption.
- assumption. }
× { apply H0 with (i:=i).
- ∃ p1. split.
+ intros contra. apply H2. right; assumption.
+ assumption.
- assumption. }
+ intros contra. inversion contra.
+ destruct H as [q [H H0]].
inversion H0; subst. assumption.
+ simpl. rewrite set_inter_In. intros contra. destruct contra.
destruct H1 as [q [H4 H5]].
inversion H5; subst q.
× simpl in H4. rewrite set_same_union_empty_l in H4.
{ apply H with (i:=i).
- ∃ q0. split; assumption.
- assumption. }
× simpl in H4. rewrite set_same_union_empty_l in H4.
{ apply H0 with (i:=i).
- ∃ q0. split; assumption.
- assumption. }
+ intros contra. inversion contra.
+ intros contra. inversion contra.
Qed.
Lemma is_flatR_prog_is_flatR_of_same :
∀ p, is_flatR_prog p →
∀ q, is_flatR_of_prog q p →
q = p.
Proof.
intros p H. induction H; intros.
- inversion H. reflexivity.
- inversion H1; subst.
inversion H; subst; inversion H5; subst;
rewrite IHis_flatR_prog with (q:=p1) by assumption; reflexivity.
Qed.
Lemma is_flatR_prog_app_reverse : ∀ p q,
is_flatR_prog (p+;+q) → is_flatR_prog p ∧ is_flatR_prog q.
Proof.
intros.
induction p.
- split. constructor. assumption.
- simpl in H. inversion H. apply IHp in H3. destruct H3.
split.
+ constructor; assumption.
+ assumption.
Qed.
Lemma maydef_prog_seq : ∀ p q,
maydef_prog (p+;+q) \equiv
set2_diff_fst (maydef_prog p) (mustdef_prog q) \cup maydef_prog q.
Proof.
intros p. induction p; intros; simpl.
- rewrite set2_diff_fst_emptyset_l.
rewrite set_same_union_empty_l. reflexivity.
- rewrite IHp. rewrite mustdef_prog_seq.
rewrite set2_diff_fst_union_distr_r.
rewrite set2_diff_fst_union_distr_l.
rewrite set2_diff_fst_twice.
rewrite set_union_assoc.
reflexivity.
Qed.
Lemma is_flatR_of_prog_mustdef_incl : ∀ q p,
is_flatR_of_prog q p → mustdef_prog p \subseteq mustdef_prog q.
Proof.
apply (is_flatR_of_prog_mutual_ind
(fun q p H ⇒ mustdef_prog p \subseteq mustdef_prog q)
(fun q s H ⇒ mustdef_stmt s \subseteq mustdef_prog q)); intros;
try (apply set_incl_refl).
- simpl. rewrite mustdef_prog_seq.
intros a. rewrite 2!set_union_In. intros. destruct H1.
+ left. apply H. assumption.
+ right. apply H0. assumption.
- simpl. rewrite set_same_union_empty_l.
apply set_inter_incl. assumption.
- simpl. rewrite set_same_union_empty_l.
rewrite set_inter_comm.
apply set_inter_incl. assumption.
- simpl. unfold set_incl; intros. inversion H1.
Qed.
Lemma is_flatR_of_prog_maydef_incl : ∀ q p,
is_flatR_of_prog q p → maydef_prog q \subseteq maydef_prog p.
Proof.
apply (is_flatR_of_prog_mutual_ind
(fun q p H ⇒ maydef_prog q \subseteq maydef_prog p)
(fun q s H ⇒ maydef_prog q \subseteq maydef_stmt s)); intros;
try (apply set_incl_refl).
- rewrite maydef_prog_seq. simpl.
intros a. destruct a.
rewrite 2!set_union_In.
rewrite 2!set2_diff_fst_In.
intros. destruct H1.
+ left. destruct H1. split.
× apply H; assumption.
× intros contra.
apply is_flatR_of_prog_mustdef_incl with (q:=p1) in contra;
try assumption.
contradiction.
+ right. apply H0; assumption.
- simpl. rewrite set2_diff_fst_emptyset_l. rewrite set_same_union_empty_l.
unfold set_incl; intros. apply set_union_In.
left; apply H; assumption.
- simpl. rewrite set2_diff_fst_emptyset_l. rewrite set_same_union_empty_l.
unfold set_incl; intros. apply set_union_In.
right; apply H; assumption.
- simpl. rewrite set2_diff_fst_emptyset_l. rewrite set_same_union_empty_l.
rewrite maydef_prog_seq.
unfold set_incl; intros. apply set_union_In in H1. destruct H1.
+ destruct a. apply set2_diff_fst_In in H1.
apply H0. apply H1.
+ apply H; assumption.
- simpl. rewrite set2_diff_fst_emptyset_l, set_same_union_empty_l.
unfold set_incl; intros. inversion H.
Qed.
Lemma maydef_flat : ∀ p i l,
set_In (i, l) (maydef_prog p) ↔
∃ q q1 s q2,
q = q1 +;+ s;; q2 ∧
(i, l) \in maydef_stmt s ∧
¬ set_In i (mustdef_prog q2) ∧
is_flatR_of_prog q p.
Proof.
split; revert p i l.
- apply (prog_mutual_ind
(fun p ⇒ ∀ i l,
set_In (i, l) (maydef_prog p) →
∃ q q1 s q2,
q = q1 +;+ s;; q2 ∧
(i, l) \in maydef_stmt s ∧
¬ set_In i (mustdef_prog q2) ∧
is_flatR_of_prog q p)
(fun s ⇒ ∀ i l,
set_In (i, l) (maydef_stmt s) →
∃ q q1 t q2,
q = q1 +;+ t;; q2 ∧
(i, l) \in maydef_stmt t ∧
¬ set_In i (mustdef_prog q2) ∧
is_flatR_of_stmt q s)); intros.
+ inversion H.
+ simpl in H1. apply set_union_In in H1. destruct H1.
× apply set2_diff_fst_In in H1.
destruct H1. apply H in H1. decompose_ex H1. decompose [and] H1; clear H1.
apply mustdef_prog_not_flat in H2.
destruct H2 as [q3 [H8 H9]].
∃ (q+;+q3), q1, t, (q2+;+q3). { repeat split.
- rewrite H3. rewrite <- seq_assoc. reflexivity.
- assumption.
- rewrite mustdef_prog_seq. rewrite set_union_In.
intros contra. destruct contra; contradiction.
- constructor; assumption. }
× apply H0 in H1. decompose_ex H1.
decompose [and] H1; clear H1.
∃ ((flat_l_stmt s)+;+q), ((flat_l_stmt s)+;+q1), s0, q2.
{ repeat split.
- rewrite H2. rewrite <- seq_assoc. reflexivity.
- assumption.
- assumption.
- constructor.
+ apply flat_l_stmt_correct.
+ assumption. }
+ inversion H.
+ simpl in H. apply set_singleton_In in H. inversion H; subst.
∃ {{i::=a<<l>>}}, {{}}, (i ::= a << l >>), {{}}.
repeat split.
× simpl. apply set_singleton_In. reflexivity.
× intros contra; inversion contra.
× constructor.
+ simpl in H1. rewrite set_union_In in H1. destruct H1.
× apply H in H1. decompose_ex H1. decompose [and] H1; clear H1.
∃ ((ASSERT << l >> b =>> l);;q), ((ASSERT << l >> b =>> l);;q1),
s, q2.
{ repeat split.
- rewrite H2. reflexivity.
- assumption.
- assumption.
- constructor; assumption. }
× apply H0 in H1. decompose_ex H1. decompose [and] H1; clear H1.
∃ ((ASSERT << l >> B_not b =>> l);;q), ((ASSERT << l >> B_not b =>> l);;q1),
s, q2.
{ repeat split.
- rewrite H2. reflexivity.
- assumption.
- assumption.
- constructor; assumption. }
+ simpl in H0. apply H in H0. decompose_ex H0. decompose [and] H0; clear H0.
∃ ((ASSERT << l >> b =>> l);;q+;+{{ASSERT << l >> B_not b =>> l}}),
((ASSERT << l >> b =>> l);;q1), s, (q2+;+{{ASSERT << l >> B_not b =>> l}}).
{ repeat split.
- rewrite H1. rewrite <- seq_assoc. reflexivity.
- assumption.
- intros contra. rewrite mustdef_prog_seq in contra. simpl in contra.
rewrite 2!set_same_union_empty_r in contra. contradiction.
- repeat constructor; assumption. }
+ inversion H.
- intros. decompose_ex H. decompose [and] H; clear H.
apply is_flatR_of_prog_maydef_incl with (q:=q); try assumption.
rewrite H0.
rewrite maydef_prog_seq. apply set_union_In. right.
simpl. apply set_union_In. left.
apply set2_diff_fst_In. split; assumption.
Qed.
Definition set_ref (s:stmt) : set id :=
match s with
| SKIP << _ >> ⇒ \emptyset
| _ ::= a << _ >> ⇒ set_of_id_aexp a
| IFB << _ >> b THEN _ ELSE _ FI ⇒ set_of_id_bexp b
| WHILE << _ >> b DO _ END ⇒ set_of_id_bexp b
| ASSERT << _ >> b =>> _ ⇒ set_of_id_bexp b
end.
Definition set_def (s:stmt) : set id :=
match s with
| i ::= _ << _ >> ⇒ \sin i
| _ ⇒ \emptyset
end.
Lemma mayread_prog_seq : ∀ p q,
mayread_prog (p+;+q) \equiv mayread_prog p \cup (set2_diff_fst (mayread_prog q) (mustdef_prog p)).
Proof.
intros. induction p.
- simpl. rewrite set2_diff_fst_emptyset_r. rewrite set_same_union_empty_l.
reflexivity.
- simpl. rewrite IHp.
rewrite set2_diff_fst_union_distr_r.
rewrite set2_diff_fst_union_distr_l.
rewrite set2_diff_fst_twice.
rewrite set_union_assoc.
rewrite set_inter_comm. reflexivity.
Qed.
Lemma is_flatR_of_prog_mayread_incl : ∀ q p, is_flatR_of_prog q p →
mayread_prog q \subseteq mayread_prog p.
Proof.
apply (is_flatR_of_prog_mutual_ind
(fun q p H ⇒
mayread_prog q \subseteq mayread_prog p)
(fun q s H ⇒
mayread_prog q \subseteq mayread_stmt s)); intros; try apply set_incl_refl.
- rewrite mayread_prog_seq. simpl.
intros a. destruct a.
rewrite 2!set_union_In.
rewrite 2!set2_diff_fst_In.
intros. destruct H1.
+ left. apply H; assumption.
+ right. destruct H1. split.
× apply H0; assumption.
× intros contra.
replace (mustdef_stmt s) with (mustdef_prog {{s}}) in contra by reflexivity.
apply is_flatR_of_prog_mustdef_incl with (q:=p) in contra.
contradiction.
apply is_flatR_of_prog_single. assumption.
- simpl. intros a. rewrite 3!set_union_In. rewrite set2_diff_fst_emptyset_r.
intros.
destruct H0.
+ left; assumption.
+ right. left. apply H; assumption.
- simpl. intros a. rewrite 3!set_union_In. rewrite set2_diff_fst_emptyset_r.
intros.
destruct H0.
+ left; assumption.
+ right. right. apply H; assumption.
- unfold set_incl; intros. simpl in H1. rewrite set2_diff_fst_emptyset_r in H1.
rewrite mayread_prog_seq in H1.
rewrite 2!set_union_In in H1.
repeat destruct H1.
+ simpl. apply set_union_In; left; assumption.
+ simpl. apply set_union_In; right; apply H0; assumption.
+ destruct a. apply set2_diff_fst_In in H1. apply H. apply H1.
- simpl. rewrite set2_diff_fst_emptyset_r. rewrite set_same_union_empty_r.
unfold set_incl; intros. rewrite set_union_In; left; assumption.
Qed.
Lemma mayread_flat : ∀ p i l,
set_In (i, l) (mayread_prog p) ↔
∃ q q1 s q2,
q = q1 +;+ s;; q2 ∧
(i, l) \in mayread_stmt s ∧
¬ set_In i (mustdef_prog q1) ∧
is_flatR_of_prog q p.
Proof.
split; revert p i l.
- apply (prog_mutual_ind
(fun p ⇒ ∀ i l, (i, l) \in mayread_prog p →
∃ q q1 s q2, q = q1 +;+ s;; q2 ∧ (i, l) \in mayread_stmt s ∧
¬ i \in mustdef_prog q1 ∧ is_flatR_of_prog q p)
(fun s ⇒ ∀ i l, (i, l) \in mayread_stmt s →
∃ q q1 t q2, q = q1 +;+ t;; q2 ∧ (i, l) \in mayread_stmt t ∧
¬ i \in mustdef_prog q1 ∧ is_flatR_of_stmt q s));
intros.
+ inversion H.
+ simpl in H1. apply set_union_In in H1. destruct H1.
× apply H in H1. decompose_ex H1. decompose [and] H1; clear H1.
∃ (q+;+flat_l_prog p), q1, t, (q2+;+flat_l_prog p).
{ repeat split; try assumption.
- rewrite H2. rewrite <- seq_assoc. reflexivity.
- constructor. assumption. apply flat_l_prog_correct. }
× apply set2_diff_fst_In in H1. destruct H1.
apply H0 in H1. decompose_ex H1. decompose [and] H1; clear H1.
replace (mustdef_stmt s) with (mustdef_prog {{s}}) in H2 by reflexivity.
apply mustdef_prog_not_flat in H2.
inversion H2 as [q3 [H9 H10]].
∃ (q3+;+q), (q3+;+q1), s0, q2. { repeat split; try assumption.
- rewrite H3. rewrite <- seq_assoc. reflexivity.
- rewrite mustdef_prog_seq. rewrite set_union_In.
apply not_or_iff. split; assumption.
- constructor. apply is_flatR_of_prog_single in H10. assumption.
assumption. }
+ inversion H.
+ simpl in H. apply set_map_In in H. inversion H as [i1 [H0 H1]].
inversion H1; subst.
∃ {{i::=a<<l>>}}, {{}}, (i::=a<<l>>), {{}}. repeat split.
× simpl. rewrite set_map_In. ∃ i1; split; assumption.
× intros contra. inversion contra.
× constructor.
+ simpl in H1. rewrite 2!set_union_In in H1.
rewrite set_map_In in H1.
decompose [or] H1; clear H1.
× inversion H2 as [i0 [H3 H4]]. inversion H4; subst.
∃ ((ASSERT << l >> b =>> l);;flat_l_prog p),
{{}}, (ASSERT << l >> b =>> l), (flat_l_prog p).
{ repeat split.
- simpl. rewrite set_map_In. ∃ i0; split; assumption.
- intros contra. inversion contra.
- constructor. apply flat_l_prog_correct. }
× apply H in H3.
decompose_ex H3. decompose [and] H3; clear H3.
∃ ((ASSERT << l >> b =>> l);;q),
((ASSERT << l >> b =>> l);;q1), s, q2.
{ repeat split; try assumption.
- rewrite H1. reflexivity.
- simpl. rewrite set_same_union_empty_l. assumption.
- constructor. assumption. }
× apply H0 in H3.
decompose_ex H3. decompose [and] H3; clear H3.
∃ ((ASSERT << l >> B_not b =>> l);;q),
((ASSERT << l >> B_not b =>> l);;q1), s, q2.
{ repeat split; try assumption.
- rewrite H1. reflexivity.
- simpl. rewrite set_same_union_empty_l. assumption.
- constructor. assumption. }
+ simpl in H0. apply set_union_In in H0. rewrite set_map_In in H0.
destruct H0.
× inversion H0 as [i0 [H1 H2]]; clear H0. inversion H2; subst.
∃ {{ASSERT << l >> B_not b =>> l}}, {{}}, (ASSERT << l >> B_not b =>> l),
{{}}.
{ repeat split.
- simpl. rewrite set_map_In. ∃ i0; split; assumption.
- intros contra. inversion contra.
- constructor. }
× apply H in H0. decompose_ex H0. decompose [and] H0; clear H0.
∃ ((ASSERT << l >> b =>>l);;q+;+{{ASSERT << l >> B_not b =>> l}}),
((ASSERT << l >> b =>>l);;q1), s, (q2+;+{{ASSERT << l >> B_not b =>> l}}).
{ repeat split; try assumption.
- rewrite H1. rewrite <- seq_assoc. reflexivity.
- simpl. rewrite set_same_union_empty_l. assumption.
- constructor. constructor. assumption. }
+ simpl in H. apply set_map_In in H. inversion H as [i0 [H0 H1]]; clear H.
inversion H1; subst.
∃ {{ASSERT << l >> b =>>l0}}, {{}}, (ASSERT << l>> b =>>l0), {{}}.
repeat split.
× simpl. rewrite set_map_In. ∃ i0; split; assumption.
× intros contra; inversion contra.
× constructor.
- intros. decompose_ex H. decompose [and] H; clear H.
apply is_flatR_of_prog_mayread_incl with (q:=q); try assumption.
rewrite H0. 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; assumption.
Qed.
Lemma is_flatR_prog_mustdef : ∀ p,
is_flatR_prog p →
∀ i, (i \in mustdef_prog p ↔ ass_inR_prog p i).
Proof.
apply (is_flatR_prog_mutual_ind
(fun p H ⇒ ∀ i, i \in mustdef_prog p ↔ ass_inR_prog p i)
(fun s H ⇒ ∀ i, i \in mustdef_stmt s ↔ ass_inR_stmt s i)); intros;
try (split; intros; inversion H; fail); simpl.
- rewrite set_union_In. rewrite H, H0. split; intros.
+ destruct H1; [ apply AIP_here | apply AIP_after ]; assumption.
+ inversion H1; [ left | right]; assumption.
- rewrite set_singleton_In. split; intros.
+ subst; constructor.
+ inversion H; reflexivity.
Qed.
Lemma is_flatR_stmt_mustdef : ∀ s,
is_flatR_stmt s →
∀ i, (i \in mustdef_stmt s ↔ stmt_is_assR_id s i).
Proof.
intros. inversion H; simpl.
- split; intros; inversion H1.
- rewrite set_singleton_In. split; intros.
+ subst; constructor.
+ inversion H1; reflexivity.
- split; intros; inversion H1.
Qed.
Lemma is_flatR_stmt_mayread : ∀ s,
is_flatR_stmt s →
∀ i l,
((i, l) \in mayread_stmt s ↔ id_inR_ref s i ∧ stmt_get_label s = l).
Proof.
intros. destruct H.
- split; intros.
+ inversion H.
+ destruct H. inversion H.
- simpl. rewrite set_map_In. split; intros.
+ inversion H as [i1 [H0 H1]]; clear H.
inversion H1; subst. split.
× constructor. apply set_of_id_aexp_correct; assumption.
× reflexivity.
+ destruct H. inversion H; subst.
∃ i. split.
× apply set_of_id_aexp_correct; assumption.
× reflexivity.
- simpl. rewrite set_map_In. split; intros.
+ inversion H as [i1 [H0 H1]]; clear H.
inversion H1; subst. split.
× constructor. apply set_of_id_bexp_correct; assumption.
× reflexivity.
+ destruct H. inversion H; subst.
∃ i. split.
× apply set_of_id_bexp_correct; assumption.
× reflexivity.
Qed.
Fixpoint set_data_prog (p:prog) : set (label × label) :=
match p with
| {{}} ⇒ \emptyset
| s;;q ⇒ set2_inner_fst (maydef_stmt s) (mayread_prog q) \cup set_data_stmt s \cup set_data_prog q
end
with set_data_stmt (s:stmt) : set (label×label) :=
match s with
| IFB << _ >> _ THEN p1 ELSE p2 FI ⇒ set_data_prog p1 \cup set_data_prog p2
| WHILE << _ >> _ DO p END as p0 ⇒
set2_inner_fst (maydef_prog p) (mayread_stmt p0) \cup set_data_prog p
| _ ⇒ \emptyset
end.
Lemma set_data_prog_equation : ∀ p, set_data_prog p =
match p with
| {{}} ⇒ \emptyset
| s;;q ⇒ set2_inner_fst (maydef_stmt s) (mayread_prog q) \cup set_data_stmt s \cup set_data_prog q
end.
Proof.
intros. destruct p; reflexivity.
Qed.
Lemma set_data_stmt_equation : ∀ s, set_data_stmt s =
match s with
| IFB << _ >> _ THEN p1 ELSE p2 FI ⇒ set_data_prog p1 \cup set_data_prog p2
| WHILE << _ >> _ DO p END as p0 ⇒
set2_inner_fst (maydef_prog p) (mayread_stmt p0) \cup set_data_prog p
| _ ⇒ \emptyset
end.
Proof.
intros. destruct s; reflexivity.
Qed.
Lemma is_flatR_stmt_maydef : ∀ s,
is_flatR_stmt s → ∀ i l,
((i, l) \in maydef_stmt s ↔ stmt_is_assR_id s i ∧ stmt_get_label s = l).
Proof.
intros. inversion H.
- split; intros.
+ inversion H1.
+ destruct H1. inversion H1.
- simpl. rewrite set_singleton_In. split; intros.
+ inversion H1; subst. split. constructor. reflexivity.
+ destruct H1. inversion H1; subst. reflexivity.
- split; intros.
+ inversion H1.
+ destruct H1. inversion H1.
Qed.
Lemma ass_inR_prog_seq : ∀ p1 p2 i,
ass_inR_prog (p1 +;+ p2) i ↔ ass_inR_prog p1 i ∨ ass_inR_prog p2 i.
Proof.
intros. induction p1.
- simpl. split; intros.
+ right; assumption.
+ destruct H. inversion H. assumption.
- simpl. split; intros.
+ inversion H.
× left. apply AIP_here; assumption.
× apply IHp1 in H3. { destruct H3.
- left. apply AIP_after; assumption.
- right; assumption. }
+ destruct H.
× { inversion H.
- apply AIP_here; assumption.
- apply AIP_after. apply IHp1. left; assumption. }
× apply AIP_after. apply IHp1. right; assumption.
Qed.
Lemma maydef_prog_single : ∀ s,
maydef_prog {{s}} \equiv maydef_stmt s.
Proof.
intros. simpl.
rewrite set2_diff_fst_emptyset_r. rewrite set_same_union_empty_r.
reflexivity.
Qed.
Lemma mayread_prog_single : ∀ s,
mayread_prog {{s}} \equiv mayread_stmt s.
Proof.
intros. simpl. rewrite set2_diff_fst_emptyset_l. rewrite set_same_union_empty_r.
reflexivity.
Qed.
Lemma set_data_prog_seq : ∀ p q,
set_data_prog (p+;+q) \equiv
set2_inner_fst (maydef_prog p) (mayread_prog q) \cup set_data_prog p \cup set_data_prog q.
Proof.
intros. induction p; simpl.
- rewrite set2_inner_fst_emptyset_l. rewrite 2!set_same_union_empty_l.
reflexivity.
- rewrite IHp. rewrite mayread_prog_seq. rewrite set2_inner_fst_union_distr_r.
rewrite set2_inner_fst_union_distr_l. rewrite set2_inner_fst_diff_lr.
rewrite 4!set_union_assoc.
rewrite set_union_comm. rewrite 4!set_union_assoc.
rewrite set_union_comm with (x:=set_data_stmt s) (y:=set2_inner_fst _ _ \cup _).
rewrite 3!set_union_assoc.
rewrite set_union_comm with (x:=set_data_prog p). rewrite 2!set_union_assoc.
rewrite set_union_comm with (x:=set_data_prog q). rewrite 2!set_union_assoc.
reflexivity.
Qed.
Lemma is_flatR_of_prog_set_data_incl : ∀ q p : prog,
is_flatR_of_prog q p → set_data_prog q \subseteq set_data_prog p.
Proof.
apply (is_flatR_of_prog_mutual_ind
(fun q p H ⇒
set_data_prog q \subseteq set_data_prog p)
(fun q s H ⇒
set_data_prog q \subseteq set_data_stmt s)); intros; try apply set_incl_refl.
- simpl. rewrite set_data_prog_seq. intros a. destruct a.
rewrite 4!set_union_In. rewrite 2!set2_inner_fst_In. intros.
decompose [or] H1.
+ left. destruct H2 as [i' [H2 H3]]. ∃ i'. split.
× rewrite <- maydef_prog_single. rewrite <- is_flatR_of_prog_single in i.
apply (is_flatR_of_prog_maydef_incl _ _ i). assumption.
× apply (is_flatR_of_prog_mayread_incl _ _ i0). assumption.
+ right; left. apply H; assumption.
+ right; right. apply H0; assumption.
- simpl. rewrite set2_inner_fst_emptyset_l. rewrite 2!set_same_union_empty_l.
unfold set_incl; intros. rewrite set_union_In. left. apply H; assumption.
- simpl. rewrite set2_inner_fst_emptyset_l. rewrite 2!set_same_union_empty_l.
unfold set_incl; intros. rewrite set_union_In. right. apply H; assumption.
- unfold set_incl; intros. simpl in H1. rewrite set2_inner_fst_emptyset_l in H1.
rewrite 2!set_same_union_empty_l in H1. rewrite set_data_prog_seq in H1.
rewrite 2!set_union_In in H1.
decompose [or] H1; clear H1.
+ destruct a. rewrite set2_inner_fst_In in H2. destruct H2 as [i' [H1 H2]].
simpl set_data_stmt.
simpl. rewrite set_union_In. left. rewrite set2_inner_fst_In.
∃ i'. split. apply (is_flatR_of_prog_maydef_incl _ _ i0). assumption.
replace (_ \cup _) with (mayread_stmt (WHILE << l >> b DO p END)) by reflexivity.
apply is_flatR_of_prog_single in i. rewrite <- mayread_prog_single.
apply (is_flatR_of_prog_mayread_incl _ _ i). assumption.
+ simpl. rewrite set_union_In; right. apply H0. assumption.
+ apply H; assumption.
- simpl. rewrite set2_inner_fst_emptyset_l. rewrite 2!set_same_union_empty_l.
unfold set_incl; intros. inversion H.
Qed.
Lemma set_data_prog_correct : ∀ p l l',
(l, l') \in set_data_prog p ↔ data_depsR_prog p l l'.
Proof.
split; revert p l l'.
- apply (prog_mutual_ind
(fun p ⇒ ∀ l l', (l, l') \in set_data_prog p → data_depsR_prog p l l')
(fun s ⇒ ∀ l l', (l, l') \in set_data_stmt s → data_depsR_prog {{s}} l l'));
intros.
+ inversion H.
+ simpl in H1. rewrite 2!set_union_In in H1.
decompose [or] H1; clear H1.
× rewrite set2_inner_fst_In in H2.
inversion H2 as [i [H3 H4]]; clear H2.
rewrite <- maydef_prog_single in H3.
apply maydef_flat in H3.
apply mayread_flat in H4.
decompose_ex H3. decompose_ex H4.
decompose [and] H3; clear H3. decompose [and] H4; clear H4.
assert (is_flatR_prog q) as Ha1.
{ apply is_flatR_of_prog_is_flatR with (p:={{s}}); assumption. }
apply is_flatR_of_prog_single in H7.
assert (is_flatR_prog q1 ∧ is_flatR_stmt s0 ∧ is_flatR_prog q2) as Ha2.
{
repeat split.
- apply is_flatR_prog_app_reverse with (q:=s0;;q2).
rewrite <- H1. 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 <- H1. assumption.
- apply is_flatR_prog_app_reverse with (p:=q1+;+{{s0}}).
rewrite <- seq_assoc.
simpl. rewrite <- H1; assumption.
}
assert (is_flatR_prog q0) as Ha3.
{ apply is_flatR_of_prog_is_flatR with (p:=p); assumption. }
assert (is_flatR_prog q3 ∧ is_flatR_stmt s1 ∧ is_flatR_prog q4) as Ha4.
{
repeat split.
- apply is_flatR_prog_app_reverse with (q:=s1;;q4).
rewrite <- H3. assumption.
- apply is_flatR_prog_single.
apply is_flatR_prog_app_reverse with (q:=q4).
apply is_flatR_prog_app_reverse with (p:=q3).
simpl. rewrite <- H3. assumption.
- apply is_flatR_prog_app_reverse with (p:=q3+;+{{s1}}).
rewrite <- seq_assoc.
simpl. rewrite <- H3; assumption.
}
{ apply DDP_flat with (p:=q+;+q0).
- constructor; assumption.
- rewrite H1, H3. rewrite <- seq_assoc.
apply flat_data_depsR_prog_grow_r.
simpl. rewrite seq_assoc.
apply is_flatR_stmt_maydef in H5; try (apply Ha2).
apply is_flatR_stmt_mayread in H8; try (apply Ha4).
destruct H5, H8. subst.
apply flat_data_depsR_prog_grow_m with (i:=i).
+ assumption.
+ apply FDP_here with (i:=i); assumption.
+ rewrite ass_inR_prog_seq. rewrite not_or_iff. split.
× rewrite <- is_flatR_prog_mustdef. assumption. apply Ha2.
× rewrite <- is_flatR_prog_mustdef. assumption. apply Ha4. }
× apply data_depsR_prog_here. apply H; assumption.
× apply data_depsR_prog_after. apply H0; assumption.
+ inversion H.
+ inversion H.
+ simpl in H1. rewrite set_union_In in H1. destruct H1.
× apply H in H1. inversion H1.
apply DDP_flat with (p:=(ASSERT << l >> b =>> l);;p1).
apply is_flatR_of_prog_single.
constructor. assumption.
apply FDP_after.
assumption.
× apply H0 in H1. inversion H1.
apply DDP_flat with (p:=(ASSERT << l >> B_not b =>> l);;p1).
apply is_flatR_of_prog_single.
constructor. assumption.
apply FDP_after.
assumption.
+ simpl in H0. rewrite set_union_In in H0. destruct H0.
× rewrite set2_inner_fst_In in H0.
destruct H0 as [i [H0 H1]].
rewrite set_union_In in H1.
apply maydef_flat in H0. decompose_ex H0. decompose [and] H0; clear H0.
assert (is_flatR_prog q) as Ha1.
{ apply is_flatR_of_prog_is_flatR with (p:=p); assumption. }
assert (is_flatR_prog q1 ∧ is_flatR_stmt s ∧ is_flatR_prog q2) as Ha2.
{
repeat split.
- apply is_flatR_prog_app_reverse with (q:=s;;q2).
rewrite <- H2. 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. assumption.
- apply is_flatR_prog_app_reverse with (p:=q1+;+{{s}}).
rewrite <- seq_assoc.
simpl. rewrite <- H2; assumption.
}
apply is_flatR_stmt_maydef in H4; try apply Ha2.
destruct H4.
{ destruct H1.
- apply DDP_flat with (p:=(ASSERT <<l >> b =>> l);;q+;+{{ASSERT << l >> B_not b =>> l}}).
+ apply is_flatR_of_prog_single. repeat constructor. assumption.
+ rewrite set_map_In in H1.
destruct H1 as [i0 [H7 H8]].
inversion H8; subst i l'.
apply FDP_after. rewrite H2. rewrite <- seq_assoc.
apply flat_data_depsR_prog_grow_r.
apply flat_data_depsR_prog_grow_m with (i:=i0).
× assumption.
× subst l0. apply FDP_here with (i:=i0).
assumption. do 2 constructor. apply set_of_id_bexp_correct; assumption.
× rewrite <- is_flatR_prog_mustdef. assumption. apply Ha2.
- apply mayread_flat in H1. decompose_ex H1. decompose [and] H1; clear H1.
assert (is_flatR_prog q0) as Ha3.
{ apply is_flatR_of_prog_is_flatR with (p:=p); assumption. }
assert (is_flatR_prog q3 ∧ is_flatR_stmt s0 ∧ is_flatR_prog q4) as Ha5.
{
repeat split.
- apply is_flatR_prog_app_reverse with (q:=s0;;q4).
rewrite <- H5. assumption.
- apply is_flatR_prog_single.
apply is_flatR_prog_app_reverse with (q:=q4).
apply is_flatR_prog_app_reverse with (p:=q3).
simpl. rewrite <- H5. assumption.
- apply is_flatR_prog_app_reverse with (p:=q3+;+{{s0}}).
rewrite <- seq_assoc.
simpl. rewrite <- H5; assumption.
}
apply DDP_flat with (p:=(ASSERT << l >> b =>> l);; q +;+
(ASSERT << l >> b =>> l);; q0 +;+
{{ASSERT << l >> B_not b =>> l}}).
+ apply is_flatR_of_prog_single. repeat constructor; assumption.
+ apply FDP_after. rewrite H2. rewrite <- seq_assoc.
apply flat_data_depsR_prog_grow_r.
simpl. apply flat_data_depsR_prog_grow_m with (i:=i).
assumption.
apply flat_data_depsR_prog_unrel with (i:=i). assumption.
intros contra; inversion contra.
rewrite H5. rewrite <- seq_assoc.
apply flat_data_depsR_prog_grow_m with (i:=i).
assumption.
simpl. apply is_flatR_stmt_mayread in H8.
destruct H8. subst l0 l'.
apply FDP_here with (i:=i); assumption.
apply Ha5. rewrite <- is_flatR_prog_mustdef. assumption.
apply Ha5. rewrite <- is_flatR_prog_mustdef. assumption.
apply Ha2. }
× apply H in H0. inversion H0; subst.
{ apply DDP_flat with (p:=(ASSERT << l >> b =>> l);; p0 +;+
{{ASSERT << l >> B_not b =>> l}}).
- apply is_flatR_of_prog_single. apply IFOS_while_loop; try assumption.
apply IFOS_while_end.
- apply FDP_after. apply flat_data_depsR_prog_grow_l. assumption. }
+ inversion H.
- intros. inversion H; subst.
apply is_flatR_of_prog_set_data_incl with (q:=p0); try assumption.
apply flat_data_depsR_prog_decomposition in H1.
decompose_ex H1. decompose [and] H1; clear H1.
rewrite H2. rewrite set_data_prog_seq.
rewrite 2!set_union_In.
right; right. simpl. rewrite set_union_In; left.
rewrite mayread_prog_seq. simpl. rewrite set2_diff_fst_union_distr_l.
rewrite 2!set2_inner_fst_union_distr_r. rewrite 2!set_union_In.
right; left.
rewrite set2_inner_fst_In. ∃ i. split.
+ rewrite is_flatR_stmt_maydef. subst l. split; try assumption; try reflexivity.
apply is_flatR_prog_single.
apply is_flatR_prog_app_reverse with (p:=p1).
apply is_flatR_prog_app_reverse with (q:=p2+;+{{s2}}+;+p3).
rewrite <- seq_assoc. simpl.
rewrite <- H2. apply is_flatR_of_prog_is_flatR with (p:=p); assumption.
+ rewrite set2_diff_fst_In. split.
× { rewrite is_flatR_stmt_mayread.
- subst l'. split; try assumption; try reflexivity.
- apply is_flatR_prog_single.
apply is_flatR_prog_app_reverse with (p:=p1+;+s1;;p2).
apply is_flatR_prog_app_reverse with (q:=p3).
rewrite <- 2!seq_assoc. simpl. rewrite <- H2.
apply is_flatR_of_prog_is_flatR with (p:=p); assumption. }
× rewrite is_flatR_prog_mustdef; try assumption.
apply is_flatR_prog_app_reverse with (p:=p1+;+{{s1}}).
apply is_flatR_prog_app_reverse with (q:=s2;;p3).
rewrite <- 2!seq_assoc. simpl. rewrite <- H2.
apply is_flatR_of_prog_is_flatR with (p:=p); assumption.
+ apply is_flatR_of_prog_is_flatR with (p:=p); assumption.
Qed.
Lemma mustdef_prog_exists_maydef :
∀ p i, i \in mustdef_prog p → ∃ l, (i, l) \in maydef_prog p.
Proof.
apply (prog_mutual_ind
(fun p ⇒ ∀ i, i \in mustdef_prog p → ∃ l, (i, l) \in maydef_prog p)
(fun s ⇒ ∀ i, i \in mustdef_stmt s → ∃ l, (i, l) \in maydef_stmt s)); intros.
- inversion H.
- simpl in H1. rewrite set_union_In in H1. destruct (set_In_dec i (mustdef_prog p)).
+ apply H0 in s0. destruct s0 as [l H2].
∃ l. simpl. rewrite set_union_In. right. assumption.
+ destruct H1; try contradiction. apply H in H1. destruct H1 as [l H1].
∃ l. simpl. rewrite set_union_In. left. rewrite set2_diff_fst_In.
split; assumption.
- inversion H.
- simpl in H. apply set_singleton_In in H. subst i0.
∃ l. apply set_singleton_In. reflexivity.
- simpl in H1. rewrite set_inter_In in H1. destruct H1.
apply H in H1. destruct H1 as [l' H1].
∃ l'. simpl. rewrite set_union_In. left; assumption.
- inversion H0.
- inversion H.
Qed.
Lemma mustdef_prog_single : ∀ s,
mustdef_prog {{s}} \equiv mustdef_stmt s.
Proof.
intros.
simpl. rewrite set_same_union_empty_r.
reflexivity.
Qed.