Top.SystemC.Lemmas

The source of this file can be found on Github.

This file mostly contains lemmas about wellformedness. Properties of wellformed types, capability sets, typing judgements and so forth.

It finally also contains regularity properties: given a typing judgements we can extract information about the compontents. In particular, we know that certain components are locally closed, wellformed, etc.

Properties of Wellformedness

If a type is well-formed in an environment, then it is locally closed.

Lemma capt_from_wf_cap : ∀ E T,
  wf_cap E T → capt T.

Lemma vtype_from_wf_vtyp : ∀ E T,
  wf_vtyp E T → vtype T
with btype_from_wf_btyp : ∀ E T,
  wf_btyp E T → btype T.

The remaining properties are analogous to the properties that we need to show for the typing relations.

Lemma wf_cap_subset : ∀ E R R0,
  R |= R0 →
  wf_cap E R →
  wf_cap E R0.

Lemma wf_cap_weakening : ∀ T E F G,
  wf_cap (G ++ E) T →
  ok (G ++ F ++ E) →
  wf_cap (G ++ F ++ E) T.

Lemma wf_cap_weaken_head : ∀ T E F,
  wf_cap E T →
  ok (F ++ E) →
  wf_cap (F ++ E) T.

Lemma wf_cap_bind_head : ∀ E R x S1,
  ok ([(x, bind_blk S1 tracked)] ++ E) →
  wf_cap E R →
  wf_cap ([(x, bind_blk S1 tracked)] ++ E) (cset_union R (cset_fvar x)).

Lemma wf_cap_lvar : ∀ E l,
  wf_cap E (cset_lvar l).

Lemma wf_cap_labels : ∀ E c,
  wf_cap E (from_labels (bound_labels c)).


Lemma wf_vtyp_weakening : ∀ T E F G,
  wf_vtyp (G ++ E) T →
  ok (G ++ F ++ E) →
  wf_vtyp (G ++ F ++ E) T
with wf_btyp_weakening : ∀ T E F G,
  wf_btyp (G ++ E) T →
  ok (G ++ F ++ E) →
  wf_btyp (G ++ F ++ E) T.

Lemma wf_vtyp_weaken_head : ∀ T E F,
  wf_vtyp E T →
  ok (F ++ E) →
  wf_vtyp (F ++ E) T
with wf_btyp_weaken_head : ∀ T E F,
  wf_btyp E T →
  ok (F ++ E) →
  wf_btyp (F ++ E) T.

Lemma wf_cap_strengthening : ∀ E F x U T,
 wf_cap (F ++ [(x, bind_val U)] ++ E) T →
 wf_cap (F ++ E) T.

Lemma wf_vtyp_strengthening : ∀ E F x U T,
 wf_vtyp (F ++ [(x, bind_val U)] ++ E) T →
 wf_vtyp (F ++ E) T
with wf_btyp_strengthening : ∀ E F x U T,
  wf_btyp (F ++ [(x, bind_val U)] ++ E) T →
  wf_btyp (F ++ E) T.

Lemma wf_cap_strengthening_blk : ∀ E F x U C T,
 wf_cap (F ++ [(x, bind_blk U (capture C))] ++ E) T →
 wf_cap (F ++ E) T.

Lemma wf_cap_strengthening_typ : ∀ E F X T,
 wf_cap (F ++ [(X, bind_typ)] ++ E) T →
 wf_cap (F ++ E) T.

Lemma wf_vtyp_strengthening_blk : ∀ E F x U C T,
 wf_vtyp (F ++ [(x, bind_blk U (capture C))] ++ E) T →
 wf_vtyp (F ++ E) T
with wf_btyp_strengthening_blk : ∀ E F x U C T,
  wf_btyp (F ++ [(x, bind_blk U (capture C))] ++ E) T →
  wf_btyp (F ++ E) T.

