language.v 3.6 KB
Newer Older
1
From iris.algebra Require Export ofe.
2
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
3

4 5 6 7 8 9
Structure language := Language {
  expr : Type;
  val : Type;
  state : Type;
  of_val : val  expr;
  to_val : expr  option val;
10
  prim_step : expr  state  expr  state  list expr  Prop;
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12
  to_of_val v : to_val (of_val v) = Some v;
  of_to_val e v : to_val e = Some v  of_val v = e;
13
  val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs  to_val e = None
Ralf Jung's avatar
Ralf Jung committed
14
}.
Janno's avatar
Janno committed
15 16 17
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Bind Scope expr_scope with expr.
18
Bind Scope val_scope with val.
19 20 21 22 23
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments prim_step {_} _ _ _ _ _.
Arguments to_of_val {_} _.
Arguments of_to_val {_} _ _ _.
24
Arguments val_stuck {_} _ _ _ _ _ _.
25

26 27 28
Canonical Structure stateC Λ := leibnizC (state Λ).
Canonical Structure valC Λ := leibnizC (val Λ).
Canonical Structure exprC Λ := leibnizC (expr Λ).
29 30

Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
Ralf Jung's avatar
Ralf Jung committed
31

32 33 34 35 36 37 38 39 40 41 42
Class LanguageCtx (Λ : language) (K : expr Λ  expr Λ) := {
  fill_not_val e :
    to_val e = None  to_val (K e) = None;
  fill_step e1 σ1 e2 σ2 efs :
    prim_step e1 σ1 e2 σ2 efs 
    prim_step (K e1) σ1 (K e2) σ2 efs;
  fill_step_inv e1' σ1 e2 σ2 efs :
    to_val e1' = None  prim_step (K e1') σ1 e2 σ2 efs 
     e2', e2 = K e2'  prim_step e1' σ1 e2' σ2 efs
}.

Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45
Instance language_ctx_id Λ : LanguageCtx Λ id.
Proof. constructor; naive_solver. Qed.

46
Section language.
47 48
  Context {Λ : language}.
  Implicit Types v : val Λ.
Ralf Jung's avatar
Ralf Jung committed
49

50
  Definition reducible (e : expr Λ) (σ : state Λ) :=
51
     e' σ' efs, prim_step e σ e' σ' efs.
52
  Definition irreducible (e : expr Λ) (σ : state Λ) :=
53 54
     e' σ' efs, ¬prim_step e σ e' σ' efs.

55
  Definition atomic (e : expr Λ) : Prop :=
56
     σ e' σ' efs, prim_step e σ e' σ' efs  irreducible e' σ'.
57

58
  Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
59
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
60
       ρ1 = (t1 ++ e1 :: t2, σ1) 
61 62
       ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) 
       prim_step e1 σ1 e2 σ2 efs 
63 64
       step ρ1 ρ2.

Robbert Krebbers's avatar
Robbert Krebbers committed
65 66
  Lemma of_to_val_flip v e : of_val v = e  to_val e = Some v.
  Proof. intros <-. by rewrite to_of_val. Qed.
67 68 69

  Lemma not_reducible e σ : ¬reducible e σ  irreducible e σ.
  Proof. unfold reducible, irreducible. naive_solver. Qed.
70
  Lemma reducible_not_val e σ : reducible e σ  to_val e = None.
71
  Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
72 73
  Lemma val_irreducible e σ : is_Some (to_val e)  irreducible e σ.
  Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed.
74
  Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
75
  Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Ralf Jung's avatar
Ralf Jung committed
76

77 78 79 80 81 82 83 84 85
  Lemma reducible_fill `{LanguageCtx Λ K} e σ :
    to_val e = None  reducible (K e) σ  reducible e σ.
  Proof.
    intros ? (e'&σ'&efs&Hstep); unfold reducible.
    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
  Qed.
  Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
    to_val e = None  irreducible e σ  irreducible (K e) σ.
  Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
86 87 88 89 90 91 92 93 94 95

  Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
    t1  t1'  step (t1,σ1) (t2,σ2)   t2', t2  t2'  step (t1',σ1) (t2',σ2).
  Proof.
    intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
    move: Ht; rewrite -Permutation_middle (symmetry_iff ()).
    intros (tl'&tr'&->&Ht)%Permutation_cons_inv.
    exists (tl' ++ e2 :: tr' ++ efs); split; [|by econstructor].
    by rewrite -!Permutation_middle !assoc_L Ht.
  Qed.
96
End language.