Library first_results

Require Import label.
Require Import seq.
Require Import control.
Require Import data.
Require Import assert.
Require Import set_relation.
Require Import semantics3.
Require Import proj_vs_traj.
Require Import last_state.

Lemma proj_prefix : ∀ p (L:set label),
  set_stable (control_depsR_prog p) L →
  set_stable (data_depsR_prog p) L →
  set_stable (assert_depsR_prog p) L →
  ∀ q, q = keep_L_prog p L →
  ∀ n ste,
  prefix (proj_traj_prog n ste p L) (proj_traj_prog n ste q L).
Proof.
  intros. revert n ste p L H H0 H1 q H2.
  apply (proj_traj_prog_ind
    (fun n ste p L ptr ⇒ set_stable (control_depsR_prog p) L →
      set_stable (data_depsR_prog p) L →
      set_stable (assert_depsR_prog p) L →
      ∀ q : prog,
      q = keep_L_prog p L → prefix ptr (proj_traj_prog n ste q L)));
  intros.
  - apply PR_nil.
  - apply PR_nil.
  - simpl in H3. rewrite e3 in H3. rewrite H3.
    simpl. rewrite e3. apply prefix_single. apply H; try reflexivity.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H5. apply DDP_flat with (p:={{SKIP << l >>}}+;+p0).
      apply IFOP_cons. constructor. assumption. simpl. apply FDP_after.
      assumption.
    + unfold set_stable. intros. unfold set_stable in H2. apply H2 with (l':=l').
      assumption. apply ADP_after. assumption.
  - simpl in H3. rewrite e3 in H3. rewrite H3.
    apply prefix_trans with (l2:=proj_traj_prog n' (Some st) (keep_L_prog q L) L).
    + {
        apply H; try reflexivity.
        + apply control_depsR_prog_stable_cons in H0. apply H0.
        + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
          assumption. inversion H5. apply DDP_flat with (p:={{SKIP << l >>}}+;+p0).
          apply IFOP_cons. constructor. assumption. simpl. apply FDP_after.
          assumption.
        + unfold set_stable. intros. unfold set_stable in H2. apply H2 with (l':=l').
          assumption. apply ADP_after. assumption.
      }
    + apply proj_traj_prog_prefix. apply le_S; apply le_n.
  - simpl in H3. rewrite e3 in H3. rewrite H3.
    simpl. rewrite e3. apply prefix_single. apply H; try reflexivity.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H5. apply DDP_flat with (p:={{i::=a << l >>}}+;+p0).
      apply IFOP_cons. constructor. assumption. simpl. apply FDP_after.
      assumption.
    + unfold set_stable. intros. unfold set_stable in H2. apply H2 with (l':=l').
      assumption. apply ADP_after. assumption.
  - simpl in H3. rewrite e3 in H3. rewrite H3.
    apply prefix_trans with
      (l2:=proj_traj_prog n' (Some (update st i (aeval st a))) (keep_L_prog q L) L).
    + {
        apply H.
        + apply control_depsR_prog_stable_cons in H0. apply H0.
        + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
          assumption. inversion H5. apply DDP_flat with (p:={{i::=a << l >>}}+;+p0).
          apply IFOP_cons. constructor. assumption. simpl. apply FDP_after.
          assumption.
        + unfold set_stable. intros. unfold set_stable in H2. apply H2 with (l':=l').
          assumption. apply ADP_after. assumption.
        + reflexivity.
      }
    
    + apply set_mem_complete_iff in e3.
      rewrite ass_not_preserved_proj_equal_ok with (a:=a) (l:=l); try assumption.
      apply proj_traj_prog_prefix. apply le_S; apply le_n.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    simpl. rewrite e3. rewrite e4. apply prefix_single. apply H.
    + apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply control_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
        assumption. apply CDS_ifb_l. assumption.
      × assumption.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H5.
      apply is_flatR_of_prog_intro in H6. inversion H6 as [q3 [q4 [H11 [H12 H13]]]].
      apply DDP_flat with (p:=({{ASSERT << l >> b =>> l}}+;+q3)+;+q4).
      apply IFOP_cons. simpl. apply IFOS_ifb_l; assumption. assumption.
      simpl. apply FDP_after. rewrite <- H11. assumption.
    + apply assert_depsR_prog_stable_cons in H2. destruct H2.
      apply assert_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
        assumption. apply ADS_ifb_l. assumption.
      × assumption.
    + symmetry. apply keep_L_prog_app.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    apply prefix_trans with (l2:=proj_traj_prog n' (Some st) (keep_L_prog q L) L).
    + {
        apply H.
        + apply control_depsR_prog_stable_cons in H0. destruct H0.
          apply control_depsR_prog_stable_app. split.
          × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
            assumption. apply CDS_ifb_l. assumption.
          × assumption.
        + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
          assumption. inversion H5.
          apply is_flatR_of_prog_intro in H6. inversion H6 as [q3 [q4 [H11 [H12 H13]]]].
          apply DDP_flat with (p:=({{ASSERT << l >> b =>> l}}+;+q3)+;+q4).
          apply IFOP_cons. simpl. apply IFOS_ifb_l; assumption. assumption.
          simpl. apply FDP_after. rewrite <- H11. assumption.
        + apply assert_depsR_prog_stable_cons in H2. destruct H2.
          apply assert_depsR_prog_stable_app. split.
          × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
            assumption. apply ADS_ifb_l. assumption.
          × assumption.
        + rewrite keep_L_prog_app. replace (keep_L_prog p1 L) with {{}}.
          reflexivity. symmetry.
          apply control_depsR_prog_stable_cons in H0. destruct H0.
          apply ifb_not_preserved_stable_not_preserved_l with (l:=l) (b:=b) (p2:=p2);
          assumption.
      }
    + apply proj_traj_prog_prefix. apply le_S; apply le_n.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    simpl. rewrite e3. rewrite e4. apply prefix_single. apply H.
    + apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply control_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
        assumption. apply CDS_ifb_r. assumption.
      × assumption.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H5.
      apply is_flatR_of_prog_intro in H6. inversion H6 as [q3 [q4 [H11 [H12 H13]]]].
      apply DDP_flat with (p:=({{ASSERT << l >> B_not b =>> l}}+;+q3)+;+q4).
      apply IFOP_cons. simpl. apply IFOS_ifb_r; assumption. assumption.
      simpl. apply FDP_after. rewrite <- H11. assumption.
    + apply assert_depsR_prog_stable_cons in H2. destruct H2.
      apply assert_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
        assumption. apply ADS_ifb_r. assumption.
      × assumption.
    + symmetry; apply keep_L_prog_app.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    apply prefix_trans with (l2:=proj_traj_prog n' (Some st) (keep_L_prog q L) L).
    + {
        apply H.
        + apply control_depsR_prog_stable_cons in H0. destruct H0.
          apply control_depsR_prog_stable_app. split.
          × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
            assumption. apply CDS_ifb_r. assumption.
          × assumption.
        + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
          assumption. inversion H5.
          apply is_flatR_of_prog_intro in H6. inversion H6 as [q3 [q4 [H11 [H12 H13]]]].
          apply DDP_flat with (p:=({{ASSERT << l >> B_not b =>> l}}+;+q3)+;+q4).
          apply IFOP_cons. simpl. apply IFOS_ifb_r; assumption. assumption.
          simpl. apply FDP_after. rewrite <- H11. assumption.
        + apply assert_depsR_prog_stable_cons in H2. destruct H2.
          apply assert_depsR_prog_stable_app. split.
          × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
            assumption. apply ADS_ifb_r. assumption.
          × assumption.
        + symmetry. rewrite keep_L_prog_app.
          rewrite ifb_not_preserved_stable_not_preserved_r with (l:=l) (b:=b) (p1:=p1).
          reflexivity. assumption. apply control_depsR_prog_stable_cons in H0.
          apply H0.
      }
    + apply proj_traj_prog_prefix. apply le_S; apply le_n.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    simpl. rewrite e3. rewrite e4. apply prefix_single. apply H.
    + pose proof H0. apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply control_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
        assumption. apply CDS_while. assumption.
      × assumption.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H5.
      apply is_flatR_of_prog_intro in H6. inversion H6 as [q3 [q4 [H11 [H12 H13]]]].
      replace ((WHILE << l >> b DO p0 END);; q)
        with ({{WHILE << l >> b DO p0 END}}+;+ q) in H13
        by reflexivity.
      apply is_flatR_of_prog_intro in H13. inversion H13 as [q5 [q6 [H14 [H15 H16]]]].
      apply DDP_flat with (p:=({{ASSERT << l >> b =>> l}}+;+q3+;+q5)+;+q6).
      apply IFOP_cons. simpl. apply is_flatR_of_prog_single in H15.
      apply IFOS_while_loop; assumption. assumption.
      simpl. apply FDP_after. rewrite <- seq_assoc. rewrite <- H14.
      rewrite <- H11. assumption.
    + pose proof H2. apply assert_depsR_prog_stable_cons in H2. destruct H2.
      apply assert_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
        assumption. apply ADS_while. assumption.
      × assumption.
    + symmetry. rewrite keep_L_prog_app. simpl. rewrite e4. reflexivity.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    apply prefix_trans with (l2:=proj_traj_prog n' (Some st) (keep_L_prog q L) L).
    + {
        apply H.
        + pose proof H0. apply control_depsR_prog_stable_cons in H0. destruct H0.
           apply control_depsR_prog_stable_app. split.
           × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
             assumption. apply CDS_while. assumption.
           × assumption.
        + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
          assumption. inversion H5.
          apply is_flatR_of_prog_intro in H6. inversion H6 as [q3 [q4 [H11 [H12 H13]]]].
          replace ((WHILE << l >> b DO p0 END);; q)
            with ({{WHILE << l >> b DO p0 END}}+;+ q) in H13
            by reflexivity.
          apply is_flatR_of_prog_intro in H13. inversion H13 as [q5 [q6 [H14 [H15 H16]]]].
          apply DDP_flat with (p:=({{ASSERT << l >> b =>> l}}+;+q3+;+q5)+;+q6).
          apply IFOP_cons. simpl. apply is_flatR_of_prog_single in H15.
          apply IFOS_while_loop; assumption. assumption.
          simpl. apply FDP_after. rewrite <- seq_assoc. rewrite <- H14.
          rewrite <- H11. assumption.
        + pose proof H2. apply assert_depsR_prog_stable_cons in H2. destruct H2.
          apply assert_depsR_prog_stable_app. split.
          × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
            assumption. apply ADS_while. assumption.
          × assumption.
        + symmetry. rewrite keep_L_prog_app. simpl. rewrite e4.
          rewrite while_not_preserved_stable_not_preserved with (l:=l) (b:=b).
          reflexivity. assumption. apply control_depsR_prog_stable_cons in H0.
          apply H0.
      }
    + apply proj_traj_prog_prefix. apply le_S; apply le_n.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    simpl. rewrite e3. rewrite e4. apply prefix_single. apply H.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H5.
      apply DDP_flat with (p:={{ASSERT << l >> B_not b =>> l}}+;+p1).
      apply IFOP_cons. apply IFOS_while_end. assumption.
      simpl. apply FDP_after. assumption.
    + apply assert_depsR_prog_stable_cons in H2. apply H2.
    + reflexivity.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    apply prefix_trans with (l2:=proj_traj_prog n' (Some st) (keep_L_prog q L) L).
    + {
        apply H.
        + apply control_depsR_prog_stable_cons in H0. apply H0.
        + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
          assumption. inversion H5.
          apply DDP_flat with (p:={{ASSERT << l >> B_not b =>> l}}+;+p1).
          apply IFOP_cons. apply IFOS_while_end. assumption.
          simpl. apply FDP_after. assumption.
        + apply assert_depsR_prog_stable_cons in H2. apply H2.
        + reflexivity.
      }
    + apply proj_traj_prog_prefix. apply le_S; apply le_n.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    simpl. rewrite e3. rewrite e4. apply prefix_single. apply H.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H5.
      apply DDP_flat with (p:={{ASSERT << l >> b =>> _x}}+;+p0).
      apply IFOP_cons. apply IFOS_assert. assumption.
      simpl. apply FDP_after. assumption.
    + apply assert_depsR_prog_stable_cons in H2. apply H2.
    + reflexivity.
  - simpl in H3. rewrite e4 in H3. rewrite H3.
    apply prefix_trans with (l2:=proj_traj_prog n' (Some st) (keep_L_prog q L) L).
    + {
        apply H.
        + apply control_depsR_prog_stable_cons in H0. apply H0.
        + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
          assumption. inversion H5.
          apply DDP_flat with (p:={{ASSERT << l >> b =>> _x}}+;+p0).
          apply IFOP_cons. apply IFOS_assert. assumption.
          simpl. apply FDP_after. assumption.
        + apply assert_depsR_prog_stable_cons in H2. apply H2.
        + reflexivity.
      }
    + apply proj_traj_prog_prefix. apply le_S; apply le_n.
  - simpl in H2. rewrite e4 in H2. rewrite H2.
    simpl. rewrite e3. rewrite e4. apply prefix_refl.
  - apply PR_nil.
  - apply PR_nil.
Qed.

Fixpoint index_proj n ste p (L:set label) N0 :=
  match N0 with
  | 0 ⇒ 0
  | S N1 ⇒
    match n with
    | 0 ⇒ 0
    | S n' ⇒
      match ste with
      | Some st ⇒
        match p with
        | {{}} ⇒ 0
        | s;;q ⇒
          match s with
          | SKIP << l >> ⇒
            if l \in? L then
            S (index_proj n' (Some st) q L N1)
            else
            S (index_proj (S n') (Some st) q L N1)
          | i ::= a << l >> ⇒
            if l \in? L then
            S (index_proj n'
                   (Some (update st i (aeval st a))) q L N1)
            else
            S (index_proj (S n')
                   (Some (update st i (aeval st a))) q L N1)
          | IFB << l >> b THEN p1 ELSE p2 FI ⇒
            if (beval st b) then
              if l \in? L then
              S (index_proj n' (Some st) (p1+;+q) L N1 )
              else
              S (index_proj (S n') (Some st) (p1+;+q) L N1 )
            else
              if l \in? L then
              S (index_proj n' (Some st) (p2+;+q) L N1 )
              else
              S (index_proj (S n') (Some st) (p2+;+q) L N1 )
          | WHILE << l >> b DO p END ⇒
            if (beval st b) then
              if l \in? L then
              S (index_proj n' (Some st) (p+;+(WHILE << l >> b DO p END;;q)) L N1 )
              else
              S (index_proj (S n') (Some st) (p+;+(WHILE << l >> b DO p END;;q)) L N1 )
            else
              if l \in? L then
              S (index_proj n' (Some st) q L N1 )
              else
              S (index_proj (S n') (Some st) q L N1 )
          | ASSERT << l >> b =>> l' ⇒
            if (beval st b) then
              if l \in? L then
              S (index_proj n' (Some st) q L N1 )
              else
              S (index_proj (S n') (Some st) q L N1 )
            else 0
          end
        end
      | None ⇒ 0
      end
    end
  end.

Functional Scheme index_proj_ind := Induction for index_proj Sort Prop.

Lemma proj_equal_bis :
  ∀ p q (L:set label),
  set_stable (control_depsR_prog p) L →
  set_stable (data_depsR_prog p) L →
  set_stable (assert_depsR_prog p) L →
  q = keep_L_prog p L →
  ∀ N0 ste,
  length (traj_prog N0 ste p) < N0 →
  last_state (traj_prog N0 ste p) ste ≠ None →
  ∀ n,
  proj_traj_prog (index_proj n ste p L N0) ste p L = proj_traj_prog n ste q L.
Proof.
  intros. revert n ste p L N0 q H H0 H1 H2 H3 H4.
  apply (index_proj_ind
    (fun n ste p L N0 ptr ⇒ ∀ q,
      set_stable (control_depsR_prog p) L →
      set_stable (data_depsR_prog p) L →
      set_stable (assert_depsR_prog p) L →
      q = keep_L_prog p L →
      length (traj_prog N0 ste p) < N0 →
      last_state (traj_prog N0 ste p) ste ≠ None →
      proj_traj_prog ptr ste p L = proj_traj_prog n ste q L));
  intros.
  - inversion H3.
  - reflexivity.
  - simpl in H2. subst q. reflexivity.
  - simpl in H3. rewrite e4 in H3. subst q0. simpl. rewrite e4.
    apply f_equal. apply H; try reflexivity.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6. apply DDP_flat with (p:={{SKIP << l >>}}+;+p0).
      apply IFOP_cons. constructor. assumption. simpl. apply FDP_after.
      assumption.
    + unfold set_stable. intros. unfold set_stable in H2. apply H2 with (l':=l').
      assumption. apply ADP_after. assumption.
    + simpl in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e4 in H3. subst q0. simpl proj_traj_prog at 1.
    rewrite e4. apply H; try reflexivity.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6. apply DDP_flat with (p:={{SKIP << l >>}}+;+p0).
      apply IFOP_cons. constructor. assumption. simpl. apply FDP_after.
      assumption.
    + unfold set_stable. intros. unfold set_stable in H2. apply H2 with (l':=l').
      assumption. apply ADP_after. assumption.
    + simpl in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e4 in H3. subst q0. simpl. rewrite e4.
    apply f_equal. apply H; try reflexivity.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6. apply DDP_flat with (p:={{i::=a << l >>}}+;+p0).
      apply IFOP_cons. constructor. assumption. simpl. apply FDP_after.
      assumption.
    + unfold set_stable. intros. unfold set_stable in H2. apply H2 with (l':=l').
      assumption. apply ADP_after. assumption.
    + simpl in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e4 in H3. subst q0. simpl proj_traj_prog at 1.
    rewrite e4.
    rewrite <- ass_not_preserved_proj_equal_ok with (a:=a) (l:=l) (i:=i) (k:=aeval st a);
    try assumption;
    [| apply set_mem_complete_iff in e4; assumption].
    apply H; try reflexivity.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6. apply DDP_flat with (p:={{i::=a << l >>}}+;+p0).
      apply IFOP_cons. constructor. assumption. simpl. apply FDP_after.
      assumption.
    + unfold set_stable. intros. unfold set_stable in H2. apply H2 with (l':=l').
      assumption. apply ADP_after. assumption.
    + simpl in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl. rewrite e4, e5.
    apply f_equal. apply H.
    + apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply control_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
        assumption. apply CDS_ifb_l. assumption.
      × assumption.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply is_flatR_of_prog_intro in H7. inversion H7 as [q3 [q4 [H12 [H13 H14]]]].
      apply DDP_flat with (p:=({{ASSERT << l >> b =>> l}}+;+q3)+;+q4).
      apply IFOP_cons. simpl. apply IFOS_ifb_l; assumption. assumption.
      simpl. apply FDP_after. rewrite <- H12. assumption.
    + apply assert_depsR_prog_stable_cons in H2. destruct H2.
      apply assert_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
        assumption. apply ADS_ifb_l. assumption.
      × assumption.
    + rewrite keep_L_prog_app. reflexivity.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl proj_traj_prog at 1.
    rewrite e4, e5. apply H.
    + apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply control_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
        assumption. apply CDS_ifb_l. assumption.
      × assumption.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply is_flatR_of_prog_intro in H7. inversion H7 as [q3 [q4 [H12 [H13 H14]]]].
      apply DDP_flat with (p:=({{ASSERT << l >> b =>> l}}+;+q3)+;+q4).
      apply IFOP_cons. simpl. apply IFOS_ifb_l; assumption. assumption.
      simpl. apply FDP_after. rewrite <- H12. assumption.
    + apply assert_depsR_prog_stable_cons in H2. destruct H2.
      apply assert_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
        assumption. apply ADS_ifb_l. assumption.
      × assumption.
    + rewrite keep_L_prog_app. replace (keep_L_prog p1 L) with {{}}.
      reflexivity. symmetry.
      apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply ifb_not_preserved_stable_not_preserved_l with (l:=l) (b:=b) (p2:=p2);
      assumption.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl. rewrite e4, e5.
    apply f_equal. apply H.
    + apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply control_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
        assumption. apply CDS_ifb_r. assumption.
      × assumption.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply is_flatR_of_prog_intro in H7. inversion H7 as [q3 [q4 [H12 [H13 H14]]]].
      apply DDP_flat with (p:=({{ASSERT << l >> B_not b =>> l}}+;+q3)+;+q4).
      apply IFOP_cons. simpl. apply IFOS_ifb_r; assumption. assumption.
      simpl. apply FDP_after. rewrite <- H12. assumption.
    + apply assert_depsR_prog_stable_cons in H2. destruct H2.
      apply assert_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
        assumption. apply ADS_ifb_r. assumption.
      × assumption.
    + rewrite keep_L_prog_app. reflexivity.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl proj_traj_prog at 1.
    rewrite e4, e5. apply H.
    + apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply control_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
        assumption. apply CDS_ifb_r. assumption.
      × assumption.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply is_flatR_of_prog_intro in H7. inversion H7 as [q3 [q4 [H12 [H13 H14]]]].
      apply DDP_flat with (p:=({{ASSERT << l >> B_not b =>> l}}+;+q3)+;+q4).
      apply IFOP_cons. simpl. apply IFOS_ifb_r; assumption. assumption.
      simpl. apply FDP_after. rewrite <- H12. assumption.
    + apply assert_depsR_prog_stable_cons in H2. destruct H2.
      apply assert_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
        assumption. apply ADS_ifb_r. assumption.
      × assumption.
    + rewrite keep_L_prog_app. replace (keep_L_prog p2 L) with {{}}.
      reflexivity. symmetry.
      apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply ifb_not_preserved_stable_not_preserved_r with (l:=l) (b:=b) (p1:=p1);
      assumption.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl. rewrite e4, e5.
    apply f_equal. apply H.
    + pose proof H0. apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply control_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
        assumption. apply CDS_while. assumption.
      × assumption.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply is_flatR_of_prog_intro in H7. inversion H7 as [q3 [q4 [H12 [H13 H14]]]].
      replace ((WHILE << l >> b DO p0 END);; q)
        with ({{WHILE << l >> b DO p0 END}}+;+ q) in H14
        by reflexivity.
      apply is_flatR_of_prog_intro in H14. inversion H14 as [q5 [q6 [H15 [H16 H17]]]].
      apply DDP_flat with (p:=({{ASSERT << l >> b =>> l}}+;+q3+;+q5)+;+q6).
      apply IFOP_cons. simpl. apply is_flatR_of_prog_single in H16.
      apply IFOS_while_loop; assumption. assumption.
      simpl. apply FDP_after. rewrite <- seq_assoc. rewrite <- H15.
      rewrite <- H12. assumption.
    + pose proof H2. apply assert_depsR_prog_stable_cons in H2. destruct H2.
      apply assert_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
        assumption. apply ADS_while. assumption.
      × assumption.
    + rewrite keep_L_prog_app. simpl. rewrite e5. reflexivity.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl proj_traj_prog at 1.
    rewrite e4, e5. apply H.
    + pose proof H0. apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply control_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H0. intros. apply H0 with (l':=l').
        assumption. apply CDS_while. assumption.
      × assumption.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply is_flatR_of_prog_intro in H7. inversion H7 as [q3 [q4 [H12 [H13 H14]]]].
      replace ((WHILE << l >> b DO p0 END);; q)
        with ({{WHILE << l >> b DO p0 END}}+;+ q) in H14
        by reflexivity.
      apply is_flatR_of_prog_intro in H14. inversion H14 as [q5 [q6 [H15 [H16 H17]]]].
      apply DDP_flat with (p:=({{ASSERT << l >> b =>> l}}+;+q3+;+q5)+;+q6).
      apply IFOP_cons. simpl. apply is_flatR_of_prog_single in H16.
      apply IFOS_while_loop; assumption. assumption.
      simpl. apply FDP_after. rewrite <- seq_assoc. rewrite <- H15.
      rewrite <- H12. assumption.
    + pose proof H2. apply assert_depsR_prog_stable_cons in H2. destruct H2.
      apply assert_depsR_prog_stable_app. split.
      × unfold set_stable. unfold set_stable in H2. intros. apply H2 with (l':=l').
        assumption. apply ADS_while. assumption.
      × assumption.
    + rewrite keep_L_prog_app. simpl. rewrite e5.
      replace (keep_L_prog p0 L) with {{}}.
      reflexivity. symmetry.
      apply control_depsR_prog_stable_cons in H0. destruct H0.
      apply while_not_preserved_stable_not_preserved with (l:=l) (b:=b) (p:=p0);
      assumption.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl. rewrite e4, e5.
    apply f_equal. apply H; try reflexivity.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply DDP_flat with (p:={{ASSERT << l >> B_not b =>> l}}+;+p1).
      apply IFOP_cons. apply IFOS_while_end. assumption.
      simpl. apply FDP_after. assumption.
    + apply assert_depsR_prog_stable_cons in H2. apply H2.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl proj_traj_prog at 1.
    rewrite e4, e5. apply H; try reflexivity.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply DDP_flat with (p:={{ASSERT << l >> B_not b =>> l}}+;+p1).
      apply IFOP_cons. apply IFOS_while_end. assumption.
      simpl. apply FDP_after. assumption.
    + apply assert_depsR_prog_stable_cons in H2. apply H2.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl. rewrite e4, e5.
    apply f_equal. apply H; try reflexivity.
   + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply DDP_flat with (p:={{ASSERT << l >> b =>> _x}}+;+p0).
      apply IFOP_cons. apply IFOS_assert. assumption.
      simpl. apply FDP_after. assumption.
    + apply assert_depsR_prog_stable_cons in H2. apply H2.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H3. rewrite e5 in H3. subst q0. simpl proj_traj_prog at 1.
    rewrite e4, e5. apply H; try reflexivity.
    + apply control_depsR_prog_stable_cons in H0. apply H0.
    + unfold set_stable. intros. unfold set_stable in H1. apply H1 with (l':=l').
      assumption. inversion H6.
      apply DDP_flat with (p:={{ASSERT << l >> b =>> _x}}+;+p0).
      apply IFOP_cons. apply IFOS_assert. assumption.
      simpl. apply FDP_after. assumption.
    + apply assert_depsR_prog_stable_cons in H2. apply H2.
    + simpl in H4. rewrite e4 in H4. apply le_S_n in H4. assumption.
    + simpl traj_prog in H5. rewrite e4 in H5.
      rewrite last_state_cons_change_default in H5. assumption.
  - simpl in H4. rewrite e4 in H4. contradiction H4. reflexivity.
  - simpl in H4. contradiction H4. reflexivity.
Qed.

Lemma index_proj_bounded : ∀ n ste p L N0,
  index_proj n ste p L N0 ≤ N0.
Proof.
  intros. functional induction (index_proj n ste p L N0);
    try apply le_0_n; try (apply le_n_S; assumption).
Qed.

Lemma proj_equal :
  ∀ p q (L:set label),
  set_stable (control_depsR_prog p) L →
  set_stable (data_depsR_prog p) L →
  set_stable (assert_depsR_prog p) L →
  q = keep_L_prog p L →
  ∀ N0 ste,
  length (traj_prog N0 ste p) < N0 →
  last_state (traj_prog N0 ste p) ste ≠ None →
  length (traj_prog N0 ste q) < N0 ∧
  last_state (traj_prog N0 ste q) ste ≠ None ∧
  proj_traj_prog N0 ste p L = proj_traj_prog N0 ste q L.
Proof.
  intros.
  pose proof (proj_equal_bis p q L H H0 H1 H2 N0 ste H3 H4 N0).
  assert (proj_traj_prog N0 ste p L = proj_traj_prog N0 ste q L).
  { apply prefix_irrefl.
    - apply proj_prefix; assumption.
    - rewrite <- H5. apply proj_traj_prog_prefix. apply index_proj_bounded.
  }
  assert (set_of_labels_prog q \subseteq L).
  { rewrite H2. rewrite keep_L_prog_label with (d:=control_depsR_prog p).
    - unfold set_incl; intros. rewrite set_inter_In in H7; apply H7.
    - assumption.
    - unfold inclusion; intros; assumption.
  }
  repeat split; try assumption.
  - rewrite <- map_length with (f:=pair_proj).
    rewrite <- proj_traj_prog_map_set_incl with (L:=L) by assumption.
    rewrite map_length. rewrite <- H6.
    apply Nat.le_lt_trans with (m:=length (traj_prog N0 ste p)).
    + apply proj_traj_prog_shorter.
    + assumption.
  - destruct ste.
    + apply traj_prog_not_none_iff; [discriminate |].
      rewrite proj_traj_prog_not_none_set_incl with (L:=L) by assumption.
      rewrite <- H6. apply proj_traj_prog_not_none.
      apply Forall_impl with (P:=fun x⇒ snd x ≠ None); [intros; assumption |].
      apply traj_prog_not_none. assumption.
    + destruct N0.
      × inversion H3.
      × simpl in H4. contradiction H4. reflexivity.
Qed.