Library assert

Require Export prog.
Require Export label.
Require Import set_relation.
Require Import Relation_Definitions.
Require Import control.

Inductive assert_depsR_prog : prog → relation label :=
  | ADP_here : ∀ s p l l', assert_depsR_stmt s l l' →
      assert_depsR_prog (s;;p) l l'
  | ADP_after : ∀ s p l l', assert_depsR_prog p l l' →
      assert_depsR_prog (s;;p) l l'
with assert_depsR_stmt : stmt → relation label :=
  | ADS_ifb_l : ∀ l b p1 p2 l' l'', assert_depsR_prog p1 l' l'' →
      assert_depsR_stmt (IFB << l >> b THEN p1 ELSE p2 FI) l' l''
  | ADS_ifb_r : ∀ l b p1 p2 l' l'', assert_depsR_prog p2 l' l'' →
      assert_depsR_stmt (IFB << l >> b THEN p1 ELSE p2 FI) l' l''
  | ADS_while : ∀ l b p l' l'', assert_depsR_prog p l' l'' →
      assert_depsR_stmt (WHILE <<l>> b DO p END) l' l''
  | ADS_assert : ∀ b l l', assert_depsR_stmt (ASSERT <<l>> b =>> l') l l'.

Scheme assert_depsR_prog_mutual_ind := Induction for assert_depsR_prog Sort Prop
 with assert_depsR_stmt_mutual_ind := Induction for assert_depsR_stmt Sort Prop.

Lemma assert_depsR_prog_label_inR_prog : ∀ p l l',
  assert_depsR_prog p l l' → label_inR_prog p l.
Proof.
  apply (assert_depsR_prog_mutual_ind
    (fun p l l' H ⇒ label_inR_prog p l)
    (fun s l l' H ⇒ label_inR_stmt s l)); intros.
  - apply LIP_here; assumption.
  - apply LIP_after; assumption.
  - apply LIS_ifb_l; assumption.
  - apply LIS_ifb_r; assumption.
  - apply LIS_while_body; assumption.
  - apply LIS_assert.
Qed.

Lemma assert_depsR_prog_stable : ∀ p,
  set_stable (assert_depsR_prog p) (set_of_labels_prog p).
Proof. unfold set_stable.
  intros. apply label_inR_prog_iff_in_set_of_labels.
  apply assert_depsR_prog_label_inR_prog with (l':=l'). assumption.
Qed.

Lemma assert_depsR_prog_dec : ∀ p l l',
  {assert_depsR_prog p l l'} + {¬assert_depsR_prog p l l'}.
Proof.
  apply (prog_mutual_rect
    (fun p ⇒ ∀ l l',
      {assert_depsR_prog p l l'} + {¬ assert_depsR_prog p l l'})
    (fun s ⇒ ∀ l l',
      {assert_depsR_stmt s l l'} + {¬ assert_depsR_stmt s l l'})); intros;
  try now (right; intros contra; inversion contra).
  - destruct (H l l').
    + left. apply ADP_here; assumption.
    + destruct (H0 l l').
      × left. apply ADP_after; assumption.
      × right. intros contra. inversion contra; contradiction.
  - destruct (H l0 l').
    + left. apply ADS_ifb_l; assumption.
    + destruct (H0 l0 l').
      × left. apply ADS_ifb_r; assumption.
      × right. intros contra. inversion contra; contradiction.
  - destruct (H l0 l').
    + left. apply ADS_while; assumption.
    + right. intros contra. inversion contra; contradiction.
  - destruct (Nat.eq_dec l l1).
    + destruct (Nat.eq_dec l0 l').
      × left. subst. apply ADS_assert.
      × right. intros contra. inversion contra; contradiction.
    + right. intros contra. inversion contra; contradiction.
Qed.

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

Lemma set_assert_prog_correct : ∀ p l l',
  (l, l') \in set_assert_prog p ↔ assert_depsR_prog p l l'.
Proof.
  apply (prog_mutual_ind
    (fun p ⇒ ∀ l l', (l, l') \in set_assert_prog p ↔ assert_depsR_prog p l l')
    (fun s ⇒ ∀ l l', (l, l') \in set_assert_stmt s ↔ assert_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 ADP_here; assumption.
      × apply ADP_after; assumption.
    + inversion H1.
      × left; assumption.
      × right; assumption.
  - rewrite set_union_In. rewrite H, H0. split; intros.
    + destruct H1.
      × apply ADS_ifb_l; assumption.
      × apply ADS_ifb_r; assumption.
    + inversion H1.
      × left; assumption.
      × right; assumption.
  - rewrite H. split; intros.
    + constructor; assumption.
    + inversion H0; assumption.
  - rewrite set_singleton_In. split; intros.
    + inversion H. constructor.
    + inversion H; reflexivity.
Qed.