Module NRAEq

Section NRAEq.

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

  Require Import List.
  Require Import String.

  Require Import Utils BasicRuntime.
  Require Import NRA.

  Local Open Scope nra_scope.

  Context {fruntime:foreign_runtime}.


  Definition nra_eq (op1 op2:nra) : Prop :=
    forall
      (h:list(string*string))
      (c:list (string*data))
      (dn_c:Forall (fun d => data_normalized h (snd d)) c)
      (x:data)
      (dn_x:data_normalized h x),
      h ⊢ op1 @ₐ x ⊣ c = h ⊢ op2 @ₐ x ⊣ c.

  Global Instance nra_equiv : Equivalence nra_eq.

Proof.

    constructor.
    - unfold Reflexive, nra_eq.
      intros; reflexivity.
    - unfold Symmetric, nra_eq.
      intros. rewrite H; trivial.
    - unfold Transitive, nra_eq.
      intros.
      rewrite H, H0 by trivial.
      trivial.
  Qed.

Global Instance aid_proper : Proper nra_eq AID.

Proof.

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

Global Instance aconst_proper : Proper (eq ==> nra_eq) AConst.

Proof.

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

Global Instance abinop_proper : Proper (binop_eq ==> nra_eq ==> nra_eq ==> nra_eq) ABinop.

Proof.

    unfold Proper, respectful, nra_eq.
    intros; simpl.
    rewrite H0, H1 by trivial.
    case_eq (h ⊢ y1 @ₐ x2 ⊣ c); case_eq (h ⊢ y0 @ₐ x2 ⊣ c); simpl; trivial.
    intros.
    rewrite (H h); eauto.
  Qed.

Global Instance aunop_proper : Proper (unaryop_eq ==> nra_eq ==> nra_eq) AUnop.

Proof.

    unfold Proper, respectful, nra_eq.
    intros; simpl.
    rewrite (H0 h c dn_c x1) by trivial.
    case_eq (h ⊢ y0 @ₐ x1 ⊣ c); simpl; trivial; intros.
    rewrite (H h); eauto.
  Qed.

  Hint Resolve data_normalized_dcoll_in.

  Global Instance amap_proper : Proper (nra_eq ==> nra_eq ==> nra_eq) AMap.

Proof.

    unfold Proper, respectful.
    intros; unfold nra_eq in *; intros; simpl.
    rewrite (H0 h c dn_c x1) by trivial.
    case_eq (h ⊢ y0 @ₐ x1 ⊣ c); simpl; trivial; intros.
    destruct d; try reflexivity.
    simpl; f_equal.
    apply rmap_ext.
    eauto.
  Qed.

  Lemma oomap_concat_eq {h:list(string*string)} op1 op2 l:
    forall (c:list (string*data))
           (dn_c:Forall (fun d => data_normalized h (snd d)) c),
      (forall x : data,
          h ⊢ op1 @ₐ x ⊣ c = h ⊢ op2 @ₐ x ⊣ c) ->
    oomap_concat (nra_eval h c op1) l = oomap_concat (nra_eval h c op2) l.

Proof.

    intros.
    unfold oomap_concat; rewrite H; reflexivity.
  Qed.

Global Instance amapconcat_proper : Proper (nra_eq ==> nra_eq ==> nra_eq) AMapConcat.

Proof.

    unfold Proper, respectful.
    intros; unfold nra_eq in *; intros; simpl.
    rewrite (H0 h c dn_c x1); case_eq (h ⊢ y0 @ₐ x1 ⊣ c); intros; trivial.
    destruct d; try reflexivity.
    apply olift_ext; inversion 1; subst; intros.
    simpl. f_equal.
    apply rmap_concat_ext; intros.
    eauto.
  Qed.

Global Instance aproduct_proper : Proper (nra_eq ==> nra_eq ==> nra_eq) AProduct.

Proof.

    unfold Proper, respectful.
    intros; unfold nra_eq in *; intros; simpl.
    rewrite (H0 h c dn_c x1) by trivial; rewrite (H h c dn_c x1) by trivial.
    reflexivity.
  Qed.

Global Instance aselect_proper : Proper (nra_eq ==> nra_eq ==> nra_eq) ASelect.

Proof.

    unfold Proper, respectful, nra_eq.
    intros; simpl.
    rewrite (H0 h c dn_c x1) by trivial.
    case_eq (h ⊢ y0 @ₐ x1 ⊣ c); intro; trivial.
    destruct d; try reflexivity.
    intros. apply olift_ext; inversion 1; subst; intros.
    simpl.
    f_equal.
    apply lift_filter_ext; intros.
    rewrite H; trivial.
    eauto.
  Qed.

Global Instance adefault_proper : Proper (nra_eq ==> nra_eq ==> nra_eq) ADefault.

Proof.

    unfold Proper, respectful, nra_eq; intros; simpl.
    rewrite (H0 h c dn_c x1) by trivial; rewrite (H h c dn_c x1) by trivial.
    case_eq (h ⊢ y0 @ₐ x1 ⊣ c); intros; case_eq (h ⊢ y @ₐ x1 ⊣ c); intros; simpl; trivial.
  Qed.

Global Instance aeither_proper : Proper (nra_eq ==> nra_eq ==> nra_eq) AEither.

Proof.

    unfold Proper, respectful, nra_eq; intros; simpl.
    destruct x1; simpl; trivial; inversion dn_x; subst; auto.
  Qed.

Global Instance aeitherconcat_proper : Proper (nra_eq ==> nra_eq ==> nra_eq) AEitherConcat.

Proof.

    unfold Proper, respectful, nra_eq; intros; simpl.
    rewrite (H0 h c dn_c x1) by trivial; rewrite (H h c dn_c x1) by trivial.
    case_eq (h ⊢ y0 @ₐ x1 ⊣ c); case_eq (h ⊢ y @ₐ x1 ⊣ c); intros; simpl; trivial.
  Qed.

Global Instance aapp_proper : Proper (nra_eq ==> nra_eq ==> nra_eq) AApp.

Proof.

    unfold Proper, respectful, nra_eq; intros; simpl.
    rewrite (H0 h c dn_c x1) by trivial. case_eq (h ⊢ y0 @ₐ x1 ⊣ c); intros; simpl; trivial.
    rewrite (H h c dn_c d); eauto.
  Qed.

Global Instance agetconstant_proper s : Proper (nra_eq) (AGetConstant s).

Proof.

    unfold Proper, respectful, nra_eq; intros; simpl.
    reflexivity.
  Qed.

End NRAEq.

Notation "X ≡ₐ Y" := (nra_eq X Y) (at level 90) : nra_scope.