Qcert.NNRC.Core.cNNRCEq

Section cNNRCEq.

Context {fruntime:foreign_runtime}.

Equivalence between expressions in the Named Nested Relational Calculus

Semantics of NNRC

  Definition nnrc_eq (e1 e2:nnrc) : Prop :=
    ∀ (h:brand_relation_t),
    ∀ (env:bindings),
      Forall (data_normalized h) (map snd env) →
      nnrc_core_eval h env e1 = nnrc_core_eval h env e2.

  Global Instance nnrc_equiv : Equivalence nnrc_eq.

  Global Instance var_proper : Proper (eq ==> nnrc_eq) NNRCVar.

  Global Instance const_proper : Proper (eq ==> nnrc_eq) NNRCConst.

  Global Instance binop_proper : Proper (binop_eq ==> nnrc_eq ==> nnrc_eq ==> nnrc_eq) NNRCBinop.

  Global Instance unop_proper : Proper (unaryop_eq ==> nnrc_eq ==> nnrc_eq) NNRCUnop.

  Global Instance let_proper : Proper (eq ==> nnrc_eq ==> nnrc_eq ==> nnrc_eq) NNRCLet.

  Global Instance for_proper : Proper (eq ==> nnrc_eq ==> nnrc_eq ==> nnrc_eq) NNRCFor.

  Global Instance if_proper : Proper (nnrc_eq ==> nnrc_eq ==> nnrc_eq ==> nnrc_eq) NNRCIf.

  Global Instance either_proper : Proper (nnrc_eq ==> eq ==> nnrc_eq ==> eq ==> nnrc_eq ==> nnrc_eq) NNRCEither.

  Global Instance group_by_proper : Proper (eq ==> eq ==> nnrc_eq ==> nnrc_eq) NNRCGroupBy.

End cNNRCEq.

Notation "X ≡ᶜᶜ Y" := (nnrc_eq X Y) (at level 90) : nnrc_scope.