Lemma wf_cap_strengthening_blk_tracked : ∀ E F x U T,
  x `notin` cset_fvars T →
  wf_cap (F ++ [(x, bind_blk U tracked)] ++ E) T →
  wf_cap (F ++ E) T.

Lemma notin_fvars_open_cset : ∀ x k T C,
  x `notin` (cset_fvars T `union` cset_fvars C) →
  x `notin` cset_fvars (open_cset k T C).

Lemma notin_fv_cvt_open_cvt : ∀ x k T C,
  x `notin` (fv_cvt T `union` cset_fvars C) →
  x `notin` fv_cvt (open_cvt_rec k C T)
with notin_fv_cbt_open_cbt : ∀ x k T C,
  x `notin` (fv_cbt T `union` cset_fvars C) →
  x `notin` fv_cbt (open_cbt_rec k C T).

Lemma notin_fv_cvt_open_tvt : ∀ x k T U,
  x `notin` (fv_cvt T `union` fv_cvt U) →
  x `notin` (fv_cvt (open_tvt_rec k U T))
with notin_fv_cbt_open_tbt : ∀ x k T U,
  x `notin` (fv_cbt T `union` fv_cvt U) →
  x `notin` (fv_cbt (open_tbt_rec k U T)).

Lemma wf_vtyp_strengthening_blk_tracked : ∀ E F x U T,
 x `notin` fv_cvt T →
 wf_vtyp (F ++ [(x, bind_blk U tracked)] ++ E) T →
 wf_vtyp (F ++ E) T
with wf_btyp_strengthening_blk_tracked : ∀ E F x U T,
  x `notin` fv_cbt T →
  wf_btyp (F ++ [(x, bind_blk U tracked)] ++ E) T →
  wf_btyp (F ++ E) T.

Lemma wf_cap_subst_tracked : ∀ F E U Z P T,
  wf_cap (F ++ [(Z, bind_blk U tracked)] ++ E) T →
  wf_cap E P →
  ok (map (subst_bbind Z P) F ++ E) →
  wf_cap (map (subst_bbind Z P) F ++ E) (subst_cset Z P T).

Lemma wf_vtyp_subst_tracked : ∀ F E Z U C T,
  wf_vtyp (F ++ [(Z, bind_blk U tracked)] ++ E) T →
  wf_cap E C →
  ok (map (subst_bbind Z C) F ++ E) →
  ok (F ++ [(Z, bind_blk U tracked)] ++ E) →
  wf_vtyp (map (subst_bbind Z C) F ++ E) (subst_cvt Z C T)
with wf_btyp_subst_tracked : ∀ F E Z U C T,
  wf_btyp (F ++ [(Z, bind_blk U tracked)] ++ E) T →
  wf_cap E C →
  ok (map (subst_bbind Z C) F ++ E) →
  ok (F ++ [(Z, bind_blk U tracked)] ++ E) →
  wf_btyp (map (subst_bbind Z C) F ++ E) (subst_cbt Z C T).

Properties of Wellformed Environments

Lemma ok_from_wf_env : ∀ E,
  wf_env E →
  ok E.

We add ok_from_wf_env as a hint here since it helps blur the distinction between wf_env and ok in proofs. The lemmas in the Environment library use ok, whereas here we naturally have (or can easily show) the stronger wf_env. Thus, ok_from_wf_env serves as a bridge that allows us to use the environments library.

Lemma wf_vtyp_from_binds_typ : ∀ x U E,
  wf_env E →
  binds x (bind_val U) E →
  wf_vtyp E U.

Lemma wf_vtyp_from_wf_env_typ : ∀ x T E,
  wf_env ([(x, bind_val T)] ++ E) →
  wf_vtyp E T.

Lemma wf_btyp_from_binds_blk : ∀ x U Q E,
  wf_env E →
  binds x (bind_blk U Q) E →
  wf_btyp E U.

Lemma wf_btyp_from_wf_env_blk : ∀ x T Q E,
  wf_env ([(x, bind_blk T Q)] ++ E) →
  wf_btyp E T.

