Library lang

Require Import Arith.
Require Import Bool.
Require Import List.

Require Import Omega ClassicalChoice basis .

Set Implicit Arguments.


Definition ffun B :=
  { f: nat -> option B & { n | forall m (LEQ: n <= m), f m = None} }.

Program Definition empty_map B : ffun B :=
  existT _ (fun y => None) (existT _ 0 _).

Program Definition ff_update B (r: ffun B) (x : nat) (b: B) : ffun B :=
  existT _ (fun y => if Peano_dec.eq_nat_dec x y then Some b else projT1 r y)
   (existT _ (max (projT1 (projT2 r)) (S x)) _).
Next Obligation.
  destruct r as (r & n & H); simpl in *.
  destruct (Peano_dec.eq_nat_dec x m); subst.
  eapply Max.max_lub_r in LEQ; omega.
  eauto using Max.max_lub_l.
Qed.


Definition termvar := nat.
Lemma eq_termvar: forall (x y : termvar), {x = y} + {x <> y}.
Proof.
  decide equality; auto with ott_coq_equality arith.
Defined.
Hint Resolve eq_termvar : ott_coq_equality.

Inductive val : Set :=
 | Vvar (x:termvar)
 | Vint (n:nat)
 | Vpair (v1:val) (v2:val)
 | Vfunc (f:termvar) (x:termvar) (e:exp)
with exp : Set :=
 | Eval (v:val)
 | Eplus (v1:val) (v2:val)
 | Epair (e1:exp) (e2:exp)
 | Elet (x:termvar) (e1:exp) (e2:exp)
 | Efst (v:val)
 | Esnd (v:val)
 | Eifnz (v:val) (e1:exp) (e2:exp)
 | Eapp (v1:val) (v2:val) .

Inductive context : Set :=
 | C_pairL (e2:exp)
 | C_pairR (e1:exp)
 | C_letL (x:termvar) (e2:exp) .

Definition identifier : Set := nat.

Inductive stack : Set :=
 | S_left (id:identifier)
 | S_right (id:identifier)
 | S_cons (C:context) (s:stack).

Inductive task : Set :=
 | T_right (id:identifier) (e:exp).

Inductive branch : Set :=
 | B_neither (s:stack)
 | B_left (v:val) (s:stack)
 | B_right (v:val) (s:stack)
 | B_finished (v:val).

Definition pidentifier : Set := nat.

Definition deque : Set := list task.

Inductive proc_config : Set :=
 | PCstart (e:exp) (s:stack)
 | PCrun (e:exp) (s:stack) (e':exp) (s':stack)
 | PCfinish : proc_config
 | PCfail (e':exp) (s':stack)
 | PCrecover : proc_config.

Inductive res : Set :=
 | Rval (v:val)
 | Rbot (e:exp)
 | Rletl (r:res) (x:termvar) (e:exp)
 | Rletr (r:res)
 | Rptuple (r1:res) (r2:res).

Inductive taskid : Set :=
 | TIDleft (id:identifier)
 | TIDright (id:identifier).

Definition result_map : Type := ffun branch.

Definition proc_map : Type := ffun (proc_config * deque).

Definition appctx_context_exp (context5:context) (exp5:exp) : exp :=
  match context5 with
  | (C_pairL e2) => (Epair exp5 e2)
  | (C_pairR e1) => (Epair e1 exp5)
  | (C_letL x e2) => (Elet x exp5 e2)
end.

Fixpoint subst_val (v_5:val) (x5:termvar) (v__6:val) {struct v__6} : val :=
  match v__6 with
  | (Vvar x) => (if eq_termvar x x5 then v_5 else (Vvar x))
  | (Vint n) => Vint n
  | (Vpair v1 v2) => Vpair (subst_val v_5 x5 v1) (subst_val v_5 x5 v2)
  | (Vfunc f x e) => Vfunc f x (if list_mem eq_termvar x5 (cons x nil) then e else (subst_exp v_5 x5 e))
