heap_lang.v 15.3 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Import Autosubst.Autosubst.
2
Require Import prelude.option prelude.gmap iris.language.
Ralf Jung's avatar
Ralf Jung committed
3

4 5
Set Bullet Behavior "Strict Subproofs".

6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
(** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1.
    They all assume such an equality is the first thing on the "stack" (goal). *)
Ltac case_depeq1 := let Heq := fresh "Heq" in
  case=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,<-).
Ltac case_depeq2 := let Heq := fresh "Heq" in
  case=>_ _ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,Heq);
  case:Heq=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,<-).
Ltac case_depeq3 := let Heq := fresh "Heq" in
  case=>_ _ _ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,Heq);
  case:Heq=>_ _ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,Heq);
  case:Heq=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,<-).

(** Expressions and values. *)
Ralf Jung's avatar
Ralf Jung committed
25 26
Definition loc := nat. (* Any countable type. *)

Ralf Jung's avatar
Ralf Jung committed
27
Inductive expr :=
28
(* Base lambda calculus *)
Ralf Jung's avatar
Ralf Jung committed
29
| Var (x : var)
Ralf Jung's avatar
Ralf Jung committed
30
| Rec (e : {bind 2 of expr}) (* These are recursive lambdas. *)
31
| App (e1 e2 : expr)
32
(* Embedding of Coq values and operations *)
33 34 35
| Lit {T : Type} (t: T)  (* arbitrary Coq values become literals *)
| Op1  {T1 To : Type} (f : T1 -> To) (e1 : expr)
| Op2  {T1 T2 To : Type} (f : T1 -> T2 -> To) (e1 : expr) (e2 : expr)
36
(* Products *)
Ralf Jung's avatar
Ralf Jung committed
37 38 39
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
40
(* Sums *)
Ralf Jung's avatar
Ralf Jung committed
41 42
| InjL (e : expr)
| InjR (e : expr)
Ralf Jung's avatar
Ralf Jung committed
43
| Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
44 45 46 47
(* Concurrency *)
| Fork (e : expr)
(* Heap *)
| Loc (l : loc)
Ralf Jung's avatar
Ralf Jung committed
48
| Alloc (e : expr)
Ralf Jung's avatar
Ralf Jung committed
49 50 51 52
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| Cas (e0 : expr) (e1 : expr) (e2 : expr)
.
Ralf Jung's avatar
Ralf Jung committed
53 54 55 56 57 58

Instance Ids_expr : Ids expr. derive. Defined.
Instance Rename_expr : Rename expr. derive. Defined.
Instance Subst_expr : Subst expr. derive. Defined.
Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.

Ralf Jung's avatar
Ralf Jung committed
59
Definition Lam (e: {bind expr}) := Rec (e.[up ids]).
Ralf Jung's avatar
Ralf Jung committed
60
Definition LitUnit := Lit tt.
Ralf Jung's avatar
Ralf Jung committed
61 62
Definition LitTrue := Lit true.
Definition LitFalse := Lit false.
Ralf Jung's avatar
Ralf Jung committed
63

Ralf Jung's avatar
Ralf Jung committed
64
Inductive value :=
Ralf Jung's avatar
Ralf Jung committed
65
| RecV (e : {bind 2 of expr})
Ralf Jung's avatar
Ralf Jung committed
66
| LitV (T : Type) (t : T)  (* arbitrary Coq values become literal values *)
Ralf Jung's avatar
Ralf Jung committed
67 68
| PairV (v1 v2 : value)
| InjLV (v : value)
69
| InjRV (v : value)
Ralf Jung's avatar
Ralf Jung committed
70 71
| LocV (l : loc)
.
Ralf Jung's avatar
Ralf Jung committed
72

73
Fixpoint v2e (v : value) : expr :=
Ralf Jung's avatar
Ralf Jung committed
74
  match v with
75
  | LitV _ t => Lit t
Ralf Jung's avatar
Ralf Jung committed
76
  | RecV e   => Rec e
Ralf Jung's avatar
Ralf Jung committed
77 78 79
  | PairV v1 v2 => Pair (v2e v1) (v2e v2)
  | InjLV v => InjL (v2e v)
  | InjRV v => InjR (v2e v)
80
  | LocV l => Loc l
Ralf Jung's avatar
Ralf Jung committed
81 82
  end.