Lemma wf_vtyp_from_sig_binds : ∀ Q l T1 T,
  wf_sig Q →
  Signatures.binds l (bind_sig T1 T) Q →
  wf_vtyp empty T.

Lemma wf_vtyp_from_sig_binds_val : ∀ Q l T1 T,
  wf_sig Q →
  Signatures.binds l (bind_sig T1 T) Q →
  wf_vtyp empty T1.

Properties of wf_env

These properties are analogous to the properties that we need to show for the typing relations.

Lemma wf_env_tail : ∀ E F,
  wf_env (F ++ E) →
  wf_env E.

Lemma wf_env_strengthening : ∀ x T E F,
  wf_env (F ++ [(x, bind_val T)] ++ E) →
  wf_env (F ++ E).

Lemma wf_env_strengthening_blk : ∀ x S1 C E F,
  wf_env (F ++ [(x, bind_blk S1 (capture C))] ++ E) →
  wf_env (F ++ E).

Lemma wf_env_subst_tracked : ∀ x U E F C,
  wf_env (F ++ [(x, bind_blk U tracked)] ++ E) →
  wf_cap E C →
  wf_env (map (subst_bbind x C) F ++ E).

Environment is unchanged by substitution for a fresh name

Lemma notin_fv_cap_wf : ∀ E (X : atom) C,
  wf_cap E C →
  X `notin` dom E →
  X `notin` cset_fvars C.

Lemma notin_cset_fvars_open_cset : ∀ (Y X : atom) k c,
  X `notin` cset_fvars (open_cset k (cset_fvar Y) c) →
  X `notin` cset_fvars c.

Lemma notin_fv_cvt_open_cvt_rec : ∀ (Y X : atom) k T,
  X `notin` fv_cvt (open_cvt_rec k (cset_fvar Y) T) →
  X `notin` fv_cvt T
with notin_fv_cbt_open_cbt_rec : ∀ (Y X : atom) k T,
  X `notin` fv_cbt (open_cbt_rec k (cset_fvar Y) T) →
  X `notin` fv_cbt T.

Lemma notin_fv_cvt_open_tvt_rec : ∀ (Y X : atom) k T,
  X `notin` fv_cvt (open_tvt_rec k Y T) →
  X `notin` fv_cvt T
with notin_fv_cbt_open_tbt_rec : ∀ (Y X : atom) k T,
  X `notin` fv_cbt (open_tbt_rec k Y T) →
  X `notin` fv_cbt T.

Lemma notin_fv_cvt_wf : ∀ E (X : atom) T,
  wf_vtyp E T →
  X `notin` dom E →
  X `notin` fv_cvt T
with notin_fv_cbt_wf : ∀ E (X : atom) T,
  wf_btyp E T →
  X `notin` dom E →
  X `notin` fv_cbt T.

Lemma subst_cvt_fresh_wf_vtyp : ∀ T x C,
  wf_vtyp empty T →
  T = subst_cvt x C T.

Lemma wf_cset_in_dom : ∀ E C,
  wf_cap E C →
  cset_fvars C `subset` dom E.

Lemma map_subst_cvt_id : ∀ G Z P,
  wf_env G →
  Z `notin` dom G →
  G = map (subst_bbind Z P) G.




Lemma notin_union_split : ∀ x a1 a2,
  x `notin` (a1 `union` a2) ↔ x `notin` a1 ∧ x `notin` a2.

Properties about free variables

Lemma notin_fv_ee_opened_ee : ∀ x k s1 s2,
  x `notin` fv_ee s1 →
  x `notin` fv_ee s2 →
  x `notin` fv_ee (open_ee_rec k s2 s1)
with notin_fv_es_opened_es : ∀ x k s1 s2,
  x `notin` fv_es s1 →
  x `notin` fv_ee s2 →
  x `notin` fv_es (open_es_rec k s2 s1)