end
with subst_exp (v_5:val) (x5:termvar) (e_5:exp) {struct e_5} : exp :=
  match e_5 with
  | (Eval v) => Eval (subst_val v_5 x5 v)
  | (Eplus v1 v2) => Eplus (subst_val v_5 x5 v1) (subst_val v_5 x5 v2)
  | (Epair e1 e2) => Epair (subst_exp v_5 x5 e1) (subst_exp v_5 x5 e2)
  | (Elet x e1 e2) => Elet x (subst_exp v_5 x5 e1) (subst_exp v_5 x5 e2)
  | (Efst v) => Efst (subst_val v_5 x5 v)
  | (Esnd v) => Esnd (subst_val v_5 x5 v)
  | (Eifnz v e1 e2) => Eifnz (subst_val v_5 x5 v) (subst_exp v_5 x5 e1) (subst_exp v_5 x5 e2)
  | (Eapp v1 v2) => Eapp (subst_val v_5 x5 v1) (subst_val v_5 x5 v2)
end.

Definition subst_context (v5:val) (x5:termvar) (C5:context) : context :=
  match C5 with
  | (C_pairL e2) => C_pairL (subst_exp v5 x5 e2)
  | (C_pairR e1) => C_pairR (subst_exp v5 x5 e1)
  | (C_letL x e2) => C_letL x (subst_exp v5 x5 e2)
end.

Fixpoint subst_stack (v5:val) (x5:termvar) (s5:stack) {struct s5} : stack :=
  match s5 with
  | (S_left id) => S_left id
  | (S_right id) => S_right id
  | (S_cons C s) => S_cons (subst_context v5 x5 C) (subst_stack v5 x5 s)
end.

Definition subst_task (v5:val) (x5:termvar) (t5:task) : task :=
  match t5 with
  | (T_right id e) => T_right id (subst_exp v5 x5 e)
end.

Fixpoint subst_res (v5:val) (x5:termvar) (r_5:res) {struct r_5} : res :=
  match r_5 with
  | (Rval v) => Rval (subst_val v5 x5 v)
  | (Rbot e) => Rbot (subst_exp v5 x5 e)
  | (Rletl r x e) => Rletl (subst_res v5 x5 r) x (subst_exp v5 x5 e)
  | (Rletr r) => Rletr (subst_res v5 x5 r)
  | (Rptuple r1 r2) => Rptuple (subst_res v5 x5 r1) (subst_res v5 x5 r2)
end.

Definition subst_branch (v5:val) (x5:termvar) (b5:branch) : branch :=
  match b5 with
  | (B_neither s) => B_neither (subst_stack v5 x5 s)
  | (B_left v s) => B_left (subst_val v5 x5 v) (subst_stack v5 x5 s)
  | (B_right v s) => B_right (subst_val v5 x5 v) (subst_stack v5 x5 s)
  | (B_finished v) => B_finished (subst_val v5 x5 v)
end.

Definition subst_proc_config (v5:val) (x5:termvar) (pc5:proc_config) : proc_config :=
  match pc5 with
  | (PCstart e s) => PCstart (subst_exp v5 x5 e) (subst_stack v5 x5 s)
  | (PCrun e s e' s') => PCrun (subst_exp v5 x5 e) (subst_stack v5 x5 s) (subst_exp v5 x5 e') (subst_stack v5 x5 s')
  | PCfinish => PCfinish
  | (PCfail e' s') => PCfail (subst_exp v5 x5 e') (subst_stack v5 x5 s')
  | PCrecover => PCrecover
end.

Fixpoint exp_not_value (x1:exp) : Prop:=
  match x1 with
  | (Eval v) => False
  | (Eplus v1 v2) => True
  | (Epair e1 e2) => True
  | (Elet x e1 e2) => True
  | (Efst v) => True
  | (Esnd v) => True
  | (Eapp v1 v2) => True
  | (Eifnz v e1 e2) => True
end
with not_value (x1:res) : Prop:=
  match x1 with
  | (Rval v) => False
  | (Rbot e) => True
  | (Rletl r x e) => True
  | (Rletr r) => True
  | (Rptuple r1 r2) => True
end.

Fixpoint res_combine (x1:res) (x2:res) : res:=
  match x1,x2 with
  | (Rval v1) , (Rval v2) => (Rval (Vpair v1 v2))
  | r1 , r2 => (Rptuple r1 r2)
end.

Fixpoint is_zero (x1:val) : Prop:=
  match x1 with
  | (Vint 0 ) => True
  | v => False
end.

