Library data
Definition of the data dependence using an inductive type data_depsR_prog
using dependences on flat programs flat_data_depsR_prog,
corresponding to finite syntactic paths.
Require Export prog.
Require Export set_prog.
Require Import set_relation.
Require Import label.
Require Import seq.
Require Import quotient.
Require Recdef.
Require Import Relation_Definitions.
Inductive is_flatR_of_prog : prog → prog → Prop :=
| IFOP_nil : is_flatR_of_prog {{}} {{}}
| IFOP_cons : ∀ s p p1 p1', is_flatR_of_stmt p s → is_flatR_of_prog p1 p1' →
is_flatR_of_prog (p+;+p1) (s;;p1')
with is_flatR_of_stmt : prog → stmt → Prop :=
| IFOS_skip : ∀ l, is_flatR_of_stmt {{SKIP << l >>}} (SKIP << l >>)
| IFOS_ass : ∀ i a l, is_flatR_of_stmt {{i ::= a << l >>}} (i ::= a << l >>)
| IFOS_ifb_l : ∀ l b p1 p2 q, is_flatR_of_prog q p1 →
is_flatR_of_stmt ((ASSERT << l >> b =>> l);;q) (IFB << l >> b THEN p1 ELSE p2 FI)
| IFOS_ifb_r : ∀ l b p1 p2 q, is_flatR_of_prog q p2 →
is_flatR_of_stmt ((ASSERT << l >> (B_not b) =>> l);;q) (IFB << l >> b THEN p1 ELSE p2 FI)
| IFOS_while_loop : ∀ l b p q0 q, is_flatR_of_stmt q0 (WHILE << l >> b DO p END) →
is_flatR_of_prog q p →
is_flatR_of_stmt ((ASSERT << l >> b =>> l);; q +;+q0) (WHILE << l >> b DO p END)
| IFOS_while_end : ∀ l b p,
is_flatR_of_stmt {{ASSERT << l >> (B_not b) =>> l}} (WHILE << l >> b DO p END)
| IFOS_assert : ∀ l b l', is_flatR_of_stmt {{ASSERT << l >> b =>> l'}} (ASSERT << l >> b =>> l').
Scheme is_flatR_of_prog_mutual_ind := Induction for is_flatR_of_prog Sort Prop
with is_flatR_of_stmt_mutual_ind := Induction for is_flatR_of_stmt Sort Prop.
Inductive stmt_is_assR : stmt → Prop :=
| SIA_ass : ∀ a l i,
stmt_is_assR (i::=a <<l>>).
Inductive stmt_is_assR_id : stmt → id → Prop :=
| SIAI_ass : ∀ a l i,
stmt_is_assR_id (i::=a <<l>>) i.
Inductive id_inR_ref : stmt → id → Prop :=
| IIR_ass : ∀ a l i i', id_inR_aexp a i' → id_inR_ref (i::=a <<l>>) i'
| IIR_ifb : ∀ l b p1 p2 i, id_inR_bexp b i →
id_inR_ref (IFB << l >> b THEN p1 ELSE p2 FI) i
| IIR_while : ∀ l b p i, id_inR_bexp b i →
id_inR_ref (WHILE << l >> b DO p END) i
| IIR_assert : ∀ b l l' i, id_inR_bexp b i →
id_inR_ref (ASSERT << l >> b =>> l') i.
Inductive ass_inR_prog : prog → id → Prop :=
| AIP_here : ∀ s p i, ass_inR_stmt s i →
ass_inR_prog (s;;p) i
| AIP_after : ∀ s p i, ass_inR_prog p i →
ass_inR_prog (s;;p) i
with ass_inR_stmt : stmt → id → Prop :=
| AIS_ass : ∀ a l i, ass_inR_stmt (i::=a <<l>>) i
| AIS_ifb_l : ∀ l b p1 p2 i, ass_inR_prog p1 i →
ass_inR_stmt (IFB << l >> b THEN p1 ELSE p2 FI) i
| AIS_ifb_r : ∀ l b p1 p2 i, ass_inR_prog p2 i →
ass_inR_stmt (IFB << l >> b THEN p1 ELSE p2 FI) i
| AIS_while : ∀ l b p i, ass_inR_prog p i →
ass_inR_stmt (WHILE << l >> b DO p END) i.
Lemma stmt_is_assR_dec : ∀ s,
{stmt_is_assR s} + {¬ stmt_is_assR s}.
Proof.
intros. destruct s;
try (right; intros contra; now inversion contra).
left; constructor.
Qed.
Lemma stmt_is_assR_id_dec : ∀ s i,
{stmt_is_assR_id s i} + {¬ stmt_is_assR_id s i}.
Proof.
intros. destruct s;
try (right; intros contra; now inversion contra).
destruct (eq_id_dec i0 i).
left; subst; constructor.
right; intros contra; inversion contra; apply n; assumption.
Qed.
Lemma ass_inR_prog_dec : ∀ p i,
{ ass_inR_prog p i } + { ¬ ass_inR_prog p i}.
Proof.
apply (prog_mutual_rect
(fun p ⇒ ∀ i, { ass_inR_prog p i } + { ¬ ass_inR_prog p i})
(fun s ⇒ ∀ i, { ass_inR_stmt s i } + { ¬ ass_inR_stmt s i}));
intros; try now (right; intros contra; inversion contra).
- destruct (H i).
+ left; apply AIP_here; assumption.
+ destruct (H0 i).
× left; apply AIP_after; assumption.
× right. intros contra. inversion contra; contradiction.
- destruct (eq_id_dec i i0).
+ subst; left; constructor.
+ right; intros contra; inversion contra; contradiction.
- destruct (H i).
+ left; apply AIS_ifb_l; assumption.
+ destruct (H0 i).
× left; apply AIS_ifb_r; assumption.
× right. intros contra. inversion contra; contradiction.
- destruct (H i).
+ left; apply AIS_while; assumption.
+ right. intros contra. inversion contra; contradiction.
Qed.
Inductive flat_data_depsR_prog : prog → relation label :=
| FDP_here : ∀ s i s', stmt_is_assR_id s i →
id_inR_ref s' i → ∀ p,
flat_data_depsR_prog (s;;s';;p) (stmt_get_label s) (stmt_get_label s')
| FDP_unrel : ∀ s i s', stmt_is_assR_id s i →
¬ stmt_is_assR_id s' i → ∀ p l,
flat_data_depsR_prog (s;;p) (stmt_get_label s) l →
flat_data_depsR_prog (s;;s';;p) (stmt_get_label s) l
| FDP_after : ∀ s p l l', flat_data_depsR_prog p l l' →
flat_data_depsR_prog (s;;p) l l'.
Inductive data_depsR_prog : prog → relation label :=
| DDP_flat : ∀ p q, is_flatR_of_prog p q → ∀ l l',
flat_data_depsR_prog p l l' → data_depsR_prog q l l'.
Lemma flat_data_depsR_label_inR_prog : ∀ p l l',
flat_data_depsR_prog p l l' →
label_inR_prog p l' ∧
label_inR_prog p l.
Proof.
intros.
induction H.
- split.
+ apply LIP_after. apply LIP_here. apply stmt_get_label_in_stmt.
+ apply LIP_here. apply stmt_get_label_in_stmt.
- destruct IHflat_data_depsR_prog. split.
+ inversion H2.
× apply LIP_here; assumption.
× apply LIP_after; apply LIP_after; assumption.
+ inversion H3.
× apply LIP_here; assumption.
× apply LIP_after; apply LIP_after; assumption.
- destruct IHflat_data_depsR_prog.
split; apply LIP_after; assumption.
Qed.
Lemma is_flatR_of_prog_label : ∀ p1 p2,
is_flatR_of_prog p1 p2 →
∀ l, label_inR_prog p1 l → label_inR_prog p2 l.
Proof.
apply (is_flatR_of_prog_mutual_ind
(fun p q H ⇒ ∀ l : label, label_inR_prog p l → label_inR_prog q l)
(fun p s H ⇒ ∀ l : label, label_inR_prog p l → label_inR_stmt s l));
intros.
- inversion H.
- apply label_inR_prog_seq in H1.
destruct H1.
+ apply LIP_here. apply H; assumption.
+ apply LIP_after. apply H0; assumption.
- inversion H. assumption. inversion H3.
- inversion H. assumption. inversion H3.
- inversion H0.
+ inversion H4; subst.
apply LIS_ifb_cond.
+ apply LIS_ifb_l. apply H; assumption.
- inversion H0.
+ inversion H4; subst.
apply LIS_ifb_cond.
+ apply LIS_ifb_r. apply H; assumption.
- inversion H1.
+ inversion H5; subst. apply LIS_while_cond; assumption.
+ apply label_inR_prog_seq in H5. destruct H5.
× apply LIS_while_body. apply H0; assumption.
× apply H; assumption.
- inversion H; subst. inversion H3; subst. apply LIS_while_cond; assumption.
inversion H3.
- inversion H. assumption. inversion H3.
Qed.
Lemma data_depsR_label_inR_prog : ∀ p l l',
data_depsR_prog p l l' →
label_inR_prog p l' ∧
label_inR_prog p l.
Proof.
intros. destruct H. pose proof H. apply flat_data_depsR_label_inR_prog in H0.
destruct H0.
split; apply is_flatR_of_prog_label with (p1:=p); assumption.
Qed.
Lemma data_depsR_prog_stable : ∀ p,
set_stable (data_depsR_prog p) (set_of_labels_prog p).
Proof. unfold set_stable.
intros. apply label_inR_prog_iff_in_set_of_labels.
apply data_depsR_label_inR_prog with (l':=l'). assumption.
Qed.
Fixpoint flat_l_prog (p:prog) :=
match p with
| {{}} ⇒ {{}}
| s;;q ⇒ (flat_l_stmt s) +;+ (flat_l_prog q)
end
with flat_l_stmt (s:stmt) :=
match s with
| SKIP << l >> ⇒ {{SKIP << l >>}}
| i ::= a << l >> ⇒ {{i ::= a << l >>}}
| IFB << l >> b THEN p1 ELSE _ FI ⇒ (ASSERT << l >> b =>> l);;flat_l_prog p1
| WHILE << l >> b DO p END ⇒ {{ASSERT << l >> B_not b =>> l}}
| ASSERT << l >> b =>> l' ⇒ {{ASSERT << l >> b =>> l'}}
end.
Lemma is_flatR_of_prog_single : ∀ s q,
is_flatR_of_prog q {{s}} ↔ is_flatR_of_stmt q s.
Proof.
split; intros.
inversion H. inversion H4. subst. rewrite seq_nil_r. assumption.
rewrite <- seq_nil_r at 1.
apply IFOP_cons. assumption. constructor.
Qed.
Lemma flat_l_prog_correct : ∀ p,
is_flatR_of_prog (flat_l_prog p) p.
Proof.
apply (prog_mutual_ind
(fun p ⇒ is_flatR_of_prog (flat_l_prog p) p)
(fun s ⇒ is_flatR_of_stmt (flat_l_stmt s) s)); intros; try now constructor.
Qed.
Lemma flat_l_stmt_correct : ∀ s,
is_flatR_of_stmt (flat_l_stmt s) s.
Proof.
apply (stmt_mutual_ind
(fun p ⇒ is_flatR_of_prog (flat_l_prog p) p)
(fun s ⇒ is_flatR_of_stmt (flat_l_stmt s) s)); intros; try now constructor.
Qed.
Lemma flat_data_depsR_prog_grow_l : ∀ p1 p2 l l',
flat_data_depsR_prog p1 l l' → flat_data_depsR_prog (p1+;+p2) l l'.
Proof.
intros. induction H.
- apply FDP_here with (i:=i); assumption.
- apply FDP_unrel with (i:=i); assumption.
- apply FDP_after; assumption.
Qed.
Lemma flat_data_depsR_prog_grow_r : ∀ p1 p2 l l',
flat_data_depsR_prog p2 l l' → flat_data_depsR_prog (p1+;+p2) l l'.
Proof.
intros. induction p1.
- simpl; assumption.
- apply FDP_after; assumption.
Qed.
Lemma data_depsR_prog_here : ∀ s p l l',
data_depsR_prog {{s}} l l' → data_depsR_prog (s;;p) l l'.
Proof.
intros. inversion H. apply DDP_flat with (p:=p0+;+flat_l_prog p).
apply IFOP_cons. apply is_flatR_of_prog_single. assumption.
apply flat_l_prog_correct.
apply flat_data_depsR_prog_grow_l. assumption.
Qed.
Lemma data_depsR_prog_after : ∀ s p l l',
data_depsR_prog p l l' → data_depsR_prog (s;;p) l l'.
Proof.
intros. inversion H. apply DDP_flat with (p:=(flat_l_stmt s) +;+ p0).
apply IFOP_cons. apply flat_l_stmt_correct. assumption.
apply flat_data_depsR_prog_grow_r. assumption.
Qed.
Definition cons_prog_list (p :prog) (lp:list prog) :=
map (fun q ⇒ p+;+q) lp.
Fixpoint app_prog_list (lp1 lp2 : list prog) :=
match lp1 with
| [] ⇒ []
| p::lp1' ⇒ (cons_prog_list p lp2) ++ (app_prog_list lp1' lp2)
end.
Fixpoint flat_list_prog (p:prog) :=
match p with
| {{}} ⇒ [{{}}]
| s;;q ⇒ app_prog_list (flat_list_stmt s) (flat_list_prog q)
end
with flat_list_stmt (s:stmt) :=
match s with
| SKIP << l >> ⇒ [{{SKIP << l >>}}]
| i::=a << l>> ⇒ [{{i::=a <<l >>}}]
| IFB << l >> b THEN p1 ELSE p2 FI ⇒
(app_prog_list [{{ASSERT <<l>> b =>> l}}]
(flat_list_prog p1)) ++
(app_prog_list [{{ASSERT << l >> B_not b =>> l}}]
(flat_list_prog p2))
| WHILE << l >> b DO p END ⇒
[{{ASSERT << l >> B_not b =>> l}}] ++
app_prog_list [{{ASSERT << l >> b =>> l}}]
((app_prog_list (flat_list_prog p)
(app_prog_list [{{ASSERT << l >> b =>> l}}]
(app_prog_list (flat_list_prog p)
[{{ASSERT << l >> B_not b =>> l}}]))))
| ASSERT << l >> b =>> l' ⇒ [{{ASSERT << l >> b =>> l'}}]
end.
Lemma cons_prog_list_nil : ∀ lp,
cons_prog_list {{}} lp = lp.
Proof.
intros. induction lp.
reflexivity.
simpl. rewrite IHlp. reflexivity.
Qed.
Lemma in_cons_prog_list : ∀ p1 lp2 p,
In p (cons_prog_list p1 lp2) ↔
∃ q, p = p1+;+q ∧ In q lp2.
Proof.
split; intros.
- induction lp2.
+ inversion H.
+ simpl in H. destruct H.
× ∃ a. split. rewrite H; reflexivity. simpl; left; reflexivity.
× apply IHlp2 in H. inversion H as [q H0]. ∃ q. destruct H0.
split. assumption. simpl; right; assumption.
- induction lp2.
+ inversion H as [q H0]. destruct H0. inversion H1.
+ simpl. inversion H as [q H0]. destruct H0. simpl in H1.
destruct H1.
× subst; left; reflexivity.
× right; apply IHlp2. ∃ q. split; assumption.
Qed.
Lemma in_app_prog_list : ∀ lp1 lp2 p,
In p (app_prog_list lp1 lp2) ↔
∃ q1 q2, p = q1+;+q2 ∧ In q1 lp1 ∧ In q2 lp2.
Proof.
split; intros.
- induction lp1.
+ inversion H.
+ simpl in H. apply in_app_or in H. destruct H.
× apply in_cons_prog_list in H. inversion H as [q H0].
∃ a. ∃ q. destruct H0. repeat split.
assumption. simpl; left; reflexivity. assumption.
× apply IHlp1 in H. inversion H as [q1 [q2 H0]].
∃ q1. ∃ q2. destruct H0 as [H1 [H2 H3]].
repeat split; try assumption. simpl; right; assumption.
- induction lp1.
+ inversion H as [q1 [q2 H0]]. destruct H0 as [H0 [H1 H2]]. inversion H1.
+ simpl. apply in_or_app. inversion H as [q1 [q2 H0]].
destruct H0 as [H0 [H1 H2]].
simpl in H1. destruct H1.
× left; subst. apply in_cons_prog_list. ∃ q2.
split. reflexivity. assumption.
× right. apply IHlp1. ∃ q1. ∃ q2. repeat split; assumption.
Qed.
Lemma flat_list_prog_correct : ∀ p,
∀ q, In q (flat_list_prog p) → is_flatR_of_prog q p.
Proof.
apply (prog_mutual_ind
(fun p ⇒ ∀ q, In q (flat_list_prog p) → is_flatR_of_prog q p)
(fun s ⇒ ∀ q, In q (flat_list_stmt s) → is_flatR_of_stmt q s));
intros.
- inversion H. subst. constructor. inversion H0.
- simpl in H1. apply in_app_prog_list in H1. inversion H1 as [q1 [q2 H2]].
destruct H2 as [H2 [H3 H4]]. subst q.
apply IFOP_cons. apply H; assumption. apply H0; assumption.
- simpl in H. destruct H. subst; constructor. inversion H.
- simpl in H. destruct H. subst; constructor. inversion H.
- simpl in H1. rewrite 2!app_nil_r in H1. apply in_app_iff in H1.
destruct H1.
+ apply in_cons_prog_list in H1.
inversion H1 as [q0 [H2 H3]]. rewrite H2. constructor.
apply H. assumption.
+ apply in_cons_prog_list in H1.
inversion H1 as [q0 [H2 H3]]. rewrite H2. constructor.
apply H0. assumption.
- simpl in H0. destruct H0.
+ subst q. apply IFOS_while_end.
+ rewrite 2!app_nil_r in H0. apply in_cons_prog_list in H0.
inversion H0 as [q0 H1]. destruct H1.
apply in_app_prog_list in H2. inversion H2 as [q1 [q2 [H3 [H4 H5]]]].
apply in_cons_prog_list in H5. inversion H5 as [q3 H6].
destruct H6. apply in_app_prog_list in H7.
inversion H7 as [q4 [q5 [H8 [H9 H10]]]]. subst.
apply IFOS_while_loop with (q0:={{ASSERT << l >> b =>> l}} +;+ q4 +;+ q5).
simpl.
apply IFOS_while_loop.
inversion H10. subst. apply IFOS_while_end. inversion H1.
apply H; assumption. apply H; assumption.
- simpl in H. destruct H. subst; constructor. inversion H.
Qed.
Fixpoint id_in_aexp (a:aexp) (i:id) :=
match a with
| A_num n ⇒ false
| A_id i' ⇒ if eq_id_dec i i' then true else false
| A_plus a1 a2 ⇒ (id_in_aexp a1 i) || (id_in_aexp a2 i)
| A_minus a1 a2 ⇒ (id_in_aexp a1 i) || (id_in_aexp a2 i)
| A_mult a1 a2 ⇒ (id_in_aexp a1 i) || (id_in_aexp a2 i)
end.
Lemma id_in_aexp_correct : ∀ a i,
id_in_aexp a i = true ↔ id_inR_aexp a i.
Proof.
split; intros.
- induction a; simpl in H.
+ inversion H.
+ destruct (eq_id_dec i i0).
subst. constructor. inversion H.
+ apply orb_true_iff in H. destruct H.
apply IIA_plus_l; apply IHa1; assumption.
apply IIA_plus_r; apply IHa2; assumption.
+ apply orb_true_iff in H. destruct H.
apply IIA_minus_l; apply IHa1; assumption.
apply IIA_minus_r; apply IHa2; assumption.
+ apply orb_true_iff in H. destruct H.
apply IIA_mult_l; apply IHa1; assumption.
apply IIA_mult_r; apply IHa2; assumption.
- induction H; simpl.
+ destruct (eq_id_dec i i). reflexivity. contradiction n; reflexivity.
+ rewrite IHid_inR_aexp. reflexivity.
+ rewrite IHid_inR_aexp. apply orb_true_r.
+ rewrite IHid_inR_aexp. reflexivity.
+ rewrite IHid_inR_aexp. apply orb_true_r.
+ rewrite IHid_inR_aexp. reflexivity.
+ rewrite IHid_inR_aexp. apply orb_true_r.
Qed.
Fixpoint id_in_bexp (b:bexp) (i:id) :=
match b with
| B_true ⇒ false
| B_false ⇒ false
| B_eq a1 a2 ⇒ (id_in_aexp a1 i) || (id_in_aexp a2 i)
| B_le a1 a2 ⇒ (id_in_aexp a1 i) || (id_in_aexp a2 i)
| B_not b' ⇒ id_in_bexp b' i
| B_and b1 b2 ⇒ (id_in_bexp b1 i) || (id_in_bexp b2 i)
end.
Lemma id_in_bexp_correct : ∀ b i,
id_in_bexp b i = true ↔ id_inR_bexp b i.
Proof.
split; intros.
- induction b; simpl in H.
+ inversion H.
+ inversion H.
+ apply orb_true_iff in H. destruct H.
apply IIB_eq_l. apply id_in_aexp_correct; assumption.
apply IIB_eq_r. apply id_in_aexp_correct; assumption.
+ apply orb_true_iff in H. destruct H.
apply IIB_le_l. apply id_in_aexp_correct; assumption.
apply IIB_le_r. apply id_in_aexp_correct; assumption.
+ constructor. apply IHb; assumption.
+ apply orb_true_iff in H. destruct H.
apply IIB_and_l. apply IHb1; assumption.
apply IIB_and_r. apply IHb2; assumption.
- induction H; simpl.
+ apply id_in_aexp_correct in H. rewrite H. reflexivity.
+ apply id_in_aexp_correct in H. rewrite H. apply orb_true_r.
+ apply id_in_aexp_correct in H. rewrite H. reflexivity.
+ apply id_in_aexp_correct in H. rewrite H. apply orb_true_r.
+ assumption.
+ rewrite IHid_inR_bexp. reflexivity.
+ rewrite IHid_inR_bexp. apply orb_true_r.
Qed.
Definition id_in_ref (s:stmt) (i:id) :=
match s with
| SKIP << _ >> ⇒ false
| _::=a << _ >> ⇒ id_in_aexp a i
| IFB << _ >> b THEN _ ELSE _ FI ⇒ id_in_bexp b i
| WHILE << _ >> b DO _ END ⇒ id_in_bexp b i
| ASSERT << _ >> b =>> _ ⇒ id_in_bexp b i
end.
Lemma id_in_ref_correct : ∀ s i,
id_in_ref s i = true ↔ id_inR_ref s i.
Proof.
split; intros.
- destruct s; simpl in H;
try (constructor; apply id_in_bexp_correct; assumption).
+ inversion H.
+ constructor. apply id_in_aexp_correct. assumption.
- destruct H; simpl; try (apply id_in_bexp_correct; assumption).
+ apply id_in_aexp_correct. assumption.
Qed.
Definition stmt_is_ass_id (s:stmt) (i:id) :=
match s with
| i' ::= _ << _ >> ⇒ if eq_id_dec i i' then true else false
| _ ⇒ false
end.
Lemma stmt_is_ass_id_correct : ∀ s i,
stmt_is_ass_id s i = true ↔ stmt_is_assR_id s i.
Proof.
split; intros.
- destruct s; simpl in H; try now inversion H.
destruct (eq_id_dec i i0). subst. constructor. inversion H.
- destruct H. simpl.
destruct (eq_id_dec i i); [|contradiction n]; reflexivity.
Qed.
Function flat_data_deps_prog (p:prog) l l' {measure num_lab_prog p} :=
match p with
| {{}} ⇒ false
| {{_}} ⇒ false
| s;;s';;q ⇒ if Nat.eqb (stmt_get_label s) l then
match s with
| i ::= a << _ >> ⇒
if id_in_ref s' i && Nat.eqb (stmt_get_label s') l' then
true
else if (stmt_is_ass_id s' i) then
flat_data_deps_prog (s';;q) l l'
else
flat_data_deps_prog (s;;q) l l' ||
flat_data_deps_prog (s';;q) l l'
| _ ⇒ flat_data_deps_prog (s';;q) l l'
end
else flat_data_deps_prog (s';;q) l l'
end.
Proof.
- intros. simpl. apply le_n_S.
replace (S (num_lab_prog q)) with (1 + num_lab_prog q) by reflexivity.
apply le_n.
- intros. simpl. apply le_n.
- intros. simpl. apply le_n.
- intros. simpl. apply le_n_S.
replace (S (num_lab_prog q)) with (1 + num_lab_prog q) by reflexivity.
apply plus_le_compat. apply num_lab_stmt_lt. apply le_n.
- intros. simpl. apply le_n_S. omega.
- intros. simpl. apply le_n_S. omega.
- intros. simpl. apply le_n_S. apply le_n.
- intros. simpl.
unfold lt.
replace (S (num_lab_stmt s' + num_lab_prog q))
with (1 + (num_lab_stmt s' + num_lab_prog q)) by reflexivity.
apply plus_le_compat.
apply num_lab_stmt_lt. apply le_n.
Defined.
Lemma flat_data_deps_prog_correct : ∀ p l l',
flat_data_deps_prog p l l' = true → flat_data_depsR_prog p l l'.
Proof.
intros. functional induction (flat_data_deps_prog p l l').
- inversion H.
- inversion H.
- apply andb_true_iff in e2. destruct e2. apply Nat.eqb_eq in H1.
apply Nat.eqb_eq in e0. rewrite <- H1, <- e0. apply FDP_here with (i:=i).
constructor. apply id_in_ref_correct. assumption.
- apply FDP_after. apply IHb. assumption.
- apply orb_true_iff in H. destruct H.
+ apply Nat.eqb_eq in e0. rewrite <- e0. apply FDP_unrel with (i:=i).
constructor. intros contra. apply stmt_is_ass_id_correct in contra.
rewrite e3 in contra. inversion contra.
rewrite e0. apply IHb. assumption.
+ apply FDP_after. apply IHb0; assumption.
- apply FDP_after. apply IHb; assumption.
- apply FDP_after; apply IHb; assumption.
Qed.
Lemma flat_data_deps_prog_complete : ∀ p l l',
flat_data_depsR_prog p l l' → flat_data_deps_prog p l l' = true.
Proof.
intros.
induction H.
- rewrite flat_data_deps_prog_equation. rewrite (Nat.eqb_refl).
inversion H. apply id_in_ref_correct in H0. rewrite H0.
rewrite Nat.eqb_refl. reflexivity.
- rewrite flat_data_deps_prog_equation.
rewrite (Nat.eqb_refl).
inversion H.
destruct (id_in_ref s' i && (stmt_get_label s' =? l)) eqn:Heqid.
reflexivity.
destruct (stmt_is_ass_id s' i) eqn:Heqass.
apply stmt_is_ass_id_correct in Heqass. contradiction.
apply orb_true_iff. left. subst. assumption.
- rewrite flat_data_deps_prog_equation.
destruct p.
inversion H.
destruct (stmt_get_label s =? l) eqn:Heqlabel; try assumption.
apply Nat.eqb_eq in Heqlabel.
destruct s; try assumption.
destruct (id_in_ref s0 i && (stmt_get_label s0 =? l')) eqn:Heqid.
reflexivity.
destruct (stmt_is_ass_id s0 i) eqn:Heqstmt.
assumption.
apply orb_true_iff. right. assumption.
Qed.
Definition data_deps_prog (p:prog) l l' :=
negb (Nat.eqb (length
(filter (fun q ⇒ flat_data_deps_prog q l l') (flat_list_prog p))) 0).
Lemma negb_filter_list : ∀ A (f:A → bool) l,
negb (Nat.eqb (length (filter f l)) 0) = true ↔
∃ a, In a l ∧ f a = true.
Proof.
split; intros.
- apply negb_true_iff in H. destruct (filter f l) eqn:Heqf.
+ inversion H.
+ ∃ a. apply filter_In. rewrite Heqf. simpl; left; reflexivity.
- inversion H as [a H0]. apply filter_In in H0.
destruct (filter f l).
+ inversion H0.
+ reflexivity.
Qed.
Lemma data_deps_prog_correct : ∀ p l l',
data_deps_prog p l l' = true → data_depsR_prog p l l'.
Proof.
intros. apply negb_filter_list in H.
inversion H as [a H0]. destruct H0.
apply flat_data_deps_prog_correct in H1. apply flat_list_prog_correct in H0.
apply DDP_flat with (p:=a); assumption.
Qed.
Lemma cons_prog_list_app : ∀ p lp1 lp2,
cons_prog_list p (lp1++lp2) =
(cons_prog_list p lp1) ++ (cons_prog_list p lp2).
Proof.
intros. induction lp1.
simpl. reflexivity.
simpl. rewrite IHlp1. reflexivity.
Qed.
Lemma app_prog_list_app_r : ∀ lp1 lp2 lp3,
app_prog_list (lp1 ++ lp2) lp3 =
(app_prog_list lp1 lp3) ++ (app_prog_list lp2 lp3).
Proof.
intros. induction lp1.
simpl. reflexivity.
simpl. rewrite IHlp1. rewrite app_assoc. reflexivity.
Qed.
Lemma in_flat_list_prog_seq : ∀ p q r,
In p (flat_list_prog (q+;+r)) ↔
In p (app_prog_list (flat_list_prog q) (flat_list_prog r)).
Proof.
split; intros.
- revert p r H.
induction q; intros.
simpl in H.
simpl. rewrite cons_prog_list_nil. rewrite app_nil_r. assumption.
simpl in H. simpl.
apply in_app_prog_list in H. inversion H as [q1 [q2 [H0 [H1 H2]]]].
apply IHq in H2.
apply in_app_prog_list in H2.
inversion H2 as [q3 [q4 [H3 [H4 H5]]]].
apply in_app_prog_list. ∃ (q1+;+q3). ∃ q4. repeat split.
rewrite <- seq_assoc. rewrite <- H3. assumption.
apply in_app_prog_list. ∃ q1. ∃ q3.
repeat split; assumption.
assumption.
- revert p r H. induction q; intros.
+ simpl. simpl in H. rewrite cons_prog_list_nil in H.
rewrite app_nil_r in H. assumption.
+ simpl. simpl in H.
apply in_app_prog_list in H.
inversion H as [q1 [q2 [H0 [H1 H2]]]].
apply in_app_prog_list in H1.
inversion H1 as [q3 [q4 [H3 [H4 H5]]]].
apply in_app_prog_list. ∃ q3. ∃ (q4+;+q2). repeat split.
rewrite seq_assoc.
rewrite <- H3. assumption. assumption.
apply IHq. apply in_app_prog_list.
∃ q4. ∃ q2. repeat split; assumption.
Qed.
Inductive is_flatR_prog : prog → Prop :=
| IFP_nil : is_flatR_prog {{}}
| IFP_cons : ∀ s p, is_flatR_stmt s → is_flatR_prog p →
is_flatR_prog (s;;p)
with is_flatR_stmt : stmt → Prop :=
| IFS_skip : ∀ l, is_flatR_stmt (SKIP << l >>)
| IFS_ass : ∀ i a l, is_flatR_stmt (i ::= a << l >>)
| IFS_assert : ∀ l b l', is_flatR_stmt (ASSERT << l >> b =>> l').
Scheme is_flatR_prog_mutual_ind := Induction for is_flatR_prog Sort Prop
with is_flatR_stmt_mutual_ind := Induction for is_flatR_stmt Sort Prop.
Lemma is_flatR_prog_single : ∀ s,
is_flatR_prog {{s}} ↔ is_flatR_stmt s.
Proof.
split; intros.
- inversion H. assumption.
- apply IFP_cons. assumption. apply IFP_nil.
Qed.
Lemma is_quotientR_prog_is_flatR : ∀ p q,
is_quotientR_prog p q →
is_flatR_prog p → is_flatR_prog q.
Proof.
is_quotientR_cases (apply (is_quotientR_prog_mutual_ind
(fun p q H ⇒ is_flatR_prog p → is_flatR_prog q)
(fun s t H ⇒ is_flatR_stmt s → is_flatR_stmt t))) Case;
intros; try now constructor.
- inversion H0. apply H; assumption.
- inversion H1. apply IFP_cons. apply H0; assumption. apply H; assumption.
- inversion H1.
- inversion H0.
Qed.
Inductive id_inR_ref_prog : prog → id → Prop :=
| IIR_here : ∀ s p i, id_inR_ref s i → id_inR_ref_prog (s;;p) i
| IIR_after : ∀ s p i, id_inR_ref_prog p i → id_inR_ref_prog (s;;p) i.
Inductive stmt_inR_prog : stmt → prog → Prop :=
| SIP_here : ∀ s p, stmt_inR_prog s (s;;p)
| SIP_after : ∀ s s' p, stmt_inR_prog s p → stmt_inR_prog s (s';;p).
Lemma is_flatR_of_prog_cut : ∀ p,
is_flatR_prog p → ∀ s, stmt_inR_prog s p →
∃ p1 p2, p = p1 +;+ {{s}} +;+ p2.
Proof.
intros. induction H0.
- ∃ {{}}. ∃ p. simpl. reflexivity.
- inversion H.
apply IHstmt_inR_prog in H4. inversion H4 as [p1 [p2 H5]].
∃ (s';;p1). ∃ p2. simpl. rewrite H5. reflexivity.
Qed.
Lemma id_inR_ref_prog_stmt_inR_prog : ∀ p i,
id_inR_ref_prog p i ↔ ∃ s, stmt_inR_prog s p ∧ id_inR_ref s i.
Proof.
intros. induction p.
- split; intros.
+ inversion H.
+ inversion H as [s [H0 H1]]. inversion H0.
- split; intros.
+ inversion H. ∃ s. split. apply SIP_here. assumption.
apply IHp in H3. inversion H3 as [s' [H4 H5]].
∃ s'. split. apply SIP_after. assumption. assumption.
+ inversion H as [s' [H0 H1]].
inversion H0; subst. apply IIR_here; assumption.
apply IIR_after. apply IHp. ∃ s'. split; assumption.
Qed.
Theorem is_quotientR_prog_nil_r : ∀ (p : prog),
is_quotientR_prog p {{}}.
Proof.
intros. induction p.
- Case "IMP_nil". constructor.
- Case "IMP_app". constructor. 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 flat_data_depsR_prog_grow_m : ∀ s p p' l l' i,
stmt_is_assR_id s i →
flat_data_depsR_prog (s;;p') l l' →
¬ ass_inR_prog p i →
flat_data_depsR_prog (s;;p+;+p') l l'.
Proof.
intros. induction p.
simpl. assumption.
simpl. apply flat_data_depsR_prog_unrel with (i:=i).
assumption.
intros contra. apply H1. apply AIP_here. inversion contra; constructor.
apply IHp. intros contra. apply H1. apply AIP_after; assumption.
Qed.
Lemma flat_data_depsR_prog_decomposition : ∀ p l l',
is_flatR_prog p →
flat_data_depsR_prog p l l' ↔
∃ p1 p2 p3 s1 s2 i, p = p1 +;+ s1;;p2+;+s2;; p3 ∧
stmt_is_assR_id s1 i ∧ ¬ ass_inR_prog p2 i ∧ id_inR_ref s2 i ∧
l = stmt_get_label s1 ∧ l' = stmt_get_label s2.
Proof.
split; intros.
- induction H0; intros.
+ ∃ {{}}. ∃ {{}}. ∃ (p). ∃ s. ∃ s'.
∃ i.
simpl. repeat split.
assumption. intros contra. inversion contra.
assumption.
+ do 2 pose proof H.
apply is_quotientR_prog_is_flatR with (q:={{s'}}) in H3.
apply is_flatR_prog_single in H3.
apply is_quotientR_prog_is_flatR with (q:=s;;p) in H4.
{
apply IHflat_data_depsR_prog in H4.
inversion H4 as [p1 [p2 [p3 [s1 [s2 [i1 H5]]]]]].
destruct H5 as [H6 [H7 [H8 [H9 [H10 H11]]]]].
clear IHflat_data_depsR_prog. clear H4.
destruct p1.
- simpl in H6. inversion H6.
∃ {{}}. ∃ (s';;p2). ∃ p3.
∃ s. ∃ s2. ∃ i. simpl.
subst. inversion H7. inversion H0. subst. inversion H11; subst.
repeat split.
+ intros contra. inversion contra; subst. apply H1.
inversion H3; subst; now inversion H13.
contradiction.
+ assumption.
- simpl in H6. inversion H6. subst s0.
∃ (s;;s';;p1). ∃ p2. ∃ p3. ∃ s1. ∃ s2.
∃ i1.
repeat split; assumption.
}
apply IQP_stmt. apply IQP_remove. apply is_quotientR_refl.
apply is_quotientR_prog_single. apply is_quotientR_refl.
apply IQP_remove. apply IQP_stmt.
apply is_quotientR_prog_nil_r. apply is_quotientR_prog_single.
apply is_quotientR_refl.
+ apply is_quotientR_prog_is_flatR with (q:=p) in H.
apply IHflat_data_depsR_prog in H.
clear IHflat_data_depsR_prog.
inversion H as [p1 [p2 [p3 [s1 [s2 [i1 H1]]]]]].
destruct H1 as [H2 [H3 [H4 [H5 [H6 H7]]]]]. clear H.
∃ (s;;p1). ∃ p2. ∃ p3. ∃ s1. ∃ s2. ∃ i1.
repeat split; try assumption. rewrite H2. reflexivity.
apply IQP_remove. apply is_quotientR_refl.
- inversion H0 as [p1 [p2 [p3 [s1 [s2 [i1 [H1 [H2 [H3 [H4 [H5 H6]]]]]]]]]]].
rewrite H1. apply flat_data_depsR_prog_grow_r. subst l.
apply flat_data_depsR_prog_grow_m with (i:=i1); try assumption.
subst l'.
apply FDP_here with (i:=i1); assumption.
Qed.
Lemma is_flatR_prog_app : ∀ p q,
is_flatR_prog p → is_flatR_prog q → is_flatR_prog (p+;+q).
Proof.
intros. induction H; simpl.
- assumption.
- apply IFP_cons; assumption.
Qed.
Lemma is_flatR_of_prog_is_flatR : ∀ q p,
is_flatR_of_prog q p → is_flatR_prog q.
Proof.
apply (is_flatR_of_prog_mutual_ind
(fun q p H ⇒ is_flatR_prog q)
(fun q s H ⇒ is_flatR_prog q)); intros;
try (now (apply is_flatR_prog_single; constructor));
try (constructor; [ constructor | assumption ]).
- constructor.
- apply is_flatR_prog_app; assumption.
- constructor. constructor.
apply is_flatR_prog_app; assumption.
Qed.
Lemma is_flatR_of_prog_self : ∀ p,
is_flatR_prog p ↔ is_flatR_of_prog p p.
Proof.
split.
- revert p.
apply (is_flatR_prog_mutual_ind
(fun p H ⇒ is_flatR_of_prog p p)
(fun s H ⇒ is_flatR_of_stmt {{s}} s)); intros; try (constructor; fail).
+ replace (s;;p) with ({{s}}+;+p) at 1 by reflexivity.
apply IFOP_cons; assumption.
- intros. apply is_flatR_of_prog_is_flatR with (p:=p); assumption.
Qed.
Lemma app_prog_list_nil_r : ∀ lp,
app_prog_list lp [{{}}] = lp.
Proof. intros. induction lp.
reflexivity.
simpl. rewrite IHlp. rewrite seq_nil_r. reflexivity.
Qed.
Lemma flat_list_prog_single : ∀ s,
flat_list_prog {{s}} = flat_list_stmt s.
Proof. intros.
simpl. apply app_prog_list_nil_r.
Qed.
Fixpoint unfold_while_prog (p:prog) :=
match p with
| {{}} ⇒ {{}}
| s;;q ⇒ (unfold_while_stmt s);; (unfold_while_prog q)
end
with unfold_while_stmt (s:stmt) :=
match s with
| SKIP << l >> ⇒ SKIP << l >>
| i::=a <<l>> ⇒ i::=a <<l>>
| IFB << l >> b THEN p1 ELSE p2 FI ⇒ IFB << l>> b THEN (unfold_while_prog p1)
ELSE (unfold_while_prog p2) FI
| WHILE << l>> b DO p END ⇒
IFB << l>> b THEN (unfold_while_prog p)+;+(ASSERT << l >> b =>> l);;
(unfold_while_prog p)+;+{{ASSERT <<l >> B_not b =>> l}} ELSE {{}} FI
| ASSERT << l >> b =>> l' ⇒ ASSERT << l >> b =>> l'
end.
Lemma is_flatR_of_prog_intro : ∀ p1 p2 q,
is_flatR_of_prog q (p1+;+p2) ↔ ∃ q1 q2, q= q1+;+q2 ∧
is_flatR_of_prog q1 p1 ∧ is_flatR_of_prog q2 p2.
Proof.
intros p1. induction p1; split; intros.
- simpl in H. ∃ {{}}. ∃ q. repeat split. constructor. assumption.
- simpl. inversion H as [q1 [q2 [H0 [H1 H2]]]].
inversion H1. subst. simpl. assumption.
- simpl in H. inversion H. apply IHp1 in H4.
inversion H4 as [q1 [q2 [H5 [H6 H7]]]]. ∃ (p+;+q1). ∃ (q2).
repeat split.
rewrite H5. rewrite seq_assoc. reflexivity.
constructor; assumption.
assumption.
- simpl. inversion H as [q1 [q2 [H0 [H1 H2]]]]. inversion H1.
rewrite H0. rewrite <- H5. rewrite <- seq_assoc.
constructor. assumption. apply IHp1. ∃ p0. ∃ q2.
repeat split; assumption.
Qed.
Lemma unfold_while_prog_is_flatR : ∀ p q,
is_flatR_of_prog q (unfold_while_prog p) → is_flatR_of_prog q p.
Proof.
apply (prog_mutual_ind
(fun p ⇒ ∀ q, is_flatR_of_prog q (unfold_while_prog p) → is_flatR_of_prog q p)
(fun s ⇒ ∀ q, is_flatR_of_stmt q (unfold_while_stmt s) → is_flatR_of_stmt q s));
intros.
- inversion H. constructor.
- simpl in H1. inversion H1. constructor. apply H; assumption.
apply H0; assumption.
- inversion H. constructor.
- inversion H. constructor.
- simpl in H1. inversion H1. constructor. apply H; assumption.
apply IFOS_ifb_r. apply H0; assumption.
- simpl in H0. inversion H0. apply is_flatR_of_prog_intro in H3.
inversion H3 as [q1 [q2 [H7 [H8 H9]]]].
inversion H9. apply is_flatR_of_prog_intro in H14.
inversion H14 as [q3 [q4 [H15 [H16 H17]]]].
rewrite H7. apply IFOS_while_loop.
rewrite <- H12. rewrite H15. inversion H13.
apply is_flatR_of_prog_single in H17. inversion H17.
simpl.
apply IFOS_while_loop. apply IFOS_while_end. apply H. assumption.
apply H; assumption. inversion H3. apply IFOS_while_end.
- simpl in H. inversion H. constructor.
Qed.