with notin_fv_eb_opened_eb : ∀ x k s1 s2,
  x `notin` fv_eb s1 →
  x `notin` fv_ee s2 →
  x `notin` fv_eb (open_eb_rec k s2 s1).

Lemma notin_fv_be_opened_be : ∀ x k s1 s2,
  x `notin` fv_be s1 →
  x `notin` fv_bb s2 →
  x `notin` fv_be (open_be_rec k s2 s1)
with notin_fv_bs_opened_bs : ∀ x k s1 s2,
  x `notin` fv_bs s1 →
  x `notin` fv_bb s2 →
  x `notin` fv_bs (open_bs_rec k s2 s1)
with notin_fv_bb_opened_bb : ∀ x k s1 s2,
  x `notin` fv_bb s1 →
  x `notin` fv_bb s2 →
  x `notin` fv_bb (open_bb_rec k s2 s1).

Lemma notin_fv_be_opened_ee : ∀ x k s1 s2,
  x `notin` fv_be s1 →
  x `notin` fv_be s2 →
  x `notin` fv_be (open_ee_rec k s2 s1)
with notin_fv_bs_opened_es : ∀ x k s1 s2,
  x `notin` fv_bs s1 →
  x `notin` fv_be s2 →
  x `notin` fv_bs (open_es_rec k s2 s1)
with notin_fv_bb_opened_eb : ∀ x k s1 s2,
  x `notin` fv_bb s1 →
  x `notin` fv_be s2 →
  x `notin` fv_bb (open_eb_rec k s2 s1).

Lemma notin_fv_ee_open_ce : ∀ x k s1 C s2,
  x `notin` fv_ee (open_ce_rec k s2 C s1) →
  x `notin` fv_ee s1
with notin_fv_es_open_cs : ∀ x k s1 C s2,
  x `notin` fv_es (open_cs_rec k s2 C s1) →
  x `notin` fv_es s1
with notin_fv_eb_open_cb : ∀ x k s1 C s2,
  x `notin` fv_eb (open_cb_rec k s2 C s1) →
  x `notin` fv_eb s1.

Lemma notin_fv_be_open_ce : ∀ x k s1 C s2,
  x `notin` fv_be (open_ce_rec k s2 C s1) →
  x `notin` fv_be s1
with notin_fv_bs_open_cs : ∀ x k s1 C s2,
  x `notin` fv_bs (open_cs_rec k s2 C s1) →
  x `notin` fv_bs s1
with notin_fv_bb_open_cb : ∀ x k s1 C s2,
  x `notin` fv_bb (open_cb_rec k s2 C s1) →
  x `notin` fv_bb s1.

Lemma notin_fv_ee_open_ee : ∀ x k s1 s2,
  x `notin` fv_ee (open_ee_rec k s2 s1) →
  x `notin` fv_ee s1
with notin_fv_es_open_es : ∀ x k s1 s2,
  x `notin` fv_es (open_es_rec k s2 s1) →
  x `notin` fv_es s1
with notin_fv_eb_open_eb : ∀ x k s1 s2,
  x `notin` fv_eb (open_eb_rec k s2 s1) →
  x `notin` fv_eb s1.

Lemma notin_fv_be_open_ee : ∀ x k s1 s2,
  x `notin` fv_be (open_ee_rec k s2 s1) →
  x `notin` fv_be s1
with notin_fv_bs_open_es : ∀ x k s1 s2,
  x `notin` fv_bs (open_es_rec k s2 s1) →
  x `notin` fv_bs s1
with notin_fv_bb_open_eb : ∀ x k s1 s2,
  x `notin` fv_bb (open_eb_rec k s2 s1) →
  x `notin` fv_bb s1.

Lemma notin_fv_be_open_be : ∀ x k s1 s2,
  x `notin` fv_be (open_be_rec k s2 s1) →
  x `notin` fv_be s1
with notin_fv_bs_open_bs : ∀ x k s1 s2,
  x `notin` fv_bs (open_bs_rec k s2 s1) →
  x `notin` fv_bs s1
