Library proj_vs_traj

Require Import Bool.
Require Import decidable.
Require Import semantics3.
Require Import last.

Lemma proj_traj_prog_shorter : ∀ n ste p L,
  length (proj_traj_prog n ste p L) ≤ length (traj_prog n ste p).
Proof.
  intros. functional induction (proj_traj_prog n ste p L);
    try (apply le_0_n);
    try (simpl; rewrite e3);
    try (apply le_n_S; assumption);
    try (apply le_S; assumption).
  apply le_n.
  Fail simpl.
Abort.

Definition option_proj {A} (x:option A) : option bool :=
  match x with
  | Some st ⇒ Some true
  | None ⇒ None
  end.

Definition pair_proj {A} (la:label×option A) :=
  let (l, a) := la in
  (l, option_proj a).

Lemma proj_traj_prog_map : ∀ n ste p L,
  map pair_proj (proj_traj_prog n ste p L) =
  map pair_proj
    (filter (fun x ⇒ fst x \in? L) (traj_prog n ste p)).
Proof.
  intros n ste p L. functional induction (proj_traj_prog n ste p L); simpl;
    try (rewrite e3; simpl); try (rewrite e4; simpl);
    try apply f_equal; try exact IHp0; reflexivity.
Qed.

Lemma filter_length : ∀ {A} (f:A → bool) (l:list A),
  length (filter f l) ≤ length l.
Proof.
  intros. induction l.
  - reflexivity.
  - simpl. destruct (f a).
    + simpl. apply le_n_S; assumption.
    + apply le_S. assumption.
Qed.

Lemma proj_traj_prog_shorter : ∀ n ste p L,
  length (proj_traj_prog n ste p L) ≤ length (traj_prog n ste p).
Proof.
  intros. rewrite <- (map_length (A:=label×partial_state_eps) pair_proj).
  rewrite proj_traj_prog_map. rewrite map_length.
  apply filter_length.
Qed.

Lemma proj_traj_prog_not_none : ∀ n ste p L,
  Forall (fun x ⇒ fst x \in L → snd x ≠ None) (traj_prog n ste p) ↔
  Forall (fun x ⇒ snd x ≠ None) (proj_traj_prog n ste p L).
Proof.
  split; intros.
  - functional induction (proj_traj_prog n ste p L); simpl; try (constructor; fail);
      try (constructor; [discriminate |]);
      try (apply IHp0; simpl in H; try rewrite e3 in H; inversion H; assumption).
    simpl in H. rewrite e3 in H. inversion H. contradiction H2; simpl.
    apply set_mem_correct_iff in e4; assumption. reflexivity.
  - functional induction (proj_traj_prog n ste p L); simpl; try (constructor; fail);
      try (try rewrite e3; constructor; [intros; discriminate|]);
      try (apply IHp0; try assumption; inversion H; assumption).
    inversion H. contradiction H2; reflexivity.
    rewrite e3. constructor. intros. simpl in H0. apply set_mem_complete_iff in e4.
    contradiction. constructor.
Qed.

