chip.closure
From mathcomp
Require Import all_ssreflect.
From chip
Require Import close_dfs.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section Closure.
Variable V : finType.
Variable g : rel V.
Variable modified : {set V}.
Definition impacted := \bigcup_( x | x \in modified) [set y | connect g x y].
Lemma impactedP x :
reflect
(exists2 v, v \in modified & connect g v x)
(x \in impacted).
Proof.
apply: (iffP idP).
- move/bigcupP => [v H_v H_i].
exists v; first by [].
by rewrite inE in H_i.
- move => [v H_m H_c].
apply/bigcupP.
exists v; first by [].
by rewrite inE.
Qed.
Lemma rclosed_impacted :
forall x y, connect g x y -> x \in impacted -> y \in impacted.
Proof.
move => x y Hc.
move/bigcupP => [v Hv] Hcx.
apply/bigcupP.
exists v => //.
rewrite inE.
rewrite inE in Hcx.
exact: connect_trans Hcx Hc.
Qed.
End Closure.
Require Import all_ssreflect.
From chip
Require Import close_dfs.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section Closure.
Variable V : finType.
Variable g : rel V.
Variable modified : {set V}.
Definition impacted := \bigcup_( x | x \in modified) [set y | connect g x y].
Lemma impactedP x :
reflect
(exists2 v, v \in modified & connect g v x)
(x \in impacted).
Proof.
apply: (iffP idP).
- move/bigcupP => [v H_v H_i].
exists v; first by [].
by rewrite inE in H_i.
- move => [v H_m H_c].
apply/bigcupP.
exists v; first by [].
by rewrite inE.
Qed.
Lemma rclosed_impacted :
forall x y, connect g x y -> x \in impacted -> y \in impacted.
Proof.
move => x y Hc.
move/bigcupP => [v Hv] Hcx.
apply/bigcupP.
exists v => //.
rewrite inE.
rewrite inE in Hcx.
exact: connect_trans Hcx Hc.
Qed.
End Closure.