Library CoreGenericEnv

Require Import Utf8.
Set Implicit Arguments.

Module Type of an implementation of environments

Require Import Equalities.

Module Type CoreGenericEnvironmentType (VarType : UsualDecidableType).

Require Import List.
Import VarType.

Definition TVar := VarType.t.

Definitions and Notations

gen_env A is an environment that binds variables to values of type A.

Parameter gen_env : Type -> Type.

Section CoreDefinitions.

Variable A B : Type.

The decidability of equality on keys (variables) is imported from Var.

Definition eq_keys_dec := VarType.eq_dec.

Empty environment.

Parameter empty : gen_env A.

Environment build upon explicit associations.

Parameter single : TVar -> A -> gen_env A.
Parameter singles : list TVar -> list A -> gen_env A.

Concatenation of environment (the second one binds first).

Parameter concat : gen_env A -> gen_env A -> gen_env A.

The main operation on environment, get the type of a variable.

Parameter get : TVar -> gen_env A -> option A.

Domain and image of an environment.

Parameter dom : gen_env A -> list TVar.
Parameter img : gen_env A -> list A.

Check the occurence of variable(s) in an environment.

Axiom belongs : TVar -> gen_env A -> Prop.
Axiom all_belongs : list TVar -> gen_env A -> Prop.

Check the non-occurence of variable(s) in an environment.

Axiom notin : TVar -> gen_env A -> Prop.
Axiom all_notin : list TVar -> gen_env A -> Prop.

Map function on types.

Parameter map : (A -> B) -> gen_env A -> gen_env B.

Updating of types with bindings of another environment.

Parameter update_one : gen_env A -> TVar -> A -> gen_env A.
Parameter update : gen_env A -> gen_env A -> gen_env A.

Remove a binding from an environment.

Parameter remove : TVar -> gen_env A -> gen_env A.
Parameter all_remove : list TVar -> gen_env A -> gen_env A.

The ok predicate states that the bindings are pairwise distinct, i.e. each variable appears only once.

Inductive ok : gen_env A -> Prop :=
| ok_nil : ok empty
| ok_cons : forall x v F, ok F ∧ notin x F -> ok (concat F (single x v))
.

End CoreDefinitions.

x ∶ v is the notation for a singleton environment mapping x to v.

Notation "x '∶' v" := (single x v)
(at level 63) : gen_env_scope.

xs ∷ vs is the notation for an environment mapping xs to vs.

Notation "xs '∷' vs" := (singles xs vs)
(at level 63) : gen_env_scope.

E & F is the notation for concatenation of E and F.

Notation "E '&' F" := (concat E F)
(at level 65, left associativity) : gen_env_scope.

E ∖ { x } is the notation for removing x from E.

Notation "E '∖' '{' x '}'" := (remove x E)
(at level 64, left associativity) : gen_env_scope.

E ∖ xs is the notation for removing xs from E.

Notation "E '∖' xs" := (all_remove xs E)
(at level 64, left associativity) : gen_env_scope.

E '[' x '<-' v ']' is the notation for updating x in E with v.

Notation "E '[' x '<-' v ']'" := (update_one E x v)
(at level 65, left associativity) : gen_env_scope.

E ::= F is the notation for updating of E with F.

Notation "E '::=' F" := (update E F)
(at level 65, left associativity) : gen_env_scope.

x ∈ E to be read x is bound in E.

Notation "x '∈' E" := (belongs x E)
(at level 67) : gen_env_scope.

xs ⊂ E to be read xs are bound in E.

Notation "xs '⊂' E" := (all_belongs xs E)
(at level 67) : gen_env_scope.

x '∉' E to be read x is unbound in E.

Notation "x '∉' E" := (notin x E)
(at level 67) : gen_env_scope.

xs '⊄' E to be read xs are unbound in E.

Notation "xs '⊄' E" := (all_notin xs E)
(at level 67) : gen_env_scope.

