Require Import FunctionalExtensionality ZArith List.
Require Import lang Vtac combine_results.

Set Implicit Arguments.

Inductive ss_star (e: exp) : exp -> Prop :=
| ss_starR : ss_star e e
| ss_starT e2 e3: step e e2 -> ss_star e2 e3 -> ss_star e e3.

Lemma ss_star_one: forall e1 e2, step e1 e2 -> ss_star e1 e2.
Proof.
  intros.
  apply ss_starT with e2.
  auto.
  apply ss_starR.
Qed.

Lemma ss_star_trans: forall e1 e2 e3, ss_star e1 e2 -> ss_star e2 e3 -> ss_star e1 e3.
Proof.
  induction 1; intros; auto.
  apply ss_starT with e2; auto.
Qed.

Lemma letFirst : forall e v e2 x, ss_star e (Eval v) -> ss_star (Elet x e e2) (Elet x (Eval v) e2).
Proof.
  intros; induction H; eauto using step, ss_star.
Qed.

Theorem soundness_helper_ss: forall e e' (H: step e e') v, reduce e' v -> reduce e v.
Proof.
  induction 1; inversion 1; subst; eauto using reduce.
Qed.

Theorem soundness_ss: forall e v, ss_star e (Eval v) -> reduce e v.
Proof.
  intros; remember (Eval v) as e'; revert v Heqe'.
  induction H; intros; subst; eauto using reduce, soundness_helper_ss.
Qed.

Lemma pairFirst : forall e e2 v, ss_star e (Eval v) -> ss_star (Epair e e2) (Epair (Eval v) e2).
Proof.
  intros; induction H; eauto using step, ss_star.
Qed.

Lemma pairSecond : forall e e1 v, ss_star e (Eval v) -> ss_star (Epair e1 e) (Epair e1 (Eval v)).
Proof.
  intros; induction H; eauto using step, ss_star.
Qed.

Theorem completeness_ss: forall e v, reduce e v -> ss_star e (Eval v).
Proof.
  intros; induction H; subst; try (assert (ss_star (Elet x e1 e2) (Elet x (Eval v1) e2)) by eauto using letFirst); eauto using step, ss_star, ss_star_one, ss_star_trans.
  eauto 6 using pairFirst, pairSecond, ss_star_trans, step, ss_star_one.
Qed.

Inductive recover_star (r:res) : res -> Prop :=
| recover_starR: recover_star r r
| recover_starT r2 r3: recover_star r r2 -> recover r2 r3 -> recover_star r r3
.

Lemma fp_implies_ff: forall e v, reducef e (Rval v) -> reduce e v.
Proof.
  intros.
  remember (Rval v) as x. revert v Heqx.
  induction H; intros; clarify; eauto using reduce.
  assert (exists v1, exists v2, r1 = (Rval v1) /\ r2 = (Rval v2) /\ v = (Vpair v1 v2)) by apply (res_combine_values r1 r2 v Heqx).
  des. subst. eauto using reduce.
Qed.

Lemma fp_recover_transitivity : forall e r1 r2, reducef e r1 -> recover r1 r2 -> reducef e r2.
Proof.
  intros.
  revert r2 H0.
  induction H; intros; try now inv H0; eauto using reducef.
    inv H1. eauto using reducef.
    remember (r1 # r2) as r; symmetry in Heqr; revert r1 r2 H H0 H1 IHreducef1 IHreducef2 Heqr.
    induction r; intros; try by exfalso; eauto using res_combine_bot, res_combine_rletl, res_combine_rletr.
    by eapply res_combine_values in Heqr; desf; ins; inv H1; eauto using reducef, reducef_tuple.
    by eapply res_combine_ptuple in Heqr; desf; inv H1; eauto using reducef, reducef_tuple.
    induction r2; try now inv H1; eauto using reducef.
    induction r; inv H2;
    try now eauto using reducef;
    try now eauto using reducef; inv H4; eauto using reducef.
Qed.

Lemma recover_implies_fp: forall e r, recover_star (Rbot e) r -> reducef e r.
Proof.
  intros.
  remember (Rbot e) as x.
  revert e Heqx.
  induction H; intros; subst; eauto using reducef.
  assert (recover_star (Rbot e) r3) by eauto using recover_star.
  assert (reducef e r2).
  apply (IHrecover_star e); reflexivity.
  eauto using fp_recover_transitivity.
Qed.

Theorem Correctness: forall e v, recover_star (Rbot e) (Rval v) -> reduce e v.
Proof.
  intros; eauto using recover_implies_fp, fp_implies_ff.
Qed.

Lemma completeness_one_step: forall e v, reduce e v -> recover (Rbot e) (Rval v).
Proof.
  intros. constructor.
    induction H; eauto using reducef, reducef_tuple.
Qed.

Theorem Completeness: forall e v, reduce e v -> recover_star (Rbot e) (Rval v).
Proof.
  eauto using recover_star, completeness_one_step.
Qed.

Inductive geq : res -> res -> Prop :=
| Geq_Bot r e: geq r (Rbot e)
| Geq_Val v r: match r with Rval v' => v' = v | _ => True end -> geq (Rval v) r
| Geq_Ptuple r11 r12 r21 r22:
  geq r11 r21 ->
  geq r12 r22 ->
  geq (Rptuple r11 r12) (Rptuple r21 r22)
| Geq_letl r1 r2 x e:
  geq r1 r2 ->
  geq (Rletl r1 x e) (Rletl r2 x e)
| Geq_letr1 r1 r2 x e:
  geq (Rletr r1) (Rletl r2 x e)
| Geq_letr2 r1 r2:
  geq r1 r2 ->
  geq (Rletr r1) (Rletr r2).

Inductive pseq : res -> res -> Prop :=
| PSeq_Bot e' e: pseq (Rbot e') (Rbot e)
| PSeq_Val v: pseq (Rval v) (Rval v)
| PSeq_Ptuple r11 r12 r21 r22:
  pseq r11 r21 ->
  pseq r12 r22 ->
  pseq (Rptuple r11 r12) (Rptuple r21 r22)
