Library control

Require Export prog.
Require Export label.
Require Export set_prog.
Require Import quotient.
Require Import seq.
Require Import set_relation.
Require Import set_instance.

Inductive control_depsR_prog : prog → relation label :=
  | CDP_here : ∀ s p l l', control_depsR_stmt s l l' →
      control_depsR_prog (s;;p) l l'
  | CDP_after : ∀ s p l l', control_depsR_prog p l l' →
      control_depsR_prog (s;;p) l l'
with control_depsR_stmt : stmt → relation label :=
  | CDS_ifb_l : ∀ l b p1 p2 l' l'', control_depsR_prog p1 l' l'' →
      control_depsR_stmt (IFB << l >> b THEN p1 ELSE p2 FI) l' l''
  | CDS_ifb_r : ∀ l b p1 p2 l' l'', control_depsR_prog p2 l' l'' →
      control_depsR_stmt (IFB << l >> b THEN p1 ELSE p2 FI) l' l''
  | CDS_ifb_cond_l : ∀ l l' b p1 p2, label_first_inR_prog p1 l' →
      control_depsR_stmt
        (IFB << l >> b THEN p1 ELSE p2 FI) l l'
  | CDS_ifb_cond_r : ∀ l l' b p1 p2, label_first_inR_prog p2 l' →
      control_depsR_stmt
        (IFB << l >> b THEN p1 ELSE p2 FI) l l'
  | CDS_while : ∀ l b p l' l'', control_depsR_prog p l' l'' →
      control_depsR_stmt (WHILE << l >> b DO p END) l' l''
  | CDS_while_cond : ∀ l l' b p, label_first_inR_prog p l' →
      control_depsR_stmt
        (WHILE << l >> b DO p END) l l'.

Scheme control_depsR_prog_mutual_ind :=
    Induction for control_depsR_prog Sort Prop
  with control_depsR_stmt_mutual_ind :=
    Induction for control_depsR_stmt Sort Prop.

Fixpoint keep_L_prog (p:prog) (L:set label) :=
  match p with
  | {{}} ⇒ {{}}
  | s;;q ⇒ if set_mem (stmt_get_label s) L then
              keep_L_stmt s L;;keep_L_prog q L
            else keep_L_prog q L
  end
with keep_L_stmt (s:stmt) (L:set label) :=
  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 (keep_L_prog p1 L)
                                                      ELSE (keep_L_prog p2 L) FI
  | WHILE << l >> b DO p END ⇒ WHILE << l >> b DO (keep_L_prog p L) END
  | ASSERT << l >> b =>> l' ⇒ ASSERT << l >> b =>> l'
  end.

Lemma keep_L_prog_quotient : ∀ (p:prog) (L:set label),
  is_quotientR_prog p (keep_L_prog p L).
