Library slice

Require Export prog.
Require Export set.
Require Import quotient.
Require Import set_relation.
Require Import control.
Require Import data.
Require Import assert.
Require Import set_deps.
Require Import set_instance.
Require Import set_relation.
Require Import semantics3.
Require Import proj_vs_traj.
Require Import first_results.
Require Import last.
Require Import last_state.
Require Import ClassicalFacts.

Class ProgWithDep (p : prog) (d : relation label) := {
  PWD_control : inclusion label (control_depsR_prog p) d;
  PWD_stable : set_stable d (set_of_labels_prog p);
  PWD_rl : set (label×label);
  PWD_correct : ∀ l l', (l, l') \in PWD_rl ↔ d l l'
}.


Section definitions.

Definition set_slice (p:prog) {d} {PWD:ProgWithDep p d} (L:set label) :=
  set_refl_trans_inverse PWD_rl (set_inter L (set_of_labels_prog p)).

Definition slice (p:prog) {d} {PWD:ProgWithDep p d} (L:set label) :=
  keep_L_prog p (set_slice p L).

Lemma set_slice_correct : ∀ (p:prog) {d:relation label}
  {PWD:ProgWithDep p d} L l,
  set_In l (set_slice p L) ↔
  ∃ l', l' \in (L \cap (set_of_labels_prog p)) ∧
    clos_refl_trans label d l l'.
