Qcert.Translation.TcNRAEnvtocNNRC

Section TcNRAEnvtocNNRC.

Type preservation for the translation from NRA to NNRC

  Context {m:basic_model}.
  Theorem tnraenv_sem_correct {τcenv} {τin τenv τout} (op:cnraenv) (tenv:tbindings) (vid venv:var) :
    prefix CONST_PREFIX vid = false →
    prefix CONST_PREFIX venv = false →
    (∀ x,
        assoc_lookupr equiv_dec (mkConstants τ cenv) x
        = lookup equiv_dec (filterConstants tenv) x ) →
    lookup equiv_dec tenv vid = Some τin →
    lookup equiv_dec tenv venv = Some τ env →
    (op ▷ τin >=> τ out ⊣ τ cenv ;τ env ) →
    nnrc_type tenv (cnraenv_to_nnrc op vid venv) τ out.

Reverse direction, main theorem

  Theorem tnraenv_sem_correct_back {τcenv} {τin τenv τout} (op:cnraenv) (tenv:tbindings) (vid venv:var) :
    prefix CONST_PREFIX vid = false →
    prefix CONST_PREFIX venv = false →
    (∀ x,
        assoc_lookupr equiv_dec (mkConstants τ cenv) x
        = lookup equiv_dec (filterConstants tenv) x ) →
    lookup equiv_dec tenv vid = Some τin →
    lookup equiv_dec tenv venv = Some τ env →
    nnrc_type tenv (cnraenv_to_nnrc op vid venv) τ out →
    (op ▷ τin >=> τ out ⊣ τ cenv ;τ env ).

Theorem 7.4: NRA<->NNRC. Final iff Theorem of type preservation for the translation from NRA to NNRC

  Theorem tnraenv_sem_correct_iff {τcenv} {τin τenv τout} (op:cnraenv) (tenv:tbindings) (vid venv:var) :
    prefix CONST_PREFIX vid = false →
    prefix CONST_PREFIX venv = false →
    (∀ x,
        assoc_lookupr equiv_dec (mkConstants τ cenv) x
        = lookup equiv_dec (filterConstants tenv) x ) →
    lookup equiv_dec tenv vid = Some τin →
    lookup equiv_dec tenv venv = Some τ env →
    nnrc_type tenv (cnraenv_to_nnrc op vid venv) τ out →
    (op ▷ τin >=> τ out ⊣ τ cenv ;τ env ).

End TcNRAEnvtocNNRC.