Lemma proj_traj_prog_last : ∀ n ste p L l l',
  last (traj_prog n ste p) (l, ste) = (l', None) →
  l' \in L →
  last (proj_traj_prog n ste p L) (l, partial_state_proj ste) = (l', None).
Proof.
  intros.
  assert (
    last (map pair_proj (proj_traj_prog n ste p L))
      (pair_proj (l, partial_state_proj ste)) =
    last (map pair_proj (filter (fun x ⇒ fst x \in? L) (traj_prog n ste p)))
      (pair_proj (l, ste))).
  { rewrite <- proj_traj_prog_map. intros. simpl.
    destruct ste; reflexivity.
  }
  rewrite 2!last_map in H1.
  rewrite last_filter in H1
    by (rewrite H; rewrite set_mem_correct_iff; assumption).
  rewrite H in H1. simpl in H1.
  fold partial_state_eps in H1.
  destruct (last (proj_traj_prog n ste p L) (l, partial_state_proj ste)) as [l'' ste'];
    simpl in H1; inversion H1.
  destruct ste'.
  - discriminate H4.
  - reflexivity.
Qed.

Lemma forall_filter : ∀ {A} (f:A → bool) (l:list A),
  Forall (fun x ⇒ f x = true) l → filter f l = l.
Proof.
  intros. induction H.
  - reflexivity.
  - simpl. rewrite H. rewrite IHForall. reflexivity.
Qed.

Lemma traj_prog_label_in : ∀ n ste p,
  Forall (fun x ⇒ fst x \in set_of_labels_prog p) (traj_prog n ste p).
Proof.
  intros. functional induction (traj_prog n ste p); simpl;
    try (constructor;
      [rewrite set_union_In; left; try rewrite set_singleton_In;
        try apply set_add_intro2; reflexivity |]);
    try (eapply Forall_impl; [| apply IHl]; intros; simpl; rewrite set_union_In;
      try (right; assumption));
      try (constructor; fail).
  - simpl in H. rewrite set_of_labels_prog_seq in H. rewrite set_union_In in H.
    destruct H.
    + left. apply set_add_intro1. rewrite set_union_In. left; assumption.
    + right; assumption.
  - simpl in H. rewrite set_of_labels_prog_seq in H. rewrite set_union_In in H.
    destruct H.
    + left. apply set_add_intro1. rewrite set_union_In. right; assumption.
    + right; assumption.
  - simpl in H. rewrite set_of_labels_prog_seq in H. simpl in H.
    rewrite 2!set_union_In in H. decompose [or] H; clear H.
    + left. apply set_add_intro1. assumption.
    + left; assumption.
    + right; assumption.
Qed.

Corollary proj_traj_prog_map_set_incl : ∀ n ste p L,
  set_of_labels_prog p \subseteq L →
  map pair_proj (proj_traj_prog n ste p L) =
  map pair_proj (traj_prog n ste p).
Proof.
  intros. rewrite proj_traj_prog_map.
  rewrite forall_filter. reflexivity.
  apply Forall_impl with (P:=fun x ⇒ fst x \in set_of_labels_prog p).
  intros. rewrite set_mem_correct_iff. apply H. assumption.
  apply traj_prog_label_in.
Qed.

Corollary proj_traj_prog_length_set_incl : ∀ n ste p L,
  set_of_labels_prog p \subseteq L →
  length (proj_traj_prog n ste p L) = length (traj_prog n ste p).
Proof.
  intros. rewrite <- (map_length (A:=label×partial_state_eps) pair_proj).
  rewrite proj_traj_prog_map_set_incl by assumption. rewrite map_length.
  reflexivity.
Qed.

Corollary proj_traj_prog_not_none_set_incl : ∀ n ste p L,
  set_of_labels_prog p \subseteq L →
  Forall (fun x ⇒ snd x ≠ None) (traj_prog n ste p) ↔
  Forall (fun x ⇒ snd x ≠ None) (proj_traj_prog n ste p L).
Proof.
  intros. rewrite <- proj_traj_prog_not_none. split; intros.
  - apply Forall_impl with (P:= fun x ⇒ snd x ≠ None); try assumption.
    intros. assumption.
  - pose proof (traj_prog_label_in n ste p).
    rewrite Forall_forall in ×. intros. apply H0; try assumption.
    apply H. apply H1; try assumption.
Qed.

Corollary proj_traj_prog_last_set_incl : ∀ n ste p L l l',
  set_of_labels_prog p \subseteq L →
  last (traj_prog n ste p) (l, ste) = (l', None) →
  last (proj_traj_prog n ste p L) (l, partial_state_proj ste) = (l', None).
Proof.
  intros. destruct (traj_prog n ste p) eqn:Heqtraj.
  - assert (proj_traj_prog n ste p L = []).
    { apply length_zero_iff_nil.
      apply Nat.le_0_r. rewrite proj_traj_prog_shorter. rewrite Heqtraj.
      reflexivity.
    }
    rewrite H1. simpl. simpl in H0. inversion H0. reflexivity.
  - rewrite <- Heqtraj in ×.
    apply proj_traj_prog_last; try assumption.
    apply H.
    assert (traj_prog n ste p ≠ []).
    { rewrite Heqtraj; discriminate. }
    apply last_not_empty_In with (a:=(l, ste)) in H1.
    rewrite H0 in H1.
    pose proof (traj_prog_label_in n ste p).
    rewrite Forall_forall in H2. apply H2 in H1. assumption.
Qed.