Bind Scope gen_env_scope with gen_env.
Delimit Scope gen_env_scope with gen_env.
Local Open Scope gen_env_scope.

Properties

Section Properties.
Implicit Types x y : TVar.
Implicit Types xs ys : list TVar.

Primary properties

Induction scheme over environments.

Axiom env_ind : forall A, forall P : gen_env A -> Prop,
  (P (@empty A)) ->
  (forall (E : gen_env A) x (v : A), P E -> P (E & (x ∶ v))) ->
  (forall (E : gen_env A), P E).

Properties of singulars

Environment built from lists.

Axiom singles_empty : forall A,
nil ∷ nil = (@empty A).
Axiom singles_cons : forall A x xs (v : A) (vs : list A),
(x :: xs) ∷ (v :: vs) = (xs ∷ vs) & (x ∶ v).

Properties of concatenation

Concatenation admits empty as neutral element, and is associative.

Axiom concat_empty_r : forall A (E : gen_env A),
  E & (@empty A) = E.
Axiom concat_empty_l : forall A (E : gen_env A),
  (@empty A) & E = E.
Axiom concat_assoc : forall A (E F G : gen_env A),
  E & (F & G) = (E & F) & G.

Properties of get

Get is None on empty.

Axiom get_empty : forall A x,
get x (@empty A) = None.

Get is Some when it binds.

Axiom get_single_eq : forall A x y (v : A),
  x = y ->
  get x (y ∶ v) = Some v.
Axiom get_single_eq_inv : forall A x y (v w : A),
  get x (y ∶ w) = Some v ->
  x = y /\ v = w.

Get is decidable.

Axiom get_dec : forall A x (E : gen_env A),
{ v : A | get x E = Some v } + { get x E = None }.

Get and concatenation.

Axiom get_concat_r : forall A x y (v : A) (E : gen_env A),
  x = y ->
  get x (E & (y ∶ v)) = Some v.
Axiom get_concat_l : forall A x y (v : A) (E : gen_env A),
  x <> y ->
  get x (E & (y ∶ v)) = get x E.
Axiom get_concat_inv : forall A x y (v w : A) (E : gen_env A),
  get x (E & (y ∶ v)) = Some w ->
  (x = y /\ v = w) \/ (x <> y /\ get x E = Some w).

Properties of dom

Dom builds a list.

Axiom dom_empty : forall A,
  dom (@empty A) = nil.
Axiom dom_empty_inv : forall A (E : gen_env A),
  dom (E) = nil ->
  E = (@empty A).
Axiom dom_single : forall A x (v : A),
  dom (x ∶ v) = (x :: nil ).
Axiom dom_singles : forall A xs (vs : list A),
  length xs = length vs ->
  dom (xs ∷ vs) = xs.
Axiom dom_singles_incl : forall A xs (vs : list A),
  List.incl (dom (xs ∷ vs)) xs.
Axiom dom_concat : forall A (E F : gen_env A),
  dom (E & F) = List.app (dom F) (dom E).

Properties of img

Img builds a list.

Axiom img_empty : forall A,
  img (@empty A) = nil.
Axiom img_empty_inv : forall A (E : gen_env A),
  img (E) = nil ->
  E = (@empty A).
Axiom img_single : forall A x (v : A),
  img (x ∶ v) = v :: nil.
Axiom img_singles : forall A xs (vs : list A),
  length xs = length vs ->
  img (xs ∷ vs) = vs.
Axiom img_singles_incl : forall A xs (vs : list A),
  List.incl (img (xs ∷ vs)) vs.
Axiom img_concat : forall A (E F : gen_env A),
  img (E & F) = List.app (img F) (img E).

Dom and img builds identity.

Axiom dom_img_id : forall A (E : gen_env A),
(dom E) ∷ (img E) = E.
Axiom length_dom_img_eq : forall A (E : gen_env A),
length (dom E) = length (img E).