Proof.
  intros p L. revert p.
  prog_cases (apply (prog_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 include_rt : ∀ {A:Type} R R',
  inclusion A R R' → inclusion A (clos_refl_trans A R) (clos_refl_trans A R').
Proof. unfold inclusion.
  intros. induction H0.
  - apply rt_step. apply H; assumption.
  - apply rt_refl.
  - apply rt_trans with (y:=y); assumption.
Qed.

Lemma control_ifb : ∀ s l',
  label_inR_stmt s l' →
  clos_refl_trans label
    (control_depsR_stmt s) (stmt_get_label s) l'.
Proof.
  prog_cases (apply (stmt_mutual_ind
    (fun p ⇒ ∀ l', label_inR_prog p l' → ∃ s,
      label_first_inR_prog p (stmt_get_label s) ∧
      clos_refl_trans label (control_depsR_prog p) (stmt_get_label s) l')
    (fun s ⇒ ∀ l' : label, label_inR_stmt s l' →
      clos_refl_trans label (control_depsR_stmt s) (stmt_get_label s) l')))
  Case; intros.
  - inversion H.
  - inversion H1.
    + ∃ s. apply H in H5. split.
      × apply LFP_here.
      × apply include_rt with (R':=control_depsR_prog (s;; p)) in H5.
        assumption. unfold inclusion; apply CDP_here.
    + apply H0 in H5. inversion H5 as [s2 H6]. ∃ s2. destruct H6. split.
      × apply LFP_after. assumption.
      × apply include_rt with (R':=control_depsR_prog (s;;p)) in H7. assumption.
        unfold inclusion; apply CDP_after.
  - inversion H. apply rt_refl.
  - inversion H. apply rt_refl.
  - inversion H1.
    + subst. apply rt_refl.
    + apply H in H7. inversion H7 as [s2 H8]. destruct H8.
      apply include_rt with
        (R':=control_depsR_stmt (IFB << l >> b THEN p ELSE p0 FI)) in H9.
      apply rt_trans with (y:=stmt_get_label s2). apply rt_step.
      apply CDS_ifb_cond_l. assumption.
      assumption.
      unfold inclusion; apply CDS_ifb_l.
    + apply H0 in H7. inversion H7 as [s2 H8]. destruct H8.
      apply include_rt with
        (R':=control_depsR_stmt (IFB << l >> b THEN p ELSE p0 FI)) in H9.
      apply rt_trans with (y:=stmt_get_label s2). apply rt_step.
      apply CDS_ifb_cond_r. assumption.
      assumption.
      unfold inclusion; apply CDS_ifb_r.
  - inversion H0.
    + subst. apply rt_refl.
    + apply H in H5. inversion H5 as [s2 H6]. destruct H6.
      apply include_rt with
        (R':=control_depsR_stmt (WHILE << l >> b DO p END)) in H7.
      apply rt_trans with (y:=stmt_get_label s2). apply rt_step.
      apply CDS_while_cond. assumption.
      assumption.
      unfold inclusion; apply CDS_while.
  - inversion H. apply rt_refl.
Qed.

Lemma set_stable_clos : ∀ L d,
  set_stable d L → set_stable (clos_refl_trans label d) L.
Proof.
  unfold set_stable.
  intros.
  induction H1.
  - apply H in H1; assumption.
  - assumption.
  - apply IHclos_refl_trans1. apply IHclos_refl_trans2. assumption.
Qed.

Lemma control_stmt_get_label : ∀ s d L,
  set_stable d L →
  inclusion label (control_depsR_stmt s) d →
  set_mem (stmt_get_label s) L = false →
  set_same (set_inter (set_of_labels_stmt s) L) empty_set.
Proof.
  intros.
  destruct s.
  - simpl in H1. simpl. apply set_inter_not_mem_empty. apply set_mem_complete1.
    assumption.
  - simpl in H1. simpl. apply set_inter_not_mem_empty. apply set_mem_complete1.
    assumption.
  - simpl in H1. simpl. unfold set_same. split.
    + unfold set_incl. intros.
       apply set_inter_elim in H2. destruct H2.
       apply set_stable_clos in H.
       assert (set_In l L).
       { unfold set_stable in H. apply H with (l':=a). assumption.
         apply include_rt in H0. apply H0.
         apply control_ifb.
         apply set_add_elim in H2. destruct H2.
         subst. apply LIS_ifb_cond.
         apply set_union_elim in H2.
         destruct H2. apply LIS_ifb_l.
         apply <- label_inR_prog_iff_in_set_of_labels.
         assumption. apply LIS_ifb_r.
         apply <- label_inR_prog_iff_in_set_of_labels. assumption.
       }
       apply set_mem_correct2 in H4.
       rewrite H1 in H4. inversion H4.
    + unfold set_incl. intros. inversion H2.
  - simpl in H1. simpl. unfold set_same. split.
    + unfold set_incl. intros.
       apply set_inter_elim in H2. destruct H2.
       apply set_stable_clos in H.
       assert (set_In l L).
       { unfold set_stable in H. apply H with (l':=a). assumption.
         apply include_rt in H0. apply H0.
         apply control_ifb.
         apply set_add_elim in H2. destruct H2.
         subst. apply LIS_while_cond. apply LIS_while_body.
         apply <- label_inR_prog_iff_in_set_of_labels.
         assumption.
       }
       apply set_mem_correct2 in H4.
       rewrite H1 in H4. inversion H4.
    + unfold set_incl. intros. inversion H2.
  - simpl in H1. simpl. apply set_inter_not_mem_empty. apply set_mem_complete1.
    assumption.
Qed.

Lemma keep_L_prog_label : ∀ (p:prog) (L:set label) d,
  set_stable d L →
  inclusion label (control_depsR_prog p) d →
  set_same (set_of_labels_prog (keep_L_prog p L)) (set_inter (set_of_labels_prog p) L).
Proof.
  intros p L d H. revert p.
  prog_cases (apply (prog_mutual_ind
    (fun p ⇒ inclusion label (control_depsR_prog p) d →
      set_same (set_of_labels_prog (keep_L_prog p L)) (set_inter (set_of_labels_prog p) L))
    (fun s ⇒ inclusion label (control_depsR_stmt s) d →
      set_same (set_of_labels_prog (keep_L_prog {{s}} L)) (set_inter (set_of_labels_stmt s) L))))
  Case; intros.
  - Case "P_nil". simpl. reflexivity.
  - Case "P_cons". simpl. destruct (set_mem (stmt_get_label s) L) eqn:Heqmem.
    rewrite set_inter_union_distr_l.
    simpl. apply set_same_union. simpl in H0. rewrite Heqmem in H0. apply H0. unfold inclusion.
    intros. apply H2. apply CDP_here; assumption.
    apply H1. unfold inclusion.
    intros. apply H2. apply CDP_after; assumption.
    rewrite set_inter_union_distr_l.
    assert (set_same (set_inter (set_of_labels_stmt s) L) empty_set).
    { apply control_stmt_get_label with (d:=d).
      assumption. unfold inclusion; intros. apply H2. apply CDP_here; assumption.
      assumption.
    }
    transitivity
      (set_union empty_set (set_inter (set_of_labels_prog p) L)).
    symmetry. rewrite set_same_union_empty_l. symmetry.
    apply H1. unfold inclusion; intros; apply H2; apply CDP_after; assumption.
    apply set_same_union. symmetry; assumption.
    reflexivity.
  - Case "S_skip". simpl. destruct (set_mem l L) eqn:Heqmem.
    + transitivity (set_singleton l). reflexivity.
      symmetry. apply set_inter_mem_singleton.
      apply set_mem_correct1; assumption.
    + simpl. symmetry. apply set_inter_not_mem_empty.
      apply set_mem_complete1; assumption.
  - Case "S_ass". simpl. destruct (set_mem l L) eqn:Heqmem.
    + transitivity (set_singleton l). reflexivity.
      symmetry. apply set_inter_mem_singleton.
      apply set_mem_correct1; assumption.
    + simpl. symmetry. apply set_inter_not_mem_empty.
      apply set_mem_complete1; assumption.
  - Case "S_ifb". simpl. destruct (set_mem l L) eqn:Heqmem.
    + simpl.
      rewrite set_same_union_empty_r.
      rewrite <- 2!set_same_union_add_singleton.
      rewrite 2!set_inter_union_distr_l.
      apply set_same_union.
      symmetry. apply set_inter_mem_singleton.
      apply set_mem_correct1; assumption.
      apply set_same_union.
      apply H0. unfold inclusion; intros. apply H2. apply CDS_ifb_l; assumption.
      apply H1. unfold inclusion; intros. apply H2. apply CDS_ifb_r; assumption.
    + simpl.
      remember (IFB << l >> b THEN p ELSE p0 FI) as s.
      assert (set_same (set_inter (set_of_labels_stmt s) L) empty_set).
      {
        apply control_stmt_get_label with (d:=d).
        assumption.
        assumption.
        rewrite Heqs. assumption.
      }
      rewrite Heqs in H3. simpl in H3.
      symmetry. assumption.
  - Case "S_while". simpl. destruct (set_mem l L) eqn:Heqmem.
    + simpl. rewrite <- 2!set_same_union_add_singleton.
      rewrite set_inter_union_distr_l.
      rewrite set_same_union_empty_r.
      apply set_same_union.
      symmetry. apply set_inter_mem_singleton.
      apply set_mem_correct1; assumption.
      apply H0. unfold inclusion; intros. apply H1. apply CDS_while; assumption.
    + remember (WHILE << l >> b DO p END) as s.
      assert (set_same (set_inter (set_of_labels_stmt s) L) empty_set).
      {
        apply control_stmt_get_label with (d:=d).
        assumption.
        assumption.
        rewrite Heqs. assumption.
      }
      rewrite Heqs in H2. simpl in H2.
      symmetry. assumption.
  - Case "S_assert". simpl. destruct (set_mem l L) eqn:Heqmem.
    + transitivity (set_singleton l). reflexivity.
      symmetry. apply set_inter_mem_singleton.
      apply set_mem_correct1; assumption.
    + simpl. symmetry. apply set_inter_not_mem_empty.
      apply set_mem_complete1; assumption.
Qed.

Lemma control_depsR_label_inR_prog : ∀ p l l',
  control_depsR_prog p l l' →
  label_inR_prog p l' ∧
  label_inR_prog p l.
Proof.
  apply (control_depsR_prog_mutual_ind
    (fun p l l' H ⇒ label_inR_prog p l' ∧ label_inR_prog p l)
    (fun s l l' H ⇒ label_inR_stmt s l' ∧ label_inR_stmt s l)); intros.
  - destruct H. split; apply LIP_here; assumption.
  - destruct H. split; apply LIP_after; assumption.
  - destruct H. split; apply LIS_ifb_l; assumption.
  - destruct H. split; apply LIS_ifb_r; assumption.
  - split.
    + apply LIS_ifb_l. apply label_first_label_inR_prog. assumption.
    + apply LIS_ifb_cond.
  - split.
    + apply LIS_ifb_r. apply label_first_label_inR_prog. assumption.
    + apply LIS_ifb_cond.
  - destruct H. split; apply LIS_while_body; assumption.
  - split.
    + apply LIS_while_body. apply label_first_label_inR_prog. assumption.
    + apply LIS_while_cond.
Qed.

Lemma trans_control_depsR_label_inR_prog : ∀ p l l',
  clos_refl_trans label (control_depsR_prog p) l l' →
  label_inR_prog p l' →
  label_inR_prog p l.
Proof.
  intros. induction H as [l l'|l|l l' l''].
  - apply control_depsR_label_inR_prog in H. destruct H; assumption.
  - assumption.
  - apply IHclos_refl_trans1. apply IHclos_refl_trans2.
    assumption.
Qed.

Lemma control_depsR_prog_stable : ∀ p,
  set_stable (control_depsR_prog p) (set_of_labels_prog p).
Proof. unfold set_stable.
  intros. apply label_inR_prog_iff_in_set_of_labels.
  apply control_depsR_label_inR_prog with (l':=l'). assumption.
Qed.

Fixpoint set_label_first_prog (p:prog) :=
  match p with
  | {{}} ⇒ \emptyset
  | s;;q ⇒ set_add (stmt_get_label s) (set_label_first_prog q)
  end.

Lemma set_label_first_prog_correct : ∀ p l,
  l \in set_label_first_prog p ↔ label_first_inR_prog p l.
Proof.
  intros p. induction p; intros.
  - simpl. split; intros; inversion H.
  - simpl. split; intros.
    + apply set_add_elim in H. destruct H.
      × subst l. apply LFP_here.
      × apply LFP_after. apply IHp. assumption.
    + inversion H.
      × apply set_add_intro2. reflexivity.
      × apply set_add_intro1. apply IHp. assumption.
Qed.

Fixpoint set_control_prog (p:prog) : set(label×label) :=
  match p with
  | {{}} ⇒ \emptyset
  | s;;q ⇒ set_control_stmt s \cup set_control_prog q
  end
with set_control_stmt (s:stmt) : set(label×label) :=
  match s with
  | SKIP << _ >> ⇒ \emptyset
  | _ ::= _ << _ >> ⇒ \emptyset
  | IFB << l >> _ THEN p1 ELSE p2 FI ⇒
      set_map (fun l' ⇒ (l, l')) (set_label_first_prog p1 \cup set_label_first_prog p2)
      \cup set_control_prog p1 \cup set_control_prog p2
  | WHILE << l >> _ DO p END ⇒
      set_map (fun l' ⇒ (l, l')) (set_label_first_prog p) \cup set_control_prog p
  | ASSERT << _ >> _ =>> _ ⇒ \emptyset
  end.

Lemma set_control_prog_correct : ∀ p l l',
  (l, l') \in set_control_prog p ↔ control_depsR_prog p l l'.
Proof.
  apply (prog_mutual_ind
    (fun p ⇒ ∀ l l', (l, l') \in set_control_prog p ↔ control_depsR_prog p l l')
    (fun s ⇒ ∀ l l', (l, l') \in set_control_stmt s ↔ control_depsR_stmt s l l'));
  intros; simpl; try (split; intros; inversion H; fail).
  - rewrite set_union_In. rewrite H, H0. split; intros.
    + destruct H1.
      × apply CDP_here; assumption.
      × apply CDP_after; assumption.
    + inversion H1.
      × left; assumption.
      × right; assumption.
  - rewrite 2!set_union_In. rewrite H, H0. split; intros.
    + decompose [or] H1; clear H1.
      × rewrite set_map_In in H2. destruct H2 as [a [H2 H3]]. inversion H3; subst.
        rewrite set_union_In in H2. { destruct H2.
        - apply CDS_ifb_cond_l. apply set_label_first_prog_correct. assumption.
        - apply CDS_ifb_cond_r. apply set_label_first_prog_correct. assumption. }
      × apply CDS_ifb_l; assumption.
      × apply CDS_ifb_r; assumption.
    + inversion H1; subst.
      × right; left. assumption.
      × right; right. assumption.
      × left. rewrite set_map_In. ∃ l'. split; try reflexivity.
        rewrite set_union_In. left. apply set_label_first_prog_correct; assumption.
      × left. rewrite set_map_In. ∃ l'. split; try reflexivity.
        rewrite set_union_In. right. apply set_label_first_prog_correct; assumption.
  - rewrite set_union_In. rewrite H. split; intros.
    + destruct H0.
      × rewrite set_map_In in H0. destruct H0 as [l'' [H0 H1]].
        inversion H1; subst. apply CDS_while_cond.
        apply set_label_first_prog_correct; assumption.
      × apply CDS_while; assumption.
    + inversion H0; subst.
      × right. assumption.
      × left. rewrite set_map_In. ∃ l'. split; try reflexivity.
        apply set_label_first_prog_correct; assumption.
Qed.