Module cNNRCEq

Section cNNRCEq.

  Require Import Equivalence.
  Require Import Morphisms.
  Require Import Setoid.
  Require Import EquivDec.
  Require Import Program.
  Require Import String.
  Require Import List.
  Require Import Arith.

  Require Import Utils BasicRuntime.
  Require Import cNNRC cNNRCNorm.

  Context {fruntime:foreign_runtime}.

Equivalence between expressions in the Named Nested Relational Calculus

Semantics of NNRC

  Definition nnrc_eq (e1 e2:nnrc) : Prop :=
    forall (h:brand_relation_t),
    forall (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.

Proof.

    constructor.
    - unfold Reflexive, nnrc_eq.
      intros; reflexivity.
    - unfold Symmetric, nnrc_eq.
      intros; rewrite (H h env) by trivial; reflexivity.
    - unfold Transitive, nnrc_eq.
      intros; rewrite (H h env) by trivial;
      rewrite (H0 h env) by trivial; reflexivity.
  Qed.

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

Proof.

    unfold Proper, respectful, nnrc_eq.
    intros; rewrite H; reflexivity.
  Qed.

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

Proof.

    unfold Proper, respectful, nnrc_eq.
    intros; rewrite H; reflexivity.
  Qed.

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

Proof.

    unfold Proper, respectful, nnrc_eq.
    intros; simpl; rewrite H0 by trivial; rewrite H1 by trivial; clear H0 H1.
    case_eq (nnrc_core_eval h env y0); case_eq (nnrc_core_eval h env y1); intros; simpl; trivial.
    rewrite (H h); eauto.
  Qed.

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

Proof.

    unfold Proper, respectful, nnrc_eq.
    intros; simpl; rewrite H0 by trivial; clear H0.
    case_eq (nnrc_core_eval h env y0); simpl; trivial; intros.
    rewrite (H h); eauto.
  Qed.

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

Proof.

    unfold Proper, respectful, nnrc_eq.
    intros; simpl. rewrite H0 by trivial; clear H0.
    case_eq (nnrc_core_eval h env y0); simpl; trivial; intros.
    rewrite H; clear H.
    rewrite H1; eauto.
    constructor; eauto.
  Qed.

    Hint Resolve data_normalized_dcoll_in.

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

Proof.

    unfold Proper, respectful, nnrc_eq.
    intros; simpl. rewrite H0 by trivial; clear H0. subst.
    case_eq (nnrc_core_eval h env y0); simpl; trivial; intros.
    destruct d; try reflexivity; simpl.
    f_equal.
    apply rmap_ext; intros.
    apply H1; simpl; eauto.
  Qed.

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

Proof.

    unfold Proper, respectful, nnrc_eq.
    intros; simpl. rewrite H by trivial; clear H.
    case_eq (nnrc_core_eval h env y); simpl; trivial; intros.
    destruct d; try reflexivity; simpl.
    destruct b; eauto.
  Qed.

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

Proof.

    unfold Proper, respectful, nnrc_eq.
    intros; simpl. subst.
    rewrite H by trivial.
    match_case; intros ? eqq1. match_destr.
    - assert (dn:data_normalized h (dleft d)) by eauto.
      inversion dn; subst.
      apply H1; simpl; eauto.
    - assert (dn:data_normalized h (dright d)) by eauto.
      inversion dn; subst.
      apply H3; simpl; eauto.
  Qed.

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

Proof.

    unfold Proper, respectful, nnrc_eq.
    intros; reflexivity.
  Qed.

End cNNRCEq.

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