| PSeq_letl r1 r2 x e:
  pseq r1 r2 ->
  pseq (Rletl r1 x e) (Rletl r2 x e)
| PSeq_letr2 r1 r2:
  pseq r1 r2 ->
  pseq (Rletr r1) (Rletr r2).

Lemma geq_reflexive: forall r, geq r r.
Proof.
  intros; induction r; eauto using geq.
Qed.

Lemma geq_impl_pseq: forall r1 r2, geq r1 r2 -> geq r2 r1 -> pseq r1 r2.
Proof.
  intros r1 r2 A B; induction A; inv B; eauto 8 using pseq.
Qed.

Lemma geq_transitive: forall r1 r2 r3, geq r1 r2 -> geq r2 r3 -> geq r1 r3.
Proof.
  intros r1 r2 r3 A B; revert r3 B.
  induction A; intros; inversion B; subst; eauto using geq.
    constructor.
    rewrite <- H. assumption.
Qed.

Theorem Progress: forall r1 r2, recover r1 r2 -> geq r2 r1.
Proof.
  intros.
  induction H; try constructor; eauto.
  unfold res_combine in *.
  induction r1'; induction r2'; subst; eauto using geq.
Qed.

Theorem ff_deterministic: forall e v1 v2 (RED1: reduce e v1) (RED2: reduce e v2), v1 = v2.
Proof.
  intros.
  revert v2 RED2.
  induction RED1; intros; inv RED2; eauto using reduce.
  apply (IHRED1_2 v0).
  assert (v1 = v4) by eauto; subst; eauto.
  f_equal; eauto.
Qed.

Theorem fp_deterministic: forall e v1 v2 (RED1: reducef e (Rval v1)) (RED2: reducef e (Rval v2)), v1 = v2.
Proof.
  intros; eauto using fp_implies_ff, ff_deterministic.
Qed.

Inductive mpstep_star : proc_map -> result_map -> proc_map -> result_map -> Prop :=
| mpstep_starR pm rm : mpstep_star pm rm pm rm
| mpstep_starT pm rm pm' rm' pm'' rm'': mpstep pm rm pm' rm' -> mpstep_star pm' rm' pm'' rm'' -> mpstep_star pm rm pm'' rm''.

Lemma mpstep_star_one: forall pm rm pm' rm', mpstep pm rm pm' rm' -> mpstep_star pm rm pm' rm'.
Proof.
  intros.
    apply mpstep_starT with pm' rm'. auto.
    apply mpstep_starR.
Qed.

Lemma mpstep_star_trans: forall pm rm pm' rm' pm'' rm'', mpstep_star pm rm pm' rm' -> mpstep_star pm' rm' pm'' rm'' -> mpstep_star pm rm pm'' rm''.
Proof.
  induction 1; intros.
    auto.
    apply mpstep_starT with pm' rm'; auto.
Qed.

Lemma rm_rus B rm id (b: B): projT1 (ff_update rm id b) id = Some b.
Proof.
  unfold ff_update; simpl; desf.
Qed.

Lemma rm_ruo B rm id (b: B) id' (NEQ: id <> id'): projT1 (ff_update rm id b) id' = projT1 rm id'.
Proof.
  unfold ff_update; simpl; desf.
Qed.

Lemma ss_impl_mpstep_s: forall e e' (S: ss_star e e') s es ss d pm pid rm,
  projT1 pm pid = Some (PCrun e s es ss, d) ->
  exists pm',
    mpstep_star pm rm pm' rm
    /\ projT1 pm' pid = Some (PCrun e' s es ss, d).
Proof.
  induction 1; intros; eauto using mpstep_star.
  edestruct IHS as (pm' & ? & ?); [eapply rm_rus|].
  eexists,; [eapply mpstep_starT|]; eauto; eauto using mpstep, spstep.
Qed.

Lemma ss_impl_mpstep_s_start: forall e e' s d pm pid rm,
  ss_star e e' ->
  projT1 pm pid = Some (PCstart e s, d) ->
  exists pm', mpstep_star pm rm pm' rm /\ projT1 pm' pid = Some (PCrun e' s e s, d).
Proof.
  ins; eapply ss_impl_mpstep_s with (pm := ff_update pm _ _) in H; eauto using rm_rus.
  des; eexists,; [eapply mpstep_starT|]; vauto.
Qed.

Fixpoint stack_app lc s :=
  match lc with
    | nil => s
    | cons C l => S_cons C (stack_app l s)
  end.

Fixpoint exp_app lc e :=
  match lc with
    | nil => e
    | cons C l => exp_app l (appctx_context_exp C e)
  end.

Fixpoint stack_last (s:stack) : stack :=
match s with
| S_cons C s' => stack_last s'
| _ => s
end.

Fixpoint stack_conts (s:stack) :=
  match s with
    | S_cons C s' => C :: stack_conts s'
    | _ => nil
  end.

Fixpoint app_stack (s:stack) (e:exp) : exp :=
match s with
| S_cons C s' => app_stack s' (appctx_context_exp C e)
| _ => e
end.