83 84
Fixpoint e2v (e : expr) : option value :=
  match e with
Ralf Jung's avatar
Ralf Jung committed
85
  | Rec e => Some (RecV e)
86
  | Lit T t => Some (LitV T t)
87 88 89 90 91
  | Pair e1 e2 => v1  e2v e1;
                  v2  e2v e2;
                  Some (PairV v1 v2)
  | InjL e => InjLV <$> e2v e
  | InjR e => InjRV <$> e2v e
92
  | Loc l => Some (LocV l)
Ralf Jung's avatar
Ralf Jung committed
93
  | _ => None
94 95 96 97 98
  end.

Lemma v2v v:
  e2v (v2e v) = Some v.
Proof.
99
  induction v; simpl; rewrite ?IHv ?IHv1 /= ?IHv2; reflexivity.
100 101
Qed.

Ralf Jung's avatar
Ralf Jung committed
102
Section e2e. (* To get local tactics. *)
103
Lemma e2e e v:
104
  e2v e = Some v -> v2e v = e.
105
Proof.
Ralf Jung's avatar
Ralf Jung committed
106 107 108 109 110 111 112 113 114 115 116 117 118 119
  Ltac case0 := case =><-; simpl; eauto using f_equal, f_equal2.
  Ltac case1 e1 := destruct (e2v e1); simpl; [|discriminate];
                   case0.
  Ltac case2 e1 e2 := destruct (e2v e1); simpl; [|discriminate];
                      destruct (e2v e2); simpl; [|discriminate];
                      case0.

  revert v; induction e; intros v; simpl; try discriminate; by (case2 e1 e2 || case1 e || case0).
Qed.
End e2e.

Lemma v2e_inj v1 v2:
  v2e v1 = v2e v2 -> v1 = v2.
Proof.
120
  revert v2; induction v1=>v2; destruct v2; simpl; try discriminate;
Ralf Jung's avatar
Ralf Jung committed
121
    first [case_depeq1 | case]; eauto using f_equal, f_equal2.
122
Qed.
123

124 125
(** The state: heaps of values. *)
Definition state := gmap loc value.
Ralf Jung's avatar
Ralf Jung committed
126

127
(** Evaluation contexts *)
Ralf Jung's avatar
Ralf Jung committed
128 129
Inductive ectx :=
| EmptyCtx
Ralf Jung's avatar
Ralf Jung committed
130
| AppLCtx (K1 : ectx)  (e2 : expr)
Ralf Jung's avatar
Ralf Jung committed
131
| AppRCtx (v1 : value) (K2 : ectx)
132
| Op1Ctx {T1 To : Type} (f : T1 -> To) (K : ectx)
Ralf Jung's avatar
Ralf Jung committed
133
| Op2LCtx {T1 T2 To : Type} (f : T1 -> T2 -> To) (K1 : ectx)  (e2 : expr)
134
| Op2RCtx {T1 T2 To : Type} (f : T1 -> T2 -> To) (v1 : value) (K2 : ectx)
Ralf Jung's avatar
Ralf Jung committed
135
| PairLCtx (K1 : ectx)  (e2 : expr)
Ralf Jung's avatar
Ralf Jung committed
136 137 138 139 140
| PairRCtx (v1 : value) (K2 : ectx)
| FstCtx (K : ectx)
| SndCtx (K : ectx)
| InjLCtx (K : ectx)
| InjRCtx (K : ectx)
141
| CaseCtx (K : ectx) (e1 : {bind expr}) (e2 : {bind expr})
Ralf Jung's avatar
Ralf Jung committed
142
| AllocCtx (K : ectx)
Ralf Jung's avatar
Ralf Jung committed
143 144 145 146 147 148 149
| LoadCtx (K : ectx)
| StoreLCtx (K1 : ectx)  (e2 : expr)
| StoreRCtx (v1 : value) (K2 : ectx)
| CasLCtx (K0 : ectx)  (e1 : expr)  (e2 : expr)
| CasMCtx (v0 : value) (K1 : ectx)  (e2 : expr)
| CasRCtx (v0 : value) (v1 : value) (K2 : ectx)
.
Ralf Jung's avatar
Ralf Jung committed
150 151 152 153 154 155

Fixpoint fill (K : ectx) (e : expr) :=
  match K with
  | EmptyCtx => e
  | AppLCtx K1 e2 => App (fill K1 e) e2
  | AppRCtx v1 K2 => App (v2e v1) (fill K2 e)
