Library scc_SCCTarjan72_WP_parameter_dfs1_6
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)).
Parameter elements: forall {a:Type} {a_WT:WhyType a}, (list a) -> (set a).
Axiom elements_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(x:a), (list.Mem.mem x l) <-> (mem x (elements l)).
Axiom elements_Nil : forall {a:Type} {a_WT:WhyType a},
((elements Init.Datatypes.nil) = (empty : (set a))).
Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.
Parameter vertices: (set vertex).
Parameter successors: vertex -> (set vertex).
Axiom successors_vertices : forall (x:vertex), (mem x vertices) -> (subset
(successors x) vertices).
Definition edge (x:vertex) (y:vertex): Prop := (mem x vertices) /\ (mem y
(successors x)).
Inductive path: vertex -> (list vertex) -> vertex -> Prop :=
| Path_empty : forall (x:vertex), (path x Init.Datatypes.nil x)
| Path_cons : forall (x:vertex) (y:vertex) (z:vertex) (l:(list vertex)),
(edge x y) -> ((path y l z) -> (path x (Init.Datatypes.cons x l) z)).
Axiom path_right_extension : forall (x:vertex) (y:vertex) (z:vertex)
(l:(list vertex)), (path x l y) -> ((edge y z) -> (path x
(Init.Datatypes.app l (Init.Datatypes.cons y Init.Datatypes.nil)) z)).
Axiom path_right_inversion : forall (x:vertex) (z:vertex) (l:(list vertex)),
(path x l z) -> (((x = z) /\ (l = Init.Datatypes.nil)) \/ exists y:vertex,
exists l':(list vertex), (path x l' y) /\ ((edge y z) /\
(l = (Init.Datatypes.app l' (Init.Datatypes.cons y Init.Datatypes.nil))))).
Axiom path_trans : forall (x:vertex) (y:vertex) (z:vertex) (l1:(list vertex))
(l2:(list vertex)), (path x l1 y) -> ((path y l2 z) -> (path x
(Init.Datatypes.app l1 l2) z)).
Axiom empty_path : forall (x:vertex) (y:vertex), (path x Init.Datatypes.nil
y) -> (x = y).
Axiom path_decomposition : forall (x:vertex) (y:vertex) (z:vertex)
(l1:(list vertex)) (l2:(list vertex)), (path x
(Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z) -> ((path x l1 y) /\
(path y (Init.Datatypes.cons y l2) z)).
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 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))).
Parameter rank: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
Axiom rank_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(list a)),
match s with
| Init.Datatypes.nil => ((rank x s) = (cardinal vertices))
| (Init.Datatypes.cons y s') => (((x = y) /\ ~ (list.Mem.mem x s')) ->
((rank x s) = (list.Length.length s'))) /\ ((~ ((x = y) /\
~ (list.Mem.mem x s'))) -> ((rank x s) = (rank x s')))
end.
Axiom rank_not_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)), (~ (list.Mem.mem x s)) -> ((rank x s) = (cardinal vertices)).
Axiom rank_range : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)), (list.Mem.mem x s) -> ((0%Z <= (rank x s))%Z /\ ((rank x
s) < (list.Length.length s))%Z).
Axiom rank_min : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(list a)), (is_last x s) -> ((list.Mem.mem y s) -> ((rank x
s) <= (rank y s))%Z).
Axiom rank_app_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)) (s':(list a)), (list.Mem.mem x s') -> ((~ (list.Mem.mem x
s)) -> ((rank x (Init.Datatypes.app s' s)) = ((rank x
s') + (list.Length.length s))%Z)).
Axiom rank_app_r : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)) (s':(list a)), (list.Mem.mem x s) -> ((rank x s) = (rank x
(Init.Datatypes.app s' s))).
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)),
((Init.Datatypes.app l1 (Init.Datatypes.cons x l2)) = (Init.Datatypes.app l3 (Init.Datatypes.cons x l4))) ->
((simplelist (Init.Datatypes.app l1 (Init.Datatypes.cons x l2))) ->
((l1 = l3) /\ (l2 = l4))).
Axiom simplelist_hd_max_rank : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (s1 = (Init.Datatypes.cons x s2)) ->
((simplelist s1) -> ((list.Mem.mem y s2) -> ((rank y s1) < (rank x
s1))%Z)).
Axiom rank_before_suffix : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (simplelist
(Init.Datatypes.app s1 s2)) -> ((is_last x s1) -> ((list.Mem.mem y s2) ->
((rank y (Init.Datatypes.app s1 s2)) < (rank x
(Init.Datatypes.app s1 s2)))%Z)).
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 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 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))).
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')).
Definition reachable (x:vertex) (y:vertex): Prop := exists l:(list vertex),
(path x l y).
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 <-> ((rank x s) < (rank y
s))%Z)))))
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) -> (((rank x s) <= (rank y
s))%Z -> (reachable x y)))) /\ forall (y:vertex), (list.Mem.mem y s) ->
exists x:vertex, (mem x g) /\ (((rank x s) <= (rank y s))%Z /\
(reachable y x))))))
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))))).
Require Import mathcomp.ssreflect.ssreflect.
Ltac compress :=
repeat (match goal with [H1: ?A, H2: ?A |- _] => clear H2 end).
Theorem WP_parameter_dfs1 : forall (x:vertex) (e:(set vertex)) (e1:(set
vertex)) (e2:(list vertex)) (e3:(set (set vertex))) (e4:Z) (e5:(map.Map.map
vertex Z)), ((mem x vertices) /\ ((access_to e1 x) /\ ((~ (mem x (union e
e1))) /\ ((wf_env (mk_env e e1 e2 e3 e4 e5)) /\ forall (cc:(set vertex)),
(mem cc e3) <-> ((subset cc e) /\ (is_scc cc)))))) -> forall (o:(set
vertex)) (o1:(set vertex)) (o2:(list vertex)) (o3:(set (set vertex)))
(o4:Z) (o5:(map.Map.map vertex Z)), let o6 := (mk_env o o1 o2 o3 o4 o5) in
(((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))))))) -> let o7 := (successors x) in (((subset
o7 vertices) /\ ((forall (x1:vertex), (mem x1 o7) -> (access_to o1 x1)) /\
((wf_env o6) /\ forall (cc:(set vertex)), (mem cc o3) <-> ((subset cc o) /\
(is_scc cc))))) -> forall (result:Z) (result1:(set vertex)) (result2:(set
vertex)) (result3:(list vertex)) (result4:(set (set vertex))) (result5:Z)
(result6:(map.Map.map vertex Z)), ((wf_env (mk_env result1 result2 result3
result4 result5 result6)) /\ ((forall (cc:(set vertex)), (mem cc
result4) <-> ((subset cc result1) /\ (is_scc cc))) /\ ((forall (x1:vertex),
(mem x1 o7) -> (result <= (map.Map.get result6 x1))%Z) /\
(((result = (cardinal vertices)) \/ exists x1:vertex, (mem x1 o7) /\
(num_of_reachable result x1 (mk_env result1 result2 result3 result4 result5
result6))) /\ ((forall (y:vertex), (xedge_to result3 o2 y) ->
(result <= (map.Map.get result6 y))%Z) /\ ((subset o7 (union result1
result2)) /\ (subenv o6 (mk_env result1 result2 result3 result4 result5
result6)))))))) -> forall (result7:(list vertex)) (result8:(list vertex)),
(((Init.Datatypes.app result7 result8) = result3) /\ ((list.Mem.mem x
result3) -> exists s':(list vertex),
(result7 = (Init.Datatypes.app s' (Init.Datatypes.cons x Init.Datatypes.nil))))) ->
(((exists s':(list vertex),
(result7 = (Init.Datatypes.app s' (Init.Datatypes.cons x Init.Datatypes.nil)))) /\
((result8 = e2) /\ (subset (elements result7) (add x result1)))) ->
((is_subscc (elements result7)) -> ((~ (result < e4)%Z) ->
forall (y:vertex), (in_same_scc y x) -> (list.Mem.mem y result7)))))).
move=> x blacks grays stack sccs sn num.
move=> [r11 [r12 [r13 [i11a i12a]]]].
move=> b0 g0 s0 sccs0 sn0 num0 e0 add_stack_incr_pc.
move: {+}add_stack_incr_pc => [_ [g0_is_xgrays [_ [s0_is_xstack [incr_sn num_x_n]]]]].
move=> roots0 [r'1 [r'2 [i'1a i'1b]]].
move=> n1 b1 g1 s1 sccs1 sn1 num1.
move=> [wf_env1 [i'2b [pc'1 [pc'2 [pc'3 [pc'4 sube0e1]]]]]].
move=> s2 s3 [s1_split s2_split] ass1 ass2.
move=> sn_le_n1.
move=> y same_scc_y_x.
move: {+} same_scc_y_x => [[lyx y_to_x] [lxy x_to_y]].
have y_not_in_s2: ~(~(mem y (elements s2))).
move=> y_not_in_s2.
have x_in_s1: mem x (elements s1).
- move: {+}sube0e1 => [[s [s1_decomp _]] _]. simpl in s1_decomp.
rewrite s1_decomp s0_is_xstack.
by apply /elements_mem /Append.mem_append; right; left.
have x_in_s2: mem x (elements s2).
- move /elements_mem /s2_split :x_in_s1 => [s2' s2_decomp].
rewrite s2_decomp.
by apply /elements_mem /Append.mem_append; right; left.
apply (xset_path_xedge x y lxy (elements s2)) in y_not_in_s2; last by []; last by [].
move: y_not_in_s2 => [x' [y' [x'_in_s2 [y'_not_in_s2 [edge_x'y' [x'_on_lxy y'_on_lxy]]]]]].
move: {+} wf_env1 => [wf_color1 _].
move: {+} wf_color1 => hcol1.
move /(wf_color_3_cases y') :hcol1 => [y'_in_sccs1 | [y'_in_s1 | y'_white]].
- apply set_of_elt in y'_in_sccs1.
move: y'_in_sccs1 => [cc [cc_in_sccs1 y'_in_cc]].
move: {+} cc_in_sccs1 => hcc.
move /i'2b :hcc => [_ cc_is_scc].
have same_scc_y'x: in_same_scc y' x.
- split.
+ apply (reachable_trans _ y); first by [].
by exists lyx.
+ move: x'_on_lxy => [lxx' pathxx'].
exists (lxx' ++ (cons x' nil))%list.
by apply path_right_extension.
have x_in_cc: mem x cc.
- by apply (scc_max y' x cc).
have x_not_in_s1: ~ mem x (elements s1).
- apply (elt_set_of _ _ sccs1) in x_in_cc; last by [].
apply (wf_color_sccs) in wf_color1. simpl in wf_color1.
by move /wf_color1 /diff_def1 :x_in_cc => [ _ x_not_in_s1].
by [].
- move :y'_in_s1; simpl.
rewrite -s1_split elts_app union_def1.
move => [y'_in_s2 | y'_in_s3]; first by [].
move /elements_mem /s2_split :x_in_s1 => [s2' s2_decomp].
move :x'_in_s2; rewrite s2_decomp.
move /elts_app /union_def1 => [x'_in_s2' | x'_eq_x].
- have rky'_lt_rkx: (rank y' s1 < rank x s1)%Z.
+ rewrite -s1_split.
apply (rank_before_suffix x y' s2 s3).
- move: {+} wf_env1 => [_ [_ [_ [simpl_s1 _]]]].
by rewrite s1_split.
- by exists s2'.
- by apply elements_mem.
move :{+} ass1 => [_ [s3_eq_stack _]].
have s1_split' : s1 = (s2' ++ x :: stack)%list.
- by rewrite s2_decomp s3_eq_stack -Append.Append_assoc in s1_split.
have n1_le_num1y': (n1 <= Map.get num1 y')%Z.
+ apply pc'3.
- split.
+ exists s2'; rewrite s0_is_xstack. split; first by [].
exists x'. split; last by[].
by apply elements_mem.
+ rewrite s0_is_xstack -s3_eq_stack.
by simpl; right; apply elements_mem.
have num1y'_lt_num1x: (Map.get num1 y' < Map.get num1 x)%Z.
- move: {+} wf_env1 => [_ [wf_num1 _]].
move :wf_num1 => [_ [_ [_ [_ numrank1]]]].
apply numrank1; last by [].
- rewrite -s1_split.
apply Append.mem_append. right.
by apply elements_mem.
- move: {+}sube0e1 => [[s [s1_decomp _]] _]. simpl in s1_decomp.
rewrite s1_decomp s0_is_xstack.
by apply Append.mem_append; right; left.
have n1_lt_num1x: (n1 < Map.get num1 x)%Z.
- by apply (Z.le_lt_trans _ (Map.get num1 y') _).
have num1x_eq_numx: Map.get num1 x = Map.get num0 x.
- move :sube0e1 => [_ [_ [_ [subnum_e0e1 g0_is_g1]]]]; simpl in g0_is_g1.
rewrite -subnum_e0e1; first by [].
simpl.
rewrite s0_is_xstack.
by simpl; left.
have numx_eq_sn: Map.get num0 x = sn.
- move :add_stack_incr_pc => [_ [_ [_ [_ [_ num0_def]]]]].
by rewrite num0_def Map.Select_eq.
have n1_lt_sn: (n1 < sn)%Z.
- by rewrite -numx_eq_sn -num1x_eq_numx.
have n1_lt_n1: (n1 < n1)%Z.
- by apply (Z.lt_le_trans _ sn _).
omega.
- move/elements_mem: x'_eq_x => [x'_eq_x | nilcase]; last by [].
have n1_le_y': (n1 <= Map.get num1 y')%Z.
- apply pc'1.
rewrite /roots0 -x'_eq_x.
by apply edge_x'y'.
have rky'_lt_rkx: (rank y' s1 < rank x s1)%Z.
- move :ass1 => [_ [s3_eq_stack _]].
move: {+}sube0e1 => [[s [s1_decomp _]] _]. simpl in s1_decomp.
rewrite s1_decomp -rank_app_r; first last.
+ rewrite s0_is_xstack; right.
rewrite -s3_eq_stack.
by apply elements_mem.
+ rewrite s0_is_xstack. rewrite -rank_app_r; last by left.
apply (simplelist_hd_max_rank x _ _ stack); first by [].
- move: i'1a => [wf_color0 [_ [_ [simpl_s0 _]]]].
by rewrite -s0_is_xstack.
- by rewrite -s3_eq_stack; apply elements_mem.
have x_in_s1: Mem.mem x s1.
- move: {+}sube0e1 => [[s [s1_decomp _]] _]. simpl in s1_decomp.
rewrite s1_decomp s0_is_xstack.
by apply Append.mem_append; right; left.
have y'_in_s1: Mem.mem y' s1.
- rewrite -s1_split.
apply Append.mem_append; right.
by apply elements_mem.
have y'_lt_x: (Map.get num1 y' < Map.get num1 x)%Z.
- move: {+} wf_env1 => [_ [wf_num1 _]].
move :wf_num1 => [_ [_ [_ [_ numrank1]]]].
by apply numrank1.
have n1_lt_num1x: (n1 < Map.get num1 x)%Z.
- by apply (Z.le_lt_trans _ (Map.get num1 y') _).
have num1x_eq_numx: Map.get num1 x = Map.get num0 x.
- move :sube0e1 => [_ [_ [_ [subnum_e0e1 _]]]].
rewrite -subnum_e0e1; first by [].
simpl.
rewrite s0_is_xstack.
by simpl; left.
have numx_eq_sn: Map.get num0 x = sn.
- move :add_stack_incr_pc => [_ [_ [_ [_ [_ num0_def]]]]].
by rewrite num0_def Map.Select_eq.
have n1_lt_sn: (n1 < sn)%Z.
- by rewrite -numx_eq_sn -num1x_eq_numx.
have n1_lt_n1: (n1 < n1)%Z.
- by apply (Z.lt_le_trans _ sn _).
omega.
- have y'_not_white: mem y' (union b1 g1).
+ move: ass1 => [_ [_ subset_s2_xb1]].
move /subset_s2_xb1 /add_def1 :x'_in_s2 => [x'_eq_x | x'_in_b1].
- apply: pc'4.
rewrite x'_eq_x in edge_x'y'.
by apply edge_x'y'.
- move: wf_env1 => [_ [_ [hnbtw1 _]]].
by apply: (hnbtw1 x' y').
by [].
have mem_dec: Mem.mem y s2 \/ ~ (Mem.mem y s2).
- by apply lmem_dec.
move: mem_dec => [mem_y_s2 | not_mem_y_s2]; first by [].
by move: not_mem_y_s2; rewrite !elements_mem.
Qed.
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)).
Parameter elements: forall {a:Type} {a_WT:WhyType a}, (list a) -> (set a).
Axiom elements_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
(x:a), (list.Mem.mem x l) <-> (mem x (elements l)).
Axiom elements_Nil : forall {a:Type} {a_WT:WhyType a},
((elements Init.Datatypes.nil) = (empty : (set a))).
Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.
Parameter vertices: (set vertex).
Parameter successors: vertex -> (set vertex).
Axiom successors_vertices : forall (x:vertex), (mem x vertices) -> (subset
(successors x) vertices).
Definition edge (x:vertex) (y:vertex): Prop := (mem x vertices) /\ (mem y
(successors x)).
Inductive path: vertex -> (list vertex) -> vertex -> Prop :=
| Path_empty : forall (x:vertex), (path x Init.Datatypes.nil x)
| Path_cons : forall (x:vertex) (y:vertex) (z:vertex) (l:(list vertex)),
(edge x y) -> ((path y l z) -> (path x (Init.Datatypes.cons x l) z)).
Axiom path_right_extension : forall (x:vertex) (y:vertex) (z:vertex)
(l:(list vertex)), (path x l y) -> ((edge y z) -> (path x
(Init.Datatypes.app l (Init.Datatypes.cons y Init.Datatypes.nil)) z)).
Axiom path_right_inversion : forall (x:vertex) (z:vertex) (l:(list vertex)),
(path x l z) -> (((x = z) /\ (l = Init.Datatypes.nil)) \/ exists y:vertex,
exists l':(list vertex), (path x l' y) /\ ((edge y z) /\
(l = (Init.Datatypes.app l' (Init.Datatypes.cons y Init.Datatypes.nil))))).
Axiom path_trans : forall (x:vertex) (y:vertex) (z:vertex) (l1:(list vertex))
(l2:(list vertex)), (path x l1 y) -> ((path y l2 z) -> (path x
(Init.Datatypes.app l1 l2) z)).
Axiom empty_path : forall (x:vertex) (y:vertex), (path x Init.Datatypes.nil
y) -> (x = y).
Axiom path_decomposition : forall (x:vertex) (y:vertex) (z:vertex)
(l1:(list vertex)) (l2:(list vertex)), (path x
(Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z) -> ((path x l1 y) /\
(path y (Init.Datatypes.cons y l2) z)).
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 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))).
Parameter rank: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
Axiom rank_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(list a)),
match s with
| Init.Datatypes.nil => ((rank x s) = (cardinal vertices))
| (Init.Datatypes.cons y s') => (((x = y) /\ ~ (list.Mem.mem x s')) ->
((rank x s) = (list.Length.length s'))) /\ ((~ ((x = y) /\
~ (list.Mem.mem x s'))) -> ((rank x s) = (rank x s')))
end.
Axiom rank_not_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)), (~ (list.Mem.mem x s)) -> ((rank x s) = (cardinal vertices)).
Axiom rank_range : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)), (list.Mem.mem x s) -> ((0%Z <= (rank x s))%Z /\ ((rank x
s) < (list.Length.length s))%Z).
Axiom rank_min : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(list a)), (is_last x s) -> ((list.Mem.mem y s) -> ((rank x
s) <= (rank y s))%Z).
Axiom rank_app_l : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)) (s':(list a)), (list.Mem.mem x s') -> ((~ (list.Mem.mem x
s)) -> ((rank x (Init.Datatypes.app s' s)) = ((rank x
s') + (list.Length.length s))%Z)).
Axiom rank_app_r : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(s:(list a)) (s':(list a)), (list.Mem.mem x s) -> ((rank x s) = (rank x
(Init.Datatypes.app s' s))).
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)),
((Init.Datatypes.app l1 (Init.Datatypes.cons x l2)) = (Init.Datatypes.app l3 (Init.Datatypes.cons x l4))) ->
((simplelist (Init.Datatypes.app l1 (Init.Datatypes.cons x l2))) ->
((l1 = l3) /\ (l2 = l4))).
Axiom simplelist_hd_max_rank : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (s1 = (Init.Datatypes.cons x s2)) ->
((simplelist s1) -> ((list.Mem.mem y s2) -> ((rank y s1) < (rank x
s1))%Z)).
Axiom rank_before_suffix : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a) (s1:(list a)) (s2:(list a)), (simplelist
(Init.Datatypes.app s1 s2)) -> ((is_last x s1) -> ((list.Mem.mem y s2) ->
((rank y (Init.Datatypes.app s1 s2)) < (rank x
(Init.Datatypes.app s1 s2)))%Z)).
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 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 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))).
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')).
Definition reachable (x:vertex) (y:vertex): Prop := exists l:(list vertex),
(path x l y).
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 <-> ((rank x s) < (rank y
s))%Z)))))
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) -> (((rank x s) <= (rank y
s))%Z -> (reachable x y)))) /\ forall (y:vertex), (list.Mem.mem y s) ->
exists x:vertex, (mem x g) /\ (((rank x s) <= (rank y s))%Z /\
(reachable y x))))))
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))))).
Require Import mathcomp.ssreflect.ssreflect.
Ltac compress :=
repeat (match goal with [H1: ?A, H2: ?A |- _] => clear H2 end).
Theorem WP_parameter_dfs1 : forall (x:vertex) (e:(set vertex)) (e1:(set
vertex)) (e2:(list vertex)) (e3:(set (set vertex))) (e4:Z) (e5:(map.Map.map
vertex Z)), ((mem x vertices) /\ ((access_to e1 x) /\ ((~ (mem x (union e
e1))) /\ ((wf_env (mk_env e e1 e2 e3 e4 e5)) /\ forall (cc:(set vertex)),
(mem cc e3) <-> ((subset cc e) /\ (is_scc cc)))))) -> forall (o:(set
vertex)) (o1:(set vertex)) (o2:(list vertex)) (o3:(set (set vertex)))
(o4:Z) (o5:(map.Map.map vertex Z)), let o6 := (mk_env o o1 o2 o3 o4 o5) in
(((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))))))) -> let o7 := (successors x) in (((subset
o7 vertices) /\ ((forall (x1:vertex), (mem x1 o7) -> (access_to o1 x1)) /\
((wf_env o6) /\ forall (cc:(set vertex)), (mem cc o3) <-> ((subset cc o) /\
(is_scc cc))))) -> forall (result:Z) (result1:(set vertex)) (result2:(set
vertex)) (result3:(list vertex)) (result4:(set (set vertex))) (result5:Z)
(result6:(map.Map.map vertex Z)), ((wf_env (mk_env result1 result2 result3
result4 result5 result6)) /\ ((forall (cc:(set vertex)), (mem cc
result4) <-> ((subset cc result1) /\ (is_scc cc))) /\ ((forall (x1:vertex),
(mem x1 o7) -> (result <= (map.Map.get result6 x1))%Z) /\
(((result = (cardinal vertices)) \/ exists x1:vertex, (mem x1 o7) /\
(num_of_reachable result x1 (mk_env result1 result2 result3 result4 result5
result6))) /\ ((forall (y:vertex), (xedge_to result3 o2 y) ->
(result <= (map.Map.get result6 y))%Z) /\ ((subset o7 (union result1
result2)) /\ (subenv o6 (mk_env result1 result2 result3 result4 result5
result6)))))))) -> forall (result7:(list vertex)) (result8:(list vertex)),
(((Init.Datatypes.app result7 result8) = result3) /\ ((list.Mem.mem x
result3) -> exists s':(list vertex),
(result7 = (Init.Datatypes.app s' (Init.Datatypes.cons x Init.Datatypes.nil))))) ->
(((exists s':(list vertex),
(result7 = (Init.Datatypes.app s' (Init.Datatypes.cons x Init.Datatypes.nil)))) /\
((result8 = e2) /\ (subset (elements result7) (add x result1)))) ->
((is_subscc (elements result7)) -> ((~ (result < e4)%Z) ->
forall (y:vertex), (in_same_scc y x) -> (list.Mem.mem y result7)))))).
move=> x blacks grays stack sccs sn num.
move=> [r11 [r12 [r13 [i11a i12a]]]].
move=> b0 g0 s0 sccs0 sn0 num0 e0 add_stack_incr_pc.
move: {+}add_stack_incr_pc => [_ [g0_is_xgrays [_ [s0_is_xstack [incr_sn num_x_n]]]]].
move=> roots0 [r'1 [r'2 [i'1a i'1b]]].
move=> n1 b1 g1 s1 sccs1 sn1 num1.
move=> [wf_env1 [i'2b [pc'1 [pc'2 [pc'3 [pc'4 sube0e1]]]]]].
move=> s2 s3 [s1_split s2_split] ass1 ass2.
move=> sn_le_n1.
move=> y same_scc_y_x.
move: {+} same_scc_y_x => [[lyx y_to_x] [lxy x_to_y]].
have y_not_in_s2: ~(~(mem y (elements s2))).
move=> y_not_in_s2.
have x_in_s1: mem x (elements s1).
- move: {+}sube0e1 => [[s [s1_decomp _]] _]. simpl in s1_decomp.
rewrite s1_decomp s0_is_xstack.
by apply /elements_mem /Append.mem_append; right; left.
have x_in_s2: mem x (elements s2).
- move /elements_mem /s2_split :x_in_s1 => [s2' s2_decomp].
rewrite s2_decomp.
by apply /elements_mem /Append.mem_append; right; left.
apply (xset_path_xedge x y lxy (elements s2)) in y_not_in_s2; last by []; last by [].
move: y_not_in_s2 => [x' [y' [x'_in_s2 [y'_not_in_s2 [edge_x'y' [x'_on_lxy y'_on_lxy]]]]]].
move: {+} wf_env1 => [wf_color1 _].
move: {+} wf_color1 => hcol1.
move /(wf_color_3_cases y') :hcol1 => [y'_in_sccs1 | [y'_in_s1 | y'_white]].
- apply set_of_elt in y'_in_sccs1.
move: y'_in_sccs1 => [cc [cc_in_sccs1 y'_in_cc]].
move: {+} cc_in_sccs1 => hcc.
move /i'2b :hcc => [_ cc_is_scc].
have same_scc_y'x: in_same_scc y' x.
- split.
+ apply (reachable_trans _ y); first by [].
by exists lyx.
+ move: x'_on_lxy => [lxx' pathxx'].
exists (lxx' ++ (cons x' nil))%list.
by apply path_right_extension.
have x_in_cc: mem x cc.
- by apply (scc_max y' x cc).
have x_not_in_s1: ~ mem x (elements s1).
- apply (elt_set_of _ _ sccs1) in x_in_cc; last by [].
apply (wf_color_sccs) in wf_color1. simpl in wf_color1.
by move /wf_color1 /diff_def1 :x_in_cc => [ _ x_not_in_s1].
by [].
- move :y'_in_s1; simpl.
rewrite -s1_split elts_app union_def1.
move => [y'_in_s2 | y'_in_s3]; first by [].
move /elements_mem /s2_split :x_in_s1 => [s2' s2_decomp].
move :x'_in_s2; rewrite s2_decomp.
move /elts_app /union_def1 => [x'_in_s2' | x'_eq_x].
- have rky'_lt_rkx: (rank y' s1 < rank x s1)%Z.
+ rewrite -s1_split.
apply (rank_before_suffix x y' s2 s3).
- move: {+} wf_env1 => [_ [_ [_ [simpl_s1 _]]]].
by rewrite s1_split.
- by exists s2'.
- by apply elements_mem.
move :{+} ass1 => [_ [s3_eq_stack _]].
have s1_split' : s1 = (s2' ++ x :: stack)%list.
- by rewrite s2_decomp s3_eq_stack -Append.Append_assoc in s1_split.
have n1_le_num1y': (n1 <= Map.get num1 y')%Z.
+ apply pc'3.
- split.
+ exists s2'; rewrite s0_is_xstack. split; first by [].
exists x'. split; last by[].
by apply elements_mem.
+ rewrite s0_is_xstack -s3_eq_stack.
by simpl; right; apply elements_mem.
have num1y'_lt_num1x: (Map.get num1 y' < Map.get num1 x)%Z.
- move: {+} wf_env1 => [_ [wf_num1 _]].
move :wf_num1 => [_ [_ [_ [_ numrank1]]]].
apply numrank1; last by [].
- rewrite -s1_split.
apply Append.mem_append. right.
by apply elements_mem.
- move: {+}sube0e1 => [[s [s1_decomp _]] _]. simpl in s1_decomp.
rewrite s1_decomp s0_is_xstack.
by apply Append.mem_append; right; left.
have n1_lt_num1x: (n1 < Map.get num1 x)%Z.
- by apply (Z.le_lt_trans _ (Map.get num1 y') _).
have num1x_eq_numx: Map.get num1 x = Map.get num0 x.
- move :sube0e1 => [_ [_ [_ [subnum_e0e1 g0_is_g1]]]]; simpl in g0_is_g1.
rewrite -subnum_e0e1; first by [].
simpl.
rewrite s0_is_xstack.
by simpl; left.
have numx_eq_sn: Map.get num0 x = sn.
- move :add_stack_incr_pc => [_ [_ [_ [_ [_ num0_def]]]]].
by rewrite num0_def Map.Select_eq.
have n1_lt_sn: (n1 < sn)%Z.
- by rewrite -numx_eq_sn -num1x_eq_numx.
have n1_lt_n1: (n1 < n1)%Z.
- by apply (Z.lt_le_trans _ sn _).
omega.
- move/elements_mem: x'_eq_x => [x'_eq_x | nilcase]; last by [].
have n1_le_y': (n1 <= Map.get num1 y')%Z.
- apply pc'1.
rewrite /roots0 -x'_eq_x.
by apply edge_x'y'.
have rky'_lt_rkx: (rank y' s1 < rank x s1)%Z.
- move :ass1 => [_ [s3_eq_stack _]].
move: {+}sube0e1 => [[s [s1_decomp _]] _]. simpl in s1_decomp.
rewrite s1_decomp -rank_app_r; first last.
+ rewrite s0_is_xstack; right.
rewrite -s3_eq_stack.
by apply elements_mem.
+ rewrite s0_is_xstack. rewrite -rank_app_r; last by left.
apply (simplelist_hd_max_rank x _ _ stack); first by [].
- move: i'1a => [wf_color0 [_ [_ [simpl_s0 _]]]].
by rewrite -s0_is_xstack.
- by rewrite -s3_eq_stack; apply elements_mem.
have x_in_s1: Mem.mem x s1.
- move: {+}sube0e1 => [[s [s1_decomp _]] _]. simpl in s1_decomp.
rewrite s1_decomp s0_is_xstack.
by apply Append.mem_append; right; left.
have y'_in_s1: Mem.mem y' s1.
- rewrite -s1_split.
apply Append.mem_append; right.
by apply elements_mem.
have y'_lt_x: (Map.get num1 y' < Map.get num1 x)%Z.
- move: {+} wf_env1 => [_ [wf_num1 _]].
move :wf_num1 => [_ [_ [_ [_ numrank1]]]].
by apply numrank1.
have n1_lt_num1x: (n1 < Map.get num1 x)%Z.
- by apply (Z.le_lt_trans _ (Map.get num1 y') _).
have num1x_eq_numx: Map.get num1 x = Map.get num0 x.
- move :sube0e1 => [_ [_ [_ [subnum_e0e1 _]]]].
rewrite -subnum_e0e1; first by [].
simpl.
rewrite s0_is_xstack.
by simpl; left.
have numx_eq_sn: Map.get num0 x = sn.
- move :add_stack_incr_pc => [_ [_ [_ [_ [_ num0_def]]]]].
by rewrite num0_def Map.Select_eq.
have n1_lt_sn: (n1 < sn)%Z.
- by rewrite -numx_eq_sn -num1x_eq_numx.
have n1_lt_n1: (n1 < n1)%Z.
- by apply (Z.lt_le_trans _ sn _).
omega.
- have y'_not_white: mem y' (union b1 g1).
+ move: ass1 => [_ [_ subset_s2_xb1]].
move /subset_s2_xb1 /add_def1 :x'_in_s2 => [x'_eq_x | x'_in_b1].
- apply: pc'4.
rewrite x'_eq_x in edge_x'y'.
by apply edge_x'y'.
- move: wf_env1 => [_ [_ [hnbtw1 _]]].
by apply: (hnbtw1 x' y').
by [].
have mem_dec: Mem.mem y s2 \/ ~ (Mem.mem y s2).
- by apply lmem_dec.
move: mem_dec => [mem_y_s2 | not_mem_y_s2]; first by [].
by move: not_mem_y_s2; rewrite !elements_mem.
Qed.