Qcert.NRAEnv.Core.cNRAEnvEq

Section cNRAEnvEq.



  Context {fruntime:foreign_runtime}.


  Definition cnraenv_eq (op1 op2:cnraenv) : Prop :=
    ∀
      (h:list(string×string))
      (c:list (string×data))
      (dn_c:Forall (fun d ⇒ data_normalized h (snd d)) c)
      (env:data)
      (dn_env:data_normalized h env)
      (x:data)
      (dn_x:data_normalized h x),
      h ⊢ₑ op1 @ₑ x ⊣ c;env = h ⊢ₑ op2 @ₑ x ⊣ c;env.

  Definition nra_eqenv (op1 op2:cnraenv) : Prop :=
    ∀
      (h:list(string×string))
      (c:list (string×data))
      (dn_c:Forall (fun d ⇒ data_normalized h (snd d)) c)
      (env:data)
      (dn_env:data_normalized h env)
      (x:data)
      (dn_x:data_normalized h x),
      h ⊢ (nra_of_cnraenv op1) @ₐ (pat_context_data (drec (rec_sort c)) env x) = h ⊢ (nra_of_cnraenv op2) @ₐ (pat_context_data (drec (rec_sort c)) env x).


  Global Instance cnraenv_equiv : Equivalence cnraenv_eq.

  Global Instance nra_eqenv_equiv : Equivalence nra_eqenv.


  Lemma nra_eqenv_same (op1 op2:cnraenv) :
    cnraenv_eq op1 op2 ↔ nra_eqenv op1 op2.


  Global Instance anid_proper : Proper cnraenv_eq ANID.

  Global Instance anideq_proper : Proper nra_eqenv ANID.

  Global Instance anconst_proper : Proper (eq ==> cnraenv_eq) ANConst.

  Global Instance anconsteq_proper : Proper (eq ==> nra_eqenv) ANConst.


  Global Instance anbinop_proper : Proper (binop_eq ==> cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANBinop.

  Global Instance anbinopeq_proper : Proper (binop_eq ==> nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANBinop.

  Global Instance anunop_proper : Proper (unaryop_eq ==> cnraenv_eq ==> cnraenv_eq) ANUnop.


  Global Instance anunopeq_proper : Proper (unaryop_eq ==> nra_eqenv ==> nra_eqenv) ANUnop.

  Global Instance anmap_proper : Proper (cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANMap.

  Global Instance anmapeq_proper : Proper (nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANMap.

  Global Instance anmapconcat_proper : Proper (cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANMapConcat.

  Global Instance anmapconcateq_proper : Proper (nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANMapConcat.

  Global Instance anproduct_proper : Proper (cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANProduct.

  Global Instance anmapproducteq_proper : Proper (nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANProduct.

  Global Instance anselect_proper : Proper (cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANSelect.

  Global Instance anselecteq_proper : Proper (nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANSelect.

  Global Instance andefault_proper : Proper (cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANDefault.

  Global Instance andefaulteq_proper : Proper (nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANDefault.

  Global Instance aneither_proper : Proper (cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANEither.

    Global Instance aneithereq_proper : Proper (nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANEither.

  Global Instance aneitherconcat_proper : Proper (cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANEitherConcat.

    Global Instance aneitherconcateq_proper : Proper (nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANEitherConcat.

  Global Instance anapp_proper : Proper (cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANApp.

  Global Instance anappeq_proper : Proper (nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANApp.

  Global Instance angetconstant_proper s : Proper (cnraenv_eq) (ANGetConstant s).

  Global Instance angetconstanteq_proper s : Proper (nra_eqenv) (ANGetConstant s).

  Global Instance anenv_proper : Proper (cnraenv_eq) ANEnv.

  Global Instance anenveq_proper : Proper (nra_eqenv) ANEnv.

  Global Instance anappenv_proper : Proper (cnraenv_eq ==> cnraenv_eq ==> cnraenv_eq) ANAppEnv.

  Global Instance anappenveq_proper : Proper (nra_eqenv ==> nra_eqenv ==> nra_eqenv) ANAppEnv.

  Global Instance anmapenv_proper : Proper (cnraenv_eq ==> cnraenv_eq) ANMapEnv.

  Global Instance anmapenveq_proper : Proper (nra_eqenv ==> nra_eqenv) ANMapEnv.

  Lemma cnraenv_of_nra_proper : Proper (nra_eq ==> cnraenv_eq) cnraenv_of_nra.

  Notation "X ≡ₑ Y" := (cnraenv_eq X Y) (at level 90).



  Lemma cnraenv_of_nra_proper_inv x y :
    (cnraenv_of_nra x ≡ₑ cnraenv_of_nra y)%cnraenv →
    (x ≡ₐ y)%nra.

  Lemma nra_of_cnraenv_proper_inv x y :
    (nra_of_cnraenv x ≡ₐ nra_of_cnraenv y)%nra →
    (x ≡ₑ y)%cnraenv.

  Definition cnraenv_always_ensures (P:data→Prop) (q:cnraenv) :=
    ∀
      (h:list(string×string))
      (c:list (string×data))
      (dn_c:Forall (fun d ⇒ data_normalized h (snd d)) c)
      (env:data)
      (dn_env:data_normalized h env)
      (x:data)
      (dn_x:data_normalized h x)
      (d:data),
      h ⊢ₑ q @ₑ x ⊣ c;env = Some d → P d.

End cNRAEnvEq.

Notation "X ≡ₑ Y" := (cnraenv_eq X Y) (at level 90) : cnraenv_scope.