156 157 158
  | Op1Ctx _ _ f K => Op1 f (fill K e)
  | Op2LCtx _ _ _ f K1 e2 => Op2 f (fill K1 e) e2
  | Op2RCtx _ _ _ f v1 K2 => Op2 f (v2e v1) (fill K2 e)
Ralf Jung's avatar
Ralf Jung committed
159 160 161 162 163 164 165
  | PairLCtx K1 e2 => Pair (fill K1 e) e2
  | PairRCtx v1 K2 => Pair (v2e v1) (fill K2 e)
  | FstCtx K => Fst (fill K e)
  | SndCtx K => Snd (fill K e)
  | InjLCtx K => InjL (fill K e)
  | InjRCtx K => InjR (fill K e)
  | CaseCtx K e1 e2 => Case (fill K e) e1 e2
Ralf Jung's avatar
Ralf Jung committed
166
  | AllocCtx K => Alloc (fill K e)
167
  | LoadCtx K => Load (fill K e)
Ralf Jung's avatar
Ralf Jung committed
168 169 170 171 172
  | StoreLCtx K1 e2 => Store (fill K1 e) e2
  | StoreRCtx v1 K2 => Store (v2e v1) (fill K2 e)
  | CasLCtx K0 e1 e2 => Cas (fill K0 e) e1 e2
  | CasMCtx v0 K1 e2 => Cas (v2e v0) (fill K1 e) e2
  | CasRCtx v0 v1 K2 => Cas (v2e v0) (v2e v1) (fill K2 e)
Ralf Jung's avatar
Ralf Jung committed
173 174 175 176 177 178 179
  end.

Fixpoint comp_ctx (Ko : ectx) (Ki : ectx) :=
  match Ko with
  | EmptyCtx => Ki
  | AppLCtx K1 e2 => AppLCtx (comp_ctx K1 Ki) e2
  | AppRCtx v1 K2 => AppRCtx v1 (comp_ctx K2 Ki)
180 181 182
  | Op1Ctx _ _ f K => Op1Ctx f (comp_ctx K Ki)
  | Op2LCtx _ _ _ f K1 e2 => Op2LCtx f (comp_ctx K1 Ki) e2
  | Op2RCtx _ _ _ f v1 K2 => Op2RCtx f v1 (comp_ctx K2 Ki)
Ralf Jung's avatar
Ralf Jung committed
183 184 185 186 187 188 189
  | PairLCtx K1 e2 => PairLCtx (comp_ctx K1 Ki) e2
  | PairRCtx v1 K2 => PairRCtx v1 (comp_ctx K2 Ki)
  | FstCtx K => FstCtx (comp_ctx K Ki)
  | SndCtx K => SndCtx (comp_ctx K Ki)
  | InjLCtx K => InjLCtx (comp_ctx K Ki)
  | InjRCtx K => InjRCtx (comp_ctx K Ki)
  | CaseCtx K e1 e2 => CaseCtx (comp_ctx K Ki) e1 e2
Ralf Jung's avatar
Ralf Jung committed
190
  | AllocCtx K => AllocCtx (comp_ctx K Ki)
191
  | LoadCtx K => LoadCtx (comp_ctx K Ki)
Ralf Jung's avatar
Ralf Jung committed
192 193 194 195 196
  | StoreLCtx K1 e2 => StoreLCtx (comp_ctx K1 Ki) e2
  | StoreRCtx v1 K2 => StoreRCtx v1 (comp_ctx K2 Ki)
  | CasLCtx K0 e1 e2 => CasLCtx (comp_ctx K0 Ki) e1 e2
  | CasMCtx v0 K1 e2 => CasMCtx v0 (comp_ctx K1 Ki) e2
  | CasRCtx v0 v1 K2 => CasRCtx v0 v1 (comp_ctx K2 Ki)
Ralf Jung's avatar
Ralf Jung committed
197 198 199 200 201 202 203 204 205 206 207
  end.

Lemma fill_empty e :
  fill EmptyCtx e = e.
Proof.
  reflexivity.
Qed.

Lemma fill_comp K1 K2 e :
  fill K1 (fill K2 e) = fill (comp_ctx K1 K2) e.
Proof.
208
  revert K2 e; induction K1 => K2 e /=; rewrite ?IHK1 ?IHK2; reflexivity.