with notin_fv_bb_open_bb : ∀ x k s1 s2,
  x `notin` fv_bb (open_bb_rec k s2 s1) →
  x `notin` fv_bb s1.

Lemma notin_fv_ee_open_be : ∀ x k s1 s2,
  x `notin` fv_ee (open_be_rec k s2 s1) →
  x `notin` fv_ee s1
with notin_fv_es_open_bs : ∀ x k s1 s2,
  x `notin` fv_es (open_bs_rec k s2 s1) →
  x `notin` fv_es s1
with notin_fv_eb_open_bb : ∀ x k s1 s2,
  x `notin` fv_eb (open_bb_rec k s2 s1) →
  x `notin` fv_eb s1.

Lemma notin_fv_ee_open_te : ∀ x k T s,
  x `notin` fv_ee (open_te_rec k T s) →
  x `notin` fv_ee s
with notin_fv_es_open_ts : ∀ x k T s,
  x `notin` fv_es (open_ts_rec k T s) →
  x `notin` fv_es s
with notin_fv_eb_open_tb : ∀ x k T s,
  x `notin` fv_eb (open_tb_rec k T s) →
  x `notin` fv_eb s.

Lemma notin_fv_ee_etyping : ∀ E Q e T x,
  E ; Q |-exp e ~: T →
  x `notin` dom E →
  x `notin` fv_ee e
with notin_fv_es_styping : ∀ E R Q e T x,
  E @ R ; Q |-stm e ~: T →
  x `notin` dom E →
  x `notin` fv_es e
with notin_fv_eb_btyping : ∀ E R Q e T x,
  E @ R ; Q |-blk e ~: T →
  x `notin` dom E →
  x `notin` fv_eb e.

Lemma notin_fv_be_open_te : ∀ x k T s,
  x `notin` fv_be (open_te_rec k T s) →
  x `notin` fv_be s
with notin_fv_bs_open_ts : ∀ x k T s,
  x `notin` fv_bs (open_ts_rec k T s) →
  x `notin` fv_bs s
with notin_fv_bb_open_tb : ∀ x k T s,
  x `notin` fv_bb (open_tb_rec k T s) →
  x `notin` fv_bb s.

Lemma notin_fv_be_etyping : ∀ E Q e T x,
  E ; Q |-exp e ~: T →
  x `notin` dom E →
  x `notin` fv_be e
with notin_fv_bs_styping : ∀ E R Q e T x,
  E @ R ; Q |-stm e ~: T →
  x `notin` dom E →
  x `notin` fv_bs e
with notin_fv_bb_btyping : ∀ E R Q e T x,
  E @ R ; Q |-blk e ~: T →
  x `notin` dom E →
  x `notin` fv_bb e.

Lemma notin_fv_tvt_open_cvt_rec : ∀ (Y X : atom) k T,
  X `notin` fv_tvt (open_cvt_rec k (cset_fvar Y) T) →
  X `notin` fv_tvt T
with notin_fv_tbt_open_cbt_rec : ∀ (Y X : atom) k T,
  X `notin` fv_tbt (open_cbt_rec k (cset_fvar Y) T) →
  X `notin` fv_tbt T.

Lemma notin_fv_tvt_open_tvt_rec : ∀ (Y X : atom) k T,
  X `notin` fv_tvt (open_tvt_rec k Y T) →
  X `notin` fv_tvt T
with notin_fv_tbt_open_tbt_rec : ∀ (Y X : atom) k T,
  X `notin` fv_tbt (open_tbt_rec k Y T) →
  X `notin` fv_tbt T.

Lemma notin_fv_tvt_wf : ∀ E (X : atom) T,
  wf_vtyp E T →
  X `notin` dom E →
  X `notin` fv_tvt T
with notin_fv_tbt_wf : ∀ E (X : atom) T,
  wf_btyp E T →
  X `notin` dom E →
  X `notin` fv_tbt T.

