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_l : 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) (add x
(inter s1 s2))).
Axiom inter_not_add_l : 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 diff_add_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s1:(set
a)) (s2:(set a)), (~ (mem x s2)) -> (infix_eqeq (diff (add x s1) s2) (add x
(diff s1 s2))).
Axiom diff_not_add_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s1:(set a)) (s2:(set a)), (mem x s2) -> (infix_eqeq (diff (add x s1) s2)
(diff s1 s2)).
Axiom subset_add_r : 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_com : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(s':(set a)), (infix_eqeq (union s s') (union s' s)).
Axiom union_var_l : 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_var_r : 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 x cc) /\ (mem cc sccs).
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 snoc_app : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (x:a),
((Init.Datatypes.app (Init.Datatypes.app l1 (Init.Datatypes.cons x Init.Datatypes.nil)) l2) = (Init.Datatypes.app l1 (Init.Datatypes.cons x 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_disjoint : 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_antisym : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(list a)), (simplelist s) -> ((precedes x y s) -> ((precedes y x s) ->
(x = y))).
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 xpath_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 gray (v:env): (set vertex) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x1
end.
Definition black (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))))))
end.
Definition no_black_to_white (black1:(set vertex)) (gray1:(set
vertex)): Prop := forall (x:vertex) (x':vertex), (edge x x') -> ((mem x
black1) -> (mem x' (union black1 gray1))).
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), (list.Mem.mem x s) -> ((list.Mem.mem y s) ->
(((map.Map.get (num e) x) <= (map.Map.get (num e) y))%Z -> (reachable x
y)))) /\ ((forall (y:vertex), (list.Mem.mem y s) -> exists x:vertex,
(mem x g) /\ (((map.Map.get (num e) x) <= (map.Map.get (num e) y))%Z /\
(reachable y x))) /\ forall (cc:(set vertex)), (mem cc (sccs e)) <->
((subset cc b) /\ (is_scc cc)))))))
end.
Definition subenv (e:env) (e':env): Prop := (exists s:(list vertex),
((stack e') = (Init.Datatypes.app s (stack e))) /\ (subset (elements s)
(black e'))) /\ ((subset (black e) (black 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
(gray e) (gray e'))))).
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).
Axiom subscc_after_last_gray : forall (e:env) (x:vertex) (s2:(list vertex))
(s3:(list vertex)), (wf_env e) ->
match e with
| (mk_env b g s _ _ _) => (mem x g) -> ((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 (black e) (gray 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 (black e) (gray e))))).
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_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))))).
Axiom simplelist_x_prec_strict_y' : forall
{alpha:Type} {alpha_WT:WhyType alpha}, forall (s1:(list alpha))
(s2:(list alpha)) (s3:(list alpha)) (x:alpha) (y':alpha),
(s1 = (Init.Datatypes.app s2 s3)) -> ((simplelist s1) -> ((is_last x s2) ->
((list.Mem.mem y' s3) -> ((precedes x y' s1) /\ ~ (y' = x))))).
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) /\ ~ (mem x (union e e1)).
Axiom H1 : (access_to e1 x).
Axiom H2 : (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 H3 : (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 H4 : (subset (successors x) vertices).
Axiom H5 : forall (x1:vertex), (mem x1 (successors x)) -> (access_to o1 x1).
Axiom H6 : (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 H7 : 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 H8 : (subset (successors x) (union result1 result2)).
Axiom H9 : forall (x1:vertex), (mem x1 (successors x)) ->
(result <= (map.Map.get result6 x1))%Z.
Axiom H10 : (result = (cardinal vertices)) \/ exists x1:vertex, (mem x1
(successors x)) /\ (num_of_reachable result x1 (mk_env result1 result2
result3 result4 result5 result6)).
Axiom H11 : forall (y:vertex), (xedge_to result3 o2 y) ->
(result <= (map.Map.get result6 y))%Z.
Axiom H12 : (result < e4)%Z.
Axiom H13 : ~ (result = (cardinal vertices)).
Axiom H14 : 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 H15 : (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) (black (mk_env o6 o7 o8 o9 o10 o11))).
Proof.
move: x e e1 e2 e3 e4 e5 H H1 H2 o o1 o2 o3 o4 o5 H3 H4 H5 H6
result result1 result2 result3 result4 result5 result6
H7 H8 H9 H10 H11 H12 H13 H14
o6 o7 o8 o9 o10 o11 H15.
move => x b g s sccs sn num H H1 wfe
b0 g0 s0 sccs0 sn0 num0
[eq1 [eq2 [eq3 [s0def [eq5 eq6]]]]]
H4 H5 H6
n1 b1 g1 s1 sccs1 sn1 num1
I' H8 H9 H10 H11 H12 H13 H14
b' g' s' sccs' sn' num' H15.
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_l : 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) (add x
(inter s1 s2))).
Axiom inter_not_add_l : 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 diff_add_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s1:(set
a)) (s2:(set a)), (~ (mem x s2)) -> (infix_eqeq (diff (add x s1) s2) (add x
(diff s1 s2))).
Axiom diff_not_add_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s1:(set a)) (s2:(set a)), (mem x s2) -> (infix_eqeq (diff (add x s1) s2)
(diff s1 s2)).
Axiom subset_add_r : 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_com : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a))
(s':(set a)), (infix_eqeq (union s s') (union s' s)).
Axiom union_var_l : 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_var_r : 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 x cc) /\ (mem cc sccs).
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 snoc_app : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (x:a),
((Init.Datatypes.app (Init.Datatypes.app l1 (Init.Datatypes.cons x Init.Datatypes.nil)) l2) = (Init.Datatypes.app l1 (Init.Datatypes.cons x 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_disjoint : 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_antisym : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(list a)), (simplelist s) -> ((precedes x y s) -> ((precedes y x s) ->
(x = y))).
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 xpath_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 gray (v:env): (set vertex) :=
match v with
| (mk_env x x1 x2 x3 x4 x5) => x1
end.
Definition black (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))))))
end.
Definition no_black_to_white (black1:(set vertex)) (gray1:(set
vertex)): Prop := forall (x:vertex) (x':vertex), (edge x x') -> ((mem x
black1) -> (mem x' (union black1 gray1))).
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), (list.Mem.mem x s) -> ((list.Mem.mem y s) ->
(((map.Map.get (num e) x) <= (map.Map.get (num e) y))%Z -> (reachable x
y)))) /\ ((forall (y:vertex), (list.Mem.mem y s) -> exists x:vertex,
(mem x g) /\ (((map.Map.get (num e) x) <= (map.Map.get (num e) y))%Z /\
(reachable y x))) /\ forall (cc:(set vertex)), (mem cc (sccs e)) <->
((subset cc b) /\ (is_scc cc)))))))
end.
Definition subenv (e:env) (e':env): Prop := (exists s:(list vertex),
((stack e') = (Init.Datatypes.app s (stack e))) /\ (subset (elements s)
(black e'))) /\ ((subset (black e) (black 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
(gray e) (gray e'))))).
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).
Axiom subscc_after_last_gray : forall (e:env) (x:vertex) (s2:(list vertex))
(s3:(list vertex)), (wf_env e) ->
match e with
| (mk_env b g s _ _ _) => (mem x g) -> ((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 (black e) (gray 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 (black e) (gray e))))).
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_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))))).
Axiom simplelist_x_prec_strict_y' : forall
{alpha:Type} {alpha_WT:WhyType alpha}, forall (s1:(list alpha))
(s2:(list alpha)) (s3:(list alpha)) (x:alpha) (y':alpha),
(s1 = (Init.Datatypes.app s2 s3)) -> ((simplelist s1) -> ((is_last x s2) ->
((list.Mem.mem y' s3) -> ((precedes x y' s1) /\ ~ (y' = x))))).
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) /\ ~ (mem x (union e e1)).
Axiom H1 : (access_to e1 x).
Axiom H2 : (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 H3 : (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 H4 : (subset (successors x) vertices).
Axiom H5 : forall (x1:vertex), (mem x1 (successors x)) -> (access_to o1 x1).
Axiom H6 : (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 H7 : 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 H8 : (subset (successors x) (union result1 result2)).
Axiom H9 : forall (x1:vertex), (mem x1 (successors x)) ->
(result <= (map.Map.get result6 x1))%Z.
Axiom H10 : (result = (cardinal vertices)) \/ exists x1:vertex, (mem x1
(successors x)) /\ (num_of_reachable result x1 (mk_env result1 result2
result3 result4 result5 result6)).
Axiom H11 : forall (y:vertex), (xedge_to result3 o2 y) ->
(result <= (map.Map.get result6 y))%Z.
Axiom H12 : (result < e4)%Z.
Axiom H13 : ~ (result = (cardinal vertices)).
Axiom H14 : 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 H15 : (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) (black (mk_env o6 o7 o8 o9 o10 o11))).
Proof.
move: x e e1 e2 e3 e4 e5 H H1 H2 o o1 o2 o3 o4 o5 H3 H4 H5 H6
result result1 result2 result3 result4 result5 result6
H7 H8 H9 H10 H11 H12 H13 H14
o6 o7 o8 o9 o10 o11 H15.
move => x b g s sccs sn num H H1 wfe
b0 g0 s0 sccs0 sn0 num0
[eq1 [eq2 [eq3 [s0def [eq5 eq6]]]]]
H4 H5 H6
n1 b1 g1 s1 sccs1 sn1 num1
I' H8 H9 H10 H11 H12 H13 H14
b' g' s' sccs' sn' num' H15.
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: I' => [wfe1 sube0e1].
move: sube0e1 => [[s2 G0] _]; simpl in G0.
move: G0 => [s1def s2black].
move: H15 => [b'def [_ [s'def _]]].
rewrite s'def b'def.
exists (s2 ++ (x :: nil) )%list; split.
- by rewrite -Append.Append_assoc /= -s0def.
- 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 => [ | y_in_nil ] //.
by move /(mem_empty y) :y_in_nil.
Qed.
move: sube0e1 => [[s2 G0] _]; simpl in G0.
move: G0 => [s1def s2black].
move: H15 => [b'def [_ [s'def _]]].
rewrite s'def b'def.
exists (s2 ++ (x :: nil) )%list; split.
- by rewrite -Append.Append_assoc /= -s0def.
- 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 => [ | y_in_nil ] //.
by move /(mem_empty y) :y_in_nil.
Qed.