Ralf Jung's avatar
Ralf Jung committed
209 210 211 212 213
Qed.

Lemma fill_inj_r K e1 e2 :
  fill K e1 = fill K e2 -> e1 = e2.
Proof.
214 215
  revert e1 e2; induction K => el er /=;
     (move=><-; reflexivity) || (case => /IHK <-; reflexivity).
Ralf Jung's avatar
Ralf Jung committed
216 217
Qed.

Ralf Jung's avatar
Ralf Jung committed
218
Lemma fill_value K e v':
219
  e2v (fill K e) = Some v' -> is_Some (e2v e).
Ralf Jung's avatar
Ralf Jung committed
220
Proof.
221
  revert v'; induction K => v' /=; try discriminate;
Ralf Jung's avatar
Ralf Jung committed
222 223 224
    try destruct (e2v (fill K e)); rewrite ?v2v; eauto.
Qed.

225 226 227
Lemma fill_not_value e K :
  e2v e = None -> e2v (fill K e) = None.
Proof.
228
  intros Hnval.  induction K =>/=; by rewrite ?v2v /= ?IHK /=.
229
Qed.
230

231 232 233 234 235 236 237 238
Lemma fill_not_value2 e K v :
  e2v e = None -> e2v (fill K e) = Some v -> False.
Proof.
  intros Hnval Hval. erewrite fill_not_value in Hval by assumption. discriminate.
Qed.


(** The stepping relation *)
Ralf Jung's avatar
Ralf Jung committed
239
Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
Ralf Jung's avatar
Ralf Jung committed
240
| BetaS e1 e2 v2 σ (Hv2 : e2v e2 = Some v2):
Ralf Jung's avatar
Ralf Jung committed
241
    prim_step (App (Rec e1) e2) σ (e1.[e2.:(Rec e1).:ids]) σ None
242 243 244 245
| Op1S T1 To (f : T1 -> To) t σ:
    prim_step (Op1 f (Lit t)) σ (Lit (f t)) σ None
| Op2S T1 T2 To (f : T1 -> T2 -> To) t1 t2 σ:
    prim_step (Op2 f (Lit t1) (Lit t2)) σ (Lit (f t1 t2)) σ None
246 247 248 249
| FstS e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2):
    prim_step (Fst (Pair e1 e2)) σ e1 σ None
| SndS e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2):
    prim_step (Snd (Pair e1 e2)) σ e2 σ None
Ralf Jung's avatar
Ralf Jung committed
250
| CaseLS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
251
    prim_step (Case (InjL e0) e1 e2) σ (e1.[e0/]) σ None
Ralf Jung's avatar
Ralf Jung committed
252 253 254
| CaseRS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
    prim_step (Case (InjR e0) e1 e2) σ (e2.[e0/]) σ None
| ForkS e σ:
255 256
    prim_step (Fork e) σ LitUnit σ (Some e)
| RefS e v σ l (Hv : e2v e = Some v) (Hfresh : σ !! l = None):
Ralf Jung's avatar
Ralf Jung committed
257
    prim_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
Ralf Jung's avatar
Ralf Jung committed
258 259 260 261 262 263 264 265 266 267 268
| LoadS l v σ (Hlookup : σ !! l = Some v):
    prim_step (Load (Loc l)) σ (v2e v) σ None
| StoreS l e v σ (Hv : e2v e = Some v) (Halloc : is_Some (σ !! l)):
    prim_step (Store (Loc l) e) σ LitUnit (<[l:=v]>σ) None
| CasFailS l e1 v1 e2 v2 vl σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2)
  (Hlookup : σ !! l = Some vl) (Hne : vl <> v1):
    prim_step (Cas (Loc l) e1 e2) σ LitFalse σ None
| CasSucS l e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2)
  (Hlookup : σ !! l = Some v1):
    prim_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None
.
269 270

Definition reducible e: Prop :=
Ralf Jung's avatar
Ralf Jung committed
271
  exists σ e' σ' ef, prim_step e σ e' σ' ef.
272

273 274 275 276 277 278
Lemma reducible_not_value e:
  reducible e -> e2v e = None.