Lemma exp_app_app l1 l2 : forall e,
  exp_app (l1 ++ l2) e = exp_app l2 (exp_app l1 e).
Proof.
  induction l1; ins.
Qed.

Lemma app_stack1 s e: app_stack s e = exp_app (stack_conts s) e.
Proof.
  revert e; induction s; ins; rewrite exp_app_app, IHs; ins.
Qed.

Lemma rm_ru :
  forall B rm id (b : B) id' b',
  projT1 (ff_update rm id' b') id = Some b <->
    id' = id /\ b' = b
  \/ projT1 rm id = Some b /\ id' <> id.
Proof.
  simpl; unfold ff_update; intros; desf; intuition congruence.
Qed.

Lemma rm_run :
  forall B rm id id' (b : B),
  projT1 (ff_update rm id b) id' = None <-> projT1 rm id' = None /\ id <> id'.
Proof.
  simpl; unfold ff_update; intros; desf; intuition congruence.
Qed.

Lemma nat_eq (pid1 pid2 : nat) : { pid1 = pid2 } + { pid1 <> pid2 }.
Proof.
  repeat decide equality.
Qed.

Fixpoint deque_taskids d :=
  match d with
    | nil => nil
    | t :: d =>
        match t with
          | T_right id _ => TIDright id
          
        end :: deque_taskids d
  end.

Fixpoint stack_taskids s :=
  match s with
    | S_left id => TIDleft id :: nil
    | S_right id => TIDright id :: nil
    | S_cons _ s => stack_taskids s
  end.

Definition taskids pcdo :=
  match pcdo with
    | Some (pc, d) =>
      (match pc with
         | PCstart es ss => stack_taskids ss
         | PCrun _ _ es ss => stack_taskids ss
         | PCfail es ss => stack_taskids ss
         | _ => nil
       end) ++ deque_taskids d
    | None => nil
  end.

Definition rm_taskids x :=
  match x with
    | None => nil
    | Some (B_neither s) => stack_taskids s
    | Some (B_left _ s) => stack_taskids s
    | Some (B_right _ s) => stack_taskids s
    | Some (B_finished _) => nil
  end.

Definition allowed_taskid (rm : ffun _) tid :=
  match tid with
    | TIDleft id => match projT1 rm id with
                      | Some (B_neither s) | Some (B_right _ s) => True
                      | _ => False
                    end
    | TIDright id => match projT1 rm id with
                       | Some (B_neither s) | Some (B_left _ s) => True
                       | _ => False
                     end
  end.

Fixpoint count_rec B (f : nat -> option B) (g: B -> Z) m n :=
  match n with 0 => 0%Z | S n =>
  Zplus match f (m + n) with None => 0 | Some k => g k end (count_rec f g m n)
  end.

Definition count B (f : ffun B) g :=
  count_rec (projT1 f) g 0 (projT1 (projT2 f)).

Lemma count_helper B (f: ffun B) g n :
  count f g = count_rec (projT1 f) g 0 (max (projT1 (projT2 f)) n).
