Module RawPrograms

Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Store.

This module defines the syntax of terms without any type annotations.

Values.

Terms.

Stores.

Definition raw_store :=
gstore raw_value.

Syntactic sugar for sequencing.

Notation RawTLet t1 t2 :=
(RawTApp (RawVAbs t2) t1).

Syntactic sugar for pair projection.

Notation RawTFirst v :=
(RawTLetPair v (RawTVal (RawVVar 1))).

Construct an appropriate mutual induction scheme.

Scheme raw_value_term_ind_v := Induction for raw_value Sort Prop
with raw_value_term_ind_t := Induction for raw_term Sort Prop.

Combined Scheme raw_value_term_ind from raw_value_term_ind_v, raw_value_term_ind_t.

De Bruijn operations over terms.

Fixpoint lift_raw_value (k : nat) (v : raw_value) : raw_value :=
  match v with
  | RawVVar x =>
      RawVVar (lift_var k x)
  | RawVAbs t =>
      RawVAbs (lift_raw_term (1 + k) t)
  | RawVPair v1 v2 =>
      RawVPair (lift_raw_value k v1) (lift_raw_value k v2)
  | RawVUnit =>
      RawVUnit
  | RawVLoc l =>
      RawVLoc l
  | RawVErased =>
      RawVErased
  end

with lift_raw_term (k : nat) (t : raw_term) : raw_term :=
  match t with
  | RawTVal v =>
      RawTVal (lift_raw_value k v)
  | RawTApp v t =>
      RawTApp (lift_raw_value k v) (lift_raw_term k t)
  | RawTLetPair v t =>
      RawTLetPair (lift_raw_value k v) (lift_raw_term (2 + k) t)
  | RawTNew v =>
      RawTNew (lift_raw_value k v)
  | RawTRead v =>
      RawTRead (lift_raw_value k v)
  | RawTWrite v =>
      RawTWrite (lift_raw_value k v)
  end.

Substitutions of values for variables within values and terms. By design of the syntax, substitution of terms for variables is not possible.

Fixpoint subst_raw_value (v : raw_value) (k : nat) (w : raw_value) : raw_value :=
  match w with
  | RawVVar x =>
      subst_var RawVVar v k x
  | RawVAbs u =>
      RawVAbs (subst_raw_term (lift_raw_value 0 v) (1 + k) u)
  | RawVPair w1 w2 =>
      RawVPair (subst_raw_value v k w1) (subst_raw_value v k w2)
  | RawVUnit =>
      RawVUnit
  | RawVLoc l =>
      RawVLoc l
  | RawVErased =>
      RawVErased
  end

with subst_raw_term (v : raw_value) (k : nat) (u : raw_term) : raw_term :=
  match u with
  | RawTVal w =>
      RawTVal (subst_raw_value v k w)
  | RawTApp w u =>
      RawTApp (subst_raw_value v k w) (subst_raw_term v k u)
  | RawTLetPair w u =>
      RawTLetPair (subst_raw_value v k w) (subst_raw_term (lift_raw_value 0 (lift_raw_value 0 v)) (2 + k) u)
  | RawTNew w =>
      RawTNew (subst_raw_value v k w)
  | RawTRead w =>
      RawTRead (subst_raw_value v k w)
  | RawTWrite w =>
      RawTWrite (subst_raw_value v k w)
  end.

De Bruijn lemmas.

Lemma raw_subst_lift_value_term:
(forall w v k, subst_raw_value v k (lift_raw_value k w) = w) /\
(forall t v k, subst_raw_term v k (lift_raw_term k t) = t).

Proof.

apply raw_value_term_ind; simpl; intros; eauto with subst_lift_db.
Qed.

Lemma raw_subst_lift_value:
subst_lift lift_raw_value subst_raw_value.

Proof.

repeat intro. eapply raw_subst_lift_value_term.
Qed.

Lemma raw_subst_lift_term:
subst_lift lift_raw_term subst_raw_term.

Proof.

repeat intro. eapply raw_subst_lift_value_term.
Qed.

Local Hint Resolve raw_subst_lift_value raw_subst_lift_term.

Lemma raw_lift_lift_value_term:
(
  forall v k1 s1,
  k1 <= s1 ->
  lift_raw_value k1 (lift_raw_value s1 v) =
  lift_raw_value (S s1) (lift_raw_value k1 v)
) /\ (
  forall t k1 s1,
  k1 <= s1 ->
  lift_raw_term k1 (lift_raw_term s1 t) =
  lift_raw_term (S s1) (lift_raw_term k1 t)
).

Proof.

apply raw_value_term_ind; intros; simpl; f_equal; eauto with lift_lift_db.
Qed.

Lemma raw_lift_lift_value:
lift_lift lift_raw_value.

Proof.

repeat intro. apply raw_lift_lift_value_term; auto.
Qed.

Lemma raw_lift_lift_term:
lift_lift lift_raw_term.

Proof.

repeat intro. apply raw_lift_lift_value_term; auto.
Qed.

Local Hint Resolve raw_lift_lift_value raw_lift_lift_term.

Lemma raw_lift_zero_lift_value:
lift_zero_lift lift_raw_value.

Proof.

lift_zero_lift_tac.
Qed.

Lemma raw_lift_zero_lift_term:
lift_zero_lift lift_raw_term.

Proof.

lift_zero_lift_tac.
Qed.

Ltac lzl_raw_value :=
  lzl lift_raw_value raw_lift_zero_lift_value.

