Library Generic_Env
Require Import Generic_Var.
Module Type Generic_Env_Type (Var : Generic_Var).
Require Import List.
Require Sets.Image.
Import Var.
gen_env A is an environment that binds variables to values of type A.
The decidability of equality on keys (variables) is imported from Var.
Empty environment.
Environment build upon explicit associations.
Concatenation of environment (the second one binds first).
The main operation on environment, get the type of a variable.
Domain and image of an environment.
Check the occurence of variable(s) in an environment.
Parameter belongs : TVar -> gen_env A -> Prop.
Parameter all_belongs : list TVar -> gen_env A -> Prop.
Parameter all_belongs : list TVar -> gen_env A -> Prop.
Check the non-occurence of variable(s) in an environment.
Map function on types.
Updating of types with bindings of another environment.
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.
End Core_Definitions.
Parameter all_remove : list TVar -> gen_env A -> gen_env A.
End Core_Definitions.
x ∶ v is the notation for a singleton environment mapping x to v.
xs ∷ vs is the notation for an environment mapping xs to vs.
E & F is the notation for concatenation of E and F.
E ∖ { x } is the notation for removing x from E.
E ∖ xs is the notation for removing xs from E.
E ::= F is the notation for updating of E with F.
x ∈ E to be read x is bound in E.
xs ⊂ E to be read xs are bound in E.
x '∉' E to be read x is unbound in E.
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.
Section Prop_Definitions.
Variable A : Type.
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 A)
| ok_cons : forall x v F, ok F ∧ x ∉ F -> ok (F & (x ∶ v))
.
| ok_nil : ok (@empty A)
| ok_cons : forall x v F, ok F ∧ x ∉ F -> ok (F & (x ∶ v))
.
Asserts the binding of a variable in an environment.
Asserts the inclusion of an environment in another.
Equivalence on environments
x '∹' v '⋲' E to be read x is bound to v in E.
E '⊏' F to be read F all_binds E, i.e. E is included in F.
E '≍' F to be read F is equivalent to E, i.e. E binds as F.
Notation "E '≍' F" := (eq E F)
(at level 68) : 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.
Section Properties.
Variable A B : Type.
Implicit Types x y : TVar.
Implicit Types xs ys : list TVar.
Implicit Types v w : A.
Implicit Types vs ws : list A.
Implicit Types E F G : gen_env A.
Implicit Types f g : A -> B.
Induction scheme over environments.
Parameter env_ind : forall P : gen_env A -> Prop,
(P (@empty A)) ->
(forall E x v, P E -> P (E & (x ∶ v))) ->
(forall E, P E).
(P (@empty A)) ->
(forall E x v, P E -> P (E & (x ∶ v))) ->
(forall E, P E).
Environment built from lists.
Parameter singles_empty :
nil ∷ nil = (@empty A).
Parameter singles_cons : forall x xs v vs,
(x :: xs) ∷ (v :: vs) = (xs ∷ vs) & (x ∶ v).
nil ∷ nil = (@empty A).
Parameter singles_cons : forall x xs v vs,
(x :: xs) ∷ (v :: vs) = (xs ∷ vs) & (x ∶ v).
Concatenation admits empty as neutral element, and is associative.
Parameter concat_empty_r : forall E,
E & (@empty A) = E.
Parameter concat_empty_l : forall E,
(@empty A) & E = E.
Parameter concat_assoc : forall E F G,
E & (F & G) = (E & F) & G.
E & (@empty A) = E.
Parameter concat_empty_l : forall E,
(@empty A) & E = E.
Parameter concat_assoc : forall E F G,
E & (F & G) = (E & F) & G.
Get is None on empty.
Get is Some when it binds.
Get is decidable.
Dom builds a list.
Parameter dom_empty :
dom (@empty A) = nil.
Parameter dom_empty_inv : forall E,
dom (E) = nil ->
E = (@empty A).
Parameter dom_single : forall x v,
dom (x ∶ v) = (x :: nil).
Parameter dom_singles : forall xs vs,
length xs = length vs ->
dom (xs ∷ vs) = xs.
Parameter dom_singles_incl : forall xs vs,
List.incl (dom (xs ∷ vs)) xs.
Parameter dom_concat : forall E F,
dom (E & F) = List.app (dom F) (dom E).
dom (@empty A) = nil.
Parameter dom_empty_inv : forall E,
dom (E) = nil ->
E = (@empty A).
Parameter dom_single : forall x v,
dom (x ∶ v) = (x :: nil).
Parameter dom_singles : forall xs vs,
length xs = length vs ->
dom (xs ∷ vs) = xs.
Parameter dom_singles_incl : forall xs vs,
List.incl (dom (xs ∷ vs)) xs.
Parameter dom_concat : forall E F,
dom (E & F) = List.app (dom F) (dom E).
Img builds a list.
Parameter img_empty :
img (@empty A) = nil.
Parameter img_empty_inv : forall E,
img (E) = nil ->
E = (@empty A).
Parameter img_single : forall x v,
img (x ∶ v) = v :: nil.
Parameter img_singles : forall xs vs,
length xs = length vs ->
img (xs ∷ vs) = vs.
Parameter img_singles_incl : forall xs vs,
List.incl (img (xs ∷ vs)) vs.
Parameter img_concat : forall E F,
img (E & F) = List.app (img F) (img E).
img (@empty A) = nil.
Parameter img_empty_inv : forall E,
img (E) = nil ->
E = (@empty A).
Parameter img_single : forall x v,
img (x ∶ v) = v :: nil.
Parameter img_singles : forall xs vs,
length xs = length vs ->
img (xs ∷ vs) = vs.
Parameter img_singles_incl : forall xs vs,
List.incl (img (xs ∷ vs)) vs.
Parameter img_concat : forall E F,
img (E & F) = List.app (img F) (img E).
Dom and img builds identity.
Parameter dom_img_id : forall E,
(dom E) ∷ (img E) = E.
Parameter length_dom_img_eq : forall E,
length (dom E) = length (img E).
(dom E) ∷ (img E) = E.
Parameter length_dom_img_eq : forall E,
length (dom E) = length (img E).
Belongs is false on empty environments.
Belongs in singular(s).
Parameter belongs_single : forall x y v,
x = y ->
x ∈ (y ∶ v).
Parameter belongs_single_inv : forall x y v,
x ∈ (y ∶ v) ->
x = y.
Parameter belongs_singles : forall x xs vs,
length xs = length vs ->
List.In x xs ->
x ∈ (xs ∷ vs).
Parameter belongs_singles_inv : forall x xs vs,
length xs = length vs ->
x ∈ (xs ∷ vs) ->
List.In x xs.
x = y ->
x ∈ (y ∶ v).
Parameter belongs_single_inv : forall x y v,
x ∈ (y ∶ v) ->
x = y.
Parameter belongs_singles : forall x xs vs,
length xs = length vs ->
List.In x xs ->
x ∈ (xs ∷ vs).
Parameter belongs_singles_inv : forall x xs vs,
length xs = length vs ->
x ∈ (xs ∷ vs) ->
List.In x xs.
Belongs and concatenation.
Parameter belongs_concat_l : forall x F G,
x ∈ F ->
x ∈ (F & G).
Parameter belongs_concat_r : forall x F G,
x ∈ F ->
x ∈ (G & F).
Parameter belongs_concat_inv : forall x F G,
x ∈ (F & G) ->
x ∈ F ∨ x ∈ G.
x ∈ F ->
x ∈ (F & G).
Parameter belongs_concat_r : forall x F G,
x ∈ F ->
x ∈ (G & F).
Parameter belongs_concat_inv : forall x F G,
x ∈ (F & G) ->
x ∈ F ∨ x ∈ G.
Belongs and dom.
Parameter belongs_dom : forall x E,
x ∈ E ->
List.In x (dom E).
Parameter belongs_dom_inv : forall x E,
List.In x (dom E) ->
x ∈ E.
x ∈ E ->
List.In x (dom E).
Parameter belongs_dom_inv : forall x E,
List.In x (dom E) ->
x ∈ E.
All_belongs and belongs.
Parameter all_belongs_belongs : forall x xs E,
(x :: xs) ⊂ E ->
x ∈ E ∧ xs ⊂ E.
Parameter belongs_all_belongs : forall x xs E,
x ∈ E ∧ xs ⊂ E ->
(x :: xs) ⊂ E.
(x :: xs) ⊂ E ->
x ∈ E ∧ xs ⊂ E.
Parameter belongs_all_belongs : forall x xs E,
x ∈ E ∧ xs ⊂ E ->
(x :: xs) ⊂ E.
All_belongs is false on empty environments.
Parameter all_belongs_empty : forall xs,
xs ⊂ (@empty A) ->
xs = nil.
Parameter all_belongs_nil : forall E,
nil ⊂ E.
xs ⊂ (@empty A) ->
xs = nil.
Parameter all_belongs_nil : forall E,
nil ⊂ E.
All_belongs in singular(s).
Parameter all_belongs_single : forall xs y v,
xs = y :: nil ->
xs ⊂ (y ∶ v).
Parameter all_belongs_single_inv : forall xs y v,
length xs = 1 ->
xs ⊂ (y ∶ v) ->
xs = y :: nil.
Parameter all_belongs_singles : forall xs ys vs,
length ys = length vs ->
List.incl xs ys ->
xs ⊂ (ys ∷ vs).
Parameter all_belongs_singles_inv : forall xs ys vs,
xs ⊂ (ys ∷ vs) ->
List.incl xs ys.
xs = y :: nil ->
xs ⊂ (y ∶ v).
Parameter all_belongs_single_inv : forall xs y v,
length xs = 1 ->
xs ⊂ (y ∶ v) ->
xs = y :: nil.
Parameter all_belongs_singles : forall xs ys vs,
length ys = length vs ->
List.incl xs ys ->
xs ⊂ (ys ∷ vs).
Parameter all_belongs_singles_inv : forall xs ys vs,
xs ⊂ (ys ∷ vs) ->
List.incl xs ys.
All_belongs and concatenation.
Parameter all_belongs_concat_l : forall xs F G,
xs ⊂ F ->
xs ⊂ (F & G).
Parameter all_belongs_concat_r : forall xs F G,
xs ⊂ F ->
xs ⊂ (G & F).
xs ⊂ F ->
xs ⊂ (F & G).
Parameter all_belongs_concat_r : forall xs F G,
xs ⊂ F ->
xs ⊂ (G & F).
All_belongs and dom.
Parameter all_belongs_dom : forall xs E,
xs ⊂ E ->
List.incl xs (dom E).
Parameter all_belongs_dom_inv : forall xs E F,
List.incl xs (dom E) ->
xs ⊂ E.
xs ⊂ E ->
List.incl xs (dom E).
Parameter all_belongs_dom_inv : forall xs E F,
List.incl xs (dom E) ->
xs ⊂ E.
Notin and belongs.
Parameter notin_belongs : forall x E,
x ∉ E ->
¬ x ∈ E.
Parameter belongs_notin : forall x E,
x ∈ E ->
¬ x ∉ E.
Parameter notin_belongs_neq : forall x y E,
x ∈ E -> y ∉ E ->
x <> y.
x ∉ E ->
¬ x ∈ E.
Parameter belongs_notin : forall x E,
x ∈ E ->
¬ x ∉ E.
Parameter notin_belongs_neq : forall x y E,
x ∈ E -> y ∉ E ->
x <> y.
Notin is true on empty environments.
Notin in singular(s).
Parameter notin_single : forall x y v,
x <> y ->
x ∉ (y ∶ v).
Parameter notin_single_inv : forall x y v,
x ∉ (y ∶ v) ->
x <> y.
Parameter notin_singles : forall x xs vs,
¬ List.In x xs ->
x ∉ (xs ∷ vs).
Parameter notin_singles_inv : forall x xs vs,
length xs = length vs ->
x ∉ (xs ∷ vs) ->
¬ List.In x xs.
x <> y ->
x ∉ (y ∶ v).
Parameter notin_single_inv : forall x y v,
x ∉ (y ∶ v) ->
x <> y.
Parameter notin_singles : forall x xs vs,
¬ List.In x xs ->
x ∉ (xs ∷ vs).
Parameter notin_singles_inv : forall x xs vs,
length xs = length vs ->
x ∉ (xs ∷ vs) ->
¬ List.In x xs.
Notin and concatenation.
Parameter notin_concat : forall x F G,
x ∉ F -> x ∉ G ->
x ∉ (F & G).
Parameter notin_concat_inv : forall x F G,
x ∉ (F & G) ->
x ∉ F ∧ x ∉ G.
x ∉ F -> x ∉ G ->
x ∉ (F & G).
Parameter notin_concat_inv : forall x F G,
x ∉ (F & G) ->
x ∉ F ∧ x ∉ G.
Notin and dom.
Parameter notin_dom : forall x E,
x ∉ E ->
¬ List.In x (dom E).
Parameter notin_dom_inv : forall x E F,
¬ List.In x (dom E) ->
x ∉ E.
x ∉ E ->
¬ List.In x (dom E).
Parameter notin_dom_inv : forall x E F,
¬ List.In x (dom E) ->
x ∉ E.
All_notin is true on empty lists.
All_notin and notin.
Parameter all_notin_notin : forall x xs E,
(x :: xs) ⊄ E ->
x ∉ E ∧ xs ⊄ E.
Parameter notin_all_notin : forall x xs E,
x ∉ E ∧ xs ⊄ E ->
(x :: xs) ⊄ E.
(x :: xs) ⊄ E ->
x ∉ E ∧ xs ⊄ E.
Parameter notin_all_notin : forall x xs E,
x ∉ E ∧ xs ⊄ E ->
(x :: xs) ⊄ E.
All_notin and belongs.
All_notin is true on empty environments.
All_notin in singular(s).
Parameter all_notin_single : forall xs y v,
¬ List.In y xs ->
xs ⊄ (y ∶ v).
Parameter all_notin_single_inv : forall xs y v,
xs ⊄ (y ∶ v) ->
¬ List.In y xs.
Parameter all_notin_singles : forall xs ys vs,
List.Forall (fun x => ¬ List.In x ys) xs ->
xs ⊄ (ys ∷ vs).
Parameter all_notin_singles_inv : forall xs ys vs,
length ys = length vs ->
xs ⊄ (ys ∷ vs) ->
List.Forall (fun x => ¬ List.In x ys) xs.
¬ List.In y xs ->
xs ⊄ (y ∶ v).
Parameter all_notin_single_inv : forall xs y v,
xs ⊄ (y ∶ v) ->
¬ List.In y xs.
Parameter all_notin_singles : forall xs ys vs,
List.Forall (fun x => ¬ List.In x ys) xs ->
xs ⊄ (ys ∷ vs).
Parameter all_notin_singles_inv : forall xs ys vs,
length ys = length vs ->
xs ⊄ (ys ∷ vs) ->
List.Forall (fun x => ¬ List.In x ys) xs.
All_notin and concatenation.
Parameter all_notin_concat : forall xs F G,
xs ⊄ F -> xs ⊄ G ->
xs ⊄ (F & G).
Parameter all_notin_concat_inv : forall xs F G,
xs ⊄ (F & G) ->
xs ⊄ F ∧ xs ⊄ G.
xs ⊄ F -> xs ⊄ G ->
xs ⊄ (F & G).
Parameter all_notin_concat_inv : forall xs F G,
xs ⊄ (F & G) ->
xs ⊄ F ∧ xs ⊄ G.
All_notin and dom.
Parameter all_notin_dom : forall xs E,
xs ⊄ E ->
List.Forall (fun x => ¬ List.In x (dom E)) xs.
Parameter all_notin_dom_inv : forall xs E,
List.Forall (fun x => ¬ List.In x (dom E)) xs ->
xs ⊄ E.
xs ⊄ E ->
List.Forall (fun x => ¬ List.In x (dom E)) xs.
Parameter all_notin_dom_inv : forall xs E,
List.Forall (fun x => ¬ List.In x (dom E)) xs ->
xs ⊄ E.
Ok is equivalent to the non-duplication of the domain.
Ok stands for empty and singular environments.
Ok stands if there is no variable duplication.
Parameter ok_singles : forall xs vs,
List.NoDup xs ->
ok (xs ∷ vs).
Parameter ok_singles_inv : forall xs vs,
length xs = length vs ->
ok (xs ∷ vs) ->
List.NoDup xs.
List.NoDup xs ->
ok (xs ∷ vs).
Parameter ok_singles_inv : forall xs vs,
length xs = length vs ->
ok (xs ∷ vs) ->
List.NoDup xs.
Ok stands on concatenation when domains are disjoints.
Parameter ok_concat : forall E F,
ok E -> ok F ->
(dom E) ⊄ F -> (dom F) ⊄ E ->
ok (E & F).
Parameter ok_concat_inv : forall E F,
ok (E & F) ->
ok E ∧ ok F ∧ (dom E) ⊄ F ∧ (dom F) ⊄ E.
Parameter ok_concat_comm : forall E F,
ok (E & F) ->
ok (F & E).
ok E -> ok F ->
(dom E) ⊄ F -> (dom F) ⊄ E ->
ok (E & F).
Parameter ok_concat_inv : forall E F,
ok (E & F) ->
ok E ∧ ok F ∧ (dom E) ⊄ F ∧ (dom F) ⊄ E.
Parameter ok_concat_comm : forall E F,
ok (E & F) ->
ok (F & E).
Belongs and concat with ok.
Parameter belongs_ok_concat_inv_l : forall x F G,
ok (F & G) ->
x ∈ F ->
x ∉ G.
Parameter belongs_ok_concat_inv_r : forall x F G,
ok (F & G) ->
x ∈ G ->
x ∉ F.
Parameter concat_not_ok : forall x F G,
x ∈ F -> x ∈ G ->
¬ ok (F & G).
ok (F & G) ->
x ∈ F ->
x ∉ G.
Parameter belongs_ok_concat_inv_r : forall x F G,
ok (F & G) ->
x ∈ G ->
x ∉ F.
Parameter concat_not_ok : forall x F G,
x ∈ F -> x ∈ G ->
¬ ok (F & G).
Ok and dom
Parameter ok_dom : forall E,
List.NoDup (dom E) -> ok E.
Parameter ok_dom_inv : forall E,
ok E -> List.NoDup (dom E).
List.NoDup (dom E) -> ok E.
Parameter ok_dom_inv : forall E,
ok E -> List.NoDup (dom E).
Map is applied on type(s).
Parameter map_empty : forall f,
map f (@empty A) = (@empty B).
Parameter map_single : forall f x v,
map f (x ∶ v) = x ∶ (f v).
Parameter map_singles : forall f xs vs,
map f (xs ∷ vs) = xs ∷ (List.map f vs).
map f (@empty A) = (@empty B).
Parameter map_single : forall f x v,
map f (x ∶ v) = x ∶ (f v).
Parameter map_singles : forall f xs vs,
map f (xs ∷ vs) = xs ∷ (List.map f vs).
Map commutes with concatenation.
Dom is unchanged by map.
Belongs commutes with map.
Parameter belongs_map : forall x E f,
x ∈ E ->
x ∈ (map f E).
Parameter belongs_map_inv : forall x E f,
x ∈ (map f E) ->
x ∈ E.
x ∈ E ->
x ∈ (map f E).
Parameter belongs_map_inv : forall x E f,
x ∈ (map f E) ->
x ∈ E.
All_belongs commutes with map.
Parameter all_belongs_map : forall xs E f,
xs ⊂ E ->
xs ⊂ (map f E).
Parameter all_belongs_map_inv : forall xs E f,
xs ⊂ (map f E) ->
xs ⊂ E.
xs ⊂ E ->
xs ⊂ (map f E).
Parameter all_belongs_map_inv : forall xs E f,
xs ⊂ (map f E) ->
xs ⊂ E.
Notin commutes with map.
Parameter notin_map : forall x E f,
x ∉ E ->
x ∉ (map f E).
Parameter notin_map_inv : forall x E f,
x ∉ (map f E) ->
x ∉ E.
x ∉ E ->
x ∉ (map f E).
Parameter notin_map_inv : forall x E f,
x ∉ (map f E) ->
x ∉ E.
All_notin commutes with map.
Parameter all_notin_map : forall xs E f,
xs ⊄ E ->
xs ⊄ (map f E).
Parameter all_notin_map_inv : forall xs E f,
xs ⊄ (map f E) ->
xs ⊄ E.
xs ⊄ E ->
xs ⊄ (map f E).
Parameter all_notin_map_inv : forall xs E f,
xs ⊄ (map f E) ->
xs ⊄ E.
Ok commutes with map.
Parameter ok_map : forall E f,
ok E ->
ok (map f E).
Parameter ok_map_inv : forall E f,
ok (map f E) ->
ok E.
ok E ->
ok (map f E).
Parameter ok_map_inv : forall E f,
ok (map f E) ->
ok E.
Update is identity in presence of empty environments.
Parameter update_empty_r : forall E,
E ::= (@empty A) = E.
Parameter update_empty_l : forall E,
(@empty A) ::= E = (@empty A).
E ::= (@empty A) = E.
Parameter update_empty_l : forall E,
(@empty A) ::= E = (@empty A).
Update with single.
Parameter update_single : forall x v y w,
x = y ->
(x ∶ v) ::= (y ∶ w) = (x ∶ w).
Parameter update_single_neq : forall x v y w,
x <> y ->
(x ∶ v) ::= (y ∶ w) = (x ∶ v).
x = y ->
(x ∶ v) ::= (y ∶ w) = (x ∶ w).
Parameter update_single_neq : forall x v y w,
x <> y ->
(x ∶ v) ::= (y ∶ w) = (x ∶ v).
Update commutes with concatenation on the right.
Dom is unchanged by updating.
Belongs commutes with update.
Parameter belongs_update : forall x E F,
x ∈ E ->
x ∈ (E ::= F).
Parameter belongs_update_inv : forall x E F,
x ∈ (E ::= F) ->
x ∈ E.
x ∈ E ->
x ∈ (E ::= F).
Parameter belongs_update_inv : forall x E F,
x ∈ (E ::= F) ->
x ∈ E.
All_belongs commutes with update.
Parameter all_belongs_update : forall xs E F,
xs ⊂ E ->
xs ⊂ (E ::= F).
Parameter all_belongs_update_inv : forall xs E F,
xs ⊂ (E ::= F) ->
xs ⊂ E.
xs ⊂ E ->
xs ⊂ (E ::= F).
Parameter all_belongs_update_inv : forall xs E F,
xs ⊂ (E ::= F) ->
xs ⊂ E.
Notin commutes with update.
Parameter notin_update : forall x E F,
x ∉ E ->
x ∉ (E ::= F).
Parameter notin_update_inv : forall x E F,
x ∉ (E ::= F) ->
x ∉ E.
x ∉ E ->
x ∉ (E ::= F).
Parameter notin_update_inv : forall x E F,
x ∉ (E ::= F) ->
x ∉ E.
All_notin commutes with update.
Parameter all_notin_update : forall xs E F,
xs ⊄ E ->
xs ⊄ (E ::= F).
Parameter all_notin_update_inv : forall xs E F,
xs ⊄ (E ::= F) ->
xs ⊄ E.
xs ⊄ E ->
xs ⊄ (E ::= F).
Parameter all_notin_update_inv : forall xs E F,
xs ⊄ (E ::= F) ->
xs ⊄ E.
Update is identity when the domains are disjoints.
Update commutes with map.
Ok commutes with update.
Parameter ok_update : forall E F,
ok E ->
ok (E ::= F).
Parameter ok_update_inv : forall E F,
ok (E ::= F) ->
ok E.
ok E ->
ok (E ::= F).
Parameter ok_update_inv : forall E F,
ok (E ::= F) ->
ok E.
Update commutes with concatenation on the left.
Remove is identity on empty environments.
Remove on singular.
Parameter remove_single_eq : forall x v y,
x = y ->
(x ∶ v) ∖ {y} = (@empty A).
Parameter remove_single_not_eq : forall x v y,
x <> y ->
(x ∶ v) ∖ {y} = (x ∶ v).
x = y ->
(x ∶ v) ∖ {y} = (@empty A).
Parameter remove_single_not_eq : forall x v y,
x <> y ->
(x ∶ v) ∖ {y} = (x ∶ v).
Remove and notin and belongs.
Parameter remove_notin : forall x E,
x ∉ E ->
E ∖ {x} = E.
Parameter notin_remove_notin : forall x y E,
x ∉ E ->
x ∉ (E ∖ {y}).
Parameter all_notin_remove_notin : forall xs y E,
xs ⊄ E ->
xs ⊄ (E ∖ {y}).
Parameter belongs_remove : forall x y E,
x <> y -> x ∈ E ->
x ∈ (E ∖ {y}).
Parameter belongs_remove_inv : forall x y E,
ok E ->
x ∈ (E ∖ {y}) -> x <> y.
x ∉ E ->
E ∖ {x} = E.
Parameter notin_remove_notin : forall x y E,
x ∉ E ->
x ∉ (E ∖ {y}).
Parameter all_notin_remove_notin : forall xs y E,
xs ⊄ E ->
xs ⊄ (E ∖ {y}).
Parameter belongs_remove : forall x y E,
x <> y -> x ∈ E ->
x ∈ (E ∖ {y}).
Parameter belongs_remove_inv : forall x y E,
ok E ->
x ∈ (E ∖ {y}) -> x <> y.
Remove and concatenation.
Parameter remove_belongs_concat_r : forall x E F,
x ∈ F ->
(E & F) ∖ {x} = E & (F ∖ {x}).
Parameter remove_belongs_concat_l : forall x E F,
x ∉ F ->
(E & F) ∖ {x} = (E ∖ {x}) & F.
x ∈ F ->
(E & F) ∖ {x} = E & (F ∖ {x}).
Parameter remove_belongs_concat_l : forall x E F,
x ∉ F ->
(E & F) ∖ {x} = (E ∖ {x}) & F.
Remove and belongs and all_belongs.
Parameter remove_ok_notin : forall x E,
ok E ->
x ∉ (E ∖ {x}).
Parameter remove_all_belongs : forall x xs F,
¬ List.In x xs -> (x :: xs) ⊂ F ->
xs ⊂ (F ∖ {x}).
ok E ->
x ∉ (E ∖ {x}).
Parameter remove_all_belongs : forall x xs F,
¬ List.In x xs -> (x :: xs) ⊂ F ->
xs ⊂ (F ∖ {x}).
Remove commutes with map and updating.
Parameter remove_map : forall f E x,
(map f E) ∖ {x} = map f (E ∖ {x}).
Parameter remove_update : forall x E F,
ok E ->
(E ::= F) ∖ {x} = (E ∖ {x}) ::= F.
Parameter remove_update_eq : forall x y v E,
x = y ->
(E ::= (y ∶ v)) ∖ {x} = E ∖ {x}.
(map f E) ∖ {x} = map f (E ∖ {x}).
Parameter remove_update : forall x E F,
ok E ->
(E ::= F) ∖ {x} = (E ∖ {x}) ::= F.
Parameter remove_update_eq : forall x y v E,
x = y ->
(E ::= (y ∶ v)) ∖ {x} = E ∖ {x}.
Ok and remove.
All_remove and remove.
All_remove is identity on empty environments.
All_remove on singular.
Parameter all_remove_single_in : forall x v xs,
List.In x xs ->
(x ∶ v) ∖ xs = (@empty A).
Parameter all_remove_single_not_in : forall x v xs,
¬ List.In x xs ->
(x ∶ v) ∖ xs = (x ∶ v).
List.In x xs ->
(x ∶ v) ∖ xs = (@empty A).
Parameter all_remove_single_not_in : forall x v xs,
¬ List.In x xs ->
(x ∶ v) ∖ xs = (x ∶ v).
All_remove on singulars.
Parameter all_remove_singles_in : forall xs vs ys,
xs = ys -> length xs = length vs ->
(xs ∷ vs) ∖ ys = (@empty A).
Parameter all_remove_singles_not_in : forall xs vs ys,
List.Forall (fun x => ¬ List.In x xs) ys ->
(xs ∷ vs) ∖ ys = (xs ∷ vs).
xs = ys -> length xs = length vs ->
(xs ∷ vs) ∖ ys = (@empty A).
Parameter all_remove_singles_not_in : forall xs vs ys,
List.Forall (fun x => ¬ List.In x xs) ys ->
(xs ∷ vs) ∖ ys = (xs ∷ vs).
All_remove and notin.
Parameter all_remove_notin : forall xs E,
xs ⊄ E ->
E ∖ xs = E.
Parameter notin_all_remove_notin : forall x ys E,
x ∉ E ->
x ∉ (E ∖ ys).
Parameter all_notin_all_remove_notin : forall xs ys E,
xs ⊄ E ->
xs ⊄ (E ∖ ys).
xs ⊄ E ->
E ∖ xs = E.
Parameter notin_all_remove_notin : forall x ys E,
x ∉ E ->
x ∉ (E ∖ ys).
Parameter all_notin_all_remove_notin : forall xs ys E,
xs ⊄ E ->
xs ⊄ (E ∖ ys).
Remove and all_notin.
All_remove and concatenation.
Parameter all_remove_belongs_concat_r : forall xs E F,
List.NoDup xs ->
xs ⊂ F ->
(E & F) ∖ xs = E & (F ∖ xs).
Parameter all_remove_belongs_concat_l : forall xs E F,
xs ⊄ F ->
(E & F) ∖ xs = (E ∖ xs) & F.
List.NoDup xs ->
xs ⊂ F ->
(E & F) ∖ xs = E & (F ∖ xs).
Parameter all_remove_belongs_concat_l : forall xs E F,
xs ⊄ F ->
(E & F) ∖ xs = (E ∖ xs) & F.
All_remove commutes with map and updating.
Parameter all_remove_map : forall f E xs,
(map f E) ∖ xs = map f (E ∖ xs).
Parameter all_remove_update : forall xs E F,
ok E ->
(E ::= F) ∖ xs = (E ∖ xs) ::= F.
(map f E) ∖ xs = map f (E ∖ xs).
Parameter all_remove_update : forall xs E F,
ok E ->
(E ::= F) ∖ xs = (E ∖ xs) ::= F.
Ok and all_remove.
Binds and empty.
Binds on singular(s).
Parameter binds_single : forall x v y w,
x = y -> v = w ->
x ∹ v ⋲ (y ∶ w).
Parameter binds_single_inv : forall x v y w,
x ∹ v ⋲ (y ∶ w) ->
x = y ∧ v = w.
Parameter binds_singles : forall x v y w ys ws,
x = y -> v = w ->
x ∹ v ⋲ (y :: ys ∷ w :: ws).
Parameter binds_singles_inv : forall x v y w ys ws,
x ∹ v ⋲ (y :: ys ∷ w :: ws) ->
(x = y ∧ v = w) ∨ (x ∹ v ⋲ (ys ∷ ws)).
x = y -> v = w ->
x ∹ v ⋲ (y ∶ w).
Parameter binds_single_inv : forall x v y w,
x ∹ v ⋲ (y ∶ w) ->
x = y ∧ v = w.
Parameter binds_singles : forall x v y w ys ws,
x = y -> v = w ->
x ∹ v ⋲ (y :: ys ∷ w :: ws).
Parameter binds_singles_inv : forall x v y w ys ws,
x ∹ v ⋲ (y :: ys ∷ w :: ws) ->
(x = y ∧ v = w) ∨ (x ∹ v ⋲ (ys ∷ ws)).
Binds is functional.
Binds and concatenation.
Parameter binds_concat_r : forall x v F G,
x ∹ v ⋲ G ->
x ∹ v ⋲ (F & G).
Parameter binds_concat_l : forall x v F G,
x ∹ v ⋲ F ->
x ∉ G ->
x ∹ v ⋲ (F & G).
Parameter binds_concat_inv : forall x v F G,
x ∹ v ⋲ (F & G) ->
(x ∹ v ⋲ G) ∨ (x ∉ G ∧ x ∹ v ⋲ F).
x ∹ v ⋲ G ->
x ∹ v ⋲ (F & G).
Parameter binds_concat_l : forall x v F G,
x ∹ v ⋲ F ->
x ∉ G ->
x ∹ v ⋲ (F & G).
Parameter binds_concat_inv : forall x v F G,
x ∹ v ⋲ (F & G) ->
(x ∹ v ⋲ G) ∨ (x ∉ G ∧ x ∹ v ⋲ F).
Binds and belongs.
Parameter binds_belongs : forall x v F,
x ∹ v ⋲ F ->
x ∈ F.
Parameter belongs_binds : forall x F,
x ∈ F ->
exists v, x ∹ v ⋲ F.
x ∹ v ⋲ F ->
x ∈ F.
Parameter belongs_binds : forall x F,
x ∈ F ->
exists v, x ∹ v ⋲ F.
Binds and map.
Parameter binds_map : forall x v E f,
x ∹ v ⋲ E ->
x ∹ (f v) ⋲ (map f E).
Parameter binds_map_inv : forall x (w : B) E f,
x ∹ w ⋲ (map f E) ->
exists v, x ∹ v ⋲ E ∧ w = f v.
x ∹ v ⋲ E ->
x ∹ (f v) ⋲ (map f E).
Parameter binds_map_inv : forall x (w : B) E f,
x ∹ w ⋲ (map f E) ->
exists v, x ∹ v ⋲ E ∧ w = f v.
Binds and update.
Parameter binds_update_notin : forall x v F G,
x ∹ v ⋲ F ->
x ∉ G ->
x ∹ v ⋲ (F ::= G).
Parameter binds_update_in : forall x v F G,
x ∈ F ->
x ∹ v ⋲ G ->
x ∹ v ⋲ (F ::= G).
Parameter binds_update_self : forall x v F,
x ∈ F ->
x ∹ v ⋲ (F ::= (x ∶ v)).
Parameter binds_update_inv : forall x v F G,
x ∹ v ⋲ (F ::= G) ->
(x ∉ G ∧ x ∹ v ⋲ F) ∨ (x ∈ F ∧ x ∹ v ⋲ G).
x ∹ v ⋲ F ->
x ∉ G ->
x ∹ v ⋲ (F ::= G).
Parameter binds_update_in : forall x v F G,
x ∈ F ->
x ∹ v ⋲ G ->
x ∹ v ⋲ (F ::= G).
Parameter binds_update_self : forall x v F,
x ∈ F ->
x ∹ v ⋲ (F ::= (x ∶ v)).
Parameter binds_update_inv : forall x v F G,
x ∹ v ⋲ (F ::= G) ->
(x ∉ G ∧ x ∹ v ⋲ F) ∨ (x ∈ F ∧ x ∹ v ⋲ G).
Binds and remove.
Parameter binds_remove : forall x y v E,
x <> y -> x ∹ v ⋲ E ->
x ∹ v ⋲ (E ∖ {y}).
Parameter binds_remove_inv : forall x y v E,
x <> y -> x ∹ v ⋲ (E ∖ {y}) ->
x ∹ v ⋲ E.
Parameter binds_all_remove : forall x ys v E,
¬ List.In x ys -> x ∹ v ⋲ E ->
x ∹ v ⋲ (E ∖ ys).
Parameter binds_all_remove_inv : forall x ys v E,
¬ List.In x ys -> x ∹ v ⋲ (E ∖ ys) ->
x ∹ v ⋲ E.
x <> y -> x ∹ v ⋲ E ->
x ∹ v ⋲ (E ∖ {y}).
Parameter binds_remove_inv : forall x y v E,
x <> y -> x ∹ v ⋲ (E ∖ {y}) ->
x ∹ v ⋲ E.
Parameter binds_all_remove : forall x ys v E,
¬ List.In x ys -> x ∹ v ⋲ E ->
x ∹ v ⋲ (E ∖ ys).
Parameter binds_all_remove_inv : forall x ys v E,
¬ List.In x ys -> x ∹ v ⋲ (E ∖ ys) ->
x ∹ v ⋲ E.
Binds and ok.
Decidability of binds.
Parameter binds_dec_exists : forall x E,
{ v | x ∹ v ⋲ E } + { forall v, ¬ x ∹ v ⋲ E }.
Parameter binds_dec : forall x v E,
(forall w w', { w = w' } + { ¬ w = w' }) ->
{ x ∹ v ⋲ E } + { ¬ x ∹ v ⋲ E }.
{ v | x ∹ v ⋲ E } + { forall v, ¬ x ∹ v ⋲ E }.
Parameter binds_dec : forall x v E,
(forall w w', { w = w' } + { ¬ w = w' }) ->
{ x ∹ v ⋲ E } + { ¬ x ∹ v ⋲ E }.
All_Binds and binds.
Parameter all_binds_binds : forall x v E,
(x ∶ v) ⊏ E ->
x ∹ v ⋲ E.
Parameter binds_all_binds : forall x v E,
x ∹ v ⋲ E ->
(x ∶ v) ⊏ E.
(x ∶ v) ⊏ E ->
x ∹ v ⋲ E.
Parameter binds_all_binds : forall x v E,
x ∹ v ⋲ E ->
(x ∶ v) ⊏ E.
All_Binds and empty.
Parameter all_binds_empty_l : forall E,
(@empty A) ⊏ E.
Parameter all_binds_empty_r : forall E,
E ⊏ (@empty A) ->
E = (@empty A).
(@empty A) ⊏ E.
Parameter all_binds_empty_r : forall E,
E ⊏ (@empty A) ->
E = (@empty A).
All_Binds on singular.
Parameter all_binds_single_empty : forall x v,
(x ∶ v) ⊏ (@empty A) ->
False.
Parameter all_binds_single_single : forall x v y w,
x = y -> v = w ->
(x ∶ v) ⊏ (y ∶ w).
Parameter all_binds_single_single_inv : forall x v y w,
(x ∶ v) ⊏ (y ∶ w) ->
x = y ∧ v = w.
Parameter all_binds_single_singles : forall x v y w ys ws,
x = y -> v = w ->
(x ∶ v) ⊏ (y :: ys ∷ w :: ws).
Parameter all_binds_single_singles_inv : forall x v y w ys ws,
(x ∶ v) ⊏ (y :: ys ∷ w :: ws) ->
(x = y ∧ v = w) ∨ ((x ∶ v) ⊏ (ys ∷ ws)).
Parameter all_binds_single_eq_inv : forall x v w E,
(x ∶ v) ⊏ E -> (x ∶ w) ⊏ E ->
v = w.
(x ∶ v) ⊏ (@empty A) ->
False.
Parameter all_binds_single_single : forall x v y w,
x = y -> v = w ->
(x ∶ v) ⊏ (y ∶ w).
Parameter all_binds_single_single_inv : forall x v y w,
(x ∶ v) ⊏ (y ∶ w) ->
x = y ∧ v = w.
Parameter all_binds_single_singles : forall x v y w ys ws,
x = y -> v = w ->
(x ∶ v) ⊏ (y :: ys ∷ w :: ws).
Parameter all_binds_single_singles_inv : forall x v y w ys ws,
(x ∶ v) ⊏ (y :: ys ∷ w :: ws) ->
(x = y ∧ v = w) ∨ ((x ∶ v) ⊏ (ys ∷ ws)).
Parameter all_binds_single_eq_inv : forall x v w E,
(x ∶ v) ⊏ E -> (x ∶ w) ⊏ E ->
v = w.
All_Binds on singulars.
Parameter all_binds_singles_singles : forall xs vs ys ws,
xs = ys -> vs = ws ->
(xs ∷ vs) ⊏ (ys ∷ ws).
xs = ys -> vs = ws ->
(xs ∷ vs) ⊏ (ys ∷ ws).
All_Binds and concatenation.
Parameter all_binds_concat_r : forall E F G,
E ⊏ G ->
E ⊏ (F & G).
Parameter all_binds_concat_l : forall E F G,
E ⊏ F ->
(dom E) ⊄ G ->
E ⊏ (F & G).
Parameter all_binds_concat_compat : forall E F G,
E ⊏ F ->
(E & G) ⊏ (F & G).
Parameter all_binds_l_concat : forall E F G,
E ⊏ G -> F ⊏ G ->
(E & F) ⊏ G.
E ⊏ G ->
E ⊏ (F & G).
Parameter all_binds_concat_l : forall E F G,
E ⊏ F ->
(dom E) ⊄ G ->
E ⊏ (F & G).
Parameter all_binds_concat_compat : forall E F G,
E ⊏ F ->
(E & G) ⊏ (F & G).
Parameter all_binds_l_concat : forall E F G,
E ⊏ G -> F ⊏ G ->
(E & F) ⊏ G.
All_Binds on singulars when ok.
Parameter all_binds_singles_eq_inv : forall xs vs vs' F,
List.NoDup xs ->
length xs = length vs ->
length xs = length vs' ->
xs ∷ vs ⊏ F -> xs ∷ vs' ⊏ F ->
vs = vs'.
List.NoDup xs ->
length xs = length vs ->
length xs = length vs' ->
xs ∷ vs ⊏ F -> xs ∷ vs' ⊏ F ->
vs = vs'.
All_Binds and belongs.
Parameter all_binds_belongs : forall E F,
E ⊏ F ->
(dom E) ⊂ F.
Parameter belongs_all_binds : forall x F,
x ∈ F ->
exists v, (x ∶ v) ⊏ F.
Parameter all_belongs_all_binds : forall xs F,
xs ⊂ F ->
exists vs, (xs ∷ vs) ⊏ F.
E ⊏ F ->
(dom E) ⊂ F.
Parameter belongs_all_binds : forall x F,
x ∈ F ->
exists v, (x ∶ v) ⊏ F.
Parameter all_belongs_all_binds : forall xs F,
xs ⊂ F ->
exists vs, (xs ∷ vs) ⊏ F.
All_Binds and map.
Parameter all_binds_map : forall f E F,
E ⊏ F ->
map f E ⊏ map f F.
Parameter all_binds_map_inv : forall f E F,
Image.injective A B f ->
map f E ⊏ map f F ->
E ⊏ F.
E ⊏ F ->
map f E ⊏ map f F.
Parameter all_binds_map_inv : forall f E F,
Image.injective A B f ->
map f E ⊏ map f F ->
E ⊏ F.
All_Binds and update.
Parameter all_binds_update_self : forall E F,
(dom E) ⊂ F ->
E ⊏ (F ::= E).
Parameter all_binds_update : forall E F G,
E ⊏ F ->
(E ::= G) ⊏ (F ::= G).
(dom E) ⊂ F ->
E ⊏ (F ::= E).
Parameter all_binds_update : forall E F G,
E ⊏ F ->
(E ::= G) ⊏ (F ::= G).
All_Binds and remove.
Parameter all_binds_remove : forall y E F,
y ∉ E -> E ⊏ F ->
E ⊏ (F ∖ {y}).
Parameter all_binds_remove_inv : forall y E F,
y ∉ E -> E ⊏ (F ∖ {y}) ->
E ⊏ F.
Parameter all_binds_all_remove : forall ys E F,
ys ⊄ E -> E ⊏ F ->
E ⊏ (F ∖ ys).
Parameter all_binds_all_remove_inv : forall ys E F,
ys ⊄ E -> E ⊏ (F ∖ ys) ->
E ⊏ F.
Parameter all_binds_remove_compat : forall x E F,
ok E -> ok F ->
E ⊏ F ->
E ∖ {x} ⊏ F ∖ {x}.
Parameter all_binds_all_remove_compat : forall xs E F,
ok E -> ok F ->
E ⊏ F ->
E ∖ xs ⊏ F ∖ xs.
y ∉ E -> E ⊏ F ->
E ⊏ (F ∖ {y}).
Parameter all_binds_remove_inv : forall y E F,
y ∉ E -> E ⊏ (F ∖ {y}) ->
E ⊏ F.
Parameter all_binds_all_remove : forall ys E F,
ys ⊄ E -> E ⊏ F ->
E ⊏ (F ∖ ys).
Parameter all_binds_all_remove_inv : forall ys E F,
ys ⊄ E -> E ⊏ (F ∖ ys) ->
E ⊏ F.
Parameter all_binds_remove_compat : forall x E F,
ok E -> ok F ->
E ⊏ F ->
E ∖ {x} ⊏ F ∖ {x}.
Parameter all_binds_all_remove_compat : forall xs E F,
ok E -> ok F ->
E ⊏ F ->
E ∖ xs ⊏ F ∖ xs.
All_Binds and ok
Parameter all_binds_ok_concat_inv : forall E F G,
ok (E & F) ->
(E & F) ⊏ G ->
E ⊏ G ∧ F ⊏ G.
Parameter all_binds_concat_ok_comm : forall E F G,
E ⊏ (F & G) ->
ok (F & G) ->
E ⊏ (G & F).
ok (E & F) ->
(E & F) ⊏ G ->
E ⊏ G ∧ F ⊏ G.
Parameter all_binds_concat_ok_comm : forall E F G,
E ⊏ (F & G) ->
ok (F & G) ->
E ⊏ (G & F).
All_Binds is reflexive, anti-symmetric and transitive
Parameter all_binds_refl : forall E F,
E = F ->
E ⊏ F.
Parameter all_binds_anti_sym : forall E F,
E ⊏ F -> F ⊏ E ->
E ≍ F.
Parameter all_binds_trans : forall E F G,
E ⊏ F -> F ⊏ G ->
E ⊏ G.
E = F ->
E ⊏ F.
Parameter all_binds_anti_sym : forall E F,
E ⊏ F -> F ⊏ E ->
E ≍ F.
Parameter all_binds_trans : forall E F G,
E ⊏ F -> F ⊏ G ->
E ⊏ G.
Decidability of all_binds.
Parameter all_binds_dec_exists : forall xs F,
List.NoDup xs ->
{ vs | length xs = length vs ∧ (xs ∷ vs) ⊏ F }
+ { forall vs, length xs = length vs -> ¬ (xs ∷ vs) ⊏ F }.
List.NoDup xs ->
{ vs | length xs = length vs ∧ (xs ∷ vs) ⊏ F }
+ { forall vs, length xs = length vs -> ¬ (xs ∷ vs) ⊏ F }.
Eq is reflexive, symmetric and transitive
Parameter eq_refl : forall E F,
E = F ->
E ≍ F.
Parameter eq_sym : forall E F,
E ≍ F ->
F ≍ E.
Parameter eq_trans : forall E F G,
E ≍ F -> F ≍ G ->
E ≍ G.
E = F ->
E ≍ F.
Parameter eq_sym : forall E F,
E ≍ F ->
F ≍ E.
Parameter eq_trans : forall E F G,
E ≍ F -> F ≍ G ->
E ≍ G.
Eq implements equivalence over bindings.
Concat is commutative with eq when ok.
Eq commutes with other operations on environments.
Parameter eq_get : forall E F,
E ≍ F ->
forall x, get x E = get x F.
Parameter eq_get_inv : forall E F,
(forall x, get x E = get x F) ->
E ≍ F.
Parameter eq_map : forall f E F,
E ≍ F ->
map f E ≍ map f F.
Parameter eq_map_inv : forall f E F,
Image.injective A B f ->
map f E ≍ map f F ->
E ≍ F.
Parameter eq_remove : forall x E F,
ok E -> ok F ->
E ≍ F ->
E ∖ {x} ≍ F ∖ {x}.
Parameter eq_all_remove : forall xs E F,
ok E -> ok F ->
E ≍ F ->
E ∖ xs ≍ F ∖ xs.
Parameter eq_update : forall E F G,
E ≍ F ->
(E ::= G) ≍ (F ::= G).
Parameter eq_belongs : forall x E F,
E ≍ F ->
x ∈ E ->
x ∈ F.
Parameter eq_all_belongs : forall xs E F,
E ≍ F ->
xs ⊂ E ->
xs ⊂ F.
Parameter eq_notin : forall x E F,
E ≍ F ->
x ∉ E ->
x ∉ F.
Parameter eq_all_notin : forall xs E F,
E ≍ F ->
xs ⊄ E ->
xs ⊄ F.
E ≍ F ->
forall x, get x E = get x F.
Parameter eq_get_inv : forall E F,
(forall x, get x E = get x F) ->
E ≍ F.
Parameter eq_map : forall f E F,
E ≍ F ->
map f E ≍ map f F.
Parameter eq_map_inv : forall f E F,
Image.injective A B f ->
map f E ≍ map f F ->
E ≍ F.
Parameter eq_remove : forall x E F,
ok E -> ok F ->
E ≍ F ->
E ∖ {x} ≍ F ∖ {x}.
Parameter eq_all_remove : forall xs E F,
ok E -> ok F ->
E ≍ F ->
E ∖ xs ≍ F ∖ xs.
Parameter eq_update : forall E F G,
E ≍ F ->
(E ::= G) ≍ (F ::= G).
Parameter eq_belongs : forall x E F,
E ≍ F ->
x ∈ E ->
x ∈ F.
Parameter eq_all_belongs : forall xs E F,
E ≍ F ->
xs ⊂ E ->
xs ⊂ F.
Parameter eq_notin : forall x E F,
E ≍ F ->
x ∉ E ->
x ∉ F.
Parameter eq_all_notin : forall xs E F,
E ≍ F ->
xs ⊄ E ->
xs ⊄ F.
Decidability of eq.