Top.SystemC.Substitution

The source of this file can be found on Github.

Weakening

The standard lemmas for weakening the environment in typing.

Lemma etyping_weakening : ∀ E F G Q e T,
  etyping (G ++ E) Q e T →
  wf_env (G ++ F ++ E) →
  etyping (G ++ F ++ E) Q e T
with btyping_weakening : ∀ E F G R Q e T,
  btyping (G ++ E) R Q e T →
  wf_env (G ++ F ++ E) →
  btyping (G ++ F ++ E) R Q e T
with styping_weakening : ∀ E F G R Q e T,
  styping (G ++ E) R Q e T →
  wf_env (G ++ F ++ E) →
  styping (G ++ F ++ E) R Q e T.

Lemma restriction_transitive : ∀ C1 C2 C3,
  C1 |= C2 →
  C2 |= C3 →
  C1 |= C3.

Capture Subsumption

Here we show that capture subsumption on blocks and statements is admissible.

Lemma btyping_weaken_restriction : ∀ C E R Q b S1,
  R |= C →
  wf_cap E R →
  E @ C ; Q |-blk b ~: S1 →
  E @ R ; Q |-blk b ~: S1
with styping_weaken_restriction : ∀ C E R Q s T,
  R |= C →
  wf_cap E R →
  E @ C ; Q |-stm s ~: T →
  E @ R ; Q |-stm s ~: T.

Substitution

We show the standard property that substitution preserves typing.

Substitution of expressions into terms

Lemma etyping_through_subst_ee : ∀ U E F Q x T e u,
  etyping (F ++ [(x, bind_val U)] ++ E) Q e T →
  etyping E Q u U →
  etyping (F ++ E) Q (subst_ee x u e) T
with btyping_through_subst_eb : ∀ U E F R Q x T e u,
  btyping (F ++ [(x, bind_val U)] ++ E) R Q e T →
  etyping E Q u U →
  btyping (F ++ E) R Q (subst_eb x u e) T
with styping_through_subst_es : ∀ U E F R Q x T e u,
  styping (F ++ [(x, bind_val U)] ++ E) R Q e T →
  etyping E Q u U →
  styping (F ++ E) R Q (subst_es x u e) T.

Substitution of monomorphic blocks into terms

Lemma etyping_through_subst_be : ∀ U C E F Q x T e u,
  etyping (F ++ [(x, bind_blk U (capture C))] ++ E) Q e T →
  btyping E C Q u U →
  etyping (F ++ E) Q (subst_be x u e) T
with btyping_through_subst_bb : ∀ U C E F R Q x T e u,
  btyping (F ++ [(x, bind_blk U (capture C))] ++ E) R Q e T →
  btyping E C Q u U →
  btyping (F ++ E) R Q (subst_bb x u e) T
with styping_through_subst_bs : ∀ U C E F R Q x T e u,
  styping (F ++ [(x, bind_blk U (capture C))] ++ E) R Q e T →
  btyping E C Q u U →
  styping (F ++ E) R Q (subst_bs x u e) T.

Substitution of polymorphic blocks into terms

Lemma etyping_through_subst_ce : ∀ (C : cap) U E F Q x T e u,
  etyping (F ++ [(x, bind_blk U tracked)] ++ E) Q e T →
  wf_cap E C →
  btyping E C Q u U →
  etyping (map (subst_bbind x C) F ++ E) Q (subst_ce x u C e) (subst_cvt x C T)
with btyping_through_subst_cb : ∀ (C : cap) U E F R Q x T e u,
  btyping (F ++ [(x, bind_blk U tracked)] ++ E) R Q e T →
  wf_cap E C →
  btyping E C Q u U →
  btyping (map (subst_bbind x C) F ++ E) (subst_cset x C R) Q (subst_cb x u C e) (subst_cbt x C T)
with styping_through_subst_cs : ∀ (C : cap) U E F R Q x T e u,
  styping (F ++ [(x, bind_blk U tracked)] ++ E) R Q e T →
  wf_cap E C →
  btyping E C Q u U →
  styping (map (subst_bbind x C) F ++ E) (subst_cset x C R) Q (subst_cs x u C e) (subst_cvt x C T).

Substitution of types into terms

We use our own induction principle to speed up termination checking.

Lemma typing_through_subst_t_ : ∀ U E Q X,
(∀ E_ Q_ e T,
  etyping E_ Q_ e T →
  (∀ F, E_ = F ++ [(X, bind_typ)] ++ E →
   Q_ = Q →
   wf_vtyp E U →
   etyping ((map (subst_tbind X U) F) ++ E) Q (subst_te X U e) (subst_tvt X U T)))
∧
(∀ E_ R Q_ e T,
  styping E_ R Q_ e T →
  (∀ F, E_ = F ++ [(X, bind_typ)] ++ E →
   Q_ = Q →
   wf_vtyp E U →
   styping ((map (subst_tbind X U) F) ++ E) R Q (subst_ts X U e) (subst_tvt X U T)))
∧
(∀ E_ R Q_ e T,
  btyping E_ R Q_ e T →
  (∀ F, E_ = F ++ [(X, bind_typ)] ++ E →
   Q_ = Q →
   wf_vtyp E U →
   btyping ((map (subst_tbind X U) F) ++ E) R Q (subst_tb X U e) (subst_tbt X U T))).

We now can state the lemmas as it is more common, using the helper above

Lemma etyping_through_subst_te: ∀ U E F Q X e T,
  wf_vtyp E U →
  etyping (F ++ [(X, bind_typ)] ++ E) Q e T →
  etyping ((map (subst_tbind X U) F) ++ E) Q (subst_te X U e) (subst_tvt X U T).

Lemma styping_through_subst_ts : ∀ U E F R Q X e T,
  wf_vtyp E U →
  styping (F ++ [(X, bind_typ)] ++ E) R Q e T →
  styping ((map (subst_tbind X U) F) ++ E) R Q (subst_ts X U e) (subst_tvt X U T).

Lemma btyping_through_subst_tb : ∀ U E F R Q X e T,
  wf_vtyp E U →
  btyping (F ++ [(X, bind_typ)] ++ E) R Q e T →
  btyping ((map (subst_tbind X U) F) ++ E) R Q (subst_tb X U e) (subst_tbt X U T).