Properties of belongs

Belongs is false on empty environments.

Axiom belongs_empty : forall A x,
x ∈ (@empty A) ->
False.

Belongs in singular(s).

Axiom belongs_single : forall A x y (v : A),
  x = y ->
  x ∈ (y ∶ v).
Axiom belongs_single_inv : forall A x y (v : A),
  x ∈ (y ∶ v) ->
  x = y.
Axiom belongs_singles : forall A x xs (vs : list A),
  length xs = length vs ->
  List.In x xs ->
  x ∈ (xs ∷ vs).
Axiom belongs_singles_inv : forall A x xs (vs : list A),
  length xs = length vs ->
  x ∈ (xs ∷ vs) ->
  List.In x xs.

Belongs and concatenation.

Axiom belongs_concat_l : forall A x (F G : gen_env A),
  x ∈ F ->
  x ∈ (F & G).
Axiom belongs_concat_r : forall A x (F G : gen_env A),
  x ∈ F ->
  x ∈ (G & F).
Axiom belongs_concat_inv : forall A x (F G : gen_env A),
  x ∈ (F & G) ->
  x ∈ F ∨ x ∈ G.

Belongs and dom.

Axiom belongs_dom : forall A x (E : gen_env A),
  x ∈ E ->
  List.In x (dom E).
Axiom belongs_dom_inv : forall A x (E : gen_env A),
  List.In x (dom E) ->
  x ∈ E.

Properties of all_belongs

All_belongs and belongs.

Axiom all_belongs_def : forall A xs (E : gen_env A),
  (forall x, List.In x xs -> x ∈ E) ->
  xs ⊂ E.
Axiom all_belongs_def_inv : forall A xs (E : gen_env A),
  xs ⊂ E ->
  (forall x, List.In x xs -> x ∈ E).
Axiom all_belongs_belongs : forall A x xs (E : gen_env A),
  (x :: xs) ⊂ E ->
  x ∈ E ∧ xs ⊂ E.
Axiom belongs_all_belongs : forall A x xs (E : gen_env A),
  x ∈ E ∧ xs ⊂ E ->
  (x :: xs) ⊂ E.

All_belongs is false on empty environments.

Axiom all_belongs_empty : forall A xs,
  xs ⊂ (@empty A) ->
  xs = nil.
Axiom all_belongs_nil : forall A (E : gen_env A),
  nil ⊂ E.

All_belongs in singular(s).

Axiom all_belongs_single : forall A xs y (v : A),
  xs = y :: nil ->
  xs ⊂ (y ∶ v).
Axiom all_belongs_single_inv : forall A xs y (v : A),
  length xs = 1 ->
  xs ⊂ (y ∶ v) ->
  xs = y :: nil.
Axiom all_belongs_singles : forall A xs ys (vs : list A),
  length ys = length vs ->
  List.incl xs ys ->
  xs ⊂ (ys ∷ vs).
Axiom all_belongs_singles_inv : forall A xs ys (vs : list A),
  xs ⊂ (ys ∷ vs) ->
  List.incl xs ys.

All_belongs and concatenation.

Axiom all_belongs_concat_l : forall A xs (F G : gen_env A),
  xs ⊂ F ->
  xs ⊂ (F & G).
Axiom all_belongs_concat_r : forall A xs (F G : gen_env A),
  xs ⊂ F ->
  xs ⊂ (G & F).

All_belongs and dom.

Axiom all_belongs_dom : forall A xs (E : gen_env A),
  xs ⊂ E ->
  List.incl xs (dom E).
Axiom all_belongs_dom_inv : forall A xs (E F : gen_env A),
  List.incl xs (dom E) ->
  xs ⊂ E.

Properties of notin

Notin and belongs.

Axiom notin_belongs : forall A x (E : gen_env A),
  x ∉ E ->
  ¬ x ∈ E.
