Qcert.LambdaNRA.Lang.LambdaNRAEq

Section LambdaNRAEq.

  Context {fruntime:foreign_runtime}.

    Definition lnra_eq (op1 op2:lnra) : Prop :=
    ∀
      (h:list(string×string))
      (cenv:bindings)
      (env:bindings)
      (dn_cenv:Forall (fun d ⇒ data_normalized h (snd d)) cenv)
      (dn_env:Forall (fun d ⇒ data_normalized h (snd d)) env),
       lnra_eval h cenv env op1 = lnra_eval h cenv env op2.

    Definition lnra_lambda_eq (op1 op2:lnra_lambda) : Prop :=
    ∀
      (h:list(string×string))
      (cenv:bindings)
      (env:bindings)
      (dn_cenv:Forall (fun d ⇒ data_normalized h (snd d)) cenv)
      (dn_env:Forall (fun d ⇒ data_normalized h (snd d)) env)
      (d:data)
      (dn_d:data_normalized h d),
      lnra_lambda_eval h cenv env op1 d = lnra_lambda_eval h cenv env op2 d.

  Global Instance lnra_equiv : Equivalence lnra_eq.

  Global Instance lnra_lambda_equiv : Equivalence lnra_lambda_eq.

  Global Instance lavar_proper : Proper (eq ==> lnra_eq) LNRAVar.

  Global Instance latable_proper : Proper (eq ==> lnra_eq) LNRATable.

  Global Instance laconst_proper : Proper (eq ==> lnra_eq) LNRAConst.

  Global Instance labinop_proper :
    Proper (eq ==> lnra_eq ==> lnra_eq ==> lnra_eq) LNRABinop.

  Global Instance launop_proper :
    Proper (eq ==> lnra_eq ==> lnra_eq) LNRAUnop.

  Global Instance lamap_proper :
    Proper (lnra_lambda_eq ==> lnra_eq ==> lnra_eq) LNRAMap.

  Global Instance lamapconcat_proper :
    Proper (lnra_lambda_eq ==> lnra_eq ==> lnra_eq) LNRAMapConcat.

  Global Instance laproduct_proper :
    Proper (lnra_eq ==> lnra_eq ==> lnra_eq) LNRAProduct.

  Global Instance lafilter_proper :
    Proper (lnra_lambda_eq ==> lnra_eq ==> lnra_eq) LNRAFilter.

  Global Instance lalambda_proper :
    Proper (eq ==> lnra_eq ==> lnra_lambda_eq) LNRALambda.

End LambdaNRAEq.