Module Qcert.cNRAEnv.Lang.cNRAEnvIgnore

Require Import Bool.
Require Import List.
Require Import String.
Require Import Utils.
Require Import DataRuntime.
Require Import NRA.
Require Import NRASugar.
Require Import NRAEq.
Require Import cNRAEnv.

Section cNRAEnvIgnore.

  Local Open Scope nra_scope.
  Local Open Scope nraenv_core_scope.

Some infrastructure for rewrites

  Context {fruntime:foreign_runtime}.

  Fixpoint nraenv_core_is_nra (e:nraenv_core) : Prop :=
    match e with
    | cNRAEnvID => True
    | cNRAEnvConst rd => True
    | cNRAEnvBinop bop e1 e2 => (nraenv_core_is_nra e1) /\ (nraenv_core_is_nra e2)
    | cNRAEnvUnop uop e1 => nraenv_core_is_nra e1
    | cNRAEnvMap e1 e2 => (nraenv_core_is_nra e1) /\ (nraenv_core_is_nra e2)
    | cNRAEnvMapProduct e1 e2 => (nraenv_core_is_nra e1) /\ (nraenv_core_is_nra e2)
    | cNRAEnvProduct e1 e2 => (nraenv_core_is_nra e1) /\ (nraenv_core_is_nra e2)
    | cNRAEnvSelect e1 e2 => (nraenv_core_is_nra e1) /\ (nraenv_core_is_nra e2)
    | cNRAEnvDefault e1 e2 => (nraenv_core_is_nra e1) /\ (nraenv_core_is_nra e2)
    | cNRAEnvEither e1 e2 => (nraenv_core_is_nra e1) /\ (nraenv_core_is_nra e2)
    | cNRAEnvEitherConcat e1 e2 => (nraenv_core_is_nra e1) /\ (nraenv_core_is_nra e2)
    | cNRAEnvApp e1 e2 => (nraenv_core_is_nra e1) /\ (nraenv_core_is_nra e2)
    | cNRAEnvGetConstant _ => True
    | cNRAEnvEnv => False
    | cNRAEnvAppEnv e1 e2 => False
    | cNRAEnvMapEnv e1 => False
    end.

  Fixpoint nraenv_core_is_nra_fun (e:nraenv_core) : bool :=
    match e with
    | cNRAEnvID => true
    | cNRAEnvConst rd => true
    | cNRAEnvBinop bop e1 e2 => andb (nraenv_core_is_nra_fun e1) (nraenv_core_is_nra_fun e2)
    | cNRAEnvUnop uop e1 => nraenv_core_is_nra_fun e1
    | cNRAEnvMap e1 e2 => andb (nraenv_core_is_nra_fun e1) (nraenv_core_is_nra_fun e2)
    | cNRAEnvMapProduct e1 e2 => andb (nraenv_core_is_nra_fun e1) (nraenv_core_is_nra_fun e2)
    | cNRAEnvProduct e1 e2 => andb (nraenv_core_is_nra_fun e1) (nraenv_core_is_nra_fun e2)
    | cNRAEnvSelect e1 e2 => andb (nraenv_core_is_nra_fun e1) (nraenv_core_is_nra_fun e2)
    | cNRAEnvDefault e1 e2 => andb (nraenv_core_is_nra_fun e1) (nraenv_core_is_nra_fun e2)
    | cNRAEnvEither e1 e2 => andb (nraenv_core_is_nra_fun e1) (nraenv_core_is_nra_fun e2)
    | cNRAEnvEitherConcat e1 e2 => andb (nraenv_core_is_nra_fun e1) (nraenv_core_is_nra_fun e2)
    | cNRAEnvApp e1 e2 => andb (nraenv_core_is_nra_fun e1) (nraenv_core_is_nra_fun e2)
    | cNRAEnvGetConstant _ => true
    | cNRAEnvEnv => false
    | cNRAEnvAppEnv e1 e2 => false
    | cNRAEnvMapEnv e1 => false
    end.

  Lemma nraenv_core_is_nra_eq (e:nraenv_core):
    nraenv_core_is_nra e <-> (nraenv_core_is_nra_fun e = true).

