Qcert.NRAEnv.Typing.TcNRAEnvEq

Section TcNRAEnvEq.

  Definition typed_cnraenv {m:basic_model} τc τenv τin τout := {op:cnraenv |op ▷ τin >=> τ out ⊣ τ c ;τ env }.

  Definition tcnraenv_eq {m:basic_model} {τc τenv τin τout} (op1 op2:typed_cnraenv τ c τ env τin τ out) : Prop :=
    ∀ (x:data) c (env: data)
           (dt_x:x ▹ τin)
           (dt_c:bindings_type c τ c)
           (dt_env:env ▹ τ env),
        brand_relation_brands ⊢ₑ (proj1_sig op1 ) @ₑ x ⊣ c ;env
        = brand_relation_brands ⊢ₑ (proj1_sig op2 ) @ₑ x ⊣ c ;env.

  Global Instance tcnraenv_equiv {m:basic_model} {τc} {τenv τin τout:rtype} : Equivalence (@tcnraenv_eq m τ c τ env τin τ out).

  Notation "t1 ⇝ₑ t2 ⊣ τc ; tenv" := (typed_cnraenv τc tenv t1 t2) (at level 80).
  Notation "X ≡τₑ Y" := (tcnraenv_eq X Y) (at level 80).

  Lemma cnraenv_eq_impl_tcnraenv_eq {m:basic_model} {τc τenv τin τout} (op1 op2: τin ⇝ₑ τ out ⊣ τ c ;τ env) :
    `op1 ≡ₑ `op2 → op1 ≡τₑ op2.

  Lemma cnraenv_eq_pf_irrel {m:basic_model} {op} {τin τout τc τenv} (pf1 pf2: op ▷ τin >=> τ out ⊣ τ c ;τ env) :
    tcnraenv_eq (exist _ op pf1) (exist _ op pf2).

  Context {m:basic_model}.

  Definition tcnraenv_rewrites_to (op1 op2:cnraenv) : Prop :=
    ∀ τc (τenv τin τout:rtype),
      op1 ▷ τin >=> τ out ⊣ τ c ;τ env →
                              (op2 ▷ τin >=> τ out ⊣ τ c ;τ env )
                              ∧ (∀ (x:data) c
                                         env
                                         (dt_x:x ▹ τin)
                                         (dt_c:bindings_type c τ c)
                                         (dt_env:env ▹ τ env),
                                    brand_relation_brands ⊢ₑ op1 @ₑ x ⊣ c ;env
                                 = brand_relation_brands ⊢ₑ op2 @ₑ x ⊣ c ;env ).

  Notation "op1 ⇒ op2" := (@tcnraenv_rewrites_to op1 op2) (at level 80).

  Lemma rewrites_typed_with_untyped (op1 op2:cnraenv) :
    op1 ≡ₑ op2 →
    (∀ {τc} {τenv τin τout:rtype}, op1 ▷ τin >=> τ out ⊣ τ c ;τ env → op2 ▷ τin >=> τ out ⊣ τ c ;τ env )
    → op1 ⇒ op2.

  Lemma talg_rewrites_eq_is_typed_eq {τc} {τenv τin τout:rtype} (op1 op2:typed_cnraenv τ c τ env τin τ out):
    (`op1 ⇒ `op2 ) → @tcnraenv_eq m τ c τ env τin τ out op1 op2.

  Global Instance tcnraenv_rewrites_to_pre : PreOrder tcnraenv_rewrites_to.

  Global Instance anid_tproper:
    Proper tcnraenv_rewrites_to ANID.

  Global Instance anconst_tproper:
    Proper (eq ==> tcnraenv_rewrites_to) ANConst.

  Global Instance anbinop_tproper:
    Proper (eq ==> tcnraenv_rewrites_to
               ==> tcnraenv_rewrites_to
               ==> tcnraenv_rewrites_to) ANBinop.

  Global Instance anunop_tproper :
    Proper (eq ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANUnop.

  Global Instance anmap_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANMap.

  Global Instance anmapconcat_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANMapConcat.

  Global Instance anproduct_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANProduct.

  Global Instance anselect_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANSelect.

  Global Instance andefault_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANDefault.

  Global Instance aneither_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANEither.

  Global Instance aneitherconcat_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANEitherConcat.

  Global Instance anapp_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANApp.

  Global Instance anenv_tproper:
    Proper tcnraenv_rewrites_to ANEnv.

  Global Instance anappenv_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANAppEnv.

  Global Instance anmapenv_tproper :
    Proper (tcnraenv_rewrites_to ==> tcnraenv_rewrites_to) ANMapEnv.

End TcNRAEnvEq.

Notation "op1 ⇒ op2" := (tcnraenv_rewrites_to op1 op2) (at level 80) : cnraenv_scope.
Notation "h ⊧ t1 ⇝ t2 ⊣ c ; tenv" := (@typed_cnraenv h c tenv t1 t2) (at level 80) : cnraenv_scope.
Notation "X ≡τ Y" := (tcnraenv_eq X Y) (at level 80) : cnraenv_scope. Notation "X ≡τ' Y" := (tcnraenv_eq (exist _ _ X) (exist _ _ Y)) (at level 80) : cnraenv_scope.