Qcert.NRA.Lang.NRAEq

Section NRAEq.





  Context {fruntime:foreign_runtime}.


  Definition nra_eq (op1 op2:nra) : Prop :=
    ∀ (h:list(string×string)),
    ∀ x:data,
      data_normalized h x →
      h ⊢ op1 @ₐ x = h ⊢ op2 @ₐ x.

  Global Instance nra_equiv : Equivalence nra_eq.


  Global Instance aid_proper : Proper nra_eq AID.

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


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

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


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


  Lemma oomap_concat_eq {h:list(string×string)} op1 op2 l:
    (∀ x : data, h ⊢ op1 @ₐ x = h ⊢ op2 @ₐ x) →
    oomap_concat (nra_eval h op1) l = oomap_concat (nra_eval h op2) l.

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

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

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

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

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

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

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

End NRAEq.

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