Qcert.NRAEnv.Typing.TNRAEnvEq

Section TNRAEnvEq.

  Definition typed_nraenv {m:basic_model} τc τenv τin τout := {op:nraenv |op ▷ₓ τin >=> τ out ⊣ τ c ;τ env }.

  Definition tnraenv_eq {m:basic_model} {τc τenv τin τout} (op1 op2:typed_nraenv τ 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 tnraenv_equiv {m:basic_model} {τc} {τenv τin τout:rtype} : Equivalence (@tnraenv_eq m τ c τ env τin τ out).

  Notation "t1 ⇝ₓ t2 ⊣ τc ; tenv" := (typed_nraenv τc tenv t1 t2) (at level 80).
  Notation "X ≡τₓ Y" := (tnraenv_eq X Y) (at level 80).

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

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

  Context {m:basic_model}.

  Definition tnraenv_rewrites_to (op1 op2:nraenv) : 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" := (@tnraenv_rewrites_to op1 op2) (at level 80).

  Lemma rewrites_typed_with_untyped (op1 op2:nraenv) :
    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_nraenv τ c τ env τin τ out):
    (`op1 ⇒ₓ `op2 ) → @tnraenv_eq m τ c τ env τin τ out op1 op2.

Thanks to shallow semantics, lifting between cnraenv and nraenv is easy

  Section eq_lift.

    Lemma lift_tcnraenv_eq_to_tnraenv_eq_r (q1 q2:cnraenv) :
      q1 ⇒ q2 → (nraenv_of_cnraenv q1 ) ⇒ₓ (nraenv_of_cnraenv q2 ).

    Lemma lift_tcnraenv_eq_to_tnraenv_eq_l (q1 q2:cnraenv) :
      (nraenv_of_cnraenv q1 ) ⇒ₓ (nraenv_of_cnraenv q2 ) → q1 ⇒ q2.

    Lemma lift_tcnraenv_eq_to_tnraenv_eq (q1 q2:cnraenv) :
      q1 ⇒ q2 ↔ (nraenv_of_cnraenv q1 ) ⇒ₓ (nraenv_of_cnraenv q2 ).

    Lemma lift_tnraenv_eq_to_tcnraenv_eq_r (q1 q2:nraenv) :
      q1 ⇒ₓ q2 → (cnraenv_of_nraenv q1 ) ⇒ (cnraenv_of_nraenv q2 ).

    Lemma lift_tnraenv_eq_to_tcnraenv_eq_l (q1 q2:nraenv) :
      (cnraenv_of_nraenv q1 ) ⇒ (cnraenv_of_nraenv q2 ) → q1 ⇒ₓ q2.

    Lemma lift_tnraenv_eq_to_tcnraenv_eq (q1 q2:nraenv) :
      q1 ⇒ₓ q2 ↔ (cnraenv_of_nraenv q1 ) ⇒ (cnraenv_of_nraenv q2 ).
  End eq_lift.

  Global Instance tnraenv_rewrites_to_pre : PreOrder tnraenv_rewrites_to.

  Global Instance nraenv_id_tproper:
    Proper tnraenv_rewrites_to NRAEnvID.

  Global Instance nraenv_const_tproper:
    Proper (eq ==> tnraenv_rewrites_to) NRAEnvConst.

  Global Instance nraenv_binop_tproper:
    Proper (eq ==> tnraenv_rewrites_to
               ==> tnraenv_rewrites_to
               ==> tnraenv_rewrites_to) NRAEnvBinop.

  Global Instance nraenv_unop_tproper :
    Proper (eq ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvUnop.

  Global Instance nraenv_map_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvMap.

  Global Instance nraenv_mapconcat_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvMapConcat.

  Global Instance nraenv_product_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvProduct.

  Global Instance nraenv_select_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvSelect.

  Global Instance nraenv_default_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvDefault.

  Global Instance nraenv_either_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvEither.

  Global Instance nraenv_eitherconcat_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvEitherConcat.

  Global Instance nraenv_app_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvApp.

  Global Instance nraenv_env_tproper:
    Proper tnraenv_rewrites_to NRAEnvEnv.

  Global Instance nraenv_appenv_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvAppEnv.

  Global Instance nraenv_mapenv_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvMapEnv.

  Global Instance nraenv_flatmap_tproper :
    Proper (tnraenv_rewrites_to ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvFlatMap.

  Global Instance nraenv_join_tproper :
    Proper (tnraenv_rewrites_to
              ==> tnraenv_rewrites_to
              ==> tnraenv_rewrites_to
              ==> tnraenv_rewrites_to) NRAEnvJoin.

  Global Instance nraenv_project_tproper :
    Proper (eq ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvProject.

  Global Instance nraenv_group_by_tproper :
    Proper (eq ==> eq ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvGroupBy.

  Global Instance nraenv_unnest_tproper :
    Proper (eq ==> eq ==> tnraenv_rewrites_to ==> tnraenv_rewrites_to) NRAEnvUnnest.

End TNRAEnvEq.

Notation "op1 ⇒ₓ op2" := (tnraenv_rewrites_to op1 op2) (at level 80) : nraenv_scope.
Notation "h ⊧ t1 ⇝ₓ t2 ⊣ c ; tenv" := (@typed_nraenv h c tenv t1 t2) (at level 80) : nraenv_scope.
Notation "X ≡τₓ Y" := (tnraenv_eq X Y) (at level 80) : nraenv_scope. Notation "X ≡τ'ₓ Y" := (tnraenv_eq (exist _ _ X) (exist _ _ Y)) (at level 80) : nraenv_scope.