Axiom belongs_notin : forall A x (E : gen_env A),
  x ∈ E ->
  ¬ x ∉ E.
Axiom not_belongs_notin : forall A x (E : gen_env A),
  ¬ x ∈ E ->
  x ∉ E.
Axiom notin_belongs_neq : forall A x y (E : gen_env A),
  x ∈ E -> y ∉ E ->
  x <> y.

Notin is true on empty environments.

Axiom notin_empty : forall A x,
x ∉ (@empty A).

Notin in singular(s).

Axiom notin_single : forall A x y (v : A),
  x <> y ->
  x ∉ (y ∶ v).
Axiom notin_single_inv : forall A x y (v : A),
  x ∉ (y ∶ v) ->
  x <> y.
Axiom notin_singles : forall A x xs (vs : list A),
  ¬ List.In x xs ->
  x ∉ (xs ∷ vs).
Axiom notin_singles_inv : forall A x xs (vs : list A),
  length xs = length vs ->
  x ∉ (xs ∷ vs) ->
  ¬ List.In x xs.

Notin and concatenation.

Axiom notin_concat : forall A x (F G : gen_env A),
  x ∉ F -> x ∉ G ->
  x ∉ (F & G).
Axiom notin_concat_inv : forall A x (F G : gen_env A),
  x ∉ (F & G) ->
  x ∉ F ∧ x ∉ G.

Notin and dom.

Axiom notin_dom : forall A x (E : gen_env A),
  x ∉ E ->
  ¬ List.In x (dom E).
Axiom notin_dom_inv : forall A x (E F : gen_env A),
  ¬ List.In x (dom E) ->
  x ∉ E.

Properties of all_notin

All_notin is true on empty lists.

Axiom all_notin_empty_l : forall A (E : gen_env A),
nil ⊄ E.

All_notin and notin.

Axiom all_notin_def : forall A xs (E : gen_env A),
  (forall x, List.In x xs -> x ∉ E) ->
  xs ⊄ E.
Axiom all_notin_def_inv : forall A xs (E : gen_env A),
  xs ⊄ E ->
  (forall x, List.In x xs -> x ∉ E).
Axiom all_notin_notin : forall A x xs (E : gen_env A),
  (x :: xs) ⊄ E ->
  x ∉ E ∧ xs ⊄ E.
Axiom notin_all_notin : forall A x xs (E : gen_env A),
  x ∉ E ∧ xs ⊄ E ->
  (x :: xs) ⊄ E.

All_notin and belongs.

Axiom all_notin_belongs_neq : forall A x ys (E : gen_env A),
x ∈ E -> ys ⊄ E ->
¬ List.In x ys.

All_notin is true on empty environments.

Axiom all_notin_empty_r : forall A xs,
xs ⊄ (@empty A).

All_notin in singular(s).

Axiom all_notin_single : forall A xs y (v : A),
  ¬ List.In y xs ->
  xs ⊄ (y ∶ v).
Axiom all_notin_single_inv : forall A xs y (v : A),
  xs ⊄ (y ∶ v) ->
  ¬ List.In y xs.
Axiom all_notin_singles : forall A xs ys (vs : list A),
  List.Forall (fun x => ¬ List.In x ys) xs ->
  xs ⊄ (ys ∷ vs).
Axiom all_notin_singles_inv : forall A xs ys (vs : list A),
  length ys = length vs ->
  xs ⊄ (ys ∷ vs) ->
  List.Forall (fun x => ¬ List.In x ys) xs.

All_notin and concatenation.

Axiom all_notin_concat : forall A xs (F G : gen_env A),
  xs ⊄ F -> xs ⊄ G ->
  xs ⊄ (F & G).
Axiom all_notin_concat_inv : forall A xs (F G : gen_env A),
  xs ⊄ (F & G) ->
  xs ⊄ F ∧ xs ⊄ G.

All_notin and dom.

