Library iris.chan_lang.lang
From iris.program_logic Require Export ectx_language ectxi_language binders.
From iris.algebra Require Export cofe.
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
Module chan_lang.
Open Scope Z_scope.
From iris.algebra Require Export cofe.
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
Module chan_lang.
Open Scope Z_scope.
Expressions and vals.
Inductive side := cleft | cright.
Inductive label := lleft | lright.
Definition loc := positive.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) (s: side).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
| PlusOp | MinusOp | LeOp | LtOp | EqOp.
Inductive expr :=
| Var (x : string)
| Rec (f x : binder) (e : expr)
| App (e1 e2 : expr)
| Lit (l : base_lit)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
| Pair (e1 e2 : expr)
| Letp (x y : binder) (e1 e2 : expr)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
| Fork (e : expr)
| Alloc
| Recv (e : expr)
| Send (e1 : expr) (e2 : expr)
| Select (e1 : expr) (s : label)
| RCase (e0 : expr) (e1 : expr) (e2 : expr).
Bind Scope cexpr_scope with expr.
Delimit Scope cexpr_scope with C.
Arguments Rec _ _ _%C.
Arguments App _%C _%C.
Arguments Lit _.
Arguments UnOp _ _%C.
Arguments BinOp _ _%C _%C.
Arguments If _%C _%C _%C.
Arguments Pair _%C _%C.
Arguments Letp _ _ _%C _%C.
Arguments InjL _%C.
Arguments InjR _%C.
Arguments Case _%C _%C _%C.
Arguments Fork _%C.
Arguments Alloc.
Arguments Recv _%C.
Arguments Send _%C _%C.
Arguments Select _%C _.
Arguments RCase _%C _%C _%C.
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Var x ⇒ bool_decide (x ∈ X)
| Rec f x e ⇒ is_closed (f :b: x :b: X) e
| Letp x y e1 e2 ⇒ is_closed X e1 && is_closed (x :b: y :b: X) e2
| Lit _ | Alloc ⇒ true
| UnOp _ e | InjL e | InjR e | Fork e | Recv e | Select e _ ⇒
is_closed X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Send e1 e2 ⇒
is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 | RCase e0 e1 e2 ⇒
is_closed X e0 && is_closed X e1 && is_closed X e2
end.
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Instance closed_decision env e : Decision (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Inductive val :=
| RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
| LitV (l : base_lit)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Bind Scope val_scope with val.
Delimit Scope val_scope with V.
Arguments PairV _%V _%V.
Arguments InjLV _%V.
Arguments InjRV _%V.
Fixpoint of_val (v : val) : expr :=
match v with
| RecV f x e _ ⇒ Rec f x e
| LitV l ⇒ Lit l
| PairV v1 v2 ⇒ Pair (of_val v1) (of_val v2)
| InjLV v ⇒ InjL (of_val v)
| InjRV v ⇒ InjR (of_val v)
end.
Fixpoint to_val (e : expr) : option val :=
match e with
| Rec f x e ⇒
if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
| Lit l ⇒ Some (LitV l)
| Pair e1 e2 ⇒ v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
| InjL e ⇒ InjLV <$> to_val e
| InjR e ⇒ InjRV <$> to_val e
| _ ⇒ None
end.
Inductive label := lleft | lright.
Definition loc := positive.
Inductive base_lit : Set :=
| LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc) (s: side).
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
| PlusOp | MinusOp | LeOp | LtOp | EqOp.
Inductive expr :=
| Var (x : string)
| Rec (f x : binder) (e : expr)
| App (e1 e2 : expr)
| Lit (l : base_lit)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
| Pair (e1 e2 : expr)
| Letp (x y : binder) (e1 e2 : expr)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
| Fork (e : expr)
| Alloc
| Recv (e : expr)
| Send (e1 : expr) (e2 : expr)
| Select (e1 : expr) (s : label)
| RCase (e0 : expr) (e1 : expr) (e2 : expr).
Bind Scope cexpr_scope with expr.
Delimit Scope cexpr_scope with C.
Arguments Rec _ _ _%C.
Arguments App _%C _%C.
Arguments Lit _.
Arguments UnOp _ _%C.
Arguments BinOp _ _%C _%C.
Arguments If _%C _%C _%C.
Arguments Pair _%C _%C.
Arguments Letp _ _ _%C _%C.
Arguments InjL _%C.
Arguments InjR _%C.
Arguments Case _%C _%C _%C.
Arguments Fork _%C.
Arguments Alloc.
Arguments Recv _%C.
Arguments Send _%C _%C.
Arguments Select _%C _.
Arguments RCase _%C _%C _%C.
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Var x ⇒ bool_decide (x ∈ X)
| Rec f x e ⇒ is_closed (f :b: x :b: X) e
| Letp x y e1 e2 ⇒ is_closed X e1 && is_closed (x :b: y :b: X) e2
| Lit _ | Alloc ⇒ true
| UnOp _ e | InjL e | InjR e | Fork e | Recv e | Select e _ ⇒
is_closed X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Send e1 e2 ⇒
is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 | RCase e0 e1 e2 ⇒
is_closed X e0 && is_closed X e1 && is_closed X e2
end.
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Instance closed_decision env e : Decision (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Inductive val :=
| RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
| LitV (l : base_lit)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Bind Scope val_scope with val.
Delimit Scope val_scope with V.
Arguments PairV _%V _%V.
Arguments InjLV _%V.
Arguments InjRV _%V.
Fixpoint of_val (v : val) : expr :=
match v with
| RecV f x e _ ⇒ Rec f x e
| LitV l ⇒ Lit l
| PairV v1 v2 ⇒ Pair (of_val v1) (of_val v2)
| InjLV v ⇒ InjL (of_val v)
| InjRV v ⇒ InjR (of_val v)
end.
Fixpoint to_val (e : expr) : option val :=
match e with
| Rec f x e ⇒
if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
| Lit l ⇒ Some (LitV l)
| Pair e1 e2 ⇒ v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
| InjL e ⇒ InjLV <$> to_val e
| InjR e ⇒ InjRV <$> to_val e
| _ ⇒ None
end.
The state: chans of vals.
Global Instance side_eq_dec: ∀ x y : side, Decision (x = y).
Proof. solve_decision. Qed.
Global Instance side_countable: Countable side.
Proof.
pose (encode := (λ s, match s with cleft ⇒ 1 | _ ⇒ 2 end)%positive).
pose (decode := (λ s, match s with 1 ⇒ Some cleft | _ ⇒ Some cright end)%positive).
eapply (Build_Countable _ _ encode decode).
by intros [|].
Qed.
Definition state := gmap loc (list val × list val).
Proof. solve_decision. Qed.
Global Instance side_countable: Countable side.
Proof.
pose (encode := (λ s, match s with cleft ⇒ 1 | _ ⇒ 2 end)%positive).
pose (decode := (λ s, match s with 1 ⇒ Some cleft | _ ⇒ Some cright end)%positive).
eapply (Build_Countable _ _ encode decode).
by intros [|].
Qed.
Definition state := gmap loc (list val × list val).
Evaluation contexts
Inductive ectx_item :=
| AppLCtx (e2 : expr)
| AppRCtx (v1 : val)
| UnOpCtx (op : un_op)
| BinOpLCtx (op : bin_op) (e2 : expr)
| BinOpRCtx (op : bin_op) (v1 : val)
| IfCtx (e1 e2 : expr)
| PairLCtx (e2 : expr)
| PairRCtx (v1 : val)
| LetpCtx (x y : binder) (eb : expr)
| InjLCtx
| InjRCtx
| CaseCtx (e1 : expr) (e2 : expr)
| RecvCtx
| SendLCtx (e2 : expr)
| SendRCtx (v1 : val)
| SelectCtx (s: label)
| RCaseCtx (e1 : expr) (e2 : expr).
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx e2 ⇒ App e e2
| AppRCtx v1 ⇒ App (of_val v1) e
| UnOpCtx op ⇒ UnOp op e
| BinOpLCtx op e2 ⇒ BinOp op e e2
| BinOpRCtx op v1 ⇒ BinOp op (of_val v1) e
| IfCtx e1 e2 ⇒ If e e1 e2
| PairLCtx e2 ⇒ Pair e e2
| PairRCtx v1 ⇒ Pair (of_val v1) e
| InjLCtx ⇒ InjL e
| InjRCtx ⇒ InjR e
| LetpCtx x y eb ⇒ Letp x y e eb
| CaseCtx e1 e2 ⇒ Case e e1 e2
| RecvCtx ⇒ Recv e
| SendLCtx e2 ⇒ Send e e2
| SendRCtx v1 ⇒ Send (of_val v1) e
| SelectCtx s ⇒ Select e s
| RCaseCtx e1 e2 ⇒ RCase e e1 e2
end.
| AppLCtx (e2 : expr)
| AppRCtx (v1 : val)
| UnOpCtx (op : un_op)
| BinOpLCtx (op : bin_op) (e2 : expr)
| BinOpRCtx (op : bin_op) (v1 : val)
| IfCtx (e1 e2 : expr)
| PairLCtx (e2 : expr)
| PairRCtx (v1 : val)
| LetpCtx (x y : binder) (eb : expr)
| InjLCtx
| InjRCtx
| CaseCtx (e1 : expr) (e2 : expr)
| RecvCtx
| SendLCtx (e2 : expr)
| SendRCtx (v1 : val)
| SelectCtx (s: label)
| RCaseCtx (e1 : expr) (e2 : expr).
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx e2 ⇒ App e e2
| AppRCtx v1 ⇒ App (of_val v1) e
| UnOpCtx op ⇒ UnOp op e
| BinOpLCtx op e2 ⇒ BinOp op e e2
| BinOpRCtx op v1 ⇒ BinOp op (of_val v1) e
| IfCtx e1 e2 ⇒ If e e1 e2
| PairLCtx e2 ⇒ Pair e e2
| PairRCtx v1 ⇒ Pair (of_val v1) e
| InjLCtx ⇒ InjL e
| InjRCtx ⇒ InjR e
| LetpCtx x y eb ⇒ Letp x y e eb
| CaseCtx e1 e2 ⇒ Case e e1 e2
| RecvCtx ⇒ Recv e
| SendLCtx e2 ⇒ Send e e2
| SendRCtx v1 ⇒ Send (of_val v1) e
| SelectCtx s ⇒ Select e s
| RCaseCtx e1 e2 ⇒ RCase e e1 e2
end.
Substitution
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
| Var y ⇒ if decide (x = y) then es else Var y
| Rec f y e ⇒
Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
| App e1 e2 ⇒ App (subst x es e1) (subst x es e2)
| Lit l ⇒ Lit l
| UnOp op e ⇒ UnOp op (subst x es e)
| BinOp op e1 e2 ⇒ BinOp op (subst x es e1) (subst x es e2)
| If e0 e1 e2 ⇒ If (subst x es e0) (subst x es e1) (subst x es e2)
| Pair e1 e2 ⇒ Pair (subst x es e1) (subst x es e2)
| Letp y z e1 e2 ⇒
Letp y z (subst x es e1) $ if decide (BNamed x ≠ y ∧ BNamed x ≠ z) then subst x es e2 else e2
| InjL e ⇒ InjL (subst x es e)
| InjR e ⇒ InjR (subst x es e)
| Case e0 e1 e2 ⇒ Case (subst x es e0) (subst x es e1) (subst x es e2)
| Fork e ⇒ Fork (subst x es e)
| Alloc ⇒ Alloc
| Recv e ⇒ Recv (subst x es e)
| Send e1 e2 ⇒ Send (subst x es e1) (subst x es e2)
| RCase e0 e1 e2 ⇒ RCase (subst x es e0) (subst x es e1) (subst x es e2)
| Select e s ⇒ Select (subst x es e) s
end.
Definition subst' (mx : binder) (es : expr) : expr → expr :=
match mx with BNamed x ⇒ subst x es | BAnon ⇒ id end.
match e with
| Var y ⇒ if decide (x = y) then es else Var y
| Rec f y e ⇒
Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
| App e1 e2 ⇒ App (subst x es e1) (subst x es e2)
| Lit l ⇒ Lit l
| UnOp op e ⇒ UnOp op (subst x es e)
| BinOp op e1 e2 ⇒ BinOp op (subst x es e1) (subst x es e2)
| If e0 e1 e2 ⇒ If (subst x es e0) (subst x es e1) (subst x es e2)
| Pair e1 e2 ⇒ Pair (subst x es e1) (subst x es e2)
| Letp y z e1 e2 ⇒
Letp y z (subst x es e1) $ if decide (BNamed x ≠ y ∧ BNamed x ≠ z) then subst x es e2 else e2
| InjL e ⇒ InjL (subst x es e)
| InjR e ⇒ InjR (subst x es e)
| Case e0 e1 e2 ⇒ Case (subst x es e0) (subst x es e1) (subst x es e2)
| Fork e ⇒ Fork (subst x es e)
| Alloc ⇒ Alloc
| Recv e ⇒ Recv (subst x es e)
| Send e1 e2 ⇒ Send (subst x es e1) (subst x es e2)
| RCase e0 e1 e2 ⇒ RCase (subst x es e0) (subst x es e1) (subst x es e2)
| Select e s ⇒ Select (subst x es e) s
end.
Definition subst' (mx : binder) (es : expr) : expr → expr :=
match mx with BNamed x ⇒ subst x es | BAnon ⇒ id end.
The stepping relation
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
match op, l with
| NegOp, LitBool b ⇒ Some (LitBool (negb b))
| MinusUnOp, LitInt n ⇒ Some (LitInt (- n))
| _, _ ⇒ None
end.
Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
match op, l1, l2 with
| PlusOp, LitInt n1, LitInt n2 ⇒ Some $ LitInt (n1 + n2)
| MinusOp, LitInt n1, LitInt n2 ⇒ Some $ LitInt (n1 - n2)
| LeOp, LitInt n1, LitInt n2 ⇒ Some $ LitBool $ bool_decide (n1 ≤ n2)
| LtOp, LitInt n1, LitInt n2 ⇒ Some $ LitBool $ bool_decide (n1 < n2)
| EqOp, LitInt n1, LitInt n2 ⇒ Some $ LitBool $ bool_decide (n1 = n2)
| _, _, _ ⇒ None
end.
Definition label_to_sum (l: label) :=
match l with
| lleft ⇒ InjLV (LitV LitUnit)
| lright ⇒ InjRV (LitV LitUnit)
end.
Inductive head_step : expr → state → expr → state → option (expr) → Prop :=
| BetaS f x e1 e2 v2 e' σ :
to_val e2 = Some v2 →
Closed (f :b: x :b: []) e1 →
e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) →
head_step (App (Rec f x e1) e2) σ e' σ None
| UnOpS op l l' σ :
un_op_eval op l = Some l' →
head_step (UnOp op (Lit l)) σ (Lit l') σ None
| BinOpS op l1 l2 l' σ :
bin_op_eval op l1 l2 = Some l' →
head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
| IfTrueS e1 e2 σ :
head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
| IfFalseS e1 e2 σ :
head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
| LetpS x y e1 v1 e2 v2 eb eb' σ:
to_val e1 = Some v1 → to_val e2 = Some v2 →
Closed (x :b: y :b: []) eb →
eb' = subst' y (of_val v2) (subst' x (of_val v1) eb) →
head_step (Letp x y (Pair e1 e2) eb) σ eb' σ None
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
| ForkS e σ:
head_step (Fork e) σ (Lit LitUnit) σ (Some e)
| AllocS σ l :
l = fresh (dom _ σ) →
head_step (Alloc) σ (Pair (Lit $ LitLoc l cleft) (Lit $ LitLoc l cright)) (<[l:=([], [])]>σ) None
| RecvLHitS l v l1 l2 σ :
σ !! l = Some (l1, v :: l2) →
head_step (Recv (Lit $ LitLoc l cleft)) σ
(Pair (Lit $ LitLoc l cleft) (of_val v)) (<[l:=(l1, l2)]>σ) None
| RecvRHitS l v l1 l2 σ :
σ !! l = Some (v :: l1, l2) →
head_step (Recv (Lit $ LitLoc l cright)) σ
(Pair (Lit $ LitLoc l cright) (of_val v)) (<[l:=(l1, l2)]>σ) None
| RecvLMissS l l1 σ :
σ !! l = Some (l1, []) →
head_step (Recv (Lit $ LitLoc l cleft)) σ (Recv (Lit $ LitLoc l cleft)) σ None
| RecvRMissS l l2 σ :
σ !! l = Some ([], l2) →
head_step (Recv (Lit $ LitLoc l cright)) σ (Recv (Lit $ LitLoc l cright)) σ None
| SendL l e v l1 l2 σ :
to_val e = Some v → σ !! l = Some (l1, l2) →
head_step (Send (Lit $ LitLoc l cleft) e) σ (Lit $ LitLoc l cleft) (<[l:=(l1 ++ [v], l2)]>σ) None
| SendR l e v l1 l2 σ :
to_val e = Some v → σ !! l = Some (l1, l2) →
head_step (Send (Lit $ LitLoc l cright) e) σ (Lit $ LitLoc l cright) (<[l:=(l1, l2 ++ [v])]>σ) None
| RCaseLLS l e1 e2 l1 l2 σ :
σ !! l = Some (l1, InjLV (LitV LitUnit) :: l2) →
head_step (RCase (Lit $ LitLoc l cleft) e1 e2) σ
(App e1 (Lit $ LitLoc l cleft)) (<[l:=(l1, l2)]>σ) None
| RCaseLRS l e1 e2 l1 l2 σ :
σ !! l = Some (l1, InjRV (LitV LitUnit) :: l2) →
head_step (RCase (Lit $ LitLoc l cleft) e1 e2) σ
(App e2 (Lit $ LitLoc l cleft)) (<[l:=(l1, l2)]>σ) None
| RCaseLMissS l e1 e2 l1 σ :
σ !! l = Some (l1, []) →
head_step (RCase (Lit $ LitLoc l cleft) e1 e2) σ
(RCase (Lit $ LitLoc l cleft) e1 e2) σ None
| RCaseRLS l e1 e2 l1 l2 σ :
σ !! l = Some (InjLV (LitV LitUnit) :: l1, l2) →
head_step (RCase (Lit $ LitLoc l cright) e1 e2) σ
(App e1 (Lit $ LitLoc l cright)) (<[l:=(l1, l2)]>σ) None
| RCaseRRS l e1 e2 l1 l2 σ :
σ !! l = Some (InjRV (LitV LitUnit) :: l1, l2) →
head_step (RCase (Lit $ LitLoc l cright) e1 e2) σ
(App e2 (Lit $ LitLoc l cright)) (<[l:=(l1, l2)]>σ) None
| RCaseRMissS l e1 e2 l2 σ :
σ !! l = Some ([], l2) →
head_step (RCase (Lit $ LitLoc l cright) e1 e2) σ
(RCase (Lit $ LitLoc l cright) e1 e2) σ None
| SelectL l s l1 l2 σ:
σ !! l = Some (l1, l2) →
head_step (Select (Lit $ LitLoc l cleft) s) σ
(Lit $ LitLoc l cleft) (<[l:=(l1 ++ [label_to_sum s], l2)]>σ) None
| SelectR l s l1 l2 σ:
σ !! l = Some (l1, l2) →
head_step (Select (Lit $ LitLoc l cright) s) σ
(Lit $ LitLoc l cright) (<[l:=(l1, l2 ++ [label_to_sum s])]>σ) None.
match op, l with
| NegOp, LitBool b ⇒ Some (LitBool (negb b))
| MinusUnOp, LitInt n ⇒ Some (LitInt (- n))
| _, _ ⇒ None
end.
Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
match op, l1, l2 with
| PlusOp, LitInt n1, LitInt n2 ⇒ Some $ LitInt (n1 + n2)
| MinusOp, LitInt n1, LitInt n2 ⇒ Some $ LitInt (n1 - n2)
| LeOp, LitInt n1, LitInt n2 ⇒ Some $ LitBool $ bool_decide (n1 ≤ n2)
| LtOp, LitInt n1, LitInt n2 ⇒ Some $ LitBool $ bool_decide (n1 < n2)
| EqOp, LitInt n1, LitInt n2 ⇒ Some $ LitBool $ bool_decide (n1 = n2)
| _, _, _ ⇒ None
end.
Definition label_to_sum (l: label) :=
match l with
| lleft ⇒ InjLV (LitV LitUnit)
| lright ⇒ InjRV (LitV LitUnit)
end.
Inductive head_step : expr → state → expr → state → option (expr) → Prop :=
| BetaS f x e1 e2 v2 e' σ :
to_val e2 = Some v2 →
Closed (f :b: x :b: []) e1 →
e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) →
head_step (App (Rec f x e1) e2) σ e' σ None
| UnOpS op l l' σ :
un_op_eval op l = Some l' →
head_step (UnOp op (Lit l)) σ (Lit l') σ None
| BinOpS op l1 l2 l' σ :
bin_op_eval op l1 l2 = Some l' →
head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
| IfTrueS e1 e2 σ :
head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
| IfFalseS e1 e2 σ :
head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
| LetpS x y e1 v1 e2 v2 eb eb' σ:
to_val e1 = Some v1 → to_val e2 = Some v2 →
Closed (x :b: y :b: []) eb →
eb' = subst' y (of_val v2) (subst' x (of_val v1) eb) →
head_step (Letp x y (Pair e1 e2) eb) σ eb' σ None
| CaseLS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
| CaseRS e0 v0 e1 e2 σ :
to_val e0 = Some v0 →
head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
| ForkS e σ:
head_step (Fork e) σ (Lit LitUnit) σ (Some e)
| AllocS σ l :
l = fresh (dom _ σ) →
head_step (Alloc) σ (Pair (Lit $ LitLoc l cleft) (Lit $ LitLoc l cright)) (<[l:=([], [])]>σ) None
| RecvLHitS l v l1 l2 σ :
σ !! l = Some (l1, v :: l2) →
head_step (Recv (Lit $ LitLoc l cleft)) σ
(Pair (Lit $ LitLoc l cleft) (of_val v)) (<[l:=(l1, l2)]>σ) None
| RecvRHitS l v l1 l2 σ :
σ !! l = Some (v :: l1, l2) →
head_step (Recv (Lit $ LitLoc l cright)) σ
(Pair (Lit $ LitLoc l cright) (of_val v)) (<[l:=(l1, l2)]>σ) None
| RecvLMissS l l1 σ :
σ !! l = Some (l1, []) →
head_step (Recv (Lit $ LitLoc l cleft)) σ (Recv (Lit $ LitLoc l cleft)) σ None
| RecvRMissS l l2 σ :
σ !! l = Some ([], l2) →
head_step (Recv (Lit $ LitLoc l cright)) σ (Recv (Lit $ LitLoc l cright)) σ None
| SendL l e v l1 l2 σ :
to_val e = Some v → σ !! l = Some (l1, l2) →
head_step (Send (Lit $ LitLoc l cleft) e) σ (Lit $ LitLoc l cleft) (<[l:=(l1 ++ [v], l2)]>σ) None
| SendR l e v l1 l2 σ :
to_val e = Some v → σ !! l = Some (l1, l2) →
head_step (Send (Lit $ LitLoc l cright) e) σ (Lit $ LitLoc l cright) (<[l:=(l1, l2 ++ [v])]>σ) None
| RCaseLLS l e1 e2 l1 l2 σ :
σ !! l = Some (l1, InjLV (LitV LitUnit) :: l2) →
head_step (RCase (Lit $ LitLoc l cleft) e1 e2) σ
(App e1 (Lit $ LitLoc l cleft)) (<[l:=(l1, l2)]>σ) None
| RCaseLRS l e1 e2 l1 l2 σ :
σ !! l = Some (l1, InjRV (LitV LitUnit) :: l2) →
head_step (RCase (Lit $ LitLoc l cleft) e1 e2) σ
(App e2 (Lit $ LitLoc l cleft)) (<[l:=(l1, l2)]>σ) None
| RCaseLMissS l e1 e2 l1 σ :
σ !! l = Some (l1, []) →
head_step (RCase (Lit $ LitLoc l cleft) e1 e2) σ
(RCase (Lit $ LitLoc l cleft) e1 e2) σ None
| RCaseRLS l e1 e2 l1 l2 σ :
σ !! l = Some (InjLV (LitV LitUnit) :: l1, l2) →
head_step (RCase (Lit $ LitLoc l cright) e1 e2) σ
(App e1 (Lit $ LitLoc l cright)) (<[l:=(l1, l2)]>σ) None
| RCaseRRS l e1 e2 l1 l2 σ :
σ !! l = Some (InjRV (LitV LitUnit) :: l1, l2) →
head_step (RCase (Lit $ LitLoc l cright) e1 e2) σ
(App e2 (Lit $ LitLoc l cright)) (<[l:=(l1, l2)]>σ) None
| RCaseRMissS l e1 e2 l2 σ :
σ !! l = Some ([], l2) →
head_step (RCase (Lit $ LitLoc l cright) e1 e2) σ
(RCase (Lit $ LitLoc l cright) e1 e2) σ None
| SelectL l s l1 l2 σ:
σ !! l = Some (l1, l2) →
head_step (Select (Lit $ LitLoc l cleft) s) σ
(Lit $ LitLoc l cleft) (<[l:=(l1 ++ [label_to_sum s], l2)]>σ) None
| SelectR l s l1 l2 σ:
σ !! l = Some (l1, l2) →
head_step (Select (Lit $ LitLoc l cright) s) σ
(Lit $ LitLoc l cright) (<[l:=(l1, l2 ++ [label_to_sum s])]>σ) None.
Basic properties about the language
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof.
by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.
Lemma of_to_val e v : to_val e = Some v → of_val v = e.
Proof.
revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.
Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Lemma fill_item_val_2 Ki e1 e2 :
is_Some (to_val e1) → is_Some (to_val e2) →
is_Some (to_val (fill_item Ki e1)) →
is_Some (to_val (fill_item Ki e2)).
Proof.
revert e1 e2. induction Ki; simplify_option_eq; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq.
match goal with
[ |- context[(to_val ?e)]] ⇒ destruct (to_val e)
end; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq.
match goal with
[ |- context[(to_val ?e)]] ⇒ destruct (to_val e)
end; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq; eauto.
Qed.
Lemma val_stuck e1 σ1 e2 σ2 ef :
head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None → to_val e2 = None →
fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
Proof.
destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
repeat match goal with
| H : to_val (of_val _) = None |- _ ⇒ by rewrite to_of_val in H
end; auto.
Qed.
Lemma alloc_fresh σ :
let l := fresh (dom _ σ) in
head_step (Alloc) σ
(Pair (Lit $ (LitLoc l) cleft) (Lit $ (LitLoc l) cright)) (<[l:=([], [])]>σ) None.
Proof. by intros; apply AllocS. Qed.
Proof.
by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.
Lemma of_to_val e v : to_val e = Some v → of_val v = e.
Proof.
revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.
Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
Lemma fill_item_val_2 Ki e1 e2 :
is_Some (to_val e1) → is_Some (to_val e2) →
is_Some (to_val (fill_item Ki e1)) →
is_Some (to_val (fill_item Ki e2)).
Proof.
revert e1 e2. induction Ki; simplify_option_eq; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq.
match goal with
[ |- context[(to_val ?e)]] ⇒ destruct (to_val e)
end; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq.
match goal with
[ |- context[(to_val ?e)]] ⇒ destruct (to_val e)
end; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq; eauto.
Qed.
Lemma val_stuck e1 σ1 e2 σ2 ef :
head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None → to_val e2 = None →
fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
Proof.
destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
repeat match goal with
| H : to_val (of_val _) = None |- _ ⇒ by rewrite to_of_val in H
end; auto.
Qed.
Lemma alloc_fresh σ :
let l := fresh (dom _ σ) in
head_step (Alloc) σ
(Pair (Lit $ (LitLoc l) cleft) (Lit $ (LitLoc l) cright)) (<[l:=([], [])]>σ) None.
Proof. by intros; apply AllocS. Qed.
Closed expressions
Lemma is_closed_weaken X Y e : is_closed X e → X `included` Y → is_closed Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.
Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
Proof.
revert X. induction e⇒ X /=; rewrite ?bool_decide_spec ?andb_True⇒ ??;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
Lemma is_closed_nil_subst e x es : is_closed [] e → subst x es e = e.
Proof. intros. apply is_closed_subst with []; set_solver. Qed.
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
Lemma is_closed_perm X X' e: is_closed X e → Permutation X X' → is_closed X' e.
Proof.
revert X X'. induction e⇒X X' /=; rewrite ?bool_decide_spec ?andb_true⇒Hclosed Hperm;
try set_solver.
- rewrite -Hperm; eauto.
- eapply IHe; eauto; rewrite /cons_binder; destruct f, x; eauto.
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
eapply IHe2; eauto; rewrite /cons_binder; destruct x, y; eauto.
Qed.
Lemma is_closed_subst_remove X e x es:
is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).
Proof.
revert X. induction e⇒X /=; rewrite ?bool_decide_spec ?andb_true⇒ ? Hclosed;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver; try set_solver.
- eapply is_closed_weaken; eauto. set_solver.
- eapply IHe; auto. eapply is_closed_perm; eauto.
rewrite /cons_binder; destruct f, x0; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
- destruct f, x0; simpl in ×.
× exfalso; try naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** intros ?; exfalso; naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** intros ?; exfalso; naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** case (decide (x = s0)).
*** intros → ?. eapply is_closed_weaken; set_solver.
*** intros ??; exfalso; naive_solver.
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
rewrite /cons_binder; destruct x0, y;
eapply is_closed_perm in H2; eauto using perm_swap.
by do 2 rewrite //= (perm_swap x).
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
destruct x0, y; simpl in ×.
× exfalso; try naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** intros ?; exfalso; naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** intros ?; exfalso; naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** case (decide (x = s0)).
*** intros → ?. eapply is_closed_weaken; set_solver.
*** intros ??; exfalso; naive_solver.
Qed.
Lemma is_closed_subst_inv_1 X e x es:
is_closed [] es → is_closed X (subst x es e) → is_closed (x :: X) e.
Proof.
revert X. induction e⇒X /=; rewrite ?bool_decide_spec ?andb_true⇒ ? Hclosed;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver; try set_solver.
- eapply (is_closed_perm (x :: f :b: x0 :b: X)); first eapply IHe; eauto.
rewrite /cons_binder; destruct f, x0; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
- destruct f, x0; simpl in *; eapply is_closed_weaken; eauto; set_solver.
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
eapply (is_closed_perm (x :: x0 :b: y :b: X)); first eapply IHe2; eauto;
rewrite /cons_binder; destruct x0, y; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
destruct x0, y; simpl in *; eapply is_closed_weaken; eauto; set_solver.
Qed.
Lemma is_closed_subst_inv_2 X e x es:
is_closed [] es → is_closed (x :: X) (subst x es e) → is_closed (x :: X) e.
Proof.
revert X. induction e⇒X /=; rewrite ?bool_decide_spec ?andb_true⇒ ? Hclosed;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver; try set_solver.
- move: Hclosed. rewrite ?bool_decide_spec. auto.
- eapply (is_closed_perm (x :: f :b: x0 :b: X)); first eapply IHe; eauto using is_closed_perm.
× eapply is_closed_perm; eauto.
rewrite /cons_binder; destruct f, x0; simpl in *; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
× rewrite /cons_binder; destruct f, x0; simpl in *; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
eapply (is_closed_perm (x :: x0 :b: y :b: X)); first eapply IHe2; eauto using is_closed_perm.
× eapply is_closed_perm; eauto.
rewrite /cons_binder; destruct x0, y; simpl in *; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
× rewrite /cons_binder; destruct x0, y; simpl in *; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
Qed.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.
Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
Proof.
revert X. induction e⇒ X /=; rewrite ?bool_decide_spec ?andb_True⇒ ??;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
Lemma is_closed_nil_subst e x es : is_closed [] e → subst x es e = e.
Proof. intros. apply is_closed_subst with []; set_solver. Qed.
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
Lemma is_closed_perm X X' e: is_closed X e → Permutation X X' → is_closed X' e.
Proof.
revert X X'. induction e⇒X X' /=; rewrite ?bool_decide_spec ?andb_true⇒Hclosed Hperm;
try set_solver.
- rewrite -Hperm; eauto.
- eapply IHe; eauto; rewrite /cons_binder; destruct f, x; eauto.
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
eapply IHe2; eauto; rewrite /cons_binder; destruct x, y; eauto.
Qed.
Lemma is_closed_subst_remove X e x es:
is_closed [] es → is_closed (x :: X) e → is_closed X (subst x es e).
Proof.
revert X. induction e⇒X /=; rewrite ?bool_decide_spec ?andb_true⇒ ? Hclosed;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver; try set_solver.
- eapply is_closed_weaken; eauto. set_solver.
- eapply IHe; auto. eapply is_closed_perm; eauto.
rewrite /cons_binder; destruct f, x0; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
- destruct f, x0; simpl in ×.
× exfalso; try naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** intros ?; exfalso; naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** intros ?; exfalso; naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** case (decide (x = s0)).
*** intros → ?. eapply is_closed_weaken; set_solver.
*** intros ??; exfalso; naive_solver.
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
rewrite /cons_binder; destruct x0, y;
eapply is_closed_perm in H2; eauto using perm_swap.
by do 2 rewrite //= (perm_swap x).
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
destruct x0, y; simpl in ×.
× exfalso; try naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** intros ?; exfalso; naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** intros ?; exfalso; naive_solver.
× case (decide (x = s)).
** intros →. eapply is_closed_weaken; set_solver.
** case (decide (x = s0)).
*** intros → ?. eapply is_closed_weaken; set_solver.
*** intros ??; exfalso; naive_solver.
Qed.
Lemma is_closed_subst_inv_1 X e x es:
is_closed [] es → is_closed X (subst x es e) → is_closed (x :: X) e.
Proof.
revert X. induction e⇒X /=; rewrite ?bool_decide_spec ?andb_true⇒ ? Hclosed;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver; try set_solver.
- eapply (is_closed_perm (x :: f :b: x0 :b: X)); first eapply IHe; eauto.
rewrite /cons_binder; destruct f, x0; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
- destruct f, x0; simpl in *; eapply is_closed_weaken; eauto; set_solver.
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
eapply (is_closed_perm (x :: x0 :b: y :b: X)); first eapply IHe2; eauto;
rewrite /cons_binder; destruct x0, y; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
destruct x0, y; simpl in *; eapply is_closed_weaken; eauto; set_solver.
Qed.
Lemma is_closed_subst_inv_2 X e x es:
is_closed [] es → is_closed (x :: X) (subst x es e) → is_closed (x :: X) e.
Proof.
revert X. induction e⇒X /=; rewrite ?bool_decide_spec ?andb_true⇒ ? Hclosed;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver; try set_solver.
- move: Hclosed. rewrite ?bool_decide_spec. auto.
- eapply (is_closed_perm (x :: f :b: x0 :b: X)); first eapply IHe; eauto using is_closed_perm.
× eapply is_closed_perm; eauto.
rewrite /cons_binder; destruct f, x0; simpl in *; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
× rewrite /cons_binder; destruct f, x0; simpl in *; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
- apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
eapply (is_closed_perm (x :: x0 :b: y :b: X)); first eapply IHe2; eauto using is_closed_perm.
× eapply is_closed_perm; eauto.
rewrite /cons_binder; destruct x0, y; simpl in *; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
× rewrite /cons_binder; destruct x0, y; simpl in *; eauto using perm_swap.
by do 2 rewrite (perm_swap x).
Qed.
Equality and other typeclass stuff
Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
Proof. solve_decision. Defined.
Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Instance label_op_dec_eq (l1 l2: label) : Decision (l1 = l2).
Proof. solve_decision. Defined.
Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Proof. solve_decision. Defined.
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
Proof.
refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Ltac existT_eq_elim :=
(match goal with
[ H: existT ?x ?e1 = existT ?x ?e2 |- _ ] ⇒
apply Eqdep_dec.inj_pair2_eq_dec in H; eauto
end).
Lemma head_step_det e σ e1' σ1' ef1' e2' σ2' ef2':
head_step e σ e1' σ1' ef1' →
head_step e σ e2' σ2' ef2' →
e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2'.
Proof.
induction 1; subst;
inversion 1; subst;
split_and!; try congruence; auto.
Qed.
Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.
End chan_lang.
Proof. solve_decision. Defined.
Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Instance label_op_dec_eq (l1 l2: label) : Decision (l1 = l2).
Proof. solve_decision. Defined.
Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Proof. solve_decision. Defined.
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
Proof.
refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
Ltac existT_eq_elim :=
(match goal with
[ H: existT ?x ?e1 = existT ?x ?e2 |- _ ] ⇒
apply Eqdep_dec.inj_pair2_eq_dec in H; eauto
end).
Lemma head_step_det e σ e1' σ1' ef1' e2' σ2' ef2':
head_step e σ e1' σ1' ef1' →
head_step e σ e2' σ2' ef2' →
e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2'.
Proof.
induction 1; subst;
inversion 1; subst;
split_and!; try congruence; auto.
Qed.
Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.
End chan_lang.
Language
Program Instance chan_ectxi_lang :
EctxiLanguage
(chan_lang.expr) chan_lang.val chan_lang.ectx_item chan_lang.state := {|
of_val := chan_lang.of_val; to_val := chan_lang.to_val;
fill_item := chan_lang.fill_item; head_step := chan_lang.head_step;
|}.
Solve Obligations with eauto using chan_lang.to_of_val, chan_lang.of_to_val,
chan_lang.val_stuck, chan_lang.fill_item_val,
chan_lang.fill_item_no_val_inj, chan_lang.head_ctx_step_val.
Canonical Structure chan_lang := ectx_lang (chan_lang.expr).
Lemma chan_prim_dec: ∀ (e: chan_lang.expr) σ,
{ t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}.
Proof.
induction e.
Abort.
Export chan_lang.
EctxiLanguage
(chan_lang.expr) chan_lang.val chan_lang.ectx_item chan_lang.state := {|
of_val := chan_lang.of_val; to_val := chan_lang.to_val;
fill_item := chan_lang.fill_item; head_step := chan_lang.head_step;
|}.
Solve Obligations with eauto using chan_lang.to_of_val, chan_lang.of_to_val,
chan_lang.val_stuck, chan_lang.fill_item_val,
chan_lang.fill_item_no_val_inj, chan_lang.head_ctx_step_val.
Canonical Structure chan_lang := ectx_lang (chan_lang.expr).
Lemma chan_prim_dec: ∀ (e: chan_lang.expr) σ,
{ t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}.
Proof.
induction e.
Abort.
Export chan_lang.