Module RawSemantics

Set Implicit Arguments.
Require Import MyTactics.
Require Import Arithmetic.
Require Import Store.
Require Import RawPrograms.


Inductive rred : raw_store -> raw_term -> raw_store -> raw_term -> Prop :=
| RawRedBeta:
    forall rs rt rv,
    rred
      rs (RawTApp (RawVAbs rt) (RawTVal rv))
      rs (subst_raw_term rv 0 rt)
| RawRedLetPair:
    forall rs rv1 rv2 rt,
    rred
      rs (RawTLetPair (RawVPair rv1 rv2) rt)
      rs (subst_raw_term rv1 0 (subst_raw_term (lift_raw_value 0 rv2) 0 rt))
| RawRedAppContext:
    forall rs1 rs2 rt1 rt2 rv,
    rred rs1 rt1 rs2 rt2 ->
    rred rs1 (RawTApp rv rt1) rs2 (RawTApp rv rt2)
| RawRedNew:
    forall rm1 limit rv rm2,
    extend rm1 limit rv = rm2 ->
    rred
      (Store limit rm1) (RawTNew rv)
      (Store (S limit) rm2) (RawTVal (RawVLoc limit))
| RawRedRead:
    forall limit rm l rv,
    rm l = Some rv ->
    rred
      (Store limit rm) (RawTRead (RawVLoc l))
      (Store limit rm) (RawTVal rv)
| RawRedWriteCap:
    forall limit rm1 l rv1 rv2 rm2,
    rm1 l = Some rv1 ->
    extend rm1 l rv2 = rm2 ->
    rred
      (Store limit rm1) (RawTWrite (RawVPair (RawVLoc l) rv2))
      (Store limit rm2) (RawTVal RawVUnit)
.

Hint Constructors rred.


Lemma values_do_not_reduce:
  forall rs1 rv rs2 rt,
  ~ rred rs1 (RawTVal rv) rs2 rt.

Ltac values_do_not_reduce :=
  match goal with h: rred _ (RawTVal _) _ _ |- _ => false; exact (values_do_not_reduce h) end.


Lemma rred_deterministic:
  forall rs rt rs1 rt1,
  rred rs rt rs1 rt1 ->
  forall rs2 rt2,
  rred rs rt rs2 rt2 ->
  rs1 = rs2 /\ rt1 = rt2.

Ltac rred_deterministic :=
  match goal with h1: rred ?rs ?rt ?rs1 ?rt1, h2: rred ?rs ?rt ?rs2 ?rt2 |- _ =>
    unpack (rred_deterministic h1 h2); clear h2; subst rs2; subst rt2
  end.


Inductive rredplus : raw_store -> raw_term -> raw_store -> raw_term -> Prop :=
| RredplusOne:
    forall rs1 rt1 rs2 rt2,
    rred rs1 rt1 rs2 rt2 ->
    rredplus rs1 rt1 rs2 rt2
| RredplusMore:
    forall rs1 rt1 rs2 rt2 rs3 rt3,
    rred rs1 rt1 rs2 rt2 ->
    rredplus rs2 rt2 rs3 rt3 ->
    rredplus rs1 rt1 rs3 rt3.

Hint Constructors rredplus.

Lemma RawRedplusAppContext:
  forall rs1 rs2 rt1 rt2 rv,
  rredplus rs1 rt1 rs2 rt2 ->
  rredplus rs1 (RawTApp rv rt1) rs2 (RawTApp rv rt2).

Hint Resolve RawRedplusAppContext.


Inductive rredstar : raw_store -> raw_term -> raw_store -> raw_term -> Prop :=
| RredstarZero:
    forall rs rt,
    rredstar rs rt rs rt
| RredstarMore:
    forall rs1 rt1 rs2 rt2 rs3 rt3,
    rred rs1 rt1 rs2 rt2 ->
    rredstar rs2 rt2 rs3 rt3 ->
    rredstar rs1 rt1 rs3 rt3.

Hint Constructors rredstar.

Lemma rredplus_implies_rredstar:
  forall rs1 rt1 rs2 rt2,
  rredplus rs1 rt1 rs2 rt2 ->
  rredstar rs1 rt1 rs2 rt2.

Hint Resolve rredplus_implies_rredstar.


Lemma rred_and_rredplus:
  forall rs rt rs1 rt1 rs2 rt2,
  rred rs rt rs1 rt1 ->
  rredplus rs rt rs2 rt2 ->
  rredstar rs1 rt1 rs2 rt2.

Lemma rred_and_rredstar:
  forall rs rt rs1 rt1 rs2 rt2,
  rred rs rt rs1 rt1 ->
  rredstar rs rt rs2 rt2 ->
  rredstar rs1 rt1 rs2 rt2 \/
  rs = rs2 /\ rt = rt2.


CoInductive diverges : raw_store -> raw_term -> Prop :=
| DivergesCons:
    forall rs1 rt1 rs2 rt2,
    rred rs1 rt1 rs2 rt2 ->
    diverges rs2 rt2 ->
    diverges rs1 rt1.


Inductive sensible_raw_store : raw_store -> Prop :=
| SensibleRawStore:
    forall rm limit,
    (forall l, l < limit -> rm l <> None) ->
    (forall l, rm l <> None -> l < limit) ->
    sensible_raw_store (Store limit rm).

Lemma empty_raw_store_is_sensible:
  sensible_raw_store (Store 0 (fun l => None)).

Lemma raw_reduction_preserves_sensible:
  forall rs1 rt1 rs2 rt2,
  rred rs1 rt1 rs2 rt2 ->
  sensible_raw_store rs1 ->
  sensible_raw_store rs2.