Proof.

  Fixpoint nraenv_core_ignores_env (e:nraenv_core) : Prop :=
    match e with
    | cNRAEnvID => True
    | cNRAEnvConst rd => True
    | cNRAEnvBinop bop e1 e2 => (nraenv_core_ignores_env e1) /\ (nraenv_core_ignores_env e2)
    | cNRAEnvUnop uop e1 => nraenv_core_ignores_env e1
    | cNRAEnvMap e1 e2 => (nraenv_core_ignores_env e1) /\ (nraenv_core_ignores_env e2)
    | cNRAEnvMapProduct e1 e2 => (nraenv_core_ignores_env e1) /\ (nraenv_core_ignores_env e2)
    | cNRAEnvProduct e1 e2 => (nraenv_core_ignores_env e1) /\ (nraenv_core_ignores_env e2)
    | cNRAEnvSelect e1 e2 => (nraenv_core_ignores_env e1) /\ (nraenv_core_ignores_env e2)
    | cNRAEnvDefault e1 e2 => (nraenv_core_ignores_env e1) /\ (nraenv_core_ignores_env e2)
    | cNRAEnvEither e1 e2 => (nraenv_core_ignores_env e1) /\ (nraenv_core_ignores_env e2)
    | cNRAEnvEitherConcat e1 e2 => (nraenv_core_ignores_env e1) /\ (nraenv_core_ignores_env e2)
    | cNRAEnvApp e1 e2 => (nraenv_core_ignores_env e1) /\ (nraenv_core_ignores_env e2)
    | cNRAEnvGetConstant _ => True
    | cNRAEnvEnv => False
    | cNRAEnvAppEnv e1 e2 => (nraenv_core_ignores_env e2)
    | cNRAEnvMapEnv e1 => False
    end.

  Fixpoint nraenv_core_ignores_env_fun (e:nraenv_core) : bool :=
    match e with
    | cNRAEnvID => true
    | cNRAEnvConst rd => true
    | cNRAEnvBinop bop e1 e2 => andb (nraenv_core_ignores_env_fun e1) (nraenv_core_ignores_env_fun e2)
    | cNRAEnvUnop uop e1 => nraenv_core_ignores_env_fun e1
    | cNRAEnvMap e1 e2 => andb (nraenv_core_ignores_env_fun e1) (nraenv_core_ignores_env_fun e2)
    | cNRAEnvMapProduct e1 e2 => andb (nraenv_core_ignores_env_fun e1) (nraenv_core_ignores_env_fun e2)
    | cNRAEnvProduct e1 e2 => andb (nraenv_core_ignores_env_fun e1) (nraenv_core_ignores_env_fun e2)
    | cNRAEnvSelect e1 e2 => andb (nraenv_core_ignores_env_fun e1) (nraenv_core_ignores_env_fun e2)
    | cNRAEnvDefault e1 e2 => andb (nraenv_core_ignores_env_fun e1) (nraenv_core_ignores_env_fun e2)
    | cNRAEnvEither e1 e2 => andb (nraenv_core_ignores_env_fun e1) (nraenv_core_ignores_env_fun e2)
    | cNRAEnvEitherConcat e1 e2 => andb (nraenv_core_ignores_env_fun e1) (nraenv_core_ignores_env_fun e2)
    | cNRAEnvApp e1 e2 => andb (nraenv_core_ignores_env_fun e1) (nraenv_core_ignores_env_fun e2)
    | cNRAEnvGetConstant _ => true
    | cNRAEnvEnv => false
    | cNRAEnvAppEnv e1 e2 => (nraenv_core_ignores_env_fun e2)
    | cNRAEnvMapEnv e1 => false
    end.

  Lemma nraenv_core_ignores_env_eq (e:nraenv_core):
    nraenv_core_ignores_env e <-> (nraenv_core_ignores_env_fun e = true).

