Qcert.NRA.Lang.NRAExtEq

Section NRAExt.

  Context {fruntime:foreign_runtime}.

  Definition nraext_eq (op1 op2:nraext) : Prop :=
    ∀ h:list(string ×string),
    ∀ x:data,
      data_normalized h x →
      h ⊢ op1 @ₓ x = h ⊢ op2 @ₓ x.

  Global Instance nraext_equiv : Equivalence nraext_eq.

  Definition nraext_eq_nra_eq (op1 op2:nraext) : nraext_eq op1 op2 ↔ nra_eq (nra_of_nraext op1) (nra_of_nraext op2).

  Global Instance eaid_proper : Proper nraext_eq AXID.

  Global Instance eaconst_proper : Proper (eq ==> nraext_eq) AXConst.

  Global Instance eabinop_proper : Proper (binop_eq ==> nraext_eq ==> nraext_eq ==> nraext_eq) AXBinop.

  Global Instance eaunop_proper : Proper (unaryop_eq ==> nraext_eq ==> nraext_eq) AXUnop.

  Global Instance eamap_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq) AXMap.

  Global Instance eamapconcat_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq) AXMapConcat.

  Global Instance eaproduct_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq) AXProduct.

  Global Instance easelect_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq) AXSelect.

  Global Instance eaeither_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq) AXEither.

  Global Instance eaeitherconcat_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq) AXEitherConcat.

  Global Instance eadefault_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq) AXDefault.

  Global Instance eaapp_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq) AXApp.

  Global Instance eajoin_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq ==> nraext_eq) AXJoin.

  Global Instance easemi_join_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq ==> nraext_eq) AXSemiJoin.

  Global Instance eaanti_join_proper : Proper (nraext_eq ==> nraext_eq ==> nraext_eq ==> nraext_eq) AXAntiJoin.

  Global Instance eamap_to_rec_proper : Proper (eq ==> nraext_eq ==> nraext_eq) AXMapToRec.

  Global Instance eamap_add_rec_proper : Proper (eq ==> nraext_eq ==> nraext_eq ==> nraext_eq) AXMapAddRec.

  Global Instance rproject_proper : Proper (eq ==> nra_eq ==> nra_eq) rproject.

  Global Instance earproject_proper : Proper (eq ==> nraext_eq ==> nraext_eq) AXRProject.

  Global Instance project_proper : Proper (eq ==> nra_eq ==> nra_eq) project.

  Global Instance eaproject_proper : Proper (eq ==> nraext_eq ==> nraext_eq) AXProject.

  Global Instance eaproject_remove_proper : Proper (eq ==> nraext_eq ==> nraext_eq) AXProjectRemove.

  Global Instance eamap_rename_rec_proper : Proper (eq ==> eq ==> nraext_eq ==> nraext_eq) AXMapRename.

  Global Instance eaunnest_one_proper : Proper (eq ==> nraext_eq ==> nraext_eq) AXUnnestOne.

  Global Instance eaunnest_two_proper : Proper (eq ==> eq ==> nraext_eq ==> nraext_eq) AXUnnestTwo.

  Global Instance group1_proper : Proper (eq ==> eq ==> nra_eq ==> nra_eq) group1.

  Global Instance eagroupby_proper : Proper (eq ==> eq ==> nraext_eq ==> nraext_eq) AXGroupBy.

End NRAExt.

Notation "X ≡ₓ Y" := (nraext_eq X Y) (at level 90) : nraext_scope.