Qcert.NRAEnv.Lang.NRAEnvIgnore
Some infrastructure for rewrites
Context {fruntime:foreign_runtime}.
Fixpoint is_nra (e:nraenv) : Prop :=
match e with
| NRAEnvID ⇒ True
| NRAEnvConst rd ⇒ True
| NRAEnvBinop bop e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvUnop uop e1 ⇒ is_nra e1
| NRAEnvMap e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvMapConcat e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvProduct e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvSelect e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvDefault e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvEither e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvEitherConcat e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvApp e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvGetConstant _ ⇒ False
| NRAEnvEnv ⇒ False
| NRAEnvAppEnv e1 e2 ⇒ False
| NRAEnvMapEnv e1 ⇒ False
| NRAEnvFlatMap e1 e2 ⇒ (is_nra e1) ∧ (is_nra e2)
| NRAEnvJoin e1 e2 e3 ⇒ (is_nra e1) ∧ (is_nra e2) ∧ (is_nra e3)
| NRAEnvProject _ e1 ⇒ (is_nra e1)
| NRAEnvGroupBy _ _ e1 ⇒ (is_nra e1)
| NRAEnvUnnest _ _ e1 ⇒ (is_nra e1)
end.
Fixpoint is_nra_fun (e:nraenv) : bool :=
match e with
| NRAEnvID ⇒ true
| NRAEnvConst rd ⇒ true
| NRAEnvBinop bop e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvUnop uop e1 ⇒ is_nra_fun e1
| NRAEnvMap e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvMapConcat e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvProduct e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvSelect e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvDefault e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvEither e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvEitherConcat e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvApp e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvGetConstant _ ⇒ false
| NRAEnvEnv ⇒ false
| NRAEnvAppEnv e1 e2 ⇒ false
| NRAEnvMapEnv e1 ⇒ false
| NRAEnvFlatMap e1 e2 ⇒ andb (is_nra_fun e1) (is_nra_fun e2)
| NRAEnvJoin e1 e2 e3 ⇒ andb (is_nra_fun e1) (andb (is_nra_fun e2) (is_nra_fun e3))
| NRAEnvProject _ e1 ⇒ (is_nra_fun e1)
| NRAEnvGroupBy _ _ e1 ⇒ (is_nra_fun e1)
| NRAEnvUnnest _ _ e1 ⇒ (is_nra_fun e1)
end.
Lemma is_nra_eq (e:nraenv):
is_nra e ↔ (is_nra_fun e = true).
Fixpoint nraenv_ignores_env (e:nraenv) : Prop :=
match e with
| NRAEnvID ⇒ True
| NRAEnvConst rd ⇒ True
| NRAEnvBinop bop e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvUnop uop e1 ⇒ nraenv_ignores_env e1
| NRAEnvMap e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvMapConcat e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvProduct e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvSelect e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvDefault e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvEither e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvEitherConcat e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvApp e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvGetConstant _ ⇒ True
| NRAEnvEnv ⇒ False
| NRAEnvAppEnv e1 e2 ⇒ (nraenv_ignores_env e2)
| NRAEnvMapEnv e1 ⇒ False
| NRAEnvFlatMap e1 e2 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2)
| NRAEnvJoin e1 e2 e3 ⇒ (nraenv_ignores_env e1) ∧ (nraenv_ignores_env e2) ∧ (nraenv_ignores_env e3)
| NRAEnvProject _ e1 ⇒ (nraenv_ignores_env e1)
| NRAEnvGroupBy _ _ e1 ⇒ (nraenv_ignores_env e1)
| NRAEnvUnnest _ _ e1 ⇒ (nraenv_ignores_env e1)
end.
Fixpoint nraenv_ignores_env_fun (e:nraenv) : bool :=
match e with
| NRAEnvID ⇒ true
| NRAEnvConst rd ⇒ true
| NRAEnvBinop bop e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvUnop uop e1 ⇒ nraenv_ignores_env_fun e1
| NRAEnvMap e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvMapConcat e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvProduct e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvSelect e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvDefault e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvEither e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvEitherConcat e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvApp e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvGetConstant _ ⇒ true
| NRAEnvEnv ⇒ false
| NRAEnvAppEnv e1 e2 ⇒ (nraenv_ignores_env_fun e2)
| NRAEnvMapEnv e1 ⇒ false
| NRAEnvFlatMap e1 e2 ⇒ andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
| NRAEnvJoin e1 e2 e3 ⇒ andb (nraenv_ignores_env_fun e1) (andb (nraenv_ignores_env_fun e2) (nraenv_ignores_env_fun e3))
| NRAEnvProject _ e1 ⇒ (nraenv_ignores_env_fun e1)
| NRAEnvGroupBy _ _ e1 ⇒ (nraenv_ignores_env_fun e1)
| NRAEnvUnnest _ _ e1 ⇒ (nraenv_ignores_env_fun e1)
end.
Lemma nraenv_ignores_env_eq (e:nraenv):
nraenv_ignores_env e ↔ (nraenv_ignores_env_fun e = true).
Fixpoint fixed_env (e:nraenv) : Prop :=
match e with
| NRAEnvID ⇒ True
| NRAEnvConst rd ⇒ True
| NRAEnvBinop bop e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvUnop uop e1 ⇒ fixed_env e1
| NRAEnvMap e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvMapConcat e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvProduct e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvSelect e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvDefault e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvEither e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvEitherConcat e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvApp e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvGetConstant _ ⇒ True
| NRAEnvEnv ⇒ True
| NRAEnvAppEnv e1 e2 ⇒ False
| NRAEnvMapEnv e1 ⇒ False
| NRAEnvFlatMap e1 e2 ⇒ (fixed_env e1) ∧ (fixed_env e2)
| NRAEnvJoin e1 e2 e3 ⇒ (fixed_env e1) ∧ (fixed_env e2) ∧ (fixed_env e3)
| NRAEnvProject _ e1 ⇒ (fixed_env e1)
| NRAEnvGroupBy _ _ e1 ⇒ (fixed_env e1)
| NRAEnvUnnest _ _ e1 ⇒ (fixed_env e1)
end.
Fixpoint fixed_env_fun (e:nraenv) : bool :=
match e with
| NRAEnvID ⇒ true
| NRAEnvConst rd ⇒ true
| NRAEnvBinop bop e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvUnop uop e1 ⇒ fixed_env_fun e1
| NRAEnvMap e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvMapConcat e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvProduct e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvSelect e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvDefault e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvEither e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvEitherConcat e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvApp e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvGetConstant _ ⇒ true
| NRAEnvEnv ⇒ true
| NRAEnvAppEnv e1 e2 ⇒ false
| NRAEnvMapEnv e1 ⇒ false
| NRAEnvFlatMap e1 e2 ⇒ andb (fixed_env_fun e1) (fixed_env_fun e2)
| NRAEnvJoin e1 e2 e3 ⇒ andb (fixed_env_fun e1) (andb (fixed_env_fun e2) (fixed_env_fun e3))
| NRAEnvProject _ e1 ⇒ (fixed_env_fun e1)
| NRAEnvGroupBy _ _ e1 ⇒ (fixed_env_fun e1)
| NRAEnvUnnest _ _ e1 ⇒ (fixed_env_fun e1)
end.
Lemma fixed_env_eq (e:nraenv):
fixed_env e ↔ (fixed_env_fun e = true).
Fixpoint nraenv_ignores_id (e:nraenv) : Prop :=
match e with
| NRAEnvID ⇒ False
| NRAEnvConst rd ⇒ True
| NRAEnvBinop bop e1 e2 ⇒ (nraenv_ignores_id e1) ∧ (nraenv_ignores_id e2)
| NRAEnvUnop uop e1 ⇒ nraenv_ignores_id e1
| NRAEnvMap e1 e2 ⇒ nraenv_ignores_id e2
| NRAEnvMapConcat e1 e2 ⇒ nraenv_ignores_id e2
| NRAEnvProduct e1 e2 ⇒ (nraenv_ignores_id e1) ∧ (nraenv_ignores_id e2)
| NRAEnvSelect e1 e2 ⇒ (nraenv_ignores_id e2)
| NRAEnvDefault e1 e2 ⇒ (nraenv_ignores_id e1) ∧ (nraenv_ignores_id e2)
| NRAEnvEither e1 e2 ⇒ False
| NRAEnvEitherConcat e1 e2 ⇒ (nraenv_ignores_id e1) ∧ (nraenv_ignores_id e2)
| NRAEnvApp e1 e2 ⇒ (nraenv_ignores_id e2)
| NRAEnvGetConstant _ ⇒ True
| NRAEnvEnv ⇒ True
| NRAEnvAppEnv e1 e2 ⇒ (nraenv_ignores_id e1) ∧ (nraenv_ignores_id e2)
| NRAEnvMapEnv e1 ⇒ (nraenv_ignores_id e1)
| NRAEnvFlatMap e1 e2 ⇒ (nraenv_ignores_id e1) ∧ (nraenv_ignores_id e2)
| NRAEnvJoin e1 e2 e3 ⇒ (nraenv_ignores_id e1) ∧ (nraenv_ignores_id e2) ∧ (nraenv_ignores_id e3)
| NRAEnvProject _ e1 ⇒ (nraenv_ignores_id e1)
| NRAEnvGroupBy _ _ e1 ⇒ (nraenv_ignores_id e1)
| NRAEnvUnnest _ _ e1 ⇒ (nraenv_ignores_id e1)
end.
Fixpoint nraenv_ignores_id_fun (e:nraenv) : bool :=
match e with
| NRAEnvID ⇒ false
| NRAEnvConst rd ⇒ true
| NRAEnvBinop bop e1 e2 ⇒ andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
| NRAEnvUnop uop e1 ⇒ nraenv_ignores_id_fun e1
| NRAEnvMap e1 e2 ⇒ nraenv_ignores_id_fun e2
| NRAEnvMapConcat e1 e2 ⇒ nraenv_ignores_id_fun e2
| NRAEnvProduct e1 e2 ⇒ andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
| NRAEnvSelect e1 e2 ⇒ (nraenv_ignores_id_fun e2)
| NRAEnvDefault e1 e2 ⇒ andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
| NRAEnvEither e1 e2 ⇒ false
| NRAEnvEitherConcat e1 e2 ⇒ andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
| NRAEnvApp e1 e2 ⇒ (nraenv_ignores_id_fun e2)
| NRAEnvGetConstant _ ⇒ true
| NRAEnvEnv ⇒ true
| NRAEnvAppEnv e1 e2 ⇒ andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
| NRAEnvMapEnv e1 ⇒ (nraenv_ignores_id_fun e1)
| NRAEnvFlatMap e1 e2 ⇒ andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
| NRAEnvJoin e1 e2 e3 ⇒ andb (nraenv_ignores_id_fun e1) (andb (nraenv_ignores_id_fun e2) (nraenv_ignores_id_fun e3))
| NRAEnvProject _ e1 ⇒ (nraenv_ignores_id_fun e1)
| NRAEnvGroupBy _ _ e1 ⇒ (nraenv_ignores_id_fun e1)
| NRAEnvUnnest _ _ e1 ⇒ (nraenv_ignores_id_fun e1)
end.
Lemma nraenv_ignores_id_eq (e:nraenv):
nraenv_ignores_id e ↔ (nraenv_ignores_id_fun e = true).
Lemma nraenv_ignores_env_cnraenv_eq (e:nraenv) :
nraenv_ignores_env e →
cnraenv_ignores_env (cnraenv_of_nraenv e).
Lemma nraenv_ignores_env_swap (e:nraenv) :
nraenv_ignores_env e → ∀ (h:list (string×string)) c,
∀ (env1 env2:data), ∀ x:data,
h ⊢ e @ₓ x ⊣ c;env1 = h ⊢ e @ₓ x ⊣ c;env2.
Lemma nraenv_ignores_id_cnraenv_eq (e:nraenv) :
nraenv_ignores_id e →
cnraenv_ignores_id (cnraenv_of_nraenv e).
Lemma nraenv_ignores_id_swap (e:nraenv) :
nraenv_ignores_id e → ∀ h:list (string×string), ∀ c,
∀ env:data, ∀ x1 x2:data,
h ⊢ e @ₓ x1 ⊣ c;env = h ⊢ e @ₓ x2 ⊣ c;env.
End NRAEnvIgnore.