Qcert.NRAEnv.Core.cNRAEnvIgnore

Section cNRAEnvIgnore.

  Context {fruntime:foreign_runtime}.

  Fixpoint cnraenv_is_nra (e:cnraenv) : Prop :=
    match e with
      | ANID ⇒ True
      | ANConst rd ⇒ True
      | ANBinop bop e1 e2 ⇒ (cnraenv_is_nra e1) ∧ (cnraenv_is_nra e2)
      | ANUnop uop e1 ⇒ cnraenv_is_nra e1
      | ANMap e1 e2 ⇒ (cnraenv_is_nra e1) ∧ (cnraenv_is_nra e2)
      | ANMapConcat e1 e2 ⇒ (cnraenv_is_nra e1) ∧ (cnraenv_is_nra e2)
      | ANProduct e1 e2 ⇒ (cnraenv_is_nra e1) ∧ (cnraenv_is_nra e2)
      | ANSelect e1 e2 ⇒ (cnraenv_is_nra e1) ∧ (cnraenv_is_nra e2)
      | ANDefault e1 e2 ⇒ (cnraenv_is_nra e1) ∧ (cnraenv_is_nra e2)
      | ANEither e1 e2 ⇒ (cnraenv_is_nra e1) ∧ (cnraenv_is_nra e2)
      | ANEitherConcat e1 e2 ⇒ (cnraenv_is_nra e1) ∧ (cnraenv_is_nra e2)
      | ANApp e1 e2 ⇒ (cnraenv_is_nra e1) ∧ (cnraenv_is_nra e2)
      | ANGetConstant _ ⇒ False
      | ANEnv ⇒ False
      | ANAppEnv e1 e2 ⇒ False
      | ANMapEnv e1 ⇒ False
    end.

  Fixpoint cnraenv_is_nra_fun (e:cnraenv) : bool :=
    match e with
      | ANID ⇒ true
      | ANConst rd ⇒ true
      | ANBinop bop e1 e2 ⇒ andb (cnraenv_is_nra_fun e1) (cnraenv_is_nra_fun e2)
      | ANUnop uop e1 ⇒ cnraenv_is_nra_fun e1
      | ANMap e1 e2 ⇒ andb (cnraenv_is_nra_fun e1) (cnraenv_is_nra_fun e2)
      | ANMapConcat e1 e2 ⇒ andb (cnraenv_is_nra_fun e1) (cnraenv_is_nra_fun e2)
      | ANProduct e1 e2 ⇒ andb (cnraenv_is_nra_fun e1) (cnraenv_is_nra_fun e2)
      | ANSelect e1 e2 ⇒ andb (cnraenv_is_nra_fun e1) (cnraenv_is_nra_fun e2)
      | ANDefault e1 e2 ⇒ andb (cnraenv_is_nra_fun e1) (cnraenv_is_nra_fun e2)
      | ANEither e1 e2 ⇒ andb (cnraenv_is_nra_fun e1) (cnraenv_is_nra_fun e2)
      | ANEitherConcat e1 e2 ⇒ andb (cnraenv_is_nra_fun e1) (cnraenv_is_nra_fun e2)
      | ANApp e1 e2 ⇒ andb (cnraenv_is_nra_fun e1) (cnraenv_is_nra_fun e2)
      | ANGetConstant _ ⇒ false
      | ANEnv ⇒ false
      | ANAppEnv e1 e2 ⇒ false
      | ANMapEnv e1 ⇒ false
    end.

  Lemma cnraenv_is_nra_eq (e:cnraenv):
    cnraenv_is_nra e ↔ (cnraenv_is_nra_fun e = true).

  Fixpoint cnraenv_ignores_env (e:cnraenv) : Prop :=
    match e with
      | ANID ⇒ True
      | ANConst rd ⇒ True
      | ANBinop bop e1 e2 ⇒ (cnraenv_ignores_env e1) ∧ (cnraenv_ignores_env e2)
      | ANUnop uop e1 ⇒ cnraenv_ignores_env e1
      | ANMap e1 e2 ⇒ (cnraenv_ignores_env e1) ∧ (cnraenv_ignores_env e2)
      | ANMapConcat e1 e2 ⇒ (cnraenv_ignores_env e1) ∧ (cnraenv_ignores_env e2)
      | ANProduct e1 e2 ⇒ (cnraenv_ignores_env e1) ∧ (cnraenv_ignores_env e2)
      | ANSelect e1 e2 ⇒ (cnraenv_ignores_env e1) ∧ (cnraenv_ignores_env e2)
      | ANDefault e1 e2 ⇒ (cnraenv_ignores_env e1) ∧ (cnraenv_ignores_env e2)
      | ANEither e1 e2 ⇒ (cnraenv_ignores_env e1) ∧ (cnraenv_ignores_env e2)
      | ANEitherConcat e1 e2 ⇒ (cnraenv_ignores_env e1) ∧ (cnraenv_ignores_env e2)
      | ANApp e1 e2 ⇒ (cnraenv_ignores_env e1) ∧ (cnraenv_ignores_env e2)
      | ANGetConstant _ ⇒ True
      | ANEnv ⇒ False
      | ANAppEnv e1 e2 ⇒ (cnraenv_ignores_env e2)
      | ANMapEnv e1 ⇒ False
    end.

  Fixpoint cnraenv_ignores_env_fun (e:cnraenv) : bool :=
    match e with
      | ANID ⇒ true
      | ANConst rd ⇒ true
      | ANBinop bop e1 e2 ⇒ andb (cnraenv_ignores_env_fun e1) (cnraenv_ignores_env_fun e2)
      | ANUnop uop e1 ⇒ cnraenv_ignores_env_fun e1
      | ANMap e1 e2 ⇒ andb (cnraenv_ignores_env_fun e1) (cnraenv_ignores_env_fun e2)
      | ANMapConcat e1 e2 ⇒ andb (cnraenv_ignores_env_fun e1) (cnraenv_ignores_env_fun e2)
      | ANProduct e1 e2 ⇒ andb (cnraenv_ignores_env_fun e1) (cnraenv_ignores_env_fun e2)
      | ANSelect e1 e2 ⇒ andb (cnraenv_ignores_env_fun e1) (cnraenv_ignores_env_fun e2)
      | ANDefault e1 e2 ⇒ andb (cnraenv_ignores_env_fun e1) (cnraenv_ignores_env_fun e2)
      | ANEither e1 e2 ⇒ andb (cnraenv_ignores_env_fun e1) (cnraenv_ignores_env_fun e2)
      | ANEitherConcat e1 e2 ⇒ andb (cnraenv_ignores_env_fun e1) (cnraenv_ignores_env_fun e2)
      | ANApp e1 e2 ⇒ andb (cnraenv_ignores_env_fun e1) (cnraenv_ignores_env_fun e2)
      | ANGetConstant _ ⇒ true
      | ANEnv ⇒ false
      | ANAppEnv e1 e2 ⇒ (cnraenv_ignores_env_fun e2)
      | ANMapEnv e1 ⇒ false
    end.

  Lemma cnraenv_ignores_env_eq (e:cnraenv):
    cnraenv_ignores_env e ↔ (cnraenv_ignores_env_fun e = true).


  Fixpoint cnraenv_fixed_env (e:cnraenv) : Prop :=
    match e with
      | ANID ⇒ True
      | ANConst rd ⇒ True
      | ANBinop bop e1 e2 ⇒ (cnraenv_fixed_env e1) ∧ (cnraenv_fixed_env e2)
      | ANUnop uop e1 ⇒ cnraenv_fixed_env e1
      | ANMap e1 e2 ⇒ (cnraenv_fixed_env e1) ∧ (cnraenv_fixed_env e2)
      | ANMapConcat e1 e2 ⇒ (cnraenv_fixed_env e1) ∧ (cnraenv_fixed_env e2)
      | ANProduct e1 e2 ⇒ (cnraenv_fixed_env e1) ∧ (cnraenv_fixed_env e2)
      | ANSelect e1 e2 ⇒ (cnraenv_fixed_env e1) ∧ (cnraenv_fixed_env e2)
      | ANDefault e1 e2 ⇒ (cnraenv_fixed_env e1) ∧ (cnraenv_fixed_env e2)
      | ANEither e1 e2 ⇒ (cnraenv_fixed_env e1) ∧ (cnraenv_fixed_env e2)
      | ANEitherConcat e1 e2 ⇒ (cnraenv_fixed_env e1) ∧ (cnraenv_fixed_env e2)
      | ANApp e1 e2 ⇒ (cnraenv_fixed_env e1) ∧ (cnraenv_fixed_env e2)
      | ANGetConstant _ ⇒ True
      | ANEnv ⇒ True
      | ANAppEnv e1 e2 ⇒ False
      | ANMapEnv e1 ⇒ False
    end.

  Fixpoint cnraenv_fixed_env_fun (e:cnraenv) : bool :=
    match e with
      | ANID ⇒ true
      | ANConst rd ⇒ true
      | ANBinop bop e1 e2 ⇒ andb (cnraenv_fixed_env_fun e1) (cnraenv_fixed_env_fun e2)
      | ANUnop uop e1 ⇒ cnraenv_fixed_env_fun e1
      | ANMap e1 e2 ⇒ andb (cnraenv_fixed_env_fun e1) (cnraenv_fixed_env_fun e2)
      | ANMapConcat e1 e2 ⇒ andb (cnraenv_fixed_env_fun e1) (cnraenv_fixed_env_fun e2)
      | ANProduct e1 e2 ⇒ andb (cnraenv_fixed_env_fun e1) (cnraenv_fixed_env_fun e2)
      | ANSelect e1 e2 ⇒ andb (cnraenv_fixed_env_fun e1) (cnraenv_fixed_env_fun e2)
      | ANDefault e1 e2 ⇒ andb (cnraenv_fixed_env_fun e1) (cnraenv_fixed_env_fun e2)
      | ANEither e1 e2 ⇒ andb (cnraenv_fixed_env_fun e1) (cnraenv_fixed_env_fun e2)
      | ANEitherConcat e1 e2 ⇒ andb (cnraenv_fixed_env_fun e1) (cnraenv_fixed_env_fun e2)
      | ANApp e1 e2 ⇒ andb (cnraenv_fixed_env_fun e1) (cnraenv_fixed_env_fun e2)
      | ANGetConstant _ ⇒ true
      | ANEnv ⇒ true
      | ANAppEnv e1 e2 ⇒ false
      | ANMapEnv e1 ⇒ false
    end.

  Lemma cnraenv_fixed_env_eq (e:cnraenv):
    cnraenv_fixed_env e ↔ (cnraenv_fixed_env_fun e = true).


  Fixpoint cnraenv_ignores_id (e:cnraenv) : Prop :=
    match e with
      | ANID ⇒ False
      | ANConst rd ⇒ True
      | ANBinop bop e1 e2 ⇒ (cnraenv_ignores_id e1) ∧ (cnraenv_ignores_id e2)
      | ANUnop uop e1 ⇒ cnraenv_ignores_id e1
      | ANMap e1 e2 ⇒ cnraenv_ignores_id e2
      | ANMapConcat e1 e2 ⇒ cnraenv_ignores_id e2
      | ANProduct e1 e2 ⇒ (cnraenv_ignores_id e1) ∧ (cnraenv_ignores_id e2)
      | ANSelect e1 e2 ⇒ (cnraenv_ignores_id e2)
      | ANDefault e1 e2 ⇒ (cnraenv_ignores_id e1) ∧ (cnraenv_ignores_id e2)
      | ANEither e1 e2 ⇒ False
      | ANEitherConcat e1 e2 ⇒ (cnraenv_ignores_id e1) ∧ (cnraenv_ignores_id e2)
      | ANApp e1 e2 ⇒ (cnraenv_ignores_id e2)
      | ANGetConstant _ ⇒ True
      | ANEnv ⇒ True
      | ANAppEnv e1 e2 ⇒ (cnraenv_ignores_id e1) ∧ (cnraenv_ignores_id e2)
      | ANMapEnv e1 ⇒ (cnraenv_ignores_id e1)
    end.

  Fixpoint cnraenv_ignores_id_fun (e:cnraenv) : bool :=
    match e with
      | ANID ⇒ false
      | ANConst rd ⇒ true
      | ANBinop bop e1 e2 ⇒ andb (cnraenv_ignores_id_fun e1) (cnraenv_ignores_id_fun e2)
      | ANUnop uop e1 ⇒ cnraenv_ignores_id_fun e1
      | ANMap e1 e2 ⇒ cnraenv_ignores_id_fun e2
      | ANMapConcat e1 e2 ⇒ cnraenv_ignores_id_fun e2
      | ANProduct e1 e2 ⇒ andb (cnraenv_ignores_id_fun e1) (cnraenv_ignores_id_fun e2)
      | ANSelect e1 e2 ⇒ (cnraenv_ignores_id_fun e2)
      | ANDefault e1 e2 ⇒ andb (cnraenv_ignores_id_fun e1) (cnraenv_ignores_id_fun e2)
      | ANEither e1 e2 ⇒ false
      | ANEitherConcat e1 e2 ⇒ andb (cnraenv_ignores_id_fun e1) (cnraenv_ignores_id_fun e2)
      | ANApp e1 e2 ⇒ (cnraenv_ignores_id_fun e2)
      | ANGetConstant _ ⇒ true
      | ANEnv ⇒ true
      | ANAppEnv e1 e2 ⇒ andb (cnraenv_ignores_id_fun e1) (cnraenv_ignores_id_fun e2)
      | ANMapEnv e1 ⇒ (cnraenv_ignores_id_fun e1)
    end.

  Lemma cnraenv_ignores_id_eq (e:cnraenv):
    cnraenv_ignores_id e ↔ (cnraenv_ignores_id_fun e = true).

  Fixpoint cnraenv_deenv_nra (ae:cnraenv) : nra :=
    match ae with
      | ANID ⇒ AID
      | ANConst d ⇒ AConst d
      | ANBinop b ae1 ae2 ⇒ ABinop b (cnraenv_deenv_nra ae1) (cnraenv_deenv_nra ae2)
      | ANUnop u ae1 ⇒ AUnop u (cnraenv_deenv_nra ae1)
      | ANMap ea1 ea2 ⇒ AMap (cnraenv_deenv_nra ea1) (cnraenv_deenv_nra ea2)
      | ANMapConcat ea1 ea2 ⇒ AMapConcat (cnraenv_deenv_nra ea1) (cnraenv_deenv_nra ea2)
      | ANProduct ea1 ea2 ⇒ AProduct (cnraenv_deenv_nra ea1) (cnraenv_deenv_nra ea2)
      | ANSelect ea1 ea2 ⇒ ASelect (cnraenv_deenv_nra ea1) (cnraenv_deenv_nra ea2)
      | ANDefault ea1 ea2 ⇒ ADefault (cnraenv_deenv_nra ea1) (cnraenv_deenv_nra ea2)
      | ANEither ea1 ea2 ⇒ AEither (cnraenv_deenv_nra ea1) (cnraenv_deenv_nra ea2)
      | ANEitherConcat ea1 ea2 ⇒ AEitherConcat (cnraenv_deenv_nra ea1) (cnraenv_deenv_nra ea2)
      | ANApp ea1 ea2 ⇒ AApp (cnraenv_deenv_nra ea1) (cnraenv_deenv_nra ea2)
      | ANGetConstant _ ⇒ AID
      | ANEnv ⇒ AID
      | ANAppEnv ea1 ea2 ⇒ AID
      | ANMapEnv ea1 ⇒ AID
    end.

  Lemma cnraenv_ignores_env_swap (e:cnraenv) :
    cnraenv_ignores_env e → ∀ (h:list (string×string)) c,
                               ∀ (env1 env2:data), ∀ x:data,
                       h ⊢ₑ e @ₑ x ⊣ c;env1 = h ⊢ₑ e @ₑ x ⊣ c;env2.

  Lemma cnraenv_ignores_id_swap (e:cnraenv) :
    cnraenv_ignores_id e → ∀ h:list (string×string), ∀ c,
      ∀ env:data, ∀ x1 x2:data,
          h ⊢ₑ e @ₑ x1 ⊣ c;env = h ⊢ₑ e @ₑ x2 ⊣ c;env.

  Lemma cnraenv_is_nra_deenv (h:list (string×string)) c (e:cnraenv) (d1 d2:data) :
    cnraenv_is_nra e →
        h ⊢ (nra_of_cnraenv e) @ₐ (pat_context_data c d1 d2) =
        h ⊢ (cnraenv_deenv_nra e) @ₐ d2.

  Fixpoint cnraenv_of_nra (a:nra) : cnraenv :=
    match a with
      | AID ⇒ ANID
      | AConst d ⇒ ANConst d
      | ABinop b e1 e2 ⇒ ANBinop b (cnraenv_of_nra e1) (cnraenv_of_nra e2)
      | AUnop u e1 ⇒ ANUnop u (cnraenv_of_nra e1)
      | AMap e1 e2 ⇒ ANMap (cnraenv_of_nra e1) (cnraenv_of_nra e2)
      | AMapConcat e1 e2 ⇒ ANMapConcat (cnraenv_of_nra e1) (cnraenv_of_nra e2)
      | AProduct e1 e2 ⇒ ANProduct (cnraenv_of_nra e1) (cnraenv_of_nra e2)
      | ASelect e1 e2 ⇒ ANSelect (cnraenv_of_nra e1) (cnraenv_of_nra e2)
      | ADefault e1 e2 ⇒ ANDefault (cnraenv_of_nra e1) (cnraenv_of_nra e2)
      | AEither opl opr ⇒ ANEither (cnraenv_of_nra opl) (cnraenv_of_nra opr)
      | AEitherConcat op1 op2 ⇒ ANEitherConcat (cnraenv_of_nra op1) (cnraenv_of_nra op2)
      | AApp e1 e2 ⇒ ANApp (cnraenv_of_nra e1) (cnraenv_of_nra e2)
    end.

  Lemma cnraenv_eval_of_nra h c e d env :
    nra_eval h e d = cnraenv_eval h c (cnraenv_of_nra e) env d.

  Lemma cnraenv_of_nra_is_nra x : cnraenv_is_nra (cnraenv_of_nra x).

  Lemma cnraenv_deenv_nra_of_nra x : cnraenv_deenv_nra (cnraenv_of_nra x) = x.

End cNRAEnvIgnore.