Proof.

  Fixpoint nraenv_core_fixed_env (e:nraenv_core) : Prop :=
    match e with
    | cNRAEnvID => True
    | cNRAEnvConst rd => True
    | cNRAEnvBinop bop e1 e2 => (nraenv_core_fixed_env e1) /\ (nraenv_core_fixed_env e2)
    | cNRAEnvUnop uop e1 => nraenv_core_fixed_env e1
    | cNRAEnvMap e1 e2 => (nraenv_core_fixed_env e1) /\ (nraenv_core_fixed_env e2)
    | cNRAEnvMapProduct e1 e2 => (nraenv_core_fixed_env e1) /\ (nraenv_core_fixed_env e2)
    | cNRAEnvProduct e1 e2 => (nraenv_core_fixed_env e1) /\ (nraenv_core_fixed_env e2)
    | cNRAEnvSelect e1 e2 => (nraenv_core_fixed_env e1) /\ (nraenv_core_fixed_env e2)
    | cNRAEnvDefault e1 e2 => (nraenv_core_fixed_env e1) /\ (nraenv_core_fixed_env e2)
    | cNRAEnvEither e1 e2 => (nraenv_core_fixed_env e1) /\ (nraenv_core_fixed_env e2)
    | cNRAEnvEitherConcat e1 e2 => (nraenv_core_fixed_env e1) /\ (nraenv_core_fixed_env e2)
    | cNRAEnvApp e1 e2 => (nraenv_core_fixed_env e1) /\ (nraenv_core_fixed_env e2)
    | cNRAEnvGetConstant _ => True
    | cNRAEnvEnv => True
    | cNRAEnvAppEnv e1 e2 => False
    | cNRAEnvMapEnv e1 => False
    end.

  Fixpoint nraenv_core_fixed_env_fun (e:nraenv_core) : bool :=
    match e with
    | cNRAEnvID => true
    | cNRAEnvConst rd => true
    | cNRAEnvBinop bop e1 e2 => andb (nraenv_core_fixed_env_fun e1) (nraenv_core_fixed_env_fun e2)
    | cNRAEnvUnop uop e1 => nraenv_core_fixed_env_fun e1
    | cNRAEnvMap e1 e2 => andb (nraenv_core_fixed_env_fun e1) (nraenv_core_fixed_env_fun e2)
    | cNRAEnvMapProduct e1 e2 => andb (nraenv_core_fixed_env_fun e1) (nraenv_core_fixed_env_fun e2)
    | cNRAEnvProduct e1 e2 => andb (nraenv_core_fixed_env_fun e1) (nraenv_core_fixed_env_fun e2)
    | cNRAEnvSelect e1 e2 => andb (nraenv_core_fixed_env_fun e1) (nraenv_core_fixed_env_fun e2)
    | cNRAEnvDefault e1 e2 => andb (nraenv_core_fixed_env_fun e1) (nraenv_core_fixed_env_fun e2)
    | cNRAEnvEither e1 e2 => andb (nraenv_core_fixed_env_fun e1) (nraenv_core_fixed_env_fun e2)
    | cNRAEnvEitherConcat e1 e2 => andb (nraenv_core_fixed_env_fun e1) (nraenv_core_fixed_env_fun e2)
    | cNRAEnvApp e1 e2 => andb (nraenv_core_fixed_env_fun e1) (nraenv_core_fixed_env_fun e2)
    | cNRAEnvGetConstant _ => true
    | cNRAEnvEnv => true
    | cNRAEnvAppEnv e1 e2 => false
    | cNRAEnvMapEnv e1 => false
    end.

  Lemma nraenv_core_fixed_env_eq (e:nraenv_core):
    nraenv_core_fixed_env e <-> (nraenv_core_fixed_env_fun e = true).