Axiom all_notin_dom : forall A xs (E : gen_env A),
  xs ⊄ E ->
  List.Forall (fun x => ¬ List.In x (dom E)) xs.
Axiom all_notin_dom_inv : forall A xs (E : gen_env A),
  List.Forall (fun x => ¬ List.In x (dom E)) xs ->
  xs ⊄ E.

Properties of map

Map is applied on type(s).

Axiom map_empty : forall A B (f : A -> B),
  map f (@empty A) = (@empty B).
Axiom map_single : forall A B (f : A -> B) x (v : A),
  map f (x ∶ v) = x ∶ (f v).
Axiom map_singles : forall A B (f : A -> B) xs (vs : list A),
  map f (xs ∷ vs) = xs ∷ (List.map f vs).

Map commutes with concatenation.

Axiom map_concat : forall A B (f : A -> B) (E F : gen_env A),
map f (E & F) = (map f E) & (map f F).

Dom is unchanged by map.

Axiom dom_map : forall A B (E : gen_env A) (f : A -> B),
dom (map f E) = dom E.

Belongs commutes with map.

Axiom belongs_map : forall A B x (E : gen_env A) (f : A -> B),
  x ∈ E ->
  x ∈ (map f E).
Axiom belongs_map_inv : forall A B x (E : gen_env A) (f : A -> B),
  x ∈ (map f E) ->
  x ∈ E.

All_belongs commutes with map.

Axiom all_belongs_map : forall A B xs (E : gen_env A) (f : A -> B),
  xs ⊂ E ->
  xs ⊂ (map f E).
Axiom all_belongs_map_inv : forall A B xs (E : gen_env A) (f : A -> B),
  xs ⊂ (map f E) ->
  xs ⊂ E.

Notin commutes with map.

Axiom notin_map : forall A B x (E : gen_env A) (f : A -> B),
  x ∉ E ->
  x ∉ (map f E).
Axiom notin_map_inv : forall A B x (E : gen_env A) (f : A -> B),
  x ∉ (map f E) ->
  x ∉ E.

All_notin commutes with map.

Axiom all_notin_map : forall A B xs (E : gen_env A) (f : A -> B),
  xs ⊄ E ->
  xs ⊄ (map f E).
Axiom all_notin_map_inv : forall A B xs (E : gen_env A) (f : A -> B),
  xs ⊄ (map f E) ->
  xs ⊄ E.

Ok commutes with map.

Axiom ok_map : forall A B (E : gen_env A) (f : A -> B),
  ok E ->
  ok (map f E).
Axiom ok_map_inv : forall A B (E : gen_env A) (f : A -> B),
  ok (map f E) ->
  ok E.

Properties of update_one

Update_one is identity on empty environments.

Axiom update_one_empty : forall A x (v : A),
(@empty A) [x <- v] = (@empty A).

Update_one with single.

Axiom update_one_single : forall A x y (v w : A),
  x = y ->
  (x ∶ v) [y <- w] = (x ∶ w).
Axiom update_one_single_neq : forall A x y (v w : A),
  x <> y ->
  (x ∶ v) [y <- w] = (x ∶ v).

Update_one and concatenation.

Axiom update_one_concat_r : forall A x (v : A) (E F : gen_env A),
  x ∈ F ->
  (E & F) [x <- v] = E & (F [x <- v]).
Axiom update_one_concat_l : forall A x (v : A) (E F : gen_env A),
  x ∉ F ->
  (E & F) [x <- v] = (E [x <- v]) & F.

Dom is unchanged by updating.

Axiom dom_update_one : forall A x (v : A) (E : gen_env A),
dom (E [x <- v]) = dom E.

Belongs commutes with update.

Axiom belongs_update_one : forall A x y (v : A) (E : gen_env A),
  y ∈ E ->
  y ∈ (E [x <- v]).
Axiom belongs_update_one_inv : forall A x y (v : A) (E : gen_env A),
  y ∈ (E [x <- v]) ->
  y ∈ E.

