Library dfs_nbtw_Dfs_nbtw_black_to_white_path_goes_thru_gray_1
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Require list.Reverse.
Require list.NumOcc.
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
Axiom set : forall (a:Type), Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
Definition subset {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(subset s s).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).
Definition is_empty {a:Type} {a_WT:WhyType a} (s:(set a)): Prop :=
forall (x:a), ~ (mem x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty : (set
a))).
Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
(empty : (set a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (mem x s) -> ((add x (remove x s)) = s).
Axiom remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), ((remove x (add x s)) = (remove x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(~ (is_empty s)) -> (mem (choose s) s).
Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.
Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
s)))%Z).
Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
Parameter elements: forall {a:Type} {a_WT:WhyType a}, (list a) -> (set a).
Axiom elements_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(x:a), (list.Mem.mem x l) <-> (mem x (elements l)).
Axiom elements_Nil : forall {a:Type} {a_WT:WhyType a},
((elements Init.Datatypes.nil) = (empty : (set a))).
Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.
Parameter vertices: (set vertex).
Parameter successors: vertex -> (set vertex).
Axiom successors_vertices : forall (x:vertex), (mem x vertices) -> (subset
(successors x) vertices).
Definition edge (x:vertex) (y:vertex): Prop := (mem x vertices) /\ (mem y
(successors x)).
Inductive path: vertex -> (list vertex) -> vertex -> Prop :=
| Path_empty : forall (x:vertex), (path x Init.Datatypes.nil x)
| Path_cons : forall (x:vertex) (y:vertex) (z:vertex) (l:(list vertex)),
(edge x y) -> ((path y l z) -> (path x (Init.Datatypes.cons x l) z)).
Axiom path_right_extension : forall (x:vertex) (y:vertex) (z:vertex)
(l:(list vertex)), (path x l y) -> ((edge y z) -> (path x
(Init.Datatypes.app l (Init.Datatypes.cons y Init.Datatypes.nil)) z)).
Axiom path_right_inversion : forall (x:vertex) (z:vertex) (l:(list vertex)),
(path x l z) -> (((x = z) /\ (l = Init.Datatypes.nil)) \/ exists y:vertex,
exists l´:(list vertex), (path x l´ y) /\ ((edge y z) /\
(l = (Init.Datatypes.app l´ (Init.Datatypes.cons y Init.Datatypes.nil))))).
Axiom path_trans : forall (x:vertex) (y:vertex) (z:vertex) (l1:(list vertex))
(l2:(list vertex)), (path x l1 y) -> ((path y l2 z) -> (path x
(Init.Datatypes.app l1 l2) z)).
Axiom empty_path : forall (x:vertex) (y:vertex), (path x Init.Datatypes.nil
y) -> (x = y).
Axiom path_decomposition : forall (x:vertex) (y:vertex) (z:vertex)
(l1:(list vertex)) (l2:(list vertex)), (path x
(Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z) -> ((path x l1 y) /\
(path y (Init.Datatypes.cons y l2) z)).
Definition path_fst_not_twice (x:vertex) (l:(list vertex))
(z:vertex): Prop := (path x (Init.Datatypes.cons x l) z) /\ ~ (list.Mem.mem
x l).
Axiom mem_decidable : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(lv:(list a)), (list.Mem.mem x lv) \/ ~ (list.Mem.mem x lv).
Definition spl {a:Type} {a_WT:WhyType a} (lv:(list a)): Prop := forall (x:a),
(list.Mem.mem x lv) -> ((list.NumOcc.num_occ x lv) = 1%Z).
Axiom spl_single : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (spl
(Init.Datatypes.cons x Init.Datatypes.nil)).
Axiom spl_expansion : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(lv:(list a)), (spl lv) -> ((~ (list.Mem.mem x lv)) -> (spl
(Init.Datatypes.app lv (Init.Datatypes.cons x Init.Datatypes.nil)))).
Axiom spl_sub : forall {a:Type} {a_WT:WhyType a}, forall (lv:(list a))
(lv1:(list a)) (lv2:(list a)), (lv = (Init.Datatypes.app lv1 lv2)) -> ((spl
lv) -> ((spl lv1) /\ (spl lv2))).
Axiom numocc_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(lv:(list a)), (0%Z <= (list.NumOcc.num_occ x lv))%Z.
Axiom path_edge : forall (x:vertex) (z:vertex), (path x
(Init.Datatypes.cons x Init.Datatypes.nil) z) -> (edge x z).
Axiom path_hd : forall (x:vertex) (y:vertex) (z:vertex) (l:(list vertex)),
(path x (Init.Datatypes.cons y l) z) -> (x = y).
Axiom path_vertex_l : forall (x:vertex) (y:vertex) (z:vertex)
(l:(list vertex)), (path x l z) -> ((list.Mem.mem y l) -> (mem y
vertices)).
Axiom path_vertex_r : forall (x:vertex) (z:vertex) (l:(list vertex)), (path x
l z) -> ((~ (l = Init.Datatypes.nil)) -> (mem z vertices)).
Axiom path_vertex_last_occ : forall (x:vertex) (y:vertex) (z:vertex)
(l:(list vertex)), (path x l z) -> ((list.Mem.mem y l) ->
exists l1:(list vertex), exists l2:(list vertex),
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons y l2))) /\
(path_fst_not_twice y l2 z)).
Definition white_vertex (x:vertex) (v:(set vertex)): Prop := ~ (mem x v).
Definition white_monotony (v1:(set vertex)) (v2:(set vertex)): Prop :=
forall (x:vertex), (white_vertex x v2) -> (white_vertex x v1).
Definition nodeflip (x:vertex) (v1:(set vertex)) (v2:(set vertex)): Prop :=
(white_vertex x v1) /\ ~ (white_vertex x v2).
Definition whitepath (x:vertex) (l:(list vertex)) (z:vertex) (v:(set
vertex)): Prop := (path x l z) /\ ((forall (y:vertex), (list.Mem.mem y
l) -> (white_vertex y v)) /\ (white_vertex z v)).
Axiom whitepath_mem_decomp : forall (x:vertex) (l1:(list vertex))
(l2:(list vertex)) (z:vertex) (y:vertex) (v:(set vertex)), (whitepath x
(Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z v) -> ((whitepath x l1
y v) /\ (whitepath y (Init.Datatypes.cons y l2) z v)).
Axiom whitepath_mem_decomp_right : forall (x:vertex) (l:(list vertex))
(z:vertex) (y:vertex) (v:(set vertex)), (whitepath x l z v) ->
((list.Mem.mem y
(Init.Datatypes.app l (Init.Datatypes.cons z Init.Datatypes.nil))) ->
exists l´:(list vertex), (whitepath y l´ z v)).
Definition nodeflip_whitepath (roots:(set vertex)) (v1:(set vertex)) (v2:(set
vertex)): Prop := forall (z:vertex), (nodeflip z v1 v2) -> exists x:vertex,
exists l:(list vertex), (mem x roots) /\ (whitepath x l z v1).
Definition whitepath_nodeflip (roots:(set vertex)) (v1:(set vertex)) (v2:(set
vertex)): Prop := forall (x:vertex) (l:(list vertex)) (z:vertex), (mem x
roots) -> ((whitepath x l z v1) -> (nodeflip z v1 v2)).
Definition reachable (x:vertex) (z:vertex): Prop := exists l:(list vertex),
(path x l z).
Axiom reachable_succ : forall (x:vertex) (x´:vertex), (edge x x´) ->
(reachable x x´).
Axiom reachable_trans : forall (x:vertex) (y:vertex) (z:vertex), (reachable x
y) -> ((reachable y z) -> (reachable x z)).
Definition access (roots:(set vertex)) (b:(set vertex)): Prop :=
forall (z:vertex), (mem z b) -> exists x:vertex, (mem x roots) /\
(reachable x z).
Axiom access_monotony_l : forall (roots:(set vertex)) (roots´:(set vertex))
(b:(set vertex)), (subset roots roots´) -> ((access roots b) -> (access
roots´ b)).
Axiom access_monotony_r : forall (roots:(set vertex)) (b:(set vertex))
(b´:(set vertex)), (subset b b´) -> ((access roots b´) -> (access roots
b)).
Axiom access_trans : forall (roots:(set vertex)) (b:(set vertex)) (b´:(set
vertex)), (access roots b´) -> ((access b´ b) -> (access roots b)).
Definition no_black_to_white (blacks:(set vertex)) (grays:(set
vertex)): Prop := forall (x:vertex) (x´:vertex), (edge x x´) -> ((mem x
blacks) -> (mem x´ (union blacks grays))).
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Require list.Reverse.
Require list.NumOcc.
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
Axiom set : forall (a:Type), Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.
Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).
Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).
Definition subset {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(subset s s).
Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
s3)).
Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).
Definition is_empty {a:Type} {a_WT:WhyType a} (s:(set a)): Prop :=
forall (x:a), ~ (mem x s).
Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty : (set
a))).
Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
(empty : (set a))).
Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).
Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).
Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).
Axiom add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (mem x s) -> ((add x (remove x s)) = s).
Axiom remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), ((remove x (add x s)) = (remove x s)).
Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)), (subset (remove x s) s).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).
Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
a).
Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).
Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset (diff s1 s2) s1).
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.
Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(~ (is_empty s)) -> (mem (choose s) s).
Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.
Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
(0%Z <= (cardinal s))%Z.
Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 0%Z) <-> (is_empty s).
Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
s)) = (1%Z + (cardinal s))%Z).
Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
s)))%Z).
Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.
Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).
Parameter elements: forall {a:Type} {a_WT:WhyType a}, (list a) -> (set a).
Axiom elements_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(x:a), (list.Mem.mem x l) <-> (mem x (elements l)).
Axiom elements_Nil : forall {a:Type} {a_WT:WhyType a},
((elements Init.Datatypes.nil) = (empty : (set a))).
Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.
Parameter vertices: (set vertex).
Parameter successors: vertex -> (set vertex).
Axiom successors_vertices : forall (x:vertex), (mem x vertices) -> (subset
(successors x) vertices).
Definition edge (x:vertex) (y:vertex): Prop := (mem x vertices) /\ (mem y
(successors x)).
Inductive path: vertex -> (list vertex) -> vertex -> Prop :=
| Path_empty : forall (x:vertex), (path x Init.Datatypes.nil x)
| Path_cons : forall (x:vertex) (y:vertex) (z:vertex) (l:(list vertex)),
(edge x y) -> ((path y l z) -> (path x (Init.Datatypes.cons x l) z)).
Axiom path_right_extension : forall (x:vertex) (y:vertex) (z:vertex)
(l:(list vertex)), (path x l y) -> ((edge y z) -> (path x
(Init.Datatypes.app l (Init.Datatypes.cons y Init.Datatypes.nil)) z)).
Axiom path_right_inversion : forall (x:vertex) (z:vertex) (l:(list vertex)),
(path x l z) -> (((x = z) /\ (l = Init.Datatypes.nil)) \/ exists y:vertex,
exists l´:(list vertex), (path x l´ y) /\ ((edge y z) /\
(l = (Init.Datatypes.app l´ (Init.Datatypes.cons y Init.Datatypes.nil))))).
Axiom path_trans : forall (x:vertex) (y:vertex) (z:vertex) (l1:(list vertex))
(l2:(list vertex)), (path x l1 y) -> ((path y l2 z) -> (path x
(Init.Datatypes.app l1 l2) z)).
Axiom empty_path : forall (x:vertex) (y:vertex), (path x Init.Datatypes.nil
y) -> (x = y).
Axiom path_decomposition : forall (x:vertex) (y:vertex) (z:vertex)
(l1:(list vertex)) (l2:(list vertex)), (path x
(Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z) -> ((path x l1 y) /\
(path y (Init.Datatypes.cons y l2) z)).
Definition path_fst_not_twice (x:vertex) (l:(list vertex))
(z:vertex): Prop := (path x (Init.Datatypes.cons x l) z) /\ ~ (list.Mem.mem
x l).
Axiom mem_decidable : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(lv:(list a)), (list.Mem.mem x lv) \/ ~ (list.Mem.mem x lv).
Definition spl {a:Type} {a_WT:WhyType a} (lv:(list a)): Prop := forall (x:a),
(list.Mem.mem x lv) -> ((list.NumOcc.num_occ x lv) = 1%Z).
Axiom spl_single : forall {a:Type} {a_WT:WhyType a}, forall (x:a), (spl
(Init.Datatypes.cons x Init.Datatypes.nil)).
Axiom spl_expansion : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(lv:(list a)), (spl lv) -> ((~ (list.Mem.mem x lv)) -> (spl
(Init.Datatypes.app lv (Init.Datatypes.cons x Init.Datatypes.nil)))).
Axiom spl_sub : forall {a:Type} {a_WT:WhyType a}, forall (lv:(list a))
(lv1:(list a)) (lv2:(list a)), (lv = (Init.Datatypes.app lv1 lv2)) -> ((spl
lv) -> ((spl lv1) /\ (spl lv2))).
Axiom numocc_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(lv:(list a)), (0%Z <= (list.NumOcc.num_occ x lv))%Z.
Axiom path_edge : forall (x:vertex) (z:vertex), (path x
(Init.Datatypes.cons x Init.Datatypes.nil) z) -> (edge x z).
Axiom path_hd : forall (x:vertex) (y:vertex) (z:vertex) (l:(list vertex)),
(path x (Init.Datatypes.cons y l) z) -> (x = y).
Axiom path_vertex_l : forall (x:vertex) (y:vertex) (z:vertex)
(l:(list vertex)), (path x l z) -> ((list.Mem.mem y l) -> (mem y
vertices)).
Axiom path_vertex_r : forall (x:vertex) (z:vertex) (l:(list vertex)), (path x
l z) -> ((~ (l = Init.Datatypes.nil)) -> (mem z vertices)).
Axiom path_vertex_last_occ : forall (x:vertex) (y:vertex) (z:vertex)
(l:(list vertex)), (path x l z) -> ((list.Mem.mem y l) ->
exists l1:(list vertex), exists l2:(list vertex),
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons y l2))) /\
(path_fst_not_twice y l2 z)).
Definition white_vertex (x:vertex) (v:(set vertex)): Prop := ~ (mem x v).
Definition white_monotony (v1:(set vertex)) (v2:(set vertex)): Prop :=
forall (x:vertex), (white_vertex x v2) -> (white_vertex x v1).
Definition nodeflip (x:vertex) (v1:(set vertex)) (v2:(set vertex)): Prop :=
(white_vertex x v1) /\ ~ (white_vertex x v2).
Definition whitepath (x:vertex) (l:(list vertex)) (z:vertex) (v:(set
vertex)): Prop := (path x l z) /\ ((forall (y:vertex), (list.Mem.mem y
l) -> (white_vertex y v)) /\ (white_vertex z v)).
Axiom whitepath_mem_decomp : forall (x:vertex) (l1:(list vertex))
(l2:(list vertex)) (z:vertex) (y:vertex) (v:(set vertex)), (whitepath x
(Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z v) -> ((whitepath x l1
y v) /\ (whitepath y (Init.Datatypes.cons y l2) z v)).
Axiom whitepath_mem_decomp_right : forall (x:vertex) (l:(list vertex))
(z:vertex) (y:vertex) (v:(set vertex)), (whitepath x l z v) ->
((list.Mem.mem y
(Init.Datatypes.app l (Init.Datatypes.cons z Init.Datatypes.nil))) ->
exists l´:(list vertex), (whitepath y l´ z v)).
Definition nodeflip_whitepath (roots:(set vertex)) (v1:(set vertex)) (v2:(set
vertex)): Prop := forall (z:vertex), (nodeflip z v1 v2) -> exists x:vertex,
exists l:(list vertex), (mem x roots) /\ (whitepath x l z v1).
Definition whitepath_nodeflip (roots:(set vertex)) (v1:(set vertex)) (v2:(set
vertex)): Prop := forall (x:vertex) (l:(list vertex)) (z:vertex), (mem x
roots) -> ((whitepath x l z v1) -> (nodeflip z v1 v2)).
Definition reachable (x:vertex) (z:vertex): Prop := exists l:(list vertex),
(path x l z).
Axiom reachable_succ : forall (x:vertex) (x´:vertex), (edge x x´) ->
(reachable x x´).
Axiom reachable_trans : forall (x:vertex) (y:vertex) (z:vertex), (reachable x
y) -> ((reachable y z) -> (reachable x z)).
Definition access (roots:(set vertex)) (b:(set vertex)): Prop :=
forall (z:vertex), (mem z b) -> exists x:vertex, (mem x roots) /\
(reachable x z).
Axiom access_monotony_l : forall (roots:(set vertex)) (roots´:(set vertex))
(b:(set vertex)), (subset roots roots´) -> ((access roots b) -> (access
roots´ b)).
Axiom access_monotony_r : forall (roots:(set vertex)) (b:(set vertex))
(b´:(set vertex)), (subset b b´) -> ((access roots b´) -> (access roots
b)).
Axiom access_trans : forall (roots:(set vertex)) (b:(set vertex)) (b´:(set
vertex)), (access roots b´) -> ((access b´ b) -> (access roots b)).
Definition no_black_to_white (blacks:(set vertex)) (grays:(set
vertex)): Prop := forall (x:vertex) (x´:vertex), (edge x x´) -> ((mem x
blacks) -> (mem x´ (union blacks grays))).
Require Import ssreflect.
Ltac compress :=
repeat (match goal with [H1: ?A, H2: ?A |- _] => clear H2 end).
Lemma path_mem:
forall (x:vertex) (l: (list vertex)) (z: vertex),
path x l z -> list.Mem.mem x l \/ x = z.
Proof.
move=> x l z hxlz.
elim: {x l z} hxlz => [x | x x´ z].
- by right.
- move => l hxx´ hx´lz´ _.
left; simpl.
by left.
Qed.
Theorem black_to_white_path_goes_thru_gray : forall (grays:(set vertex))
(blacks:(set vertex)), (no_black_to_white blacks grays) ->
forall (x:vertex) (l:(list vertex)) (z:vertex), (path x l z) -> ((mem x
blacks) -> ((~ (mem z (union blacks grays))) -> exists y:vertex,
(list.Mem.mem y l) /\ (mem y grays))).
Proof.
move=> grays blacks hnbtw x l z hxlz.
elim: {x l z} hxlz => [x |x x´ z l´].
- move=> hxb hxnotbg.
have hxbg: mem x (union blacks grays).
by apply union_def1; left.
by apply hxnotbg in hxbg.
- move=> hxx´ hx´l´z HIx´z hxb hnotzbg.
apply (hnbtw x x´) in hxb.
apply union_def1 in hxb.
move: hxb => [hx´b | hx´g].
+ apply HIx´z in hx´b.
move: hx´b => [y hyl´].
exists y.
move: hyl´ => [hmemyl´ hzg].
apply conj.
- by simpl; right.
- by [].
+ by [].
- exists x´.
apply conj.
+ apply path_mem in hx´l´z.
simpl.
move: hx´l´z => [hmemx´l´ | eqx´z].
- by right.
- rewrite eqx´z in hx´g.
have hzbg: mem z (union blacks grays).
+ by apply union_def1; right.
by apply hnotzbg in hzbg.
+ exact hx´g.
- exact hxx´.
Qed.