Hint Extern 1 => lzl_raw_value : lift_subst_1_db.
Hint Extern 1 => lzl_raw_value : lift_subst_2_db.
Hint Extern 1 => lzl_raw_value : subst_subst_db.

Lemma raw_lift_subst_1_value_term:
(
  forall w k1 v s1,
  k1 <= s1 ->
  lift_raw_value k1 (subst_raw_value v s1 w) =
  subst_raw_value (lift_raw_value k1 v) (S s1) (lift_raw_value k1 w)
) /\ (
  forall t k1 v s1,
  k1 <= s1 ->
  lift_raw_term k1 (subst_raw_term v s1 t) =
  subst_raw_term (lift_raw_value k1 v) (S s1) (lift_raw_term k1 t)
).

Proof.

apply raw_value_term_ind; simpl; intros; eauto 6 with lift_subst_1_db.
Qed.

Lemma raw_lift_subst_1_value:
lift_subst_1 lift_raw_value lift_raw_value subst_raw_value.

Proof.

repeat intro. apply raw_lift_subst_1_value_term; auto.
Qed.

Lemma raw_lift_subst_1_term:
lift_subst_1 lift_raw_value lift_raw_term subst_raw_term.

Proof.

repeat intro. apply raw_lift_subst_1_value_term; auto.
Qed.

Local Hint Resolve raw_lift_subst_1_value raw_lift_subst_1_term.

Hint Extern 1 => rewrite raw_lift_subst_1_value; [ idtac | omega ] : subst_subst_db.

Lemma raw_lift_subst_2_value_term:
(
  forall w k1 v s1,
  k1 <= s1 ->
  lift_raw_value s1 (subst_raw_value v k1 w) =
  subst_raw_value (lift_raw_value s1 v) k1 (lift_raw_value (S s1) w)
) /\ (
  forall t k1 v s1,
  k1 <= s1 ->
  lift_raw_term s1 (subst_raw_term v k1 t) =
  subst_raw_term (lift_raw_value s1 v) k1 (lift_raw_term (S s1) t)
).

Proof.

apply raw_value_term_ind; simpl; intros; eauto 6 with lift_subst_2_db.
Qed.

Lemma raw_lift_subst_2_value:
lift_subst_2 lift_raw_value lift_raw_value subst_raw_value.

Proof.

repeat intro. apply raw_lift_subst_2_value_term; auto.
Qed.

Lemma raw_lift_subst_2_term:
lift_subst_2 lift_raw_value lift_raw_term subst_raw_term.

Proof.

repeat intro. apply raw_lift_subst_2_value_term; auto.
Qed.

Lemma raw_lift_subst_2_term_rawverased:
  forall u k1 s1,
  k1 <= s1 ->
  lift_raw_term s1 (subst_raw_term RawVErased k1 u) =
  subst_raw_term RawVErased k1 (lift_raw_term (S s1) u).

Proof.

intros. rewrite raw_lift_subst_2_term; simpl; eauto.
Qed.

Local Hint Resolve raw_lift_subst_2_value raw_lift_subst_2_term.

Lemma raw_subst_subst_value_term:
(
  forall v k1 t u s1,
  k1 <= s1 ->
  subst_raw_value t s1 (subst_raw_value u k1 v) =
  subst_raw_value (subst_raw_value t s1 u) k1 (subst_raw_value (lift_raw_value k1 t) (S s1) v)
) /\ (
  forall v k1 t u s1,
  k1 <= s1 ->
  subst_raw_term t s1 (subst_raw_term u k1 v) =
  subst_raw_term (subst_raw_value t s1 u) k1 (subst_raw_term (lift_raw_value k1 t) (S s1) v)
).

Proof.

apply raw_value_term_ind; simpl; intros; eauto with subst_subst_db;

some more difficult cases

f_equal; eauto 6 with subst_subst_db.
Qed.

Lemma raw_subst_subst_value:
subst_subst lift_raw_value subst_raw_value subst_raw_value.

Proof.

repeat intro. apply raw_subst_subst_value_term; auto.
Qed.

Lemma raw_subst_subst_term:
subst_subst lift_raw_value subst_raw_value subst_raw_term.

Proof.

repeat intro. apply raw_subst_subst_value_term; auto.
Qed.

Local Hint Resolve raw_subst_subst_value raw_subst_subst_term.

Lemma raw_pun_1:
(forall u k, subst_raw_value (RawVVar k) (S k) (lift_raw_value k u) = u) /\
(forall u k, subst_raw_term (RawVVar k) (S k) (lift_raw_term k u) = u).

Proof.

apply raw_value_term_ind; simpl; intros; f_equal; eauto using pun_1_var.
Qed.

Lemma raw_pun_2:
(forall u k, subst_raw_value (RawVVar k) k (lift_raw_value (S k) u) = u) /\
(forall u k, subst_raw_term (RawVVar k) k (lift_raw_term (S k) u) = u).

Proof.

apply raw_value_term_ind; simpl; intros; f_equal; eauto using pun_2_var.
Qed.

Lemma lift_raw_value_term_injective:
(
  forall v1 v2 k,
  lift_raw_value k v1 = lift_raw_value k v2 ->
  v1 = v2
) /\ (
  forall t1 t2 k,
  lift_raw_term k t1 = lift_raw_term k t2 ->
  t1 = t2
).

Proof.

apply raw_value_term_ind; simpl; intros; invert_lift_equality; f_equal; eauto using lift_var_injective.
Qed.