Proof.
  split; intros.
  - unfold set_slice in H.
    rewrite (set_rel_clos_relation_stable_iff2 d _ PWD_correct) in H.
    destruct H as [l' [H H0]].
    ∃ l'. split; assumption.
  - destruct H as [l' [H H0]].
    unfold set_slice.
    apply (set_rel_clos_relation_stable_iff2 d _ PWD_correct).
    ∃ l'. split; assumption.
Qed.

Lemma slice_quotient : ∀ p {d} {PWD:ProgWithDep p d} L,
  is_quotientR_prog p (slice p L).
Proof.
  intros. unfold slice. apply keep_L_prog_quotient.
Qed.

Lemma set_slice_include : ∀ p {d} {PWD:ProgWithDep p d} L,
  set_slice p L \subseteq set_of_labels_prog p.
Proof.
  unfold set_incl; intros.
  apply set_slice_correct in H. inversion H as [l' [H0 H1]].
  rewrite set_inter_In in H0. destruct H0.
  apply (set_rel_carrier_stable d _ (PWD_stable) _ l'); assumption.
Qed.

Lemma set_slice_stable : ∀ p {d} {PWD:ProgWithDep p d} L,
  set_stable d (set_slice p L).
Proof.
  intros. apply set_rel_clos_refl_trans_inverse_stable2. exact PWD_correct.
Qed.

Lemma slice_label : ∀ p {d} {PWD:ProgWithDep p d} L,
  set_of_labels_prog (slice p L) \equiv set_slice p L.
Proof.
  intros. unfold slice.
  rewrite keep_L_prog_label with (d:=d).
  - rewrite set_inter_comm.
    apply set_inter_same. apply set_slice_include.
  - apply set_slice_stable.
  - exact PWD_control.
Qed.

End definitions.

Instance PWD_cda p :
  ProgWithDep p (union label (control_depsR_prog p)
                       (union label (data_depsR_prog p) (assert_depsR_prog p))).
Proof.
  split with (PWD_rl:=
    (set_control_prog p \cup set_data_prog p \cup set_assert_prog p)).
  - unfold inclusion; intros. unfold union at 1.
    left; assumption.
  - unfold set_stable; intros. unfold union in H0.
    decompose [or] H0; clear H0.
    + apply control_depsR_prog_stable with (l':=l'); assumption.
    + apply data_depsR_prog_stable with (l':=l'); assumption.
    + apply assert_depsR_prog_stable with (l':=l'); assumption.
  - intros. rewrite 2!set_union_In. unfold union. split; intros.
    + decompose [or] H; clear H.
      × left. apply set_control_prog_correct. assumption.
      × right; left. apply set_data_prog_correct. assumption.
      × right; right. apply set_assert_prog_correct. assumption.
    + decompose [or] H.
      × left. apply set_control_prog_correct. assumption.
      × right; left. apply set_data_prog_correct. assumption.
      × right; right. apply set_assert_prog_correct. assumption.
Defined.

Theorem slice_proj_prefix :
  ∀ p L n ste,
  prefix (proj_traj_prog n ste p (set_slice p L))
         (proj_traj_prog n ste (slice p L) (set_slice p L)).
Proof.
  intros. apply proj_prefix; try (unfold set_stable;
    intros; apply set_slice_stable with (l':=l'); try assumption; unfold union).
  - left; assumption.
  - right; left; assumption.
  - right; right; assumption.
  - reflexivity.
Qed.

Theorem slice_proj_equal :
  ∀ n ste p L,
  length (traj_prog n ste p) < n →
  last_state (traj_prog n ste p) ste ≠ None →
  length (traj_prog n ste (slice p L)) < n ∧
  last_state (traj_prog n ste (slice p L)) ste ≠ None ∧
  proj_traj_prog n ste p (set_slice p L) =
  proj_traj_prog n ste (slice p L) (set_slice p L).
Proof.
  intros. apply proj_equal; try assumption; try (unfold set_stable;
    intros; apply set_slice_stable with (l':=l'); try assumption; unfold union).
  - left; assumption.
  - right; left; assumption.
  - right; right; assumption.
  - reflexivity.
Qed.

Lemma prefix_include : ∀ {A} (l1 l2 :list A),
  prefix l1 l2 → include l1 l2.
Proof.
  intros. induction H.
  - apply include_nil_l.
  - apply include_here. assumption.
Qed.

Lemma slice_no_error_ste : ∀ n ste p L,
  Forall (fun x ⇒ snd x ≠ None) (traj_prog n ste (slice p L)) →
  Forall (fun x ⇒ fst x \in (set_slice p L) → snd x ≠ None) (traj_prog n ste p).
Proof.
  intros. rewrite proj_traj_prog_not_none.
  apply include_forall with (l':=proj_traj_prog n ste (slice p L) (set_slice p L)).
  apply prefix_include. apply slice_proj_prefix.
  rewrite <- proj_traj_prog_not_none.
  apply Forall_impl with (P:=fun x ⇒ snd x ≠ None). intros. assumption.
  assumption.
Qed.

Theorem slice_no_error : ∀ p L,
  (∀ n ste, Forall (fun x ⇒ snd x ≠ None) (traj_prog n ste (slice p L))) →
  ∀ n ste, Forall (fun x ⇒ fst x \in (set_slice p L) → snd x ≠ None) (traj_prog n ste p).
Proof.
  intros. apply slice_no_error_ste. apply H.
Qed.

Lemma proj_traj_prog_none_in : ∀ n ste p L l,
  In (l, None) (proj_traj_prog n ste p L) →
  ∀ lste, last (proj_traj_prog n ste p L) lste = (l, None).
Proof.
  intros n ste p L.
  functional induction (proj_traj_prog n ste p L); intros;
    try (inversion H; fail);
    try (apply IHp0; assumption);
    try (rewrite last_cons_change_default; apply IHp0; simpl in H;
      destruct H; [discriminate H | assumption]).
  simpl in H. destruct H.
  - inversion H. reflexivity.
  - inversion H.
Qed.

Theorem slice_error :
  ∀ (ste:state_eps) p L l l',
  (∃ N1, last (traj_prog N1 ste (slice p L)) (l, ste) = (l', None)) →
  (∃ N0, length (traj_prog N0 ste p) < N0) →
  (∃ n, last (traj_prog n ste p) (l, ste) = (l', None)) ∨
  (∃ n l'', last (traj_prog n ste p) (l, ste) = (l'', None) ∧ ¬ l'' \in set_slice p L).
Proof.
  intros. destruct H as [N1 H].
  destruct H0 as [N0 H0].
  remember (max N0 N1) as N2.
  assert (last (traj_prog N2 ste (slice p L)) (l, ste) = (l', None)).
  { rewrite traj_prog_none_end with (n:=N1); try assumption.
    - rewrite last_state_map with (a:=l). unfold state_eps in ×. rewrite H.
      reflexivity.
    - rewrite HeqN2. apply Nat.le_max_r.
  }
  clear H.
  assert (length (traj_prog N2 ste p) < N2).
  { rewrite traj_prog_length_not_reached with (m:=N0); try assumption.
    apply Nat.lt_le_trans with (m:=N0).
    - assumption.
    - rewrite HeqN2. apply Nat.le_max_l.
    - rewrite HeqN2. apply Nat.le_max_l.
  }
  clear H0 HeqN2 N1 N0.
  destruct (last_state (traj_prog N2 ste p) ste) eqn:Heqlast.
  -
    assert (last_state (traj_prog N2 ste p) ste ≠ None) by (rewrite Heqlast; discriminate).
    pose proof (slice_proj_equal N2 ste p L H H0).
    destruct H2 as [H2 [H3 H4]].
    contradiction H3.
    rewrite last_state_map with (a:=l). unfold state_eps in ×. rewrite H1. reflexivity.
  -
    destruct (last (traj_prog N2 ste p) (l, ste)) as [l'' ste'] eqn:Heqlast'.
    assert(ste' = None).
    { rewrite last_state_map with (a:=l) in Heqlast.
      unfold state_eps in ×.
      rewrite Heqlast' in Heqlast. simpl in Heqlast. assumption.
    }
    subst ste'.
    destruct (set_In_dec l'' (set_slice p L)).
    +
      left. ∃ N2. pose proof Heqlast' as Heqlast''.
      apply proj_traj_prog_last with (L:=set_slice p L) in Heqlast'; try assumption.
      assert(traj_prog N2 ste (slice p L) = [] ∨ traj_prog N2 ste (slice p L) ≠ []).
      { destruct (traj_prog N2 ste (slice p L)).
        - left; reflexivity.
        - right; discriminate.
      }
      destruct H0.
      × rewrite H0 in H1. simpl in H1. inversion H1. destruct N2; reflexivity.
      × { apply proj_traj_prog_last with (L:=set_slice p L) in H1.
        - assert(proj_traj_prog N2 ste p (set_slice p L) = [] ∨
                 proj_traj_prog N2 ste p (set_slice p L) ≠ []).
          { destruct (proj_traj_prog N2 ste p (set_slice p L)).
            - left; reflexivity.
            - right; discriminate.
          }
          destruct H2.
          + rewrite H2 in ×. simpl in Heqlast'. inversion Heqlast'.
            destruct ste; [discriminate H5 |].
            destruct N2; contradiction H0; reflexivity.
          + assert (last (proj_traj_prog N2 ste (slice p L)
              (set_slice p L)) (l, partial_state_proj ste) = (l'', None)).
            { apply proj_traj_prog_none_in.
              apply (include_incl _ _ (prefix_include _ _ (slice_proj_prefix p L N2 ste))).
              rewrite <- Heqlast'.
              apply last_not_empty_In; assumption.
            }
            rewrite H3 in H1. inversion H1. subst l''. assumption.
        - pose proof (traj_prog_label_in N2 ste (slice p L)).
          rewrite Forall_forall in H2. specialize (H2 (l', None)).
          rewrite slice_label in H2. apply H2. rewrite <- H1.
          apply last_not_empty_In. assumption. }
    + right. ∃ N2, l''. split; assumption.
Qed.

Theorem slice_error_classical :
  excluded_middle →
  ∀ (ste:state_eps) p L l l',
  (∃ N1, last (traj_prog N1 ste (slice p L)) (l, ste) = (l', None)) →
  (∃ n, last (traj_prog n ste p) (l, ste) = (l', None)) ∨
  (∃ n l'', last (traj_prog n ste p) (l, ste) = (l'', None) ∧ ¬ l'' \in set_slice p L) ∨
  ¬ (∃ n, length (traj_prog n ste p) < n).
Proof.
  intros. rewrite <- or_assoc.
  specialize (H (∃ n, length (traj_prog n ste p) < n)).
  destruct H.
  - left. apply slice_error; assumption.
  - right. assumption.
Qed.