Proof.
  intros (σ' & e'' & σ'' & ef & Hstep). destruct Hstep; simpl in *; reflexivity.
Qed.

279 280 281 282 283 284 285 286
Definition stuck (e : expr) : Prop :=
  forall K e',
    e = fill K e' ->
    ~reducible e'.

Lemma values_stuck v :
  stuck (v2e v).
Proof.
Ralf Jung's avatar
Ralf Jung committed
287 288 289
  intros ?? Heq.
  edestruct (fill_value K) as [v' Hv'].
  { by rewrite <-Heq, v2v. }
290 291
  clear -Hv' => Hred. apply reducible_not_value in Hred.
  destruct (e2v e'); discriminate.
Ralf Jung's avatar
Ralf Jung committed
292
Qed.
293

Ralf Jung's avatar
Ralf Jung committed
294
Section step_by_value.
295 296 297 298
(* When something does a step, and another decomposition of the same
     expression has a non-value e in the hole, then K is a left
     sub-context of K' - in other words, e also contains the reducible
     expression *)
299
Lemma step_by_value {K K' e e'} :
300 301 302 303 304
  fill K e = fill K' e' ->
  reducible e' ->
  e2v e = None ->
  exists K'', K' = comp_ctx K K''.
Proof.
305 306 307 308
  Ltac bad_fill := intros; exfalso; subst;
                   (eapply values_stuck; eassumption) || (eapply fill_not_value2; first eassumption;
                    try match goal with [ H : fill _ _ = _ |- _ ] => erewrite ->H end;
                    by erewrite ?v2v).
309
  Ltac bad_red   Hfill e' Hred := exfalso; destruct e'; try discriminate Hfill; [];
Ralf Jung's avatar
Ralf Jung committed
310 311 312 313
      case: Hfill; intros; subst; destruct Hred as (σ' & e'' & σ'' & ef & Hstep);
      inversion Hstep; done || (clear Hstep; subst;
      eapply fill_not_value2; last (
        try match goal with [ H : _ = fill _ _ |- _ ] => erewrite <-H end; simpl;
Ralf Jung's avatar
Ralf Jung committed
314
        repeat match goal with [ H : e2v _ = _ |- _ ] => erewrite H; clear H; simpl end
Ralf Jung's avatar
Ralf Jung committed
315
      ); eassumption || done).
316
  Ltac good IH := intros; subst; 
Ralf Jung's avatar
Ralf Jung committed
317 318 319 320
    let K'' := fresh "K''" in edestruct IH as [K'' Hcomp]; first eassumption;
    exists K''; by eauto using f_equal, f_equal2, f_equal3, v2e_inj.

  intros Hfill Hred Hnval. 
321
  Time revert K' Hfill; induction K=>K' /= Hfill;
322
    first (now eexists; reflexivity);
323 324 325 326 327 328
    (destruct K'; simpl;
      (* The first case is: K' is EmpyCtx. *)
      first (by bad_red Hfill e' Hred);
      (* Many of the other cases result in contradicting equalities. *)
      try discriminate Hfill;
      (* The remaining cases are "compatible" contexts - that result in the same head symbol of the expression.
329 330 331 332 333 334 335 336 337 338 339 340 341
         Test whether the context als has the same head, and use the appropriate tactic.
         Furthermore, the Op* contexts need special treatment due to the inhomogenuous equalities
         they induce. *)
      by match goal with
      | [ |- exists x, Op1Ctx _ _ = Op1Ctx _ _ ] => move: Hfill; case_depeq2; good IHK
      | [ |- exists x, Op2LCtx _ _ _ = Op2LCtx _ _ _ ] => move: Hfill; case_depeq3; good IHK
      | [ |- exists x, Op2RCtx _ _ _ = Op2RCtx _ _ _ ] => move: Hfill; case_depeq3; good IHK
      | [ |- exists x, ?C _ = ?C _ ] => case: Hfill; good IHK
      | [ |- exists x, ?C _ _ = ?C _ _ ] => case: Hfill; good IHK
      | [ |- exists x, ?C _ _ _ = ?C _ _ _ ] => case: Hfill; good IHK
      | [ |- exists x, Op2LCtx _ _ _ = Op2RCtx _ _ _ ] => move: Hfill; case_depeq3; bad_fill
      | [ |- exists x, Op2RCtx _ _ _ = Op2LCtx _ _ _ ] => move: Hfill; case_depeq3; bad_fill
      | _ => case: Hfill; bad_fill
342
      end).
Ralf Jung's avatar
Ralf Jung committed
343 344
Qed.
End step_by_value.
345

346 347 348
(** Atomic expressions *)
Definition atomic (e: expr) :=
  match e with
Ralf Jung's avatar
Ralf Jung committed
349
  | Alloc e => is_Some (e2v e)
350
  | Load e => is_Some (e2v e)
Ralf Jung's avatar
Ralf Jung committed
351 352
  | Store e1 e2 => is_Some (e2v e1) /\ is_Some (e2v e2)
  | Cas e0 e1 e2 => is_Some (e2v e0) /\ is_Some (e2v e1) /\ is_Some (e2v e2)
353 354 355
  | _ => False
  end.

356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375
Lemma atomic_not_value e :
  atomic e -> e2v e = None.
Proof.
  destruct e; simpl; contradiction || reflexivity.
Qed.

Lemma atomic_step e1 σ1 e2 σ2 ef :
  atomic e1 ->
  prim_step e1 σ1 e2 σ2 ef ->
  is_Some (e2v e2).
Proof.
  destruct e1; simpl; intros Hatomic Hstep; inversion Hstep; try contradiction Hatomic; rewrite ?v2v /=; eexists; reflexivity.
Qed.

(* Atomics must not contain evaluation positions. *)
Lemma atomic_fill e K :
  atomic (fill K e) ->
  e2v e = None ->
  K = EmptyCtx.
Proof.
Ralf Jung's avatar
Ralf Jung committed
376 377
  destruct K; simpl; first reflexivity; unfold is_Some; intros Hatomic Hnval; exfalso; try assumption;
    try (destruct_conjs; eapply fill_not_value2; eassumption).
378 379
Qed.

380
(** Tests, making sure that stuff works. *)
381
Module Tests.
Ralf Jung's avatar
Ralf Jung committed
382
  Definition add := Op2 plus (Lit 21) (Lit 21).
383

Ralf Jung's avatar
Ralf Jung committed
384
  Goal forall σ, prim_step add σ (Lit 42) σ None.
385 386 387
  Proof.
    apply Op2S.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
388 389 390 391 392 393 394 395 396 397 398 399 400 401

  Definition rec := Rec (App (Var 1) (Var 0)). (* fix f x => f x *)
  Definition rec_app := App rec (Lit 0).
  Goal forall σ, prim_step rec_app σ rec_app σ None.
  Proof.
    move=>?. eapply BetaS. (* Honestly, I have no idea why this works. *)
    reflexivity.
  Qed.

  Definition lam := Lam (Op2 plus (Var 0) (Lit 21)).
  Goal forall σ, prim_step (App lam (Lit 21)) σ add σ None.
  Proof.
    move=>?. eapply BetaS. reflexivity.
  Qed.
402
End Tests.
403 404 405 406 407

(** Instantiate the Iris language interface. This closes reduction under evaluation contexts.
    We could potentially make this a generic construction. *)
Section Language.

408
  Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
409 410
    exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef.

411
  Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ectx_step.
412 413 414 415
  Proof.
    - exact v2v.
    - exact e2e.
    - intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2.
416 417 418 419 420 421 422
      eapply fill_not_value. eapply reducible_not_value. do 4 eexists; eassumption.
    - exact atomic_not_value.
    - intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep).
      subst. move: (Hatomic). rewrite (atomic_fill e1' K). (* RJ: this is kind of annoying. *)
      + rewrite !fill_empty. eauto using atomic_step.
      + assumption.
      + clear Hatomic. eapply reducible_not_value. do 4 eexists; eassumption.
423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439
  Defined.

  (** We can have bind with arbitrary evaluation contexts **)
  Lemma fill_is_ctx K: is_ctx (fill K).
  Proof.
    split; last split.
    - intros ? [v Hval]. eapply fill_value. eassumption.
    - intros ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
      exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
      split; last split; reflexivity || assumption.
    - intros ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep).
      destruct (step_by_value Heq1) as [K' HeqK].
      + do 4 eexists. eassumption.
      + assumption.
      + subst e2 K''. rewrite -fill_comp in Heq1. apply fill_inj_r in Heq1. subst e1'.
        exists (fill K' e2''). split; first by rewrite -fill_comp.
        do 3 eexists. split; last split; eassumption || reflexivity.
440
  Qed.
441

442
End Language.