Qcert.NNRC.Lang.NNRCEq

Section NNRCEq.

Context {fruntime:foreign_runtime}.

Equivalence between expressions in the Named Nested Relational Calculus

Semantics of NNRC

  Definition nnrc_ext_eq (e1 e2:nnrc) : Prop :=
    ∀ (h:brand_relation_t),
    ∀ (env:bindings),
      Forall (data_normalized h) (map snd env) →
      @nnrc_ext_eval _ h env e1 = @nnrc_ext_eval _ h env e2.

  Global Instance nnrc_ext_equiv : Equivalence nnrc_ext_eq.

  Global Instance var_ext_proper : Proper (eq ==> nnrc_ext_eq) NNRCVar.

  Global Instance const_ext_proper : Proper (eq ==> nnrc_ext_eq) NNRCConst.

  Global Instance binop_ext_proper : Proper (binop_eq ==> nnrc_ext_eq ==> nnrc_ext_eq ==> nnrc_ext_eq) NNRCBinop.

  Global Instance unop_ext_proper : Proper (unaryop_eq ==> nnrc_ext_eq ==> nnrc_ext_eq) NNRCUnop.

  Global Instance let_ext_proper : Proper (eq ==> nnrc_ext_eq ==> nnrc_ext_eq ==> nnrc_ext_eq) NNRCLet.

  Global Instance for_ext_proper : Proper (eq ==> nnrc_ext_eq ==> nnrc_ext_eq ==> nnrc_ext_eq) NNRCFor.

  Global Instance if_ext_proper : Proper (nnrc_ext_eq ==> nnrc_ext_eq ==> nnrc_ext_eq ==> nnrc_ext_eq) NNRCIf.

  Global Instance either_ext_proper : Proper (nnrc_ext_eq ==> eq ==> nnrc_ext_eq ==> eq ==> nnrc_ext_eq ==> nnrc_ext_eq) NNRCEither.

  Global Instance group_by_ext_proper : Proper (eq ==> eq ==> nnrc_ext_eq ==> nnrc_ext_eq) NNRCGroupBy.

End NNRCEq.

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