All_belongs commutes with update.

Axiom all_belongs_update_one : forall A x xs (v : A) (E : gen_env A),
  xs ⊂ E ->
  xs ⊂ (E [x <- v]).
Axiom all_belongs_update_one_inv : forall A x xs (v : A) (E : gen_env A),
  xs ⊂ (E [x <- v]) ->
  xs ⊂ E.

Notin commutes with update.

Axiom notin_update_one : forall A x y (v : A) (E : gen_env A),
  y ∉ E ->
  y ∉ (E [x <- v]).
Axiom notin_update_one_inv : forall A x y (v : A) (E : gen_env A),
  y ∉ (E [x <- v]) ->
  y ∉ E.

All_notin commutes with update.

Axiom all_notin_update_one : forall A x xs (v : A) (E : gen_env A),
  xs ⊄ E ->
  xs ⊄ (E [x <- v]).
Axiom all_notin_update_one_inv : forall A x xs (v : A) (E : gen_env A),
  xs ⊄ (E [x <- v]) ->
  xs ⊄ E.

Update is identity when the domains are disjoints.

Axiom update_one_notin : forall A x (v : A) (E : gen_env A),
x ∉ E ->
E [x <- v] = E.

Update commutes with map.

Axiom map_update_one : forall A B (f : A -> B) x (v : A) (E : gen_env A),
map f (E [x <- v]) = (map f E) [x <- f v].

Ok commutes with update.

Axiom ok_update_one : forall A x (v : A) (E : gen_env A),
  ok E ->
  ok (E [x <- v]).
Axiom ok_update_one_inv : forall A x (v : A) (E : gen_env A),
  ok (E [x <- v]) ->
  ok E.

Properties of update

Update is identity in presence of empty environments.

Axiom update_empty_r : forall A (E : gen_env A),
E ::= (@empty A) = E.
Axiom update_empty_l : forall A (E : gen_env A),
(@empty A) ::= E = (@empty A).

Update with single.

Axiom update_update_one : forall A x (v : A) (E : gen_env A),
  E ::= (x ∶ v) = E [x <- v].
Axiom update_single_single : forall A x y (v w : A),
  x = y ->
  (x ∶ v) ::= (y ∶ w) = (x ∶ w).
Axiom update_single_single_neq : forall A x y (v w : A),
  x <> y ->
  (x ∶ v) ::= (y ∶ w) = (x ∶ v).

Update commutes with concatenation on the right.

Axiom update_concat_r : forall A (E F G : gen_env A),
E ::= (F & G) = (E ::= F) ::= G.

Dom is unchanged by updating.

Axiom dom_update : forall A (E F : gen_env A),
dom (E ::= F) = dom E.

Belongs commutes with update.

Axiom belongs_update : forall A x (E F : gen_env A),
  x ∈ E ->
  x ∈ (E ::= F).
Axiom belongs_update_inv : forall A x (E F : gen_env A),
  x ∈ (E ::= F) ->
  x ∈ E.

All_belongs commutes with update.

Axiom all_belongs_update : forall A xs (E F : gen_env A),
  xs ⊂ E ->
  xs ⊂ (E ::= F).
Axiom all_belongs_update_inv : forall A xs (E F : gen_env A),
  xs ⊂ (E ::= F) ->
  xs ⊂ E.

Notin commutes with update.

Axiom notin_update : forall A x (E F : gen_env A),
  x ∉ E ->
  x ∉ (E ::= F).
Axiom notin_update_inv : forall A x (E F : gen_env A),
  x ∉ (E ::= F) ->
  x ∉ E.

All_notin commutes with update.

Axiom all_notin_update : forall A xs (E F : gen_env A),
  xs ⊄ E ->
  xs ⊄ (E ::= F).
