Module Qcert.NRAEnv.Lang.NRAEnvEq


Section NRAEnvEq.
  Require Import String.
  Require Import List.
  Require Import Compare_dec.
  Require Import Utils.
  Require Import CommonRuntime.
  Require Import cNRAEnv.
  Require Import cNRAEnvEq.
  Require Import NRAEnv.


  Local Open Scope nraenv_core_scope.
  Local Open Scope nraenv_scope.

  Context {fruntime:foreign_runtime}.

  Definition nraenv_eq (op1 op2:nraenv) : Prop :=
    forall (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.

  Require Import Equivalence.
  Require Import Morphisms.
  Require Import Setoid.
  Require Import EquivDec.
  Require Import Program.

  Global Instance nraenv_equiv : Equivalence nraenv_eq.
Proof.
    constructor.
    - unfold Reflexive, nraenv_eq.
      intros; reflexivity.
    - unfold Symmetric, nraenv_eq.
      intros. rewrite (H h c dn_c env dn_env x0) by trivial; reflexivity.
    - unfold Transitive, nraenv_eq.
      intros. rewrite (H h c dn_c env dn_env x0) by trivial; rewrite (H0 h c dn_c env dn_env x0) by trivial; reflexivity.
  Qed.

  Definition nraenv_eq_nraenv_core_eq (op1 op2:nraenv) : nraenv_eq op1 op2 <-> nraenv_core_eq (nraenv_to_nraenv_core op1) (nraenv_to_nraenv_core op2).
Proof.
    split; intro; assumption.
  Qed.

  Notation "X ≡ₓ Y" := (nraenv_eq X Y) (at level 90) : nraenv_scope.
Thanks to shallow semantics, lifting between nraenv_core and nraenv is easy
  Section eq_lift.
    Require Import cNRAEnv cNRAEnvEq.
    Open Scope nraenv_core_scope.

    Lemma lift_nraenv_core_eq_to_nraenv_eq_r (q1 q2:nraenv_core) :
      q1 ≡ₑ q2 -> (nraenv_core_to_nraenv q1) ≡ₓ (nraenv_core_to_nraenv q2).
Proof.
      unfold nraenv_eq.
      unfold nraenv_core_eq.
      intros.
      unfold nraenv_eval in *.
      rewrite nraenv_roundtrip.
      rewrite nraenv_roundtrip.
      auto.
    Qed.

    Lemma lift_nraenv_core_eq_to_nraenv_eq_l (q1 q2:nraenv_core) :
      (nraenv_core_to_nraenv q1) ≡ₓ (nraenv_core_to_nraenv q2) -> q1 ≡ₑ q2.
Proof.
      unfold nraenv_eq.
      unfold nraenv_core_eq.
      intros.
      unfold nraenv_eval in *.
      rewrite nraenv_roundtrip in H.
      rewrite nraenv_roundtrip in H.
      specialize (H _ _ dn_c _ dn_env _ dn_x); intros.
      assumption.
    Qed.

    Lemma lift_nraenv_core_eq_to_nraenv_eq (q1 q2:nraenv_core) :
      q1 ≡ₑ q2 <-> (nraenv_core_to_nraenv q1) ≡ₓ (nraenv_core_to_nraenv q2).
Proof.
      split.
      apply lift_nraenv_core_eq_to_nraenv_eq_r.
      apply lift_nraenv_core_eq_to_nraenv_eq_l.
    Qed.

    Lemma lift_nraenv_eq_to_nraenv_core_eq_r (q1 q2:nraenv) :
      q1 ≡ₓ q2 -> (nraenv_to_nraenv_core q1) ≡ₑ (nraenv_to_nraenv_core q2).
Proof.
      unfold nraenv_eq.
      unfold nraenv_core_eq.
      intros.
      unfold nraenv_eval in *.
      specialize (H _ _ dn_c _ dn_env _ dn_x); intros.
      assumption.
    Qed.
  
    Lemma lift_nraenv_eq_to_nraenv_core_eq_l (q1 q2:nraenv) :
      (nraenv_to_nraenv_core q1) ≡ₑ (nraenv_to_nraenv_core q2) -> q1 ≡ₓ q2.
Proof.
      unfold nraenv_eq.
      unfold nraenv_core_eq.
      intros.
      unfold nraenv_eval in *.
      specialize (H _ _ dn_c _ dn_env _ dn_x); intros.
      assumption.
    Qed.
  
    Lemma lift_nraenv_eq_to_nraenv_core_eq (q1 q2:nraenv) :
      q1 ≡ₓ q2 <-> (nraenv_to_nraenv_core q1) ≡ₑ (nraenv_to_nraenv_core q2).
Proof.
      split.
      apply lift_nraenv_eq_to_nraenv_core_eq_r.
      apply lift_nraenv_eq_to_nraenv_core_eq_l.
    Qed.
  End eq_lift.
  

  Global Instance proper_NRAEnvGetConstant s : Proper nraenv_eq (NRAEnvGetConstant s).
Proof.
    unfold Proper, respectful, nraenv_eq.
    apply proper_cNRAEnvGetConstant; assumption.
  Qed.
  
  Global Instance proper_NRAEnvID : Proper nraenv_eq NRAEnvID.
Proof.
    unfold Proper, respectful, nraenv_eq.
    apply proper_cNRAEnvID; assumption.
  Qed.

  Global Instance proper_NRAEnvConst : Proper (eq ==> nraenv_eq) NRAEnvConst.
Proof.
    unfold Proper, respectful, nraenv_eq; intros.
    apply proper_cNRAEnvConst; assumption.
  Qed.

  Global Instance proper_NRAEnvBinop : Proper (binary_op_eq ==> nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvBinop.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvBinop; assumption.
  Qed.

  Global Instance proper_NRAEnvUnop : Proper (unary_op_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvUnop.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvUnop; assumption.
  Qed.

  Global Instance proper_NRAEnvMap : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvMap.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvMap; assumption.
  Qed.

  Global Instance proper_NRAEnvMapProduct : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvMapProduct.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvMapProduct; assumption.
  Qed.

  Global Instance proper_NRAEnvProduct : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvProduct.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvProduct; assumption.
  Qed.

  Global Instance proper_NRAEnvSelect : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvSelect.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvSelect; assumption.
  Qed.

  Global Instance proper_NRAEnvEither : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvEither.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros; simpl.
    destruct x1; simpl; trivial; inversion dn_x; subst; eauto.
  Qed.

  Global Instance proper_NRAEnvEitherConcat : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvEitherConcat.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros; simpl.
    rewrite (H0 h c dn_c env dn_env x1) by trivial; rewrite (H h c dn_c env dn_env x1) by trivial.
    case_eq (h ⊢ₑ nraenv_to_nraenv_core y0 @ₑ x1c;env); case_eq (h ⊢ₑ nraenv_to_nraenv_core y @ₑ x1c;env); intros; simpl; trivial.
  Qed.
  
  Global Instance proper_NRAEnvDefault : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvDefault.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvDefault; assumption.
  Qed.

  Global Instance proper_NRAEnvApp : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvApp.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvApp; assumption.
  Qed.

  Global Instance proper_NRAEnvEnv : Proper nraenv_eq NRAEnvEnv.
Proof.
    unfold Proper, respectful, nraenv_eq.
    apply proper_cNRAEnvEnv; assumption.
  Qed.

  Global Instance proper_NRAEnvAppEnv : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvAppEnv.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvAppEnv; assumption.
  Qed.

  Global Instance proper_NRAEnvMapEnv : Proper (nraenv_eq ==> nraenv_eq) NRAEnvMapEnv.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvMapEnv; assumption.
  Qed.

  Global Instance proper_NRAEnvFlatMap : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvFlatMap.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvUnop; try assumption; try reflexivity.
    apply proper_cNRAEnvMap; assumption.
  Qed.

  Global Instance proper_NRAEnvJoin : Proper (nraenv_eq ==> nraenv_eq ==> nraenv_eq ==> nraenv_eq) NRAEnvJoin.
Proof.
    unfold Proper, respectful, nraenv_eq, nraenv_eval; intros.
    apply proper_cNRAEnvSelect; try assumption.
    apply proper_cNRAEnvProduct; assumption.
  Qed.

  Global Instance proper_NRAEnvProject : Proper (eq ==> nraenv_eq ==> nraenv_eq) NRAEnvProject.
Proof.
    unfold Proper, respectful.
    intros; subst.
    rewrite nraenv_eq_nraenv_core_eq in *.
    simpl.
    unfold macro_cNRAEnvProject.
    rewrite H0 by trivial.
    reflexivity.
  Qed.

  Global Instance proper_NRAEnvGroupBy : Proper (eq ==> eq ==> nraenv_eq ==> nraenv_eq) NRAEnvGroupBy.
Proof.
    unfold Proper, respectful.
    intros; subst.
    rewrite nraenv_eq_nraenv_core_eq in *.
    simpl. unfold macro_cNRAEnvGroupBy.
    rewrite H1 by trivial.
    reflexivity.
  Qed.

  Global Instance proper_NRAEnvUnnest : Proper (eq ==> eq ==> nraenv_eq ==> nraenv_eq) NRAEnvUnnest.
Proof.
    unfold Proper, respectful.
    intros; subst.
    rewrite nraenv_eq_nraenv_core_eq in *.
    simpl. unfold macro_cNRAEnvUnnest.
    rewrite H1 by trivial.
    reflexivity.
  Qed.

End NRAEnvEq.

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