Lemma map_subst_tbind_id : ∀ G Z P,
  wf_env G →
  Z `notin` dom G →
  G = map (subst_tbind Z P) G.

Lemma wf_cap_subst_tbind : ∀ F E Z P C,
  wf_cap (F ++ [(Z, bind_typ)] ++ E) C →
  wf_vtyp E P →
  ok (F ++ E) →
  wf_cap (map (subst_tbind Z P) F ++ E) C.

Lemma wf_vtyp_subst_tbind : ∀ F E Z P T,
  wf_vtyp (F ++ [(Z, bind_typ)] ++ E) T →
  wf_vtyp E P →
  ok (F ++ E) →
  wf_vtyp (map (subst_tbind Z P) F ++ E) (subst_tvt Z P T)
with wf_btyp_subst_tbind : ∀ F E Z P T,
  wf_btyp (F ++ [(Z, bind_typ)] ++ E) T →
  wf_vtyp E P →
  ok (F ++ E) →
  wf_btyp (map (subst_tbind Z P) F ++ E) (subst_tbt Z P T).

Lemma wf_env_subst_tbind : ∀ X U E F,
  wf_env (F ++ [(X, bind_typ)] ++ E) →
  wf_vtyp E U →
  wf_env (map (subst_tbind X U) F ++ E).

Lemma wf_typ_open : ∀ E U T,
  ok E →
  wf_btyp E (typ_tfun T) →
  wf_vtyp E U →
  wf_btyp E (open_tbt T U).

Regularity of relations

Lemma etyping_regular : ∀ E Q e T,
  E ; Q |-exp e ~: T →
  wf_env E ∧ expr e ∧ wf_vtyp E T ∧ wf_sig Q
with btyping_regular : ∀ E R Q (b : blk) S,
  E @ R ; Q |-blk b ~: S →
  wf_env E ∧ block b ∧ wf_btyp E S ∧ wf_cap E R ∧ wf_sig Q
with styping_regular : ∀ E R Q s T,
  E @ R ; Q |-stm s ~: T →
  wf_env E ∧ stmt s ∧ wf_vtyp E T ∧ wf_cap E R ∧ wf_sig Q.

Lemma typing_ctx_regular : ∀ R Q c T,
  (R ; Q |-ctx c ~: T) →
  wf_cap empty R ∧ wf_sig Q.

Lemma typing_cnt_regular : ∀ C Q c S T,
  (C ; Q |-cnt c ~: S ~> T) →
  wf_cap empty C ∧ wf_sig Q.

Automation

The lemma ok_from_wf_env was already added above as a hint since it helps blur the distinction between wf_env and ok in proofs.

As currently stated, the regularity lemmas are ill-suited to be used with auto and eauto since they end in conjunctions. Even if we were, for example, to split sub_regularity into three separate lemmas, the resulting lemmas would be usable only by eauto and there is no guarantee that eauto would be able to find proofs effectively. Thus, the hints below apply the regularity lemmas and type_from_wf_typ to discharge goals about local closure and well-formedness, but in such a way as to minimize proof search.

The first hint introduces an wf_env fact into the context. It works well when combined with the lemmas relating wf_env and wf_typ. We choose to use those lemmas explicitly via (auto using ...) tactics rather than add them as hints. When used this way, the explicitness makes the proof more informative rather than more cluttered (with useless details).

The other three hints try outright to solve their respective goals.

Extra Lemmas using automation concerning plug

Lemma notin_fv_es_plug : ∀ k e R C T1 T2 x,
  R ; C |-cnt k ~: T1 ~> T2 →
  x `notin` fv_ee e →
  x `notin` fv_es (plug k e).

Lemma notin_fv_bs_plug : ∀ k e R C T1 T2 x,
  R ; C |-cnt k ~: T1 ~> T2 →
  x `notin` fv_be e →
  x `notin` fv_bs (plug k e).