Inductive step : exp -> exp -> Prop :=
 | step_plus : forall (n1 n2:nat),
     step (Eplus (Vint n1) (Vint n2)) (Eval (Vint ( n1 + n2 ) ))
 | step_letI : forall (x:termvar) (e1 e2 e1':exp),
     step e1 e1' ->
     step (Elet x e1 e2) (Elet x e1' e2)
 | step_letII : forall (x:termvar) (v1:val) (e2:exp),
     step (Elet x (Eval v1) e2) (subst_exp v1 x e2 )
 | step_app : forall (f x:termvar) (e:exp) (v:val),
     step (Eapp (Vfunc f x e) v) (subst_exp (Vfunc f x e) f (subst_exp v x e ) )
 | step_first : forall (v1 v2:val),
     step (Efst (Vpair v1 v2)) (Eval v1)
 | step_second : forall (v1 v2:val),
     step (Esnd (Vpair v1 v2)) (Eval v2)
 | step_ifnz_true : forall (n:nat) (e1 e2:exp),
      n <> 0 ->
     step (Eifnz (Vint n) e1 e2) e1
 | step_ifnz_false : forall (e1 e2:exp),
     step (Eifnz (Vint 0 ) e1 e2) e2
 | step_par_left : forall (e1 e2 e1':exp),
     step e1 e1' ->
     step (Epair e1 e2) (Epair e1' e2)
 | step_par_right : forall (e1 e2 e2':exp),
     step e2 e2' ->
     step (Epair e1 e2) (Epair e1 e2')
 | step_par_join : forall (v1 v2:val),
     step (Epair (Eval v1) (Eval v2)) (Eval (Vpair v1 v2)).

Inductive spstep : proc_config -> proc_config -> Prop :=
 | spstep_eval : forall (e1:exp) (s:stack) (e':exp) (s':stack) (e2:exp),
     step e1 e2 ->
     spstep (PCrun e1 s e' s') (PCrun e2 s e' s')
 | spstep_run : forall (e:exp) (s:stack),
     spstep (PCstart e s) (PCrun e s e s)
 | spstep_push_context : forall (C:context) (e:exp) (s:stack) (e':exp) (s':stack),
      (exp_not_value e ) ->
     spstep (PCrun (appctx_context_exp C e ) s e' s') (PCrun e (S_cons C s) e' s')
 | spstep_apply_context : forall (v:val) (C:context) (s:stack) (e':exp) (s':stack),
     spstep (PCrun (Eval v) (S_cons C s) e' s') (PCrun (appctx_context_exp C (Eval v) ) s e' s')
 | spstep_fail : forall (e:exp) (s:stack) (e':exp) (s':stack),
     spstep (PCrun e s e' s') (PCfail e' s').

Inductive mpstep : proc_map -> result_map -> proc_map -> result_map -> Prop :=
 | mpstep_fork : forall (pm:proc_map) (rm:result_map) (pid1:pidentifier) (e1:exp) (id:identifier) (e2:exp) (d:deque) (s:stack) (e':exp) (s':stack),
      projT1 pm pid1 = Some ( (PCrun (Epair e1 e2) s e' s') , d ) ->
      projT1 rm id = None ->
     mpstep pm rm (ff_update pm pid1 ( (PCstart e1 (S_left id)) , ( (T_right id e2) :: d ) )) (ff_update rm id (B_neither s) )
 | mpstep_recover : forall (pm:proc_map) (rm:result_map) (pid1:pidentifier) (d:deque) (pid2:pidentifier) (e:exp) (s:stack) (d':deque),
      projT1 pm pid1 = Some ( (PCfail e s) , d ) ->
      projT1 pm pid2 = Some ( PCfinish , d' ) ->
     mpstep pm rm (ff_update (ff_update pm pid1 ( PCrecover , d )) pid2 ( (PCstart e s) , d' )) rm
 | mpstep_steal : forall (pm:proc_map) (rm:result_map) (pid1:pidentifier) (pc1:proc_config) (t:task) (d1:deque) (pid2:pidentifier) (pc2:proc_config) (d2:deque),
      projT1 pm pid1 = Some ( pc1 , d1 ) ->
      projT1 pm pid2 = Some ( pc2 , ( d2 ++(cons t nil)) ) ->
      pid1 <> pid2 ->
     mpstep pm rm (ff_update (ff_update pm pid1 ( pc1 , ( t :: d1 ) )) pid2 ( pc2 , d2 )) rm
 | mpstep_local : forall (pm:proc_map) (rm:result_map) (pid1:pidentifier) (pc2:proc_config) (d:deque) (pc1:proc_config),
     spstep pc1 pc2 ->
      projT1 pm pid1 = Some ( pc1 , d ) ->
     mpstep pm rm (ff_update pm pid1 ( pc2 , d )) rm
 | mpstep_pop_task : forall (pm:proc_map) (rm:result_map) (pid1:pidentifier) (e:exp) (id:identifier) (d:deque),
      projT1 pm pid1 = Some ( PCfinish , ( (T_right id e) :: d ) ) ->
     mpstep pm rm (ff_update pm pid1 ( (PCstart e (S_right id)) , d )) rm
 | mpstep_left_first : forall (pm:proc_map) (rm:result_map) (pid1:pidentifier) (d:deque) (id:identifier) (v:val) (s:stack) (e':exp) (s':stack),
      projT1 pm pid1 = Some ( (PCrun (Eval v) (S_left id) e' s') , d ) ->
      projT1 rm id = Some (B_neither s) ->
     mpstep pm rm (ff_update pm pid1 ( PCfinish , d )) (ff_update rm id (B_left v s) )
 | mpstep_left_last : forall (pm:proc_map) (rm:result_map) (pid1:pidentifier) (v v2:val) (s:stack) (d:deque) (id:identifier) (e':exp) (s':stack),
      projT1 pm pid1 = Some ( (PCrun (Eval v) (S_left id) e' s') , d ) ->
      projT1 rm id = Some (B_right v2 s) ->
     mpstep pm rm (ff_update pm pid1 ( (PCstart (Eval (Vpair v v2)) s) , d )) (ff_update rm id (B_finished (Vpair v v2)) )
 | mpstep_right_first : forall (pm:proc_map) (rm:result_map) (pid1:pidentifier) (d:deque) (id:identifier) (v:val) (s:stack) (e':exp) (s':stack),
      projT1 pm pid1 = Some ( (PCrun (Eval v) (S_right id) e' s') , d ) ->
      projT1 rm id = Some (B_neither s) ->
     mpstep pm rm (ff_update pm pid1 ( PCfinish , d )) (ff_update rm id (B_right v s) )
 | mpstep_right_last : forall (pm:proc_map) (rm:result_map) (pid1:pidentifier) (v1 v:val) (s:stack) (d:deque) (id:identifier) (e':exp) (s':stack),
      projT1 pm pid1 = Some ( (PCrun (Eval v) (S_right id) e' s') , d ) ->
      projT1 rm id = Some (B_left v1 s) ->
     mpstep pm rm (ff_update pm pid1 ( (PCstart (Eval (Vpair v1 v)) s) , d )) (ff_update rm id (B_finished (Vpair v1 v)) ) .

Inductive reduce : exp -> val -> Prop :=
 | reduce_init : forall (v:val),
     reduce (Eval v) v
 | reduce_plus : forall (n1 n2:nat),
     reduce (Eplus (Vint n1) (Vint n2)) (Vint ( n1 + n2 ) )
 | reduce_let : forall (x:termvar) (e1 e2:exp) (v2 v1:val),
     reduce e1 v1 ->
     reduce (subst_exp v1 x e2 ) v2 ->
     reduce (Elet x e1 e2) v2
 | reduce_app : forall (f x:termvar) (e:exp) (v v1:val),
     reduce (subst_exp (Vfunc f x e) f (subst_exp v x e ) ) v1 ->
     reduce (Eapp (Vfunc f x e) v) v1
 | reduce_first : forall (v1 v2:val),
     reduce (Efst (Vpair v1 v2)) v1
 | reduce_second : forall (v1 v2:val),
     reduce (Esnd (Vpair v1 v2)) v2
 | reduce_if_true : forall (n:nat) (e1 e2:exp) (v1:val),
      n <> 0 ->
     reduce e1 v1 ->
     reduce (Eifnz (Vint n) e1 e2) v1
 | reduce_if_false : forall (e1 e2:exp) (v2:val),
     reduce e2 v2 ->
     reduce (Eifnz (Vint 0 ) e1 e2) v2
 | reduce_ptuple : forall (e1 e2:exp) (v1 v2:val),
     reduce e1 v1 ->
     reduce e2 v2 ->
     reduce (Epair e1 e2) (Vpair v1 v2).

Inductive reducef : exp -> res -> Prop :=
 | reducef_init : forall (v:val),
     reducef (Eval v) (Rval v)
 | reducef_plus : forall (n1 n2:nat),
     reducef (Eplus (Vint n1) (Vint n2)) (Rval (Vint ( n1 + n2 ) ))
 | reducef_let : forall (x:termvar) (e1 e2:exp) (v2 v1:val),
     reducef e1 (Rval v1) ->
     reducef (subst_exp v1 x e2 ) (Rval v2) ->
     reducef (Elet x e1 e2) (Rval v2)
 | reducef_app : forall (f x:termvar) (e:exp) (v2:val) (r:res),
     reducef (subst_exp (Vfunc f x e) f (subst_exp v2 x e ) ) r ->
     reducef (Eapp (Vfunc f x e) v2) r
 | reducef_first : forall (v1 v2:val),
     reducef (Efst (Vpair v1 v2)) (Rval v1)
 | reducef_second : forall (v1 v2:val),
     reducef (Esnd (Vpair v1 v2)) (Rval v2)
 | reducef_if_true : forall (n:nat) (e1 e2:exp) (r1:res),
      n <> 0 ->
     reducef e1 r1 ->
     reducef (Eifnz (Vint n) e1 e2) r1
 | reducef_if_false : forall (e1 e2:exp) (r2:res),
     reducef e2 r2 ->
     reducef (Eifnz (Vint 0 ) e1 e2) r2
 | reducef_ptuple : forall (e1 e2:exp) (r1 r2:res),
     reducef e1 r1 ->
     reducef e2 r2 ->
     reducef (Epair e1 e2) (res_combine r1 r2 )
 | reducef_bottom : forall (e:exp),
     reducef e (Rbot e)
 | reducef_letFL : forall (x:termvar) (e1 e2:exp) (r1:res),
     reducef e1 r1 ->
      (not_value r1 ) ->
     reducef (Elet x e1 e2) (Rletl r1 x e2)
 | reducef_letFR : forall (x:termvar) (e1 e2:exp) (r:res) (v1:val),
     reducef e1 (Rval v1) ->
     reducef (subst_exp v1 x e2 ) r ->
      (not_value r ) ->
     reducef (Elet x e1 e2) (Rletr r).

Inductive recover : res -> res -> Prop :=
 | recover_init : forall (v:val),
     recover (Rval v) (Rval v)
 | recover_bottom : forall (e:exp) (r:res),
     reducef e r ->
     recover (Rbot e) r
 | recover_letLS : forall (r:res) (x:termvar) (e:exp) (v2 v:val),
     recover r (Rval v) ->
     reducef (subst_exp v x e ) (Rval v2) ->
     recover (Rletl r x e) (Rval v2)
 | recover_letLFL : forall (r:res) (x:termvar) (e:exp) (r1:res),
     recover r r1 ->
      (not_value r1 ) ->
     recover (Rletl r x e) (Rletl r1 x e)
 | recover_letLFR : forall (r:res) (x:termvar) (e:exp) (r2:res) (v:val),
     recover r (Rval v) ->
     reducef (subst_exp v x e ) r2 ->
      (not_value r2 ) ->
     recover (Rletl r x e) (Rletr r2)
 | recover_letRS : forall (r:res) (v:val),
     recover r (Rval v) ->
     recover (Rletr r) (Rval v)
 | recover_letRF : forall (r r1:res),
     recover r r1 ->
      (not_value r1 ) ->
     recover (Rletr r) (Rletr r1)
 | recover_ptuple : forall (r1 r2 r1' r2':res),
     recover r1 r1' ->
     recover r2 r2' ->
     recover (Rptuple r1 r2) (res_combine r1' r2' ) .

Lemma recover_tuple: forall r1 r1' r2 r2' r,
  recover r1 r1' ->
  recover r2 r2' ->
  r = res_combine r1' r2' ->
  recover (Rptuple r1 r2) r.
Proof. intros; subst; eauto using recover. Qed.

Lemma reducef_tuple: forall e1 r1' e2 r2' r,
  reducef e1 r1' ->
  reducef e2 r2' ->
  r = res_combine r1' r2' ->
  reducef (Epair e1 e2) r.
Proof. intros; subst; eauto using reducef. Qed.