Qcert.NRAEnv.Lang.NRAEnvEq

Section NRAEnvEq.




  Context {fruntime:foreign_runtime}.

  Definition nraenv_eq (op1 op2:nraenv) : Prop :=
    ∀ (h:list(string×string))
           (c:list (string×data))
           (dn_c: Forall (fun d : string × data ⇒ data_normalized h (snd d)) c)
           (env:data)
           (dn_env:data_normalized h env)
           (x:data)
           (dn_x:data_normalized h x),
        nraenv_eval h c op1 env x = nraenv_eval h c op2 env x.


  Global Instance nraenv_equiv : Equivalence nraenv_eq.

  Definition nraenv_eq_cnraenv_eq (op1 op2:nraenv) : nraenv_eq op1 op2 ↔ cnraenv_eq (cnraenv_of_nraenv op1) (cnraenv_of_nraenv op2).

  Notation "X ≡ₓ Y" := (nraenv_eq X Y) (at level 90) : nraenv_scope.

  Section eq_lift.

    Lemma lift_cnraenv_eq_to_nraenv_eq_r (q1 q2:cnraenv) :
      q1 ≡ₑ q2 → (nraenv_of_cnraenv q1) ≡ₓ (nraenv_of_cnraenv q2).

    Lemma lift_cnraenv_eq_to_nraenv_eq_l (q1 q2:cnraenv) :
      (nraenv_of_cnraenv q1) ≡ₓ (nraenv_of_cnraenv q2) → q1 ≡ₑ q2.

    Lemma lift_cnraenv_eq_to_nraenv_eq (q1 q2:cnraenv) :
      q1 ≡ₑ q2 ↔ (nraenv_of_cnraenv q1) ≡ₓ (nraenv_of_cnraenv q2).

    Lemma lift_nraenv_eq_to_cnraenv_eq_r (q1 q2:nraenv) :
      q1 ≡ₓ q2 → (cnraenv_of_nraenv q1) ≡ₑ (cnraenv_of_nraenv q2).

    Lemma lift_nraenv_eq_to_cnraenv_eq_l (q1 q2:nraenv) :
      (cnraenv_of_nraenv q1) ≡ₑ (cnraenv_of_nraenv q2) → q1 ≡ₓ q2.

    Lemma lift_nraenv_eq_to_cnraenv_eq (q1 q2:nraenv) :
      q1 ≡ₓ q2 ↔ (cnraenv_of_nraenv q1) ≡ₑ (cnraenv_of_nraenv q2).
  End eq_lift.


  Global Instance nraenv_id_proper : Proper nraenv_eq NRAEnvID.

  Global Instance nraenv_const_proper : Proper (eq ==> nraenv_eq) NRAEnvConst.


  Global Instance nraenv_binop_proper : Proper (binop_eq ==> nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvBinop.

  Global Instance nraenv_unop_proper : Proper (unaryop_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvUnop.

  Global Instance nraenv_map_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvMap.

  Global Instance nraenv_mapconcat_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvMapConcat.

  Global Instance nraenv_product_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvProduct.

  Global Instance nraenv_select_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvSelect.

  Global Instance nraenv_either_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvEither.

  Global Instance nraenv_eitherconcat_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvEitherConcat.

  Global Instance nraenv_default_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvDefault.

  Global Instance nraenv_app_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvApp.

  Global Instance nraenv_getconstant_proper s : Proper nraenv_eq (NRAEnvGetConstant s).

  Global Instance nraenv_env_proper : Proper nraenv_eq NRAEnvEnv.

  Global Instance nraenv_appenv_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvAppEnv.

  Global Instance nraenv_mapenv_proper : Proper (nraenv_eq ==> nraenv_eq) NRAEnvMapEnv.

  Global Instance nraenv_flatmap_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvFlatMap.

  Global Instance nraenv_join_proper : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvJoin.

  Global Instance nraenv_project_proper : Proper (eq ==> nraenv_eq ==> nraenv_eq) NRAEnvProject.

  Global Instance nraenv_group_by_proper : Proper (eq ==> eq ==> nraenv_eq ==> nraenv_eq) NRAEnvGroupBy.

  Global Instance nraenv_unnest_proper : Proper (eq ==> eq ==> nraenv_eq ==> nraenv_eq) NRAEnvUnnest.

End NRAEnvEq.

Notation "X ≡ₓ Y" := (nraenv_eq X Y) (at level 90) : nraenv_scope.