Proof.
  destruct f as (f & n' & PF); unfold count; simpl.
  destruct (Max.max_spec n' n) as [[? ->]|[? ->]]; try done.
  replace n with ((n - n') + n').
    induction (n - n'); ins; rewrite PF; ins; omega.
  apply NPeano.Nat.sub_add; auto with arith.
Qed.

Lemma count_split B (f: nat -> option B) g m n1 n2 :
  count_rec f g m (n1 + n2) =
  Zplus (count_rec f g m n1)
        (count_rec f g (m + n1) n2).
Proof.
  induction n2; ins; rewrite ?NPeano.Nat.add_0_r, ?NPeano.Nat.add_succ_r; ins;
     try omega.
  rewrite Plus.plus_assoc; desf; omega.
Qed.

Lemma count_rec_upd :
  forall B f g k (b: B) m n,
    k < m \/ k >= m + n ->
    count_rec (fun y => if Peano_dec.eq_nat_dec k y then Some b else f y) g m n =
    count_rec f g m n.
Proof.
  induction n; ins; destruct (Peano_dec.eq_nat_dec); omega.
Qed.

Lemma count_update B (f: ffun B) g id v :
  count (ff_update f id v) g =
    (count f g + g v - match projT1 f id with None => 0 | Some x => g x end)%Z.
Proof.
  rewrite (count_helper f g (S id)).
  destruct f as (f & n & PF); unfold count; simpl.
  replace (max n (S id)) with (id + 1 + (n - S id)).
    2: pose proof (Max.max_spec n (S id)); omega.
  rewrite !count_split; simpl.
  rewrite !count_rec_upd, !Plus.plus_0_r; try omega; simpl.
  desf; ins; omega.
Qed.

Fixpoint stack_istid tid s :=
  (match s, tid with
    | S_cons _ s', _ => stack_istid tid s'
    | S_left id, TIDleft id' => if eq_nat_dec id id' then 1 else 0
    | S_right id, TIDright id' => if eq_nat_dec id id' then 1 else 0
    | _, _ => 0
  end)%Z.

Definition tid_eq : forall x y : taskid, { x = y } + { x <> y }.
Proof.
  decide equality; apply eq_nat_dec.
Qed.

Fixpoint count_list x l :=
  match l with
    | nil => 0%Z
    | y :: l' => if tid_eq x y then (1 + count_list x l')%Z else count_list x l'
  end.

Arguments Zplus : simpl never.

Lemma count_list_app x l1 l2 :
  count_list x (l1 ++ l2) = (count_list x l1 + count_list x l2)%Z.
Proof.
  induction l1; ins; desf; omega.
Qed.

Definition task_istid tid t :=
  (match t, tid with
    | T_right id _, TIDright id' => if eq_nat_dec id id' then 1 else 0
    
    | _, _ => 0
  end)%Z.

Fixpoint list_sum A f (l: list A) :=
  (match l with
    | nil => 0
    | x :: l => f x + list_sum f l
  end)%Z.

Lemma list_sum_app A f (l1 l2 : list A):
  (list_sum f (l1 ++ l2) = list_sum f l1 + list_sum f l2)%Z.
Proof.
  induction l1; ins; omega.
Qed.

Definition pm_istid tid pcd :=
  let '(pc,d) := pcd in
  (match pc with
     | PCstart es ss => stack_istid tid ss
     | PCrun _ _ es ss => stack_istid tid ss
     | PCfail es ss => stack_istid tid ss
     | _ => 0
   end + list_sum (task_istid tid) d)%Z.

Definition rm_istid tid x :=
  match x with
    | (B_neither s)
    | (B_left _ s)
    | (B_right _ s) => stack_istid tid s
    | (B_finished _) => 0%Z
  end.

Definition well_formed_nd (pm:proc_map) (rm:result_map) :=
  forall id,
   (count pm (pm_istid (TIDleft id)) +
    count rm (rm_istid (TIDleft id)) =
      match projT1 rm id with
        | Some (B_neither _) | Some (B_right _ _) => 1
        | _ => 0
      end /\
    count pm (pm_istid (TIDright id)) +
    count rm (rm_istid (TIDright id)) =
      match projT1 rm id with
        | Some (B_neither _) | Some (B_left _ _) => 1
        | _ => 0
      end )%Z.

Definition well_formed_nd_alt (pm:proc_map) (rm:result_map) :=

  << PPND: forall pid1 pid2 (NEQ: pid1 <> pid2),
             NoDup (taskids (projT1 pm pid1) ++ taskids (projT1 pm pid2)) >> /\

  << RRND : forall id1 id2 (NEQ: id1 <> id2),
             NoDup (rm_taskids (projT1 rm id1) ++ rm_taskids (projT1 rm id2)) >> /\
  << PRND : forall pid id, NoDup (taskids (projT1 pm pid) ++ rm_taskids (projT1 rm id)) >> /\
  << PALL : forall pid x (IN: In x (taskids (projT1 pm pid))), allowed_taskid rm x >> /\
  << RALL : forall id x (IN: In x (rm_taskids (projT1 rm id))), allowed_taskid rm x >>.

Lemma wf_preserved_nd pm rm pm' rm'
      (WF: well_formed_nd pm rm)
      (SEQ: forall pid e s es ss d (PEQ: projT1 pm pid = Some (PCrun e s es ss, d)) tid,
              stack_istid tid s = stack_istid tid ss)
      (STEP: mpstep pm rm pm' rm') :
  well_formed_nd pm' rm'.
Proof.
  unfold well_formed_nd in *; ins.
  generalize (WF id); clear WF; inv STEP;
    try match goal with H : spstep _ _ |- _ => inv H end;
    simpl; rewrite ?count_update; simpl;
  repeat destruct eq_nat_dec; clarify;
  repeat match goal with
      H : _ = _ |- _ => rewrite H; simpl
    | H : projT1 pm _ = Some (PCrun _ _ _ _, _) |- _ => rewrite (SEQ _ _ _ _ _ _ H)
    end;
   rewrite ?list_sum_app; simpl;
  repeat match goal with
      H : projT1 pm _ = Some (PCrun _ _ _ _, _) |- _ =>
      rewrite <- (SEQ _ _ _ _ _ _ H); simpl
    end;
  repeat destruct eq_nat_dec; clarify; omega.
Qed.

Lemma in_count x l : In x l <-> (0 < count_list x l)%Z.
Proof.
  induction l; ins; rewrite IHl; clear; split; ins; desf; vauto.
  by clear; induction l; ins; desf; omega.
  by clear; induction l; ins; desf; omega.
Qed.

Lemma nodup_count l (H: forall x, (count_list x l <= 1)%Z): NoDup l.
Proof.
  induction l; econstructor.
    specialize (H a); ins; desf; rewrite in_count; omega.
  eapply IHl; intros; specialize (H x); ins; desf; omega.
Qed.

Lemma count1_int B (f : nat -> option B) g (POS: forall y:B, (0 <= g y)%Z) n x b:
  x < n ->
  f x = Some b ->
  (0 <= g b <= count_rec f g 0 n)%Z.
Proof.
  split; auto; induction n; ins; [omega|].
  destruct (eq_nat_dec x n).
    desf; clear - POS.
    induction n; ins; desf; try specialize (POS b0); omega.
  assert (X: x < n) by omega.
  specialize (IHn X); desf; try specialize (POS b0); omega.
Qed.

Lemma count1 B (f: ffun B) g (POS: forall y, (0 <= g y)%Z) x:
  match (projT1 f x) with
    | None => True
    | Some y => (0 <= g y <= count f g)%Z
  end.
Proof.
  desf; unfold count; destruct f as (f & n & H); ins.
  destruct (lt_dec x n); [|rewrite H in *; try done; omega].
  eauto using count1_int.
Qed.

Lemma count2 B (f: ffun B) g (POS: forall y, (0 <= g y)%Z) x y (NEQ: x <> y) :
  match projT1 f x, projT1 f y with
    | Some x, Some y => (0 <= g x + g y <= count f g)%Z
    | None, Some x
    | Some x, None => (0 <= g x <= count f g)%Z
    | None, None => True
  end.
Proof.
  desf; unfold count in *; destruct f as (f & n & H); ins;
    try (destruct (lt_dec x n); [|rewrite H in Heq; try done; omega]);
    try (destruct (lt_dec y n); [clear H|rewrite H in Heq0; try done; omega]);
    eauto using count1_int.

  induction n; ins; [omega|].
  destruct (eq_nat_dec x n), (eq_nat_dec y n); desf;
    try assert (X: x < n) by omega;
    try assert (Y: y < n) by omega;
    try specialize (POS b1); try omega; try tauto.
  eapply count1_int in Heq0; try split; eauto using Z.add_nonneg_nonneg; try omega.
  eapply count1_int in Heq; try split; eauto using Z.add_nonneg_nonneg; try omega.
  intuition.
Qed.

Lemma count_list_stack x s:
  count_list x (stack_taskids s) = stack_istid x s.
Proof.
  induction s; ins; desf.
Qed.

Lemma count_list_deque x d:
  count_list x (deque_taskids d) = list_sum (task_istid x) d.
Proof.
  induction d; ins; desf; ins; desf; omega.
Qed.

Lemma stack_istid_nonneg x s: (0 <= stack_istid x s)%Z.
Proof.
  induction s; ins; desf.
Qed.
Hint Resolve stack_istid_nonneg : zarith.

Lemma rm_istid_nonneg x y : (0 <= rm_istid x y)%Z.
Proof.
  destruct x, y; ins; auto with zarith.
Qed.
Hint Resolve rm_istid_nonneg : zarith.

Lemma task_istid_nonneg x y : (0 <= task_istid x y)%Z.
Proof.
  destruct x, y; ins; desf.
Qed.
Hint Resolve task_istid_nonneg : zarith.

Lemma list_sum_nonneg A f l (H: forall x:A, (0 <= f x)%Z) : (0 <= list_sum f l)%Z.
Proof.
  induction l; ins; desf; auto with zarith.
Qed.
Hint Resolve list_sum_nonneg : zarith.

Lemma pm_istid_nonneg x y : (0 <= pm_istid x y)%Z.
Proof.
  destruct x, y; ins; desf; auto with zarith.
Qed.
Hint Resolve pm_istid_nonneg : zarith.

Lemma count_nonneg B f g (H: forall y : B, Zle 0 (g y)) : Zle 0 (count f g).
Proof.
  unfold count; destruct f as (f & n & M); ins; clear M.
  induction n; ins; desf; auto with zarith.
Qed.
Hint Resolve count_nonneg : zarith.

Lemma wf_ppnd pm rm (WF: well_formed_nd pm rm):
  forall pid1 pid2 (NEQ: pid1 <> pid2),
    NoDup (taskids (projT1 pm pid1) ++ taskids (projT1 pm pid2)).
Proof.
  intros; eapply nodup_count; ins; rewrite count_list_app;
  eapply (count2 pm (pm_istid x)) in NEQ; auto with zarith.
  assert (count pm (pm_istid x) <= 1)%Z.
    clear - WF; pose proof (count_nonneg rm _ (rm_istid_nonneg x));
    destruct x; specialize (WF id); [apply proj1 in WF | apply proj2 in WF];
    desf; omega.
  do 2 (desf; ins); rewrite ?count_list_app, ?count_list_stack, ?count_list_deque; omega.
Qed.

Lemma wf_rrnd pm rm (WF: well_formed_nd pm rm):
  forall id1 id2 (NEQ: id1 <> id2),
    NoDup (rm_taskids (projT1 rm id1) ++ rm_taskids (projT1 rm id2)).
Proof.
  intros; eapply nodup_count; ins; rewrite count_list_app;
  eapply (count2 rm (rm_istid x)) in NEQ; auto with zarith.
  assert (count rm (rm_istid x) <= 1)%Z.
    clear - WF; pose proof (count_nonneg pm _ (pm_istid_nonneg x));
    destruct x; specialize (WF id); [apply proj1 in WF | apply proj2 in WF];
    desf; omega.
  do 2 (desf; ins); rewrite ?count_list_app, ?count_list_stack, ?count_list_deque; omega.
Qed.

Lemma wf_prnd pm rm (WF: well_formed_nd pm rm):
  forall id1 id2,
    NoDup (taskids (projT1 pm id1) ++ rm_taskids (projT1 rm id2)).
Proof.
  intros; eapply nodup_count; ins; rewrite count_list_app;
  exploit (count1 pm (pm_istid x)); auto with zarith; instantiate (1 := id1).
  exploit (count1 rm (rm_istid x)); auto with zarith; instantiate (1 := id2).
  pose proof (count_nonneg pm _ (pm_istid_nonneg x));
  pose proof (count_nonneg rm _ (rm_istid_nonneg x)).
  assert (count pm (pm_istid x) + count rm (rm_istid x) <= 1)%Z.
    clear - WF; destruct x; specialize (WF id); [apply proj1 in WF | apply proj2 in WF];
    desf; omega.
  do 2 (desf; ins); rewrite ?count_list_app, ?count_list_stack, ?count_list_deque; omega.
Qed.

Lemma wf_nd_altI pm rm (WF: well_formed_nd pm rm) :
  well_formed_nd_alt pm rm.
Proof.
  repeat split; unnw; eauto using wf_ppnd, wf_rrnd, wf_prnd.
Case 1.
  ins; eapply in_count in IN.
  exploit (count1 pm (pm_istid x)); auto with zarith; instantiate (1 := pid).
  pose proof (count_nonneg pm _ (pm_istid_nonneg x));
  pose proof (count_nonneg rm _ (rm_istid_nonneg x)).
  destruct x; specialize (WF id); [apply proj1 in WF|apply proj2 in WF];
  do 2 (desf; ins); rewrite ?count_list_app, ?count_list_stack, ?count_list_deque in *; omega.
Case 2.
  ins; eapply in_count in IN.
  exploit (count1 rm (rm_istid x)); auto with zarith; instantiate (1 := id).
  pose proof (count_nonneg pm _ (pm_istid_nonneg x));
  pose proof (count_nonneg rm _ (rm_istid_nonneg x)).
  destruct x; specialize (WF id0); [apply proj1 in WF|apply proj2 in WF];
  do 2 (desf; ins); rewrite ?count_list_app, ?count_list_stack, ?count_list_deque in *; omega.
Qed.

Definition well_formed (pm:proc_map) (rm:result_map) :=
  (forall pid e s es ss d (PEQ: projT1 pm pid = Some (PCrun e s es ss, d)),
    << WFRo: stack_last s = stack_last ss >> /\
    << WFR: ss_star (app_stack ss es) (app_stack s e) >>) /\
  well_formed_nd pm rm.

Lemma step_app_stack e s e' (S: step e e') : step (app_stack s e) (app_stack s e').
Proof.
  revert e e' S; induction s; ins; destruct C; ins; eauto using step.
Qed.

Lemma step_exp_app e s e' (S: step e e') : step (exp_app s e) (exp_app s e').
Proof.
  revert e e' S; induction s as [|[]]; ins; eauto using step.
Qed.

Lemma NoDup_app A (l1 l2 : list A) :
  NoDup (l1 ++ l2) <-> NoDup l1 /\ NoDup l2 /\ (forall x, In x l1 -> In x l2 -> False).
Proof.
  split; induction l1; ins; intuition; vauto;
  try by inv H; try rewrite in_app_iff in *; try constructor; try tauto.
  by inv H; intuition; try constructor; eauto.
  by inv H0; intuition; eauto; constructor; try rewrite in_app_iff in *; eauto; intro; des; eauto.
Qed.

Lemma deque_taskids_app l l' :
  deque_taskids (l ++ l') = deque_taskids l ++ deque_taskids l'.
Proof.
  by induction l; ins; desf; ins; f_equal; eauto.
Qed.

Lemma allowed_taskid_upd :
  forall rm x id b,
    allowed_taskid rm x ->
    match b with
      | B_neither _ => True
      | B_left _ _ => x <> TIDleft id
      | B_right _ _ => x <> TIDright id
      | B_finished _ => x <> TIDleft id /\ x <> TIDright id
    end ->
    allowed_taskid (ff_update rm id b) x.
Proof.
  ins; destruct x; ins; desf; desf.
Qed.

Lemma wf_preserved pm rm pm' rm' (WF: well_formed pm rm) (STEP: mpstep pm rm pm' rm') :
  well_formed pm' rm'.
Proof.
  destruct WF; split; eauto using wf_preserved_nd; unnw; intros.
  inv STEP; rewrite !rm_ru in *; desf; eauto.
  inv H1; simpl; eauto using ss_starR;
   eapply H in H2; desf; eauto using ss_star_trans, ss_star_one, step_app_stack.
  eapply wf_preserved_nd; eauto; intros; exploit H; eauto.
  clear; intros [A _]; revert e es ss A; induction s; ins; clarify; eauto;
   induction ss; ins; clarify; eauto.
Qed.

Inductive cexp_rel_left (pm : proc_map) (rm: result_map) (id : identifier) (e : exp) : Prop :=
  | cexp_rel_left_Start pid d e' lc
      (PM: projT1 pm pid = Some (PCstart e' (stack_app lc (S_left id)), d))
      (EQ: e = exp_app lc e')
  | cexp_rel_left_Run pid ce s d e' lc
      (PM: projT1 pm pid = Some (PCrun ce s e' (stack_app lc (S_left id)), d))
      (EQ: e = exp_app lc e')
  | cexp_rel_left_Fail pid d e' lc
      (PM: projT1 pm pid = Some (PCfail e' (stack_app lc (S_left id)), d))
      (EQ: e = exp_app lc e')
  | cexp_rel_left_Finished v
      (RM: (exists s, projT1 rm id = Some (B_left v s)) \/
           (exists v', projT1 rm id = Some (B_finished (Vpair v v'))))
      (EQ: e = Eval v)
  | cexp_rel_left_Neither id' lc e1 e2
       (RM: projT1 rm id' = Some (B_neither (stack_app lc (S_left id))))
       (LEFT: cexp_rel_left pm rm id' e1)
       (RIGHT: cexp_rel_right pm rm id' e2)
       (EQ: e = exp_app lc (Epair e1 e2))
  | cexp_rel_left_Left id' lc v1 e2
       (RM: projT1 rm id' = Some (B_left v1 (stack_app lc (S_left id))))
       (RIGHT: cexp_rel_right pm rm id' e2)
       (EQ: e = exp_app lc (Epair (Eval v1) e2))
  | cexp_rel_left_Right id' lc e1 v2
       (RM: projT1 rm id' = Some (B_right v2 (stack_app lc (S_left id))))
       (LEFT: cexp_rel_left pm rm id' e1)
       (EQ: e = exp_app lc (Epair e1 (Eval v2)))

with cexp_rel_right (pm : proc_map) (rm : result_map) (id : identifier) (e : exp) : Prop :=
  | cexp_rel_right_Thunk pid pc d
      (PM: projT1 pm pid = Some (pc, d))
      (IN: In (T_right id e) d)
  | cexp_rel_right_Start pid d e' lc
      (PM: projT1 pm pid = Some (PCstart e' (stack_app lc (S_right id)), d))
      (EQ: e = exp_app lc e')
  | cexp_rel_right_Run pid ce s d e' lc
      (PM: projT1 pm pid = Some (PCrun ce s e' (stack_app lc (S_right id)), d))
      (EQ: e = exp_app lc e')
  | cexp_rel_right_Fail pid d e' lc
      (PM: projT1 pm pid = Some (PCfail e' (stack_app lc (S_right id)), d))
      (EQ: e = exp_app lc e')
  | cexp_rel_right_Finished v
      (RM: (exists s, projT1 rm id = Some (B_right v s)) \/
           (exists v', projT1 rm id = Some (B_finished (Vpair v' v))))
      (EQ: e = Eval v)
  | cexp_rel_right_Neither id' lc e1 e2
       (RM: projT1 rm id' = Some (B_neither (stack_app lc (S_right id))))
       (LEFT: cexp_rel_left pm rm id' e1)
       (RIGHT: cexp_rel_right pm rm id' e2)
       (EQ: e = exp_app lc (Epair e1 e2))
  | cexp_rel_right_Left id' lc v1 e2
       (RM: projT1 rm id' = Some (B_left v1 (stack_app lc (S_right id))))
       (RIGHT: cexp_rel_right pm rm id' e2)
       (EQ: e = exp_app lc (Epair (Eval v1) e2))
  | cexp_rel_right_Right id' lc e1 v2
       (RM: projT1 rm id' = Some (B_right v2 (stack_app lc (S_right id))))
       (LEFT: cexp_rel_left pm rm id' e1)
       (EQ: e = exp_app lc (Epair e1 (Eval v2)))
.

Scheme cexp_rel_left_ind1 := Induction for cexp_rel_left Sort Prop

with cexp_rel_right_ind1 := Induction for cexp_rel_right Sort Prop.

Combined Scheme cexp_rel_ind from cexp_rel_left_ind1, cexp_rel_right_ind1.

Lemma finished_stable pm rm pm' rm'
  (STEP : mpstep pm rm pm' rm') id v
  (RM : projT1 rm id = Some (B_finished v)) :
  projT1 rm' id = Some (B_finished v).
Proof.
  inv STEP; ins; desf; vauto.
Qed.

Lemma mpstep_neither pm rm pm' rm'
  (STEP : mpstep pm rm pm' rm') id s
  (RM : projT1 rm id = Some (B_neither s)) :
  projT1 rm' id = Some (B_neither s) \/
  (exists v pid d es ss,
    projT1 rm' id = Some (B_left v s) /\
    projT1 pm pid = Some (PCrun (Eval v) (S_left id) es ss, d) /\
    projT1 pm' pid = Some (PCfinish, d) \/
    projT1 rm' id = Some (B_right v s) /\
    projT1 pm pid = Some (PCrun (Eval v) (S_right id) es ss, d) /\
    projT1 pm' pid = Some (PCfinish, d)).
Proof.
  inv STEP; rewrite ?rm_ru; try destruct (nat_eq id0 id); vauto;
  try by right; repeat eexists; eauto using rm_rus.
Qed.

Lemma mpstep_left pm rm pm' rm'
  (STEP : mpstep pm rm pm' rm') id v s
  (RM : projT1 rm id = Some (B_left v s)) :
  projT1 rm' id = Some (B_left v s) \/
  (exists v' pid d es ss,
    projT1 rm' id = Some (B_finished (Vpair v v')) /\
    projT1 pm pid = Some (PCrun (Eval v') (S_right id) es ss, d) /\
    projT1 pm' pid = Some (PCstart (Eval (Vpair v v')) s, d)).
Proof.
  inv STEP; rewrite ?rm_ru; try destruct (nat_eq id0 id); vauto;
  try by right; repeat eexists; eauto using rm_rus.
Qed.

Lemma mpstep_right pm rm pm' rm'
  (STEP : mpstep pm rm pm' rm') id v s
  (RM : projT1 rm id = Some (B_right v s)) :
  projT1 rm' id = Some (B_right v s) \/
  (exists v' pid d es ss,
    projT1 rm' id = Some (B_finished (Vpair v' v)) /\
    projT1 pm pid = Some (PCrun (Eval v') (S_left id) es ss, d) /\
    projT1 pm' pid = Some (PCstart (Eval (Vpair v' v)) s, d)).
Proof.
  inv STEP; rewrite ?rm_ru; try destruct (nat_eq id0 id); vauto;
  try by right; repeat eexists; eauto using rm_rus.
Qed.

Lemma ss_star_exp_app e s e' (S: ss_star e e') : ss_star (exp_app s e) (exp_app s e').
Proof.
  induction S; eauto using step_exp_app, ss_star.
Qed.

Lemma ss_star_pair :
  forall e1 e1' (S1: ss_star e1 e1') e2 e2' (S2: ss_star e2 e2'),
    ss_star (Epair e1 e2) (Epair e1' e2').
Proof.
  induction 1; induction 1; eauto using step, ss_star.
Qed.

Lemma start_step pm rm pm' rm'
  (STEP : mpstep pm rm pm' rm') pid e s d
  (PM : projT1 pm pid = Some (PCstart e s, d)) :
  exists d',
  projT1 pm' pid = Some (PCstart e s, d') \/
  projT1 pm' pid = Some (PCrun e s e s, d').
Proof.
  inv STEP; eauto;
    destruct (nat_eq pid1 pid); try destruct (nat_eq pid2 pid); subst;
      repeat first [rewrite rm_rus | rewrite rm_ruo; [|done]]; clarify; eauto.
  inv H; eauto.
Qed.

Lemma run_step pm rm pm' rm'
  (STEP : mpstep pm rm pm' rm') pid e s es ss d
  (PM : projT1 pm pid = Some (PCrun e s es ss, d)) :
  (exists e' s' d', projT1 pm' pid = Some (PCrun e' s' es ss, d')) \/
  (projT1 pm' pid = Some (PCfail es ss, d)) \/
  (exists e1 e2 id,
    e = Epair e1 e2 /\
    projT1 rm id = None /\
    pm' = ff_update pm pid (PCstart e1 (S_left id), T_right id e2 :: d) /\
    rm' = ff_update rm id (B_neither s)) \/
  (exists v id s',
    e = Eval v /\
    s = S_left id /\
    projT1 rm id = Some (B_neither s') /\
    pm' = ff_update pm pid (PCfinish, d) /\
    rm' = ff_update rm id (B_left v s')) \/
  (exists v1 v2 id s',
    e = Eval v1 /\
    s = S_left id /\
    projT1 rm id = Some (B_right v2 s') /\
    pm' = ff_update pm pid (PCstart (Eval (Vpair v1 v2)) s', d) /\
    rm' = ff_update rm id (B_finished (Vpair v1 v2))) \/
  (exists v id s',
    e = Eval v /\
    s = S_right id /\
    projT1 rm id = Some (B_neither s') /\
    pm' = ff_update pm pid (PCfinish, d) /\
    rm' = ff_update rm id (B_right v s')) \/
  (exists v1 v2 id s',
    e = Eval v2 /\
    s = S_right id /\
    projT1 rm id = Some (B_left v1 s') /\
    pm' = ff_update pm pid (PCstart (Eval (Vpair v1 v2)) s' , d) /\
    rm' = ff_update rm id (B_finished (Vpair v1 v2))).
Proof.
  inv STEP;
    destruct (nat_eq pid1 pid); try destruct (nat_eq pid2 pid); subst;
      repeat first [rewrite rm_rus | rewrite rm_ruo; [|done]]; clarify;
    try (by left; repeat eexists; eauto).
  by do 2 right; left; repeat eexists; eauto.
  by inv H; eauto; try by left; repeat eexists; eauto.
  by do 3 right; left; repeat eexists; eauto.
  by do 4 right; left; repeat eexists; eauto.
  by do 5 right; left; repeat eexists; eauto.
  by do 6 right; repeat eexists; eauto.
Qed.

Lemma fail_step pm rm pm' rm'
  (STEP : mpstep pm rm pm' rm') pid es ss d
  (PM : projT1 pm pid = Some (PCfail es ss, d)) :
  (exists d', projT1 pm' pid = Some (PCfail es ss, d')) \/
  (exists pid' d', projT1 pm' pid' = Some (PCstart es ss, d')).
Proof.
  inv STEP;
    destruct (nat_eq pid1 pid); try destruct (nat_eq pid2 pid); subst;
      repeat first [rewrite rm_rus | rewrite rm_ruo; [|done]]; clarify;
    try (by left; repeat eexists; eauto).
  by right; exists pid2; eauto using rm_rus.
  by inv H.
Qed.

Lemma indeq_step pm rm pm' rm'
  (STEP : mpstep pm rm pm' rm') pid pc d
  (PM : projT1 pm pid = Some (pc, d)) x
  (IN : In x d):
  (exists pid' pc' d', projT1 pm' pid' = Some (pc', d') /\ In x d') \/
  (exists id e d, x = T_right id e /\ projT1 pm' pid = Some (PCstart e (S_right id), d)).
Proof.
  inv STEP;
   destruct (nat_eq pid1 pid); try destruct (nat_eq pid2 pid); subst;
      repeat first [rewrite rm_rus | rewrite rm_ruo; [|done]]; clarify;
    try (match goal with H : spstep _ _ _ _ |- _ => inv H end);
    try (eapply in_app_or in IN); simpl in IN; des; clarify; eauto 6;
    try (by left; repeat eexists; try eapply rm_ru; eauto using rm_rus, in_cons, in_eq);
    try (by left; repeat eexists; try eapply rm_ru; eauto);
    try (by clear H H0; left; repeat eexists; [eapply rm_ru; right; split; [eapply rm_ru|]|]; eauto).
Qed.

Lemma stack_taskids_app lc s:
  stack_taskids (stack_app lc s) = stack_taskids s.
Proof.
  induction lc; eauto.
Qed.

Lemma stack_app_det_left: forall lc lc' id,
  stack_app lc (S_left id) = stack_app lc' (S_left id) ->
  lc = lc'.
Proof.
  induction lc; destruct lc'; ins; clarify; f_equal; eauto.
Qed.

Lemma stack_app_det_right: forall lc lc' id,
  stack_app lc (S_right id) = stack_app lc' (S_right id) ->
  lc = lc'.
Proof.
  induction lc; destruct lc'; ins; clarify; f_equal; eauto.
Qed.

Lemma In_right_deq id e d:
  In (T_right id e) d -> In (TIDright id) (deque_taskids d).
Proof.
  induction d; ins; intuition; desf; ins; desf; eauto.
Qed.