Proof.

  Fixpoint nraenv_core_ignores_id (e:nraenv_core) : Prop :=
    match e with
    | cNRAEnvID => False
    | cNRAEnvConst rd => True
    | cNRAEnvBinop bop e1 e2 => (nraenv_core_ignores_id e1) /\ (nraenv_core_ignores_id e2)
    | cNRAEnvUnop uop e1 => nraenv_core_ignores_id e1
    | cNRAEnvMap e1 e2 => nraenv_core_ignores_id e2
    | cNRAEnvMapProduct e1 e2 => nraenv_core_ignores_id e2
    | cNRAEnvProduct e1 e2 => (nraenv_core_ignores_id e1) /\ (nraenv_core_ignores_id e2)
    | cNRAEnvSelect e1 e2 => (nraenv_core_ignores_id e2)
    | cNRAEnvDefault e1 e2 => (nraenv_core_ignores_id e1) /\ (nraenv_core_ignores_id e2)
    | cNRAEnvEither e1 e2 => False
    | cNRAEnvEitherConcat e1 e2 => (nraenv_core_ignores_id e1) /\ (nraenv_core_ignores_id e2)
    | cNRAEnvApp e1 e2 => (nraenv_core_ignores_id e2)
    | cNRAEnvGetConstant _ => True
    | cNRAEnvEnv => True
    | cNRAEnvAppEnv e1 e2 => (nraenv_core_ignores_id e1) /\ (nraenv_core_ignores_id e2)
    | cNRAEnvMapEnv e1 => (nraenv_core_ignores_id e1)
    end.

  Fixpoint nraenv_core_ignores_id_fun (e:nraenv_core) : bool :=
    match e with
    | cNRAEnvID => false
    | cNRAEnvConst rd => true
    | cNRAEnvBinop bop e1 e2 => andb (nraenv_core_ignores_id_fun e1) (nraenv_core_ignores_id_fun e2)
    | cNRAEnvUnop uop e1 => nraenv_core_ignores_id_fun e1
    | cNRAEnvMap e1 e2 => nraenv_core_ignores_id_fun e2
    | cNRAEnvMapProduct e1 e2 => nraenv_core_ignores_id_fun e2
    | cNRAEnvProduct e1 e2 => andb (nraenv_core_ignores_id_fun e1) (nraenv_core_ignores_id_fun e2)
    | cNRAEnvSelect e1 e2 => (nraenv_core_ignores_id_fun e2)
    | cNRAEnvDefault e1 e2 => andb (nraenv_core_ignores_id_fun e1) (nraenv_core_ignores_id_fun e2)
    | cNRAEnvEither e1 e2 => false
    | cNRAEnvEitherConcat e1 e2 => andb (nraenv_core_ignores_id_fun e1) (nraenv_core_ignores_id_fun e2)
    | cNRAEnvApp e1 e2 => (nraenv_core_ignores_id_fun e2)
    | cNRAEnvGetConstant _ => true
    | cNRAEnvEnv => true
    | cNRAEnvAppEnv e1 e2 => andb (nraenv_core_ignores_id_fun e1) (nraenv_core_ignores_id_fun e2)
    | cNRAEnvMapEnv e1 => (nraenv_core_ignores_id_fun e1)
    end.

  Lemma nraenv_core_ignores_id_eq (e:nraenv_core):
    nraenv_core_ignores_id e <-> (nraenv_core_ignores_id_fun e = true).

Proof.

  Fixpoint nraenv_core_deenv_nra (ae:nraenv_core) : nra :=
    match ae with
    | cNRAEnvID => NRAID
    | cNRAEnvConst d => NRAConst d
    | cNRAEnvBinop b ae1 ae2 => NRABinop b (nraenv_core_deenv_nra ae1) (nraenv_core_deenv_nra ae2)
    | cNRAEnvUnop u ae1 => NRAUnop u (nraenv_core_deenv_nra ae1)
    | cNRAEnvMap ea1 ea2 => NRAMap (nraenv_core_deenv_nra ea1) (nraenv_core_deenv_nra ea2)
    | cNRAEnvMapProduct ea1 ea2 => NRAMapProduct (nraenv_core_deenv_nra ea1) (nraenv_core_deenv_nra ea2)
    | cNRAEnvProduct ea1 ea2 => NRAProduct (nraenv_core_deenv_nra ea1) (nraenv_core_deenv_nra ea2)
    | cNRAEnvSelect ea1 ea2 => NRASelect (nraenv_core_deenv_nra ea1) (nraenv_core_deenv_nra ea2)
    | cNRAEnvDefault ea1 ea2 => NRADefault (nraenv_core_deenv_nra ea1) (nraenv_core_deenv_nra ea2)
    | cNRAEnvEither ea1 ea2 => NRAEither (nraenv_core_deenv_nra ea1) (nraenv_core_deenv_nra ea2)
    | cNRAEnvEitherConcat ea1 ea2 => NRAEitherConcat (nraenv_core_deenv_nra ea1) (nraenv_core_deenv_nra ea2)
    | cNRAEnvApp ea1 ea2 => NRAApp (nraenv_core_deenv_nra ea1) (nraenv_core_deenv_nra ea2)
    | cNRAEnvGetConstant s => NRAGetConstant s
    | cNRAEnvEnv => NRAID
    | cNRAEnvAppEnv ea1 ea2 => NRAID
    | cNRAEnvMapEnv ea1 => NRAID
    end.

  Lemma nraenv_core_ignores_env_swap (e:nraenv_core) :
    nraenv_core_ignores_env e -> forall (h:list (string*string)) c,
                               forall (env1 env2:data), forall x:data,
                       h ⊢ₑ e @ₑ x ⊣ c;env1 = h ⊢ₑ e @ₑ x ⊣ c;env2.