Axiom all_notin_update_inv : forall A xs (E F : gen_env A),
  xs ⊄ (E ::= F) ->
  xs ⊄ E.

Update is identity when the domains are disjoints.

Axiom update_notin : forall A (E F : gen_env A),
(dom F) ⊄ E ->
E ::= F = E.

Update commutes with map.

Axiom map_update : forall A B (f : A -> B) (E F : gen_env A),
map f (E ::= F) = (map f E) ::= (map f F).

Ok commutes with update.

Axiom ok_update : forall A (E F : gen_env A),
  ok E ->
  ok (E ::= F).
Axiom ok_update_inv : forall A (E F : gen_env A),
  ok (E ::= F) ->
  ok E.

Properties of remove

Remove is identity on empty environments.

Axiom remove_empty : forall A x,
(@empty A) ∖ {x} = (@empty A).

Remove on singular.

Axiom remove_single_eq : forall A x y (v : A),
  x = y ->
  (x ∶ v) ∖ {y} = (@empty A).
Axiom remove_single_neq : forall A x y (v : A),
  x <> y ->
  (x ∶ v) ∖ {y} = (x ∶ v).

Remove and notin and belongs.

Axiom remove_notin : forall A x (E : gen_env A),
  x ∉ E ->
  E ∖ {x} = E.
Axiom notin_remove_notin : forall A x y (E : gen_env A),
  x ∉ E ->
  x ∉ (E ∖ {y}).
Axiom all_notin_remove_notin : forall A xs y (E : gen_env A),
  xs ⊄ E ->
  xs ⊄ (E ∖ {y}).
Axiom belongs_remove : forall A x y (E : gen_env A),
  x <> y -> x ∈ E ->
  x ∈ (E ∖ {y}).
Axiom belongs_remove_inv : forall A x y (E : gen_env A),
  ok E ->
  x ∈ (E ∖ {y}) -> x <> y.

Remove and concatenation.

Axiom remove_belongs_concat_r : forall A x (E F : gen_env A),
  x ∈ F ->
  (E & F) ∖ {x} = E & (F ∖ {x}).
Axiom remove_belongs_concat_l : forall A x (E F : gen_env A),
  x ∉ F ->
  (E & F) ∖ {x} = (E ∖ {x}) & F.

Remove and belongs and all_belongs.

Axiom remove_ok_notin : forall A x (E : gen_env A),
  ok E ->
  x ∉ (E ∖ {x}).
Axiom remove_all_belongs : forall A x xs (F : gen_env A),
  ¬ List.In x xs -> (x :: xs) ⊂ F ->
  xs ⊂ (F ∖ {x}).

Remove commutes with map and updating.

Axiom remove_map : forall A B (f : A -> B) (E : gen_env A) x,
  (map f E) ∖ {x} = map f (E ∖ {x}).
Axiom remove_update : forall A x (E F : gen_env A),
  ok E ->
  (E ::= F) ∖ {x} = (E ∖ {x}) ::= F.
Axiom remove_update_eq : forall A x y (v : A) (E : gen_env A),
  x = y ->
  (E ::= (y ∶ v)) ∖ {x} = E ∖ {x}.

Ok and remove.

Axiom ok_remove : forall A x (E : gen_env A),
ok E ->
ok (E ∖ {x}).

Properties of all_remove

All_remove and remove.

Axiom all_remove_remove : forall A x xs (E : gen_env A),
E ∖ (x :: xs) = (E ∖ {x}) ∖ xs.

All_remove is identity on empty environments.

Axiom all_remove_empty : forall A xs,
(@empty A) ∖ xs = (@empty A).
Axiom all_remove_nil : forall A (E : gen_env A),
E ∖ nil = E.

All_remove on singular.

Axiom all_remove_single_in : forall A x xs (v : A),
  List.In x xs ->
  (x ∶ v) ∖ xs = (@empty A).
Axiom all_remove_single_not_in : forall A x xs (v : A),
  ¬ List.In x xs ->
  (x ∶ v) ∖ xs = (x ∶ v).

