Library scc_SCCTarjan72_WP_parameter_dfs1_2
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require map.Const.
Require list.Append.
Require list.Reverse.
Require list.NumOcc.
Definition unit := unit.
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 subset_eq : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> (((cardinal s1) = (cardinal s2)) ->
(infix_eqeq s1 s2)).
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)).
Fixpoint elements {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: (set
a) :=
match l with
| Init.Datatypes.nil => (empty : (set a))
| (Init.Datatypes.cons x r) => (add x (elements r))
end.
Axiom elements_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (list.Mem.mem x l) <-> (mem x (elements l)).
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)).
Axiom lmem_dec : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)),
(list.Mem.mem x l) \/ ~ (list.Mem.mem x l).
Axiom inter_com : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq (inter s1 s2) (inter s2 s1)).
Axiom inter_add : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (~ (mem x s2)) -> (infix_eqeq (inter (add x s1) s2)
(inter s1 s2)).
Axiom set_elt : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s1:(set a))
(s2:(set a)) (s3:(set a)), (~ (mem x s3)) -> (infix_eqeq (union (add x s1)
(diff s2 s3)) (union s1 (diff (add x s2) s3))).
Axiom set_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s1:(set a))
(s2:(set a)) (s3:(set a)) (s4:(set a)), (infix_eqeq s1 (union s2 (diff s3
s4))) -> ((infix_eqeq (inter s2 s4) (empty : (set a))) -> ((mem x s1) ->
~ (mem x s4))).
Axiom inter_subset_inter : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set
a)) (s2:(set a)) (s2':(set a)), ((inter s1 s2) = (empty : (set a))) ->
((subset s2' s2) -> ((inter s1 s2') = (empty : (set a)))).
Axiom subset_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set a))
(s':(set a)), (subset s' (add x s)) -> ((mem x s') \/ (subset s' s)).
Axiom union_add_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)) (s':(set a)), (infix_eqeq (union (add x s) s') (add x (union s s'))).
Axiom union_add_r : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)) (s':(set a)), (infix_eqeq (union s (add x s')) (add x (union s s'))).
Axiom union_sym : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(s':(set a)), (infix_eqeq (union s s') (union s' s)).
Axiom union_var1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(s':(set a)) (t:(set a)), (subset s s') -> (subset (union s t) (union s'
t)).
Axiom union_var2 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(t:(set a)) (t':(set a)), (subset t t') -> (subset (union s t) (union s
t')).
Parameter set_of: forall {a:Type} {a_WT:WhyType a}, (set (set a)) -> (set a).
Axiom set_of_empty : forall {a:Type} {a_WT:WhyType a}, ((set_of (empty : (set
(set a)))) = (empty : (set a))).
Axiom set_of_add : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(sx:(set (set a))), (infix_eqeq (set_of (add s sx)) (union s (set_of sx))).
Definition one_in_set_of {a:Type} {a_WT:WhyType a} (sccs:(set (set
a))): Prop := forall (x:a), (mem x (set_of sccs)) -> exists cc:(set a),
(mem cc sccs) /\ (mem x cc).
Axiom Induction : (forall (s:(set (set vertex))), (is_empty s) ->
(one_in_set_of s)) -> ((forall (s:(set (set vertex))), (one_in_set_of s) ->
forall (t:(set vertex)), (~ (mem t s)) -> (one_in_set_of (add t s))) ->
forall (s:(set (set vertex))), (one_in_set_of s)).
Axiom set_of_elt : forall (sccs:(set (set vertex))), (one_in_set_of sccs).
Axiom elt_set_of : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (cc:(set
a)) (sccs:(set (set a))), (mem x cc) -> ((mem cc sccs) -> (mem x
(set_of sccs))).
Axiom subset_set_of : forall (s:(set (set vertex))) (s':(set (set vertex))),
(subset s s') -> (subset (set_of s) (set_of s')).
Axiom elts_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (infix_eqeq (elements (Init.Datatypes.cons x l)) (add x
(elements l))).
Axiom elts_app : forall {a:Type} {a_WT:WhyType a}, forall (s:(list a))
(s':(list a)), (infix_eqeq (elements (Init.Datatypes.app s s'))
(union (elements s) (elements s'))).
Axiom list_simpl_r : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l:(list a)),
((Init.Datatypes.app l1 l) = (Init.Datatypes.app l2 l)) -> (l1 = l2).
Axiom list_assoc_cons : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)) (x:a),
((Init.Datatypes.app l1 (Init.Datatypes.cons x l2)) = (Init.Datatypes.app (Init.Datatypes.app l1 (Init.Datatypes.cons x Init.Datatypes.nil)) l2)).
Definition is_last {a:Type} {a_WT:WhyType a} (x:a) (s:(list a)): Prop :=
exists s':(list a),
(s = (Init.Datatypes.app s' (Init.Datatypes.cons x Init.Datatypes.nil))).
Definition precedes {a:Type} {a_WT:WhyType a} (x:a) (y:a)
(s:(list a)): Prop := exists s1:(list a), exists s2:(list a),
(s = (Init.Datatypes.app s1 (Init.Datatypes.cons x s2))) /\ (list.Mem.mem y
(Init.Datatypes.cons x s2)).
Axiom precedes_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(list a)), (precedes x y s) -> ((list.Mem.mem x s) /\ (list.Mem.mem y
s)).
Axiom head_precedes : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(list a)), (list.Mem.mem y (Init.Datatypes.cons x s)) -> (precedes x y
(Init.Datatypes.cons x s)).
Axiom precedes_tail : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(z:a) (s:(list a)), (~ (x = z)) -> ((precedes x y
(Init.Datatypes.cons z s)) <-> (precedes x y s)).
Axiom tail_not_precedes : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s:(list a)), (precedes y x (Init.Datatypes.cons x s)) ->
((~ (list.Mem.mem x s)) -> (y = x)).
Axiom split_list_precedes : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (list.Mem.mem y
(Init.Datatypes.app s1 (Init.Datatypes.cons x Init.Datatypes.nil))) ->
(precedes y x (Init.Datatypes.app s1 (Init.Datatypes.cons x s2))).
Axiom precedes_refl : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)), (precedes x x s) <-> (list.Mem.mem x s).
Axiom precedes_append_left : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (precedes x y s1) -> (precedes x y
(Init.Datatypes.app s2 s1)).
Axiom precedes_append_left_iff : forall {a:Type} {a_WT:WhyType a},
forall (x:a) (y:a) (s1:(list a)) (s2:(list a)), (~ (list.Mem.mem x s1)) ->
((precedes x y (Init.Datatypes.app s1 s2)) <-> (precedes x y s2)).
Axiom precedes_append_right : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (precedes x y s1) -> (precedes x y
(Init.Datatypes.app s1 s2)).
Axiom precedes_append_right_iff : forall {a:Type} {a_WT:WhyType a},
forall (x:a) (y:a) (s1:(list a)) (s2:(list a)), (~ (list.Mem.mem y s2)) ->
((precedes x y (Init.Datatypes.app s1 s2)) <-> (precedes x y s1)).
Definition simplelist {a:Type} {a_WT:WhyType a} (l:(list a)): Prop :=
forall (x:a), ((list.NumOcc.num_occ x l) <= 1%Z)%Z.
Axiom simplelist_tl : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (simplelist (Init.Datatypes.cons x l)) -> ((simplelist l) /\
~ (list.Mem.mem x l)).
Axiom simplelist_split : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)) (l3:(list a)) (l4:(list a)), (simplelist
(Init.Datatypes.app l1 (Init.Datatypes.cons x l2))) ->
(((Init.Datatypes.app l1 (Init.Datatypes.cons x l2)) = (Init.Datatypes.app l3 (Init.Datatypes.cons x l4))) ->
((l1 = l3) /\ (l2 = l4))).
Axiom simplelist_app_inter : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (simplelist
(Init.Datatypes.app l1 l2)) -> ((inter (elements l1)
(elements l2)) = (empty : (set a))).
Axiom simplelist_length : forall {a:Type} {a_WT:WhyType a},
forall (s:(list a)), (simplelist s) ->
((list.Length.length s) = (cardinal (elements s))).
Axiom precedes_trans : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(z:a) (s:(list a)), (simplelist s) -> ((precedes x y s) -> ((precedes y z
s) -> (precedes x z s))).
Definition reachable (x:vertex) (y:vertex): Prop := exists l:(list vertex),
(path x l y).
Axiom reachable_refl : forall (x:vertex), (reachable x x).
Axiom reachable_trans : forall (x:vertex) (y:vertex) (z:vertex), (reachable x
y) -> ((reachable y z) -> (reachable x z)).
Axiom xset_path_xedge : forall (x:vertex) (y:vertex) (l:(list vertex))
(s:(set vertex)), (mem x s) -> ((~ (mem y s)) -> ((path x l y) ->
exists x':vertex, exists y':vertex, (mem x' s) /\ ((~ (mem y' s)) /\ ((edge
x' y') /\ ((reachable x x') /\ (reachable y' y)))))).
Definition in_same_scc (x:vertex) (y:vertex): Prop := (reachable x y) /\
(reachable y x).
Definition is_subscc (s:(set vertex)): Prop := forall (x:vertex) (y:vertex),
(mem x s) -> ((mem y s) -> (in_same_scc x y)).
Definition is_scc (s:(set vertex)): Prop := (~ (is_empty s)) /\ ((is_subscc
s) /\ forall (s':(set vertex)), (subset s s') -> ((is_subscc s') ->
(infix_eqeq s s'))).
Axiom same_scc_refl : forall (x:vertex), (in_same_scc x x).
Axiom same_scc_sym : forall (x:vertex) (z:vertex), (in_same_scc x z) ->
(in_same_scc z x).
Axiom same_scc_trans : forall (x:vertex) (y:vertex) (z:vertex), (in_same_scc
x y) -> ((in_same_scc y z) -> (in_same_scc x z)).
Axiom subscc_add : forall (x:vertex) (y:vertex) (cc:(set vertex)), (is_subscc
cc) -> ((mem x cc) -> ((in_same_scc x y) -> (is_subscc (add y cc)))).
Axiom scc_max : forall (x:vertex) (y:vertex) (cc:(set vertex)), (is_scc
cc) -> ((mem x cc) -> ((in_same_scc x y) -> (mem y cc))).
Inductive env :=
| mk_env : (set vertex) -> (set vertex) -> (list vertex) -> (set (set
vertex)) -> Z -> (map.Map.map vertex Z) -> env.
Axiom env_WhyType : WhyType env.
Existing Instance env_WhyType.
Definition num (v:env): (map.Map.map vertex Z) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x5
end.
Definition sn (v:env): Z := match v with
| (mk_env x x1 x2 x3 x4 x5) => x4
end.
Definition sccs (v:env): (set (set vertex)) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x3
end.
Definition stack (v:env): (list vertex) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x2
end.
Definition grays (v:env): (set vertex) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x1
end.
Definition blacks (v:env): (set vertex) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x
end.
Definition wf_color (e:env): Prop :=
match e with
| (mk_env b g s ccs _ _) => (subset (union g b) vertices) /\ ((infix_eqeq
(inter b g) (empty : (set vertex))) /\ ((infix_eqeq (elements s)
(union g (diff b (set_of ccs)))) /\ (subset (set_of ccs) b)))
end.
Definition wf_num (e:env): Prop :=
match e with
| (mk_env b g s ccs n f) => (forall (x:vertex),
(((-1%Z)%Z <= (map.Map.get f x))%Z /\ (((map.Map.get f x) < n)%Z /\
(n <= (cardinal vertices))%Z)) \/ ((map.Map.get f
x) = (cardinal vertices))) /\ ((n = (cardinal (union g b))) /\
((forall (x:vertex), ((map.Map.get f x) = (cardinal vertices)) <-> (mem
x (set_of ccs))) /\ ((forall (x:vertex), ((map.Map.get f
x) = (-1%Z)%Z) <-> ~ (mem x (union g b))) /\ ((forall (x:vertex)
(y:vertex), (list.Mem.mem x s) -> ((list.Mem.mem y s) ->
(((map.Map.get f x) <= (map.Map.get f y))%Z <-> (precedes y x s)))) /\
forall (x:vertex) (y:vertex), (list.Mem.mem x s) -> ((list.Mem.mem y
s) -> (((map.Map.get f x) = (map.Map.get f y)) -> (x = y)))))))
end.
Definition no_black_to_white (blacks1:(set vertex)) (grays1:(set
vertex)): Prop := forall (x:vertex) (x':vertex), (edge x x') -> ((mem x
blacks1) -> (mem x' (union blacks1 grays1))).
Definition wf_env (e:env): Prop :=
match e with
| (mk_env b g s _ _ _) => (wf_color e) /\ ((wf_num e) /\
((no_black_to_white b g) /\ ((simplelist s) /\ ((forall (x:vertex)
(y:vertex), (mem x g) -> ((list.Mem.mem y s) -> ((precedes y x s) ->
(reachable x y)))) /\ ((forall (y:vertex), (list.Mem.mem y s) ->
exists x:vertex, (mem x g) /\ ((precedes y x s) /\ (reachable y x))) /\
forall (cc:(set vertex)), (mem cc (sccs e)) <-> ((subset cc b) /\
(is_scc cc)))))))
end.
Definition access_from (x:vertex) (s:(set vertex)): Prop :=
forall (y:vertex), (mem y s) -> (reachable x y).
Definition access_to (s:(set vertex)) (y:vertex): Prop := forall (x:vertex),
(mem x s) -> (reachable x y).
Definition num_of_reachable (n:Z) (x:vertex) (e:env): Prop :=
exists y:vertex, (list.Mem.mem y (stack e)) /\ ((n = (map.Map.get (num e)
y)) /\ (reachable x y)).
Definition xedge_to (s1:(list vertex)) (s3:(list vertex)) (y:vertex): Prop :=
(exists s2:(list vertex), (s1 = (Init.Datatypes.app s2 s3)) /\
exists x:vertex, (list.Mem.mem x s2) /\ (edge x y)) /\ (list.Mem.mem y s3).
Definition subenv (e:env) (e':env): Prop := (exists s:(list vertex),
((stack e') = (Init.Datatypes.app s (stack e))) /\ (subset (elements s)
(blacks e'))) /\ ((subset (blacks e) (blacks e')) /\ ((subset (sccs e)
(sccs e')) /\ ((forall (x:vertex), (list.Mem.mem x (stack e)) ->
((map.Map.get (num e) x) = (map.Map.get (num e') x))) /\ (infix_eqeq
(grays e) (grays e'))))).
Axiom subscc_after_last_gray : forall (x:vertex) (e:env) (g:(set vertex))
(s2:(list vertex)) (s3:(list vertex)), (infix_eqeq (grays e) (add x g)) ->
((wf_env e) ->
match e with
| (mk_env b _ s _ _ _) => (s = (Init.Datatypes.app s2 s3)) -> ((is_last x
s2) -> ((subset (elements s2) (add x b)) -> (is_subscc (elements s2))))
end).
Axiom wf_color_postcond_split : forall (s2:(set vertex)) (s3:(set vertex))
(g:(set vertex)) (b:(set vertex)) (sccs1:(set vertex)), (infix_eqeq
(union s2 s3) (union g (diff b sccs1))) -> ((infix_eqeq (inter s2 s3)
(empty : (set vertex))) -> ((infix_eqeq (inter g s2) (empty : (set
vertex))) -> (infix_eqeq s3 (union g (diff b (union s2 sccs1)))))).
Axiom wf_color_sccs : forall (e:env), (wf_color e) -> (infix_eqeq
(set_of (sccs e)) (diff (union (blacks e) (grays e))
(elements (stack e)))).
Axiom wf_color_3_cases : forall (x:vertex) (e:env), (wf_color e) -> ((mem x
(set_of (sccs e))) \/ ((mem x (elements (stack e))) \/ ~ (mem x
(union (blacks e) (grays e))))).
Axiom subenv_num : forall (e:env) (e':env) (x:vertex), (wf_env e) -> ((wf_env
e') -> ((subenv e e') -> ((map.Map.get (num e) x) <= (map.Map.get (num e')
x))%Z)).
Axiom num_lmem : forall (e:env) (x:vertex), (wf_env e) ->
(((0%Z <= (map.Map.get (num e) x))%Z /\ ((map.Map.get (num e)
x) < (cardinal vertices))%Z) <-> (list.Mem.mem x (stack e))).
Axiom num_inj : forall (e:env) (x:vertex) (y:vertex), (wf_env e) ->
(((0%Z <= (map.Map.get (num e) x))%Z /\ (((map.Map.get (num e)
x) = (map.Map.get (num e) y)) /\ ((map.Map.get (num e)
y) < (cardinal vertices))%Z)) -> (x = y)).
Axiom num_rank : forall (e:env) (x:vertex) (y:vertex), (wf_env e) ->
(((0%Z <= (map.Map.get (num e) x))%Z /\ (((map.Map.get (num e)
x) <= (map.Map.get (num e) y))%Z /\ ((map.Map.get (num e)
y) < (cardinal vertices))%Z)) -> (precedes y x (stack e))).
Axiom num_rank_strict : forall (e:env) (x:vertex) (y:vertex), (wf_env e) ->
((list.Mem.mem x (stack e)) -> ((list.Mem.mem y (stack e)) ->
(((map.Map.get (num e) x) < (map.Map.get (num e) y))%Z <-> ((precedes y x
(stack e)) /\ ~ (x = y))))).
Parameter x: vertex.
Parameter e: (set vertex).
Parameter e1: (set vertex).
Parameter e2: (list vertex).
Parameter e3: (set (set vertex)).
Parameter e4: Z.
Parameter e5: (map.Map.map vertex Z).
Axiom H : (mem x vertices).
Axiom H1 : (access_to e1 x).
Axiom H2 : ~ (mem x (union e e1)).
Axiom H3 : (wf_env (mk_env e e1 e2 e3 e4 e5)).
Parameter o: (set vertex).
Parameter o1: (set vertex).
Parameter o2: (list vertex).
Parameter o3: (set (set vertex)).
Parameter o4: Z.
Parameter o5: (map.Map.map vertex Z).
Axiom H4 : (o = e) /\ ((o1 = (add x e1)) /\ ((o3 = e3) /\
((o2 = (Init.Datatypes.cons x e2)) /\ ((o4 = (e4 + 1%Z)%Z) /\
(o5 = (map.Map.set e5 x e4)))))).
Axiom H5 : (subset (successors x) vertices).
Axiom H6 : forall (x1:vertex), (mem x1 (successors x)) -> (access_to o1 x1).
Axiom H7 : (wf_env (mk_env o o1 o2 o3 o4 o5)).
Parameter result: Z.
Parameter result1: (set vertex).
Parameter result2: (set vertex).
Parameter result3: (list vertex).
Parameter result4: (set (set vertex)).
Parameter result5: Z.
Parameter result6: (map.Map.map vertex Z).
Axiom H8 : let e' := (mk_env result1 result2 result3 result4 result5
result6) in ((wf_env e') /\ (subenv (mk_env o o1 o2 o3 o4 o5) e')).
Axiom H9 : (subset (successors x) (union result1 result2)).
Axiom H10 : forall (x1:vertex), (mem x1 (successors x)) ->
(result <= (map.Map.get result6 x1))%Z.
Axiom H11 : (result = (cardinal vertices)) \/ exists x1:vertex, (mem x1
(successors x)) /\ (num_of_reachable result x1 (mk_env result1 result2
result3 result4 result5 result6)).
Axiom H12 : forall (y:vertex), (xedge_to result3 o2 y) ->
(result <= (map.Map.get result6 y))%Z.
Axiom H13 : (result < e4)%Z.
Axiom H14 : exists y:vertex, (~ (y = x)) /\ ((precedes x y result3) /\
(reachable x y)).
Axiom H15 : exists y:vertex, (~ (y = x)) /\ ((mem y result2) /\
(((map.Map.get result6 y) < (map.Map.get result6 x))%Z /\ (in_same_scc x
y))).
Parameter o6: (set vertex).
Parameter o7: (set vertex).
Parameter o8: (list vertex).
Parameter o9: (set (set vertex)).
Parameter o10: Z.
Parameter o11: (map.Map.map vertex Z).
Axiom H16 : (o6 = (add x result1)) /\ ((o7 = (remove x result2)) /\
((o8 = result3) /\ ((o9 = result4) /\ ((o10 = result5) /\
(o11 = result6))))).
Require Import mathcomp.ssreflect.ssreflect.
Ltac compress :=
repeat (match goal with [H1: ?A, H2: ?A |- _] => clear H2 end).
Theorem WP_parameter_dfs1 : exists s:(list vertex), ((stack (mk_env o6 o7 o8
o9 o10 o11)) = (Init.Datatypes.app s (stack (mk_env e e1 e2 e3 e4 e5)))) /\
(subset (elements s) (blacks (mk_env o6 o7 o8 o9 o10 o11))).
Proof.
move: x e e1 e2 e3 e4 e5 H H1 H2 H3 o o1 o2 o3 o4 o5 H4 H5 H6 H7
result result1 result2 result3 result4 result5 result6
H8 H9 H10 H11 H12 H13 H14 H15
o6 o7 o8 o9 o10 o11 H16.
move => x b g s sccs sn num H H1 H2 wfe b0 g0 s0 sccs0 sn0 num0 H4 H5 H6 H7
n1 b1 g1 s1 sccs1 sn1 num1
I' H9 H10 H11 H12 H13 H14 H15
b' g' s' sccs' sn' num' H16.
pose e := mk_env b g s sccs sn num.
pose e0 := mk_env b0 g0 s0 sccs0 sn0 num0.
pose e1 := mk_env b1 g1 s1 sccs1 sn1 num1.
pose e' := mk_env b' g' s' sccs' sn' num'.
simpl.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require map.Const.
Require list.Append.
Require list.Reverse.
Require list.NumOcc.
Definition unit := unit.
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 subset_eq : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (subset s1 s2) -> (((cardinal s1) = (cardinal s2)) ->
(infix_eqeq s1 s2)).
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)).
Fixpoint elements {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: (set
a) :=
match l with
| Init.Datatypes.nil => (empty : (set a))
| (Init.Datatypes.cons x r) => (add x (elements r))
end.
Axiom elements_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (list.Mem.mem x l) <-> (mem x (elements l)).
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)).
Axiom lmem_dec : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)),
(list.Mem.mem x l) \/ ~ (list.Mem.mem x l).
Axiom inter_com : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)), (infix_eqeq (inter s1 s2) (inter s2 s1)).
Axiom inter_add : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
(s2:(set a)) (x:a), (~ (mem x s2)) -> (infix_eqeq (inter (add x s1) s2)
(inter s1 s2)).
Axiom set_elt : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s1:(set a))
(s2:(set a)) (s3:(set a)), (~ (mem x s3)) -> (infix_eqeq (union (add x s1)
(diff s2 s3)) (union s1 (diff (add x s2) s3))).
Axiom set_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s1:(set a))
(s2:(set a)) (s3:(set a)) (s4:(set a)), (infix_eqeq s1 (union s2 (diff s3
s4))) -> ((infix_eqeq (inter s2 s4) (empty : (set a))) -> ((mem x s1) ->
~ (mem x s4))).
Axiom inter_subset_inter : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set
a)) (s2:(set a)) (s2':(set a)), ((inter s1 s2) = (empty : (set a))) ->
((subset s2' s2) -> ((inter s1 s2') = (empty : (set a)))).
Axiom subset_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set a))
(s':(set a)), (subset s' (add x s)) -> ((mem x s') \/ (subset s' s)).
Axiom union_add_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)) (s':(set a)), (infix_eqeq (union (add x s) s') (add x (union s s'))).
Axiom union_add_r : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
a)) (s':(set a)), (infix_eqeq (union s (add x s')) (add x (union s s'))).
Axiom union_sym : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(s':(set a)), (infix_eqeq (union s s') (union s' s)).
Axiom union_var1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(s':(set a)) (t:(set a)), (subset s s') -> (subset (union s t) (union s'
t)).
Axiom union_var2 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(t:(set a)) (t':(set a)), (subset t t') -> (subset (union s t) (union s
t')).
Parameter set_of: forall {a:Type} {a_WT:WhyType a}, (set (set a)) -> (set a).
Axiom set_of_empty : forall {a:Type} {a_WT:WhyType a}, ((set_of (empty : (set
(set a)))) = (empty : (set a))).
Axiom set_of_add : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(sx:(set (set a))), (infix_eqeq (set_of (add s sx)) (union s (set_of sx))).
Definition one_in_set_of {a:Type} {a_WT:WhyType a} (sccs:(set (set
a))): Prop := forall (x:a), (mem x (set_of sccs)) -> exists cc:(set a),
(mem cc sccs) /\ (mem x cc).
Axiom Induction : (forall (s:(set (set vertex))), (is_empty s) ->
(one_in_set_of s)) -> ((forall (s:(set (set vertex))), (one_in_set_of s) ->
forall (t:(set vertex)), (~ (mem t s)) -> (one_in_set_of (add t s))) ->
forall (s:(set (set vertex))), (one_in_set_of s)).
Axiom set_of_elt : forall (sccs:(set (set vertex))), (one_in_set_of sccs).
Axiom elt_set_of : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (cc:(set
a)) (sccs:(set (set a))), (mem x cc) -> ((mem cc sccs) -> (mem x
(set_of sccs))).
Axiom subset_set_of : forall (s:(set (set vertex))) (s':(set (set vertex))),
(subset s s') -> (subset (set_of s) (set_of s')).
Axiom elts_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (infix_eqeq (elements (Init.Datatypes.cons x l)) (add x
(elements l))).
Axiom elts_app : forall {a:Type} {a_WT:WhyType a}, forall (s:(list a))
(s':(list a)), (infix_eqeq (elements (Init.Datatypes.app s s'))
(union (elements s) (elements s'))).
Axiom list_simpl_r : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l:(list a)),
((Init.Datatypes.app l1 l) = (Init.Datatypes.app l2 l)) -> (l1 = l2).
Axiom list_assoc_cons : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)) (x:a),
((Init.Datatypes.app l1 (Init.Datatypes.cons x l2)) = (Init.Datatypes.app (Init.Datatypes.app l1 (Init.Datatypes.cons x Init.Datatypes.nil)) l2)).
Definition is_last {a:Type} {a_WT:WhyType a} (x:a) (s:(list a)): Prop :=
exists s':(list a),
(s = (Init.Datatypes.app s' (Init.Datatypes.cons x Init.Datatypes.nil))).
Definition precedes {a:Type} {a_WT:WhyType a} (x:a) (y:a)
(s:(list a)): Prop := exists s1:(list a), exists s2:(list a),
(s = (Init.Datatypes.app s1 (Init.Datatypes.cons x s2))) /\ (list.Mem.mem y
(Init.Datatypes.cons x s2)).
Axiom precedes_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(list a)), (precedes x y s) -> ((list.Mem.mem x s) /\ (list.Mem.mem y
s)).
Axiom head_precedes : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(list a)), (list.Mem.mem y (Init.Datatypes.cons x s)) -> (precedes x y
(Init.Datatypes.cons x s)).
Axiom precedes_tail : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(z:a) (s:(list a)), (~ (x = z)) -> ((precedes x y
(Init.Datatypes.cons z s)) <-> (precedes x y s)).
Axiom tail_not_precedes : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s:(list a)), (precedes y x (Init.Datatypes.cons x s)) ->
((~ (list.Mem.mem x s)) -> (y = x)).
Axiom split_list_precedes : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (list.Mem.mem y
(Init.Datatypes.app s1 (Init.Datatypes.cons x Init.Datatypes.nil))) ->
(precedes y x (Init.Datatypes.app s1 (Init.Datatypes.cons x s2))).
Axiom precedes_refl : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)), (precedes x x s) <-> (list.Mem.mem x s).
Axiom precedes_append_left : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (precedes x y s1) -> (precedes x y
(Init.Datatypes.app s2 s1)).
Axiom precedes_append_left_iff : forall {a:Type} {a_WT:WhyType a},
forall (x:a) (y:a) (s1:(list a)) (s2:(list a)), (~ (list.Mem.mem x s1)) ->
((precedes x y (Init.Datatypes.app s1 s2)) <-> (precedes x y s2)).
Axiom precedes_append_right : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (precedes x y s1) -> (precedes x y
(Init.Datatypes.app s1 s2)).
Axiom precedes_append_right_iff : forall {a:Type} {a_WT:WhyType a},
forall (x:a) (y:a) (s1:(list a)) (s2:(list a)), (~ (list.Mem.mem y s2)) ->
((precedes x y (Init.Datatypes.app s1 s2)) <-> (precedes x y s1)).
Definition simplelist {a:Type} {a_WT:WhyType a} (l:(list a)): Prop :=
forall (x:a), ((list.NumOcc.num_occ x l) <= 1%Z)%Z.
Axiom simplelist_tl : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (simplelist (Init.Datatypes.cons x l)) -> ((simplelist l) /\
~ (list.Mem.mem x l)).
Axiom simplelist_split : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)) (l3:(list a)) (l4:(list a)), (simplelist
(Init.Datatypes.app l1 (Init.Datatypes.cons x l2))) ->
(((Init.Datatypes.app l1 (Init.Datatypes.cons x l2)) = (Init.Datatypes.app l3 (Init.Datatypes.cons x l4))) ->
((l1 = l3) /\ (l2 = l4))).
Axiom simplelist_app_inter : forall {a:Type} {a_WT:WhyType a},
forall (l1:(list a)) (l2:(list a)), (simplelist
(Init.Datatypes.app l1 l2)) -> ((inter (elements l1)
(elements l2)) = (empty : (set a))).
Axiom simplelist_length : forall {a:Type} {a_WT:WhyType a},
forall (s:(list a)), (simplelist s) ->
((list.Length.length s) = (cardinal (elements s))).
Axiom precedes_trans : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(z:a) (s:(list a)), (simplelist s) -> ((precedes x y s) -> ((precedes y z
s) -> (precedes x z s))).
Definition reachable (x:vertex) (y:vertex): Prop := exists l:(list vertex),
(path x l y).
Axiom reachable_refl : forall (x:vertex), (reachable x x).
Axiom reachable_trans : forall (x:vertex) (y:vertex) (z:vertex), (reachable x
y) -> ((reachable y z) -> (reachable x z)).
Axiom xset_path_xedge : forall (x:vertex) (y:vertex) (l:(list vertex))
(s:(set vertex)), (mem x s) -> ((~ (mem y s)) -> ((path x l y) ->
exists x':vertex, exists y':vertex, (mem x' s) /\ ((~ (mem y' s)) /\ ((edge
x' y') /\ ((reachable x x') /\ (reachable y' y)))))).
Definition in_same_scc (x:vertex) (y:vertex): Prop := (reachable x y) /\
(reachable y x).
Definition is_subscc (s:(set vertex)): Prop := forall (x:vertex) (y:vertex),
(mem x s) -> ((mem y s) -> (in_same_scc x y)).
Definition is_scc (s:(set vertex)): Prop := (~ (is_empty s)) /\ ((is_subscc
s) /\ forall (s':(set vertex)), (subset s s') -> ((is_subscc s') ->
(infix_eqeq s s'))).
Axiom same_scc_refl : forall (x:vertex), (in_same_scc x x).
Axiom same_scc_sym : forall (x:vertex) (z:vertex), (in_same_scc x z) ->
(in_same_scc z x).
Axiom same_scc_trans : forall (x:vertex) (y:vertex) (z:vertex), (in_same_scc
x y) -> ((in_same_scc y z) -> (in_same_scc x z)).
Axiom subscc_add : forall (x:vertex) (y:vertex) (cc:(set vertex)), (is_subscc
cc) -> ((mem x cc) -> ((in_same_scc x y) -> (is_subscc (add y cc)))).
Axiom scc_max : forall (x:vertex) (y:vertex) (cc:(set vertex)), (is_scc
cc) -> ((mem x cc) -> ((in_same_scc x y) -> (mem y cc))).
Inductive env :=
| mk_env : (set vertex) -> (set vertex) -> (list vertex) -> (set (set
vertex)) -> Z -> (map.Map.map vertex Z) -> env.
Axiom env_WhyType : WhyType env.
Existing Instance env_WhyType.
Definition num (v:env): (map.Map.map vertex Z) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x5
end.
Definition sn (v:env): Z := match v with
| (mk_env x x1 x2 x3 x4 x5) => x4
end.
Definition sccs (v:env): (set (set vertex)) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x3
end.
Definition stack (v:env): (list vertex) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x2
end.
Definition grays (v:env): (set vertex) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x1
end.
Definition blacks (v:env): (set vertex) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x
end.
Definition wf_color (e:env): Prop :=
match e with
| (mk_env b g s ccs _ _) => (subset (union g b) vertices) /\ ((infix_eqeq
(inter b g) (empty : (set vertex))) /\ ((infix_eqeq (elements s)
(union g (diff b (set_of ccs)))) /\ (subset (set_of ccs) b)))
end.
Definition wf_num (e:env): Prop :=
match e with
| (mk_env b g s ccs n f) => (forall (x:vertex),
(((-1%Z)%Z <= (map.Map.get f x))%Z /\ (((map.Map.get f x) < n)%Z /\
(n <= (cardinal vertices))%Z)) \/ ((map.Map.get f
x) = (cardinal vertices))) /\ ((n = (cardinal (union g b))) /\
((forall (x:vertex), ((map.Map.get f x) = (cardinal vertices)) <-> (mem
x (set_of ccs))) /\ ((forall (x:vertex), ((map.Map.get f
x) = (-1%Z)%Z) <-> ~ (mem x (union g b))) /\ ((forall (x:vertex)
(y:vertex), (list.Mem.mem x s) -> ((list.Mem.mem y s) ->
(((map.Map.get f x) <= (map.Map.get f y))%Z <-> (precedes y x s)))) /\
forall (x:vertex) (y:vertex), (list.Mem.mem x s) -> ((list.Mem.mem y
s) -> (((map.Map.get f x) = (map.Map.get f y)) -> (x = y)))))))
end.
Definition no_black_to_white (blacks1:(set vertex)) (grays1:(set
vertex)): Prop := forall (x:vertex) (x':vertex), (edge x x') -> ((mem x
blacks1) -> (mem x' (union blacks1 grays1))).
Definition wf_env (e:env): Prop :=
match e with
| (mk_env b g s _ _ _) => (wf_color e) /\ ((wf_num e) /\
((no_black_to_white b g) /\ ((simplelist s) /\ ((forall (x:vertex)
(y:vertex), (mem x g) -> ((list.Mem.mem y s) -> ((precedes y x s) ->
(reachable x y)))) /\ ((forall (y:vertex), (list.Mem.mem y s) ->
exists x:vertex, (mem x g) /\ ((precedes y x s) /\ (reachable y x))) /\
forall (cc:(set vertex)), (mem cc (sccs e)) <-> ((subset cc b) /\
(is_scc cc)))))))
end.
Definition access_from (x:vertex) (s:(set vertex)): Prop :=
forall (y:vertex), (mem y s) -> (reachable x y).
Definition access_to (s:(set vertex)) (y:vertex): Prop := forall (x:vertex),
(mem x s) -> (reachable x y).
Definition num_of_reachable (n:Z) (x:vertex) (e:env): Prop :=
exists y:vertex, (list.Mem.mem y (stack e)) /\ ((n = (map.Map.get (num e)
y)) /\ (reachable x y)).
Definition xedge_to (s1:(list vertex)) (s3:(list vertex)) (y:vertex): Prop :=
(exists s2:(list vertex), (s1 = (Init.Datatypes.app s2 s3)) /\
exists x:vertex, (list.Mem.mem x s2) /\ (edge x y)) /\ (list.Mem.mem y s3).
Definition subenv (e:env) (e':env): Prop := (exists s:(list vertex),
((stack e') = (Init.Datatypes.app s (stack e))) /\ (subset (elements s)
(blacks e'))) /\ ((subset (blacks e) (blacks e')) /\ ((subset (sccs e)
(sccs e')) /\ ((forall (x:vertex), (list.Mem.mem x (stack e)) ->
((map.Map.get (num e) x) = (map.Map.get (num e') x))) /\ (infix_eqeq
(grays e) (grays e'))))).
Axiom subscc_after_last_gray : forall (x:vertex) (e:env) (g:(set vertex))
(s2:(list vertex)) (s3:(list vertex)), (infix_eqeq (grays e) (add x g)) ->
((wf_env e) ->
match e with
| (mk_env b _ s _ _ _) => (s = (Init.Datatypes.app s2 s3)) -> ((is_last x
s2) -> ((subset (elements s2) (add x b)) -> (is_subscc (elements s2))))
end).
Axiom wf_color_postcond_split : forall (s2:(set vertex)) (s3:(set vertex))
(g:(set vertex)) (b:(set vertex)) (sccs1:(set vertex)), (infix_eqeq
(union s2 s3) (union g (diff b sccs1))) -> ((infix_eqeq (inter s2 s3)
(empty : (set vertex))) -> ((infix_eqeq (inter g s2) (empty : (set
vertex))) -> (infix_eqeq s3 (union g (diff b (union s2 sccs1)))))).
Axiom wf_color_sccs : forall (e:env), (wf_color e) -> (infix_eqeq
(set_of (sccs e)) (diff (union (blacks e) (grays e))
(elements (stack e)))).
Axiom wf_color_3_cases : forall (x:vertex) (e:env), (wf_color e) -> ((mem x
(set_of (sccs e))) \/ ((mem x (elements (stack e))) \/ ~ (mem x
(union (blacks e) (grays e))))).
Axiom subenv_num : forall (e:env) (e':env) (x:vertex), (wf_env e) -> ((wf_env
e') -> ((subenv e e') -> ((map.Map.get (num e) x) <= (map.Map.get (num e')
x))%Z)).
Axiom num_lmem : forall (e:env) (x:vertex), (wf_env e) ->
(((0%Z <= (map.Map.get (num e) x))%Z /\ ((map.Map.get (num e)
x) < (cardinal vertices))%Z) <-> (list.Mem.mem x (stack e))).
Axiom num_inj : forall (e:env) (x:vertex) (y:vertex), (wf_env e) ->
(((0%Z <= (map.Map.get (num e) x))%Z /\ (((map.Map.get (num e)
x) = (map.Map.get (num e) y)) /\ ((map.Map.get (num e)
y) < (cardinal vertices))%Z)) -> (x = y)).
Axiom num_rank : forall (e:env) (x:vertex) (y:vertex), (wf_env e) ->
(((0%Z <= (map.Map.get (num e) x))%Z /\ (((map.Map.get (num e)
x) <= (map.Map.get (num e) y))%Z /\ ((map.Map.get (num e)
y) < (cardinal vertices))%Z)) -> (precedes y x (stack e))).
Axiom num_rank_strict : forall (e:env) (x:vertex) (y:vertex), (wf_env e) ->
((list.Mem.mem x (stack e)) -> ((list.Mem.mem y (stack e)) ->
(((map.Map.get (num e) x) < (map.Map.get (num e) y))%Z <-> ((precedes y x
(stack e)) /\ ~ (x = y))))).
Parameter x: vertex.
Parameter e: (set vertex).
Parameter e1: (set vertex).
Parameter e2: (list vertex).
Parameter e3: (set (set vertex)).
Parameter e4: Z.
Parameter e5: (map.Map.map vertex Z).
Axiom H : (mem x vertices).
Axiom H1 : (access_to e1 x).
Axiom H2 : ~ (mem x (union e e1)).
Axiom H3 : (wf_env (mk_env e e1 e2 e3 e4 e5)).
Parameter o: (set vertex).
Parameter o1: (set vertex).
Parameter o2: (list vertex).
Parameter o3: (set (set vertex)).
Parameter o4: Z.
Parameter o5: (map.Map.map vertex Z).
Axiom H4 : (o = e) /\ ((o1 = (add x e1)) /\ ((o3 = e3) /\
((o2 = (Init.Datatypes.cons x e2)) /\ ((o4 = (e4 + 1%Z)%Z) /\
(o5 = (map.Map.set e5 x e4)))))).
Axiom H5 : (subset (successors x) vertices).
Axiom H6 : forall (x1:vertex), (mem x1 (successors x)) -> (access_to o1 x1).
Axiom H7 : (wf_env (mk_env o o1 o2 o3 o4 o5)).
Parameter result: Z.
Parameter result1: (set vertex).
Parameter result2: (set vertex).
Parameter result3: (list vertex).
Parameter result4: (set (set vertex)).
Parameter result5: Z.
Parameter result6: (map.Map.map vertex Z).
Axiom H8 : let e' := (mk_env result1 result2 result3 result4 result5
result6) in ((wf_env e') /\ (subenv (mk_env o o1 o2 o3 o4 o5) e')).
Axiom H9 : (subset (successors x) (union result1 result2)).
Axiom H10 : forall (x1:vertex), (mem x1 (successors x)) ->
(result <= (map.Map.get result6 x1))%Z.
Axiom H11 : (result = (cardinal vertices)) \/ exists x1:vertex, (mem x1
(successors x)) /\ (num_of_reachable result x1 (mk_env result1 result2
result3 result4 result5 result6)).
Axiom H12 : forall (y:vertex), (xedge_to result3 o2 y) ->
(result <= (map.Map.get result6 y))%Z.
Axiom H13 : (result < e4)%Z.
Axiom H14 : exists y:vertex, (~ (y = x)) /\ ((precedes x y result3) /\
(reachable x y)).
Axiom H15 : exists y:vertex, (~ (y = x)) /\ ((mem y result2) /\
(((map.Map.get result6 y) < (map.Map.get result6 x))%Z /\ (in_same_scc x
y))).
Parameter o6: (set vertex).
Parameter o7: (set vertex).
Parameter o8: (list vertex).
Parameter o9: (set (set vertex)).
Parameter o10: Z.
Parameter o11: (map.Map.map vertex Z).
Axiom H16 : (o6 = (add x result1)) /\ ((o7 = (remove x result2)) /\
((o8 = result3) /\ ((o9 = result4) /\ ((o10 = result5) /\
(o11 = result6))))).
Require Import mathcomp.ssreflect.ssreflect.
Ltac compress :=
repeat (match goal with [H1: ?A, H2: ?A |- _] => clear H2 end).
Theorem WP_parameter_dfs1 : exists s:(list vertex), ((stack (mk_env o6 o7 o8
o9 o10 o11)) = (Init.Datatypes.app s (stack (mk_env e e1 e2 e3 e4 e5)))) /\
(subset (elements s) (blacks (mk_env o6 o7 o8 o9 o10 o11))).
Proof.
move: x e e1 e2 e3 e4 e5 H H1 H2 H3 o o1 o2 o3 o4 o5 H4 H5 H6 H7
result result1 result2 result3 result4 result5 result6
H8 H9 H10 H11 H12 H13 H14 H15
o6 o7 o8 o9 o10 o11 H16.
move => x b g s sccs sn num H H1 H2 wfe b0 g0 s0 sccs0 sn0 num0 H4 H5 H6 H7
n1 b1 g1 s1 sccs1 sn1 num1
I' H9 H10 H11 H12 H13 H14 H15
b' g' s' sccs' sn' num' H16.
pose e := mk_env b g s sccs sn num.
pose e0 := mk_env b0 g0 s0 sccs0 sn0 num0.
pose e1 := mk_env b1 g1 s1 sccs1 sn1 num1.
pose e' := mk_env b' g' s' sccs' sn' num'.
simpl.
s' extends s with black vertices
move: H4 => [_ [_ [_ [s0def _]]]].
move: I' => [wfe1 sube0e1].
move: sube0e1 => [[s2 G0] _]; simpl in G0.
move: G0 => [s1def s2black].
move: H16 => [b'def [_ [s'def _]]].
rewrite s'def; exists (s2 ++ (x :: nil) )%list.
split.
- by rewrite -Append.Append_assoc /= -s0def.
- rewrite b'def.
move => y ymem; rewrite add_def1.
move /elts_app /union_def1 :ymem => [y_in_s2 | y_is_x].
+ by right; move /s2black :y_in_s2.
+ left.
move /add_def1 :y_is_x => [eq_yx | y_in_nil]; first by [].
by have absurd: False by apply: (mem_empty y).
Qed.
move: I' => [wfe1 sube0e1].
move: sube0e1 => [[s2 G0] _]; simpl in G0.
move: G0 => [s1def s2black].
move: H16 => [b'def [_ [s'def _]]].
rewrite s'def; exists (s2 ++ (x :: nil) )%list.
split.
- by rewrite -Append.Append_assoc /= -s0def.
- rewrite b'def.
move => y ymem; rewrite add_def1.
move /elts_app /union_def1 :ymem => [y_in_s2 | y_is_x].
+ by right; move /s2black :y_in_s2.
+ left.
move /add_def1 :y_is_x => [eq_yx | y_in_nil]; first by [].
by have absurd: False by apply: (mem_empty y).
Qed.