Library set_prog

Require Export prog.
Require Export set.
Require Import label.
Require Import set_instance.

Section label.

Fixpoint set_of_labels_prog (p : prog) : set label :=
  match p with
  | {{}} ⇒ empty_set
  | s ;; q ⇒ set_union (set_of_labels_stmt s) (set_of_labels_prog q)
  end
with set_of_labels_stmt (s : stmt) : set label :=
  match s with
  | SKIP << l >> ⇒ \sin l
  | _ ::= _ << l >> ⇒ \sin l
  | IFB << l >> _ THEN p1 ELSE p2 FI ⇒
      l \oplus
        set_of_labels_prog p1 \cup set_of_labels_prog p2
  | WHILE << l >> _ DO p1 END ⇒ l \oplus set_of_labels_prog p1
  | ASSERT << l >> _ =>> _ ⇒ set_singleton l
  end.

Lemma set_of_labels_prog_seq : ∀ p q,
  set_of_labels_prog (p+;+q) \equiv set_of_labels_prog p \cup set_of_labels_prog q.
Proof.
  intros p. induction p; intros.
  - simpl. rewrite set_same_union_empty_l. reflexivity.
  - simpl. rewrite IHp. rewrite set_union_assoc. reflexivity.
Qed.

Lemma label_inR_prog_iff_in_set_of_labels : ∀ p l,
  label_inR_prog p l ↔ set_In l (set_of_labels_prog p).
Proof.
  intros. revert p.
  prog_cases (apply (prog_mutual_ind
    (fun p ⇒ label_inR_prog p l ↔ set_In l (set_of_labels_prog p))
    (fun s ⇒ label_inR_stmt s l ↔ set_In l (set_of_labels_stmt s))))
  Case; intros; simpl.
  - split; intros; inversion H.
  - split; intros.
    + inversion H1.
      apply set_union_intro1. apply H. assumption.
      apply set_union_intro2. apply H0. assumption.
    + apply set_union_elim in H1.
      destruct H1. apply LIP_here; apply H; assumption.
      apply LIP_after; apply H0; assumption.
  - split; intros. left. inversion H. reflexivity.
    destruct H. rewrite H. apply LIS_skip. inversion H.
  - split; intros. left. inversion H. reflexivity.
    destruct H. rewrite H. apply LIS_ass. inversion H.
  - split; intros.
    + apply set_add_intro. inversion H1. left; reflexivity.
      right. apply set_union_intro1. apply H; assumption.
      right. apply set_union_intro2. apply H0; assumption.
    + apply set_add_elim in H1. destruct H1.
      rewrite H1. apply LIS_ifb_cond.
      apply set_union_elim in H1.
      rewrite <- H in H1. rewrite <- H0 in H1.
      destruct H1.
      apply LIS_ifb_l; assumption. apply LIS_ifb_r; assumption.
  - split; intros.
    + apply set_add_intro.
      inversion H0. left; reflexivity.
      right; apply H; assumption.
    + apply set_add_elim in H0. destruct H0.
      rewrite H0. apply LIS_while_cond.
      rewrite <- H in H0. apply LIS_while_body; assumption.
  - split; intros. left. inversion H. reflexivity.
    destruct H. rewrite H. apply LIS_assert. inversion H.
Qed.

End label.

Section id.

Fixpoint set_of_id_aexp a :=
  match a with
  | A_num n ⇒ empty_set
  | A_id i ⇒ set_singleton i
  | A_plus a1 a2 ⇒ set_union (set_of_id_aexp a1) (set_of_id_aexp a2)
  | A_minus a1 a2 ⇒ set_union (set_of_id_aexp a1) (set_of_id_aexp a2)
  | A_mult a1 a2 ⇒ set_union (set_of_id_aexp a1) (set_of_id_aexp a2)
  end.

Fixpoint set_of_id_bexp b :=
  match b with
  | B_true ⇒ empty_set
  | B_false ⇒ empty_set
  | B_eq a1 a2 ⇒ set_union (set_of_id_aexp a1) (set_of_id_aexp a2)
  | B_le a1 a2 ⇒ set_union (set_of_id_aexp a1) (set_of_id_aexp a2)
  | B_not b0 ⇒ set_of_id_bexp b0
  | B_and b1 b2 ⇒ set_union (set_of_id_bexp b1) (set_of_id_bexp b2)
  end.

Lemma set_of_id_aexp_correct : ∀ a i,
  set_In i (set_of_id_aexp a) ↔ id_inR_aexp a i.
Proof.
  split; intros.
  - induction a; simpl in H.
    + inversion H.
    + apply set_singleton_In in H; subst; constructor.
    + apply set_union_elim in H. destruct H.
      × apply IIA_plus_l. apply IHa1; assumption.
      × apply IIA_plus_r. apply IHa2; assumption.
    + apply set_union_elim in H. destruct H.
      × apply IIA_minus_l. apply IHa1; assumption.
      × apply IIA_minus_r. apply IHa2; assumption.
    + apply set_union_elim in H. destruct H.
      × apply IIA_mult_l. apply IHa1; assumption.
      × apply IIA_mult_r. apply IHa2; assumption.
  - induction H; simpl;
      try (apply set_union_intro1; assumption);
      try (apply set_union_intro2; assumption).
    + apply set_singleton_In. reflexivity.
Qed.

Lemma set_of_id_bexp_correct : ∀ b i,
  set_In i (set_of_id_bexp b) ↔ id_inR_bexp b i.
Proof.
  split; intros.
  - induction b; simpl in H.
    + inversion H.
    + inversion H.
    + apply set_union_elim in H. destruct H.
      × apply IIB_eq_l. apply set_of_id_aexp_correct. assumption.
      × apply IIB_eq_r. apply set_of_id_aexp_correct. assumption.
    + apply set_union_elim in H. destruct H.
      × apply IIB_le_l. apply set_of_id_aexp_correct. assumption.
      × apply IIB_le_r. apply set_of_id_aexp_correct. assumption.
    + apply IIB_not. apply IHb. assumption.
    + apply set_union_elim in H. destruct H.
      × apply IIB_and_l. apply IHb1; assumption.
      × apply IIB_and_r. apply IHb2; assumption.
  - induction H; simpl; try apply set_of_id_aexp_correct in H;
      try (apply set_union_intro1; assumption);
      try (apply set_union_intro2; assumption).
    + assumption.
Qed.

Fixpoint set_of_id_prog (p:prog) :=
  match p with
  | {{}} ⇒ \emptyset
  | s;;q ⇒ set_of_id_stmt s \cup set_of_id_prog q
  end
with set_of_id_stmt (s:stmt) :=
  match s with
  | SKIP << _ >> ⇒ \emptyset
  | i ::= a << _ >> ⇒ i \oplus set_of_id_aexp a
  | IFB << _ >> b THEN p1 ELSE p2 FI ⇒
    set_of_id_bexp b \cup set_of_id_prog p1 \cup set_of_id_prog p2
  | WHILE << _ >> b DO p END ⇒
    set_of_id_bexp b \cup set_of_id_prog p
  | ASSERT << _ >> b =>> _ ⇒ set_of_id_bexp b
  end.

End id.