All_remove on singulars.

Axiom all_remove_singles_in : forall A xs ys (vs : list A),
  xs = ys -> length xs = length vs ->
  (xs ∷ vs) ∖ ys = (@empty A).
Axiom all_remove_singles_not_in : forall A xs ys (vs : list A),
  List.Forall (fun x => ¬ List.In x xs) ys ->
  (xs ∷ vs) ∖ ys = (xs ∷ vs).

All_remove and notin.

Axiom all_remove_notin : forall A xs (E : gen_env A),
  xs ⊄ E ->
  E ∖ xs = E.
Axiom notin_all_remove_notin : forall A x ys (E : gen_env A),
  x ∉ E ->
  x ∉ (E ∖ ys).
Axiom all_notin_all_remove_notin : forall A xs ys (E : gen_env A),
  xs ⊄ E ->
  xs ⊄ (E ∖ ys).

Remove and all_notin.

Axiom all_remove_ok_notin : forall A xs (E : gen_env A),
ok E ->
xs ⊄ (E ∖ xs).

All_remove and concatenation.

Axiom all_remove_belongs_concat_r : forall A xs (E F : gen_env A),
  List.NoDup xs ->
  xs ⊂ F ->
  (E & F) ∖ xs = E & (F ∖ xs).
Axiom all_remove_belongs_concat_l : forall A xs (E F : gen_env A),
  xs ⊄ F ->
  (E & F) ∖ xs = (E ∖ xs) & F.

All_remove commutes with map and updating.

Axiom all_remove_map : forall A B (f : A -> B) (E : gen_env A) xs,
  (map f E) ∖ xs = map f (E ∖ xs).
Axiom all_remove_update : forall A xs (E F : gen_env A),
  ok E ->
  (E ::= F) ∖ xs = (E ∖ xs) ::= F.

Ok and all_remove.

Axiom ok_all_remove : forall A xs (E : gen_env A),
ok E ->
ok (E ∖ xs).

Properties of ok

Ok stands for empty and singular environments.

Axiom ok_empty : forall A,
ok (@empty A).
Axiom ok_single : forall A x (v : A),
ok (x ∶ v).

Ok stands if there is no variable duplication.

Axiom ok_singles : forall A xs (vs : list A),
  List.NoDup xs ->
  ok (xs ∷ vs).
Axiom ok_singles_inv : forall A xs (vs : list A),
  length xs = length vs ->
  ok (xs ∷ vs) ->
  List.NoDup xs.

Ok stands on concatenation when domains are disjoints.

Axiom ok_concat : forall A (E F : gen_env A),
  ok E -> ok F ->
  (dom E) ⊄ F -> (dom F) ⊄ E ->
  ok (E & F).
Axiom ok_concat_inv : forall A (E F : gen_env A),
  ok (E & F) ->
  ok E ∧ ok F ∧ (dom E) ⊄ F ∧ (dom F) ⊄ E.
Axiom ok_concat_comm : forall A (E F : gen_env A),
  ok (E & F) ->
  ok (F & E).

Belongs and concat with ok.

Axiom belongs_ok_concat_inv_l : forall A x (F G : gen_env A),
  ok (F & G) ->
  x ∈ F ->
  x ∉ G.
Axiom belongs_ok_concat_inv_r : forall A x (F G : gen_env A),
  ok (F & G) ->
  x ∈ G ->
  x ∉ F.
Axiom concat_not_ok : forall A x (F G : gen_env A),
  x ∈ F -> x ∈ G ->
  ¬ ok (F & G).

Additional properties when ok stands.

Update commutes with concatenation on the left.

Axiom update_concat_l : forall A (E F G : gen_env A),
ok (E & F) ->
(E & F) ::= G = (E ::= G) & (F ::= G).

End Properties.

End CoreGenericEnvironmentType.