Proof.

  Lemma nraenv_core_ignores_id_swap (e:nraenv_core) :
    nraenv_core_ignores_id e -> forall h:list (string*string), forall c,
        forall env:data, forall x1 x2:data,
            h ⊢ₑ e @ₑ x1 ⊣ c;env = h ⊢ₑ e @ₑ x2 ⊣ c;env.

Proof.

  Lemma nraenv_core_is_nra_deenv (h:list (string*string)) c (e:nraenv_core) (d1 d2:data) :
    nraenv_core_is_nra e ->
        h ⊢ (nra_of_nraenv_core e) @ₐ (nra_context_data d1 d2) ⊣ c =
        h ⊢ (nraenv_core_deenv_nra e) @ₐ d2 ⊣ c.

Proof.

  Fixpoint nraenv_core_of_nra (a:nra) : nraenv_core :=
    match a with
      | NRAGetConstant s => cNRAEnvGetConstant s
      | NRAID => cNRAEnvID
      | NRAConst d => cNRAEnvConst d
      | NRABinop b e1 e2 => cNRAEnvBinop b (nraenv_core_of_nra e1) (nraenv_core_of_nra e2)
      | NRAUnop u e1 => cNRAEnvUnop u (nraenv_core_of_nra e1)
      | NRAMap e1 e2 => cNRAEnvMap (nraenv_core_of_nra e1) (nraenv_core_of_nra e2)
      | NRAMapProduct e1 e2 => cNRAEnvMapProduct (nraenv_core_of_nra e1) (nraenv_core_of_nra e2)
      | NRAProduct e1 e2 => cNRAEnvProduct (nraenv_core_of_nra e1) (nraenv_core_of_nra e2)
      | NRASelect e1 e2 => cNRAEnvSelect (nraenv_core_of_nra e1) (nraenv_core_of_nra e2)
      | NRADefault e1 e2 => cNRAEnvDefault (nraenv_core_of_nra e1) (nraenv_core_of_nra e2)
      | NRAEither opl opr => cNRAEnvEither (nraenv_core_of_nra opl) (nraenv_core_of_nra opr)
      | NRAEitherConcat op1 op2 => cNRAEnvEitherConcat (nraenv_core_of_nra op1) (nraenv_core_of_nra op2)
      | NRAApp e1 e2 => cNRAEnvApp (nraenv_core_of_nra e1) (nraenv_core_of_nra e2)
    end.

  Lemma nraenv_core_eval_of_nra h c e d env :
    nra_eval h c e d = nraenv_core_eval h c (nraenv_core_of_nra e) env d.

Proof.

Lemma nraenv_core_of_nra_is_nra x : nraenv_core_is_nra (nraenv_core_of_nra x).

Proof.

Lemma nraenv_core_deenv_nra_of_nra x : nraenv_core_deenv_nra (nraenv_core_of_nra x) = x.

Proof.

End cNRAEnvIgnore.