Table des matières
Preuves sur les graphes
(:brush=isabelle:) text ‹
CentraleSupélec Algorithms course: Proofs of the theorems of the first practical session frederic.boulanger@centralesupelec.fr, November 2018
› (*<*) theory AlgoST2_TD1 imports Main begin (*>*)
section‹Graph type› text‹
We define here graphs as a set of vertices and a set of edges, an edge being a pair of vertices. We add the constraint that the extremities of the edges must belong to the set of vertices. Vertices are represented with natural integers. These types allow the representation of directed or not directed graphs, the directedness depends on how we interpret the set of edges. Loops (edges from a vertex to the same vertex) are allowed, as well as infinite graphs. Multigraphs (with more than one edge between two given vertices) are not supported.
› type_synonym vertex = ‹nat› type_synonym edge = ‹vertex × vertex› typedef graph = ‹{(V::vertex set, E::edge set). E ⊆ V×V}› by blast
text‹
The constraint in the type definition makes the graph type distinct from its support. We obtain the representation of a graph as a pair (E,V) using \<^term>‹Rep_graph›, and we can obtain a graph from an \<^term>‹(E,V)› pair that satisfies the constraint using \<^term>‹Abs_graph›. We define here two abbreviations for accessing the set of vertices and the set of edges of a graph:
›
abbreviation ‹vertices g ≡ (fst (Rep_graph g))› abbreviation ‹edges g ≡ (snd (Rep_graph g))›
text‹An example of a graph:› (*
1 -- 2 -- 3 -- 4 | \ | \/ | | | \ | /\ | | 5 6 -- 7 -- 8
- )
definition ‹g1::graph ≡ Abs_graph (
{1,2,3,4,5,6,7,8}, {(1,2),(1,5),(1,6), (2,3),(2,6),(2,7), (3,4),(3,6),(3,8), (4,8), (6,3), (7,2),(7,3),(7,8) })›
text‹
Neighbours of a node, in a graph as well as in a directed graph:
› definition neighbours :: ‹graph ⇒ vertex ⇒ vertex set› where
‹neighbours g v ≡ {w ∈ vertices g. ∃ e ∈ edges g. e = (v, w) ∨ e = (w, v)}›
definition directedNeighbours :: ‹graph ⇒ vertex ⇒ vertex set› where
‹directedNeighbours g v ≡ {w ∈ vertices g. ∃ e ∈ edges g. e = (v, w)}›
subsection‹Some basic lemmas about edges and vertices› text‹
The set of edges of a graph is included in the cartesian product of the set of its vertices:
› lemma edges_in_vertprod:‹edges g ⊆ vertices g × vertices g› proof -
{ fix e assume h:‹e ∈ edges g› from Rep_graph have ‹Rep_graph g ∈ {(V, E). E ⊆ V×V}› . hence ‹∃V E. Rep_graph g = (V, E) ∧ E ⊆ V×V› by blast from this obtain V and E where rep:‹Rep_graph g = (V, E) ∧ E ⊆ V×V› by blast with h have ‹e ∈ V×V› by auto with rep have ‹e ∈ vertices g × vertices g› by auto } thus ?thesis by (simp add: subsetI)
qed
text‹
The extremities of an edge are vertices:
› lemma edges_link_vertices:
assumes ‹e ∈ edges g› shows ‹(fst e) ∈ vertices g› and ‹(snd e) ∈ vertices g› using assms edges_in_vertprod by fastforce+
section‹Paths and cycles› text‹
A directed path is a list of vertices such that each pair formed of consecutive nodes is an edge.
› definition isDirectedPath where
‹isDirectedPath l g ≡ length l > 1 ∧ (∀i. Suc i < length l ⟶ (l!i, l!Suc i) ∈ edges g)›
text‹
All elements in a directed path are vertices.
› lemma dpath_in_vertices:
assumes ‹isDirectedPath l g› shows ‹set l ⊆ vertices g›
proof
fix v assume ‹v ∈ set l› hence ‹∃i < length l. l!i = v› by (simp add: in_set_conv_nth) from this obtain i where i_def:‹i < length l ∧ l!i = v› by blast show ‹v ∈ vertices g› proof (cases ‹i = 0›) case True with assms have ‹Suc i < length l› unfolding isDirectedPath_def by simp with assms have ‹(l!i, l!(Suc i)) ∈ edges g› unfolding isDirectedPath_def by simp thus ?thesis using edges_link_vertices i_def by fastforce next case False from this obtain k where ‹i = Suc k› using gr0_implies_Suc by blast with i_def assms have ‹(l!k, l!i) ∈ edges g› unfolding isDirectedPath_def by blast thus ?thesis using edges_link_vertices i_def by fastforce qed
qed
text‹
A directed path in a subgraph is a directed path of the graph.
› lemma dpath_subgraph:
assumes ‹edges sg ⊆ edges g› and ‹isDirectedPath l sg› shows ‹isDirectedPath l g›
proof -
from assms(2) have len:‹length l > 1› and edge:‹∀i. Suc i < length l ⟶ (l!i, l!(Suc i)) ∈ edges sg› unfolding isDirectedPath_def by simp+ from edge and assms(1) have ‹∀i. Suc i < length l ⟶ (l!i, l!(Suc i)) ∈ edges g› by blast with len show ?thesis unfolding isDirectedPath_def by simp
qed
text‹
A path is similar but does not take the orientation of the edges into account.
› definition isPath where
‹isPath l g ≡ length l > 1 ∧ (∀i. Suc i < length l ⟶ (l!i, l!Suc i) ∈ edges g ∨ (l!Suc i, l!i) ∈ edges g)›
text‹
All elements in a path are vertices.
› lemma path_in_vertices:
assumes ‹isPath l g› shows ‹set l ⊆ vertices g›
proof
fix v assume ‹v ∈ set l› hence ‹∃i < length l. l!i = v› by (simp add: in_set_conv_nth) from this obtain i where i_def:‹i < length l ∧ l!i = v› by blast show ‹v ∈ vertices g› proof (cases ‹i = 0›) case True with assms have ‹Suc i < length l› unfolding isPath_def by simp with assms have ‹(l!i, l!(Suc i)) ∈ edges g ∨ (l!(Suc i), l!i) ∈ edges g› unfolding isPath_def by simp thus ?thesis using edges_link_vertices i_def by fastforce next case False from this obtain k where ‹i = Suc k› using gr0_implies_Suc by blast with i_def assms have ‹(l!k, l!i) ∈ edges g ∨ (l!i, l!k) ∈ edges g› unfolding isPath_def by blast thus ?thesis using edges_link_vertices i_def by fastforce qed
qed
text‹
A path in a subgraph is a path of the graph.
› lemma path_subgraph:
assumes ‹edges sg ⊆ edges g› and ‹isPath l sg› shows ‹isPath l g›
proof -
from assms(2) have len:‹length l > 1› and edge:‹∀i. Suc i < length l ⟶ (l!i, l!(Suc i)) ∈ edges sg ∨ (l!(Suc i), l!i) ∈ edges sg› unfolding isPath_def by simp+ from edge and assms(1) have ‹∀i. Suc i < length l ⟶ (l!i, l!(Suc i)) ∈ edges g ∨ (l!(Suc i), l!i) ∈ edges g› by blast with len show ?thesis unfolding isPath_def by simp
qed
text‹
A directed cycle is a directed path which ends where it starts and contains at least two nodes.
› definition isDirectedCycle
where ‹isDirectedCycle l g ≡ l!0 = l!(length l - 1) ∧ isDirectedPath l g ›
text‹
A cycle is a path which ends where it starts and contains at least two nodes.
› definition isCycle
where ‹isCycle l g ≡ length l > 1 ∧ l!0 = l!(length l - 1) ∧ isPath l g ›
section‹Properties of graphs› text‹
A bipartite graph has a partition of its vertices into two sets, such that all edges have an extremity in one set of the partition and the other extremity in the other set.
› abbreviation ‹twoParts g V1 V2 ≡
V1 ∪ V2 = vertices g ∧ V1 ∩ V2 = {} ∧ (∀ e ∈ edges g. ((fst e) ∈ V1 ∧ (snd e) ∈ V2) ∨ ((fst e) ∈ V2 ∧ (snd e) ∈ V1))›
definition isBipartite
where ‹isBipartite g ≡ (∃V1 V2. twoParts g V1 V2)›
text‹
A 2-colorable graph is a graph in which it is possible, using only two colors, to assign a color to each node without having two adjacent nodes with the same color. Here, we choose \<^term>‹True› and \<^term>‹False› as colors :
› definition isTwoColorable where
‹isTwoColorable g ≡ ∃f::nat ⇒ bool. ∀ e ∈ edges g. f (fst e) ≠ f (snd e)›
text‹
A directed acyclic graph is a directed graph with no cycle.
› definition isDAG where
‹isDAG g ≡ (∀l::vertex list. ¬isDirectedCycle l g)›
text‹
Subgraphs of a DAG are DAGs.
› lemma dag_subgraph:
assumes ‹isDAG g› and ‹edges sg ⊆ edges g› shows ‹isDAG sg› unfolding isDAG_def isDirectedCycle_def using assms(1) dpath_subgraph[OF assms(2)] isDAG_def isDirectedCycle_def by blast
section‹First theorem about bipartite graphs› text‹
All cycles in a bipartite graph have an even length (number of edges). We first show that for a list \<^term>‹l› of vertices and a partition \<^term>‹(V, V')› of graph, if the first node of the list is in \<^term>‹V›, then: ▪ after following an even number of edges, we have a node in \<^term>‹V› ▪ after following an odd number of edges, we have a node in \<^term>‹V'›
› lemma step2V:
assumes ‹∀i. Suc (Suc i) < length l ∧ l!i ∈ V ⟶ l!(Suc(Suc i)) ∈ V› and ‹∀i. Suc i < length l ∧ l!i ∈ V ⟶ l!(Suc i) ∈ V'› and ‹l!0 ∈ V› shows ‹((Suc^^(2*k)) 0 < length l ⟶ l!((Suc^^(2*k)) 0) ∈ V) ∧ ((Suc^^(2*k+1)) 0 < length l ⟶ l!((Suc^^(2*k+1)) 0) ∈ V')›
proof (induction k)
case 0 text‹ The case \<^term>‹k=0› is easy because \<^term>‹Suc^^0 = id› and \<^term>‹Suc^^1 = Suc›. › thus ?case using assms(2,3) by simp
next
case (Suc k') text‹First, if \<^term>‹2+2*k' < length l› then \<^term>‹2*k' < length l›› have ‹Suc (Suc ((Suc^^(2 * k')) 0)) < length l ⟶ (Suc^^(2 * k')) 0 < length l› by auto text‹With the induction hypothesis, we know that after \<^term>‹2*k'› edges, we have a node in V.› with Suc.IH have ‹Suc (Suc ((Suc^^(2 * k')) 0)) < length l ⟶ l!(Suc^^(2 * k')) 0 ∈ V› by blast text‹With the first assumption, we know that after \<^term>‹2+2*k'› edges, we have a node in V.› with assms(1) have ‹Suc (Suc ((Suc^^(2 * k')) 0)) < length l ⟶ l!(Suc (Suc ((Suc^^(2 * k')) 0))) ∈ V› by blast text‹With some massaging of the powers of Suc, we get the first part of our theorem.› moreover have ‹Suc^^(2*(Suc k')) = Suc^^(2*k') ∘ Suc ∘ Suc› by auto ultimately have 1:‹(Suc^^(2*(Suc k'))) 0 < length l ⟶ l!(Suc^^(2 * (Suc k'))) 0 ∈ V› by auto text‹With the second assumption, we get the second part of our theorem.› with assms(2) have ‹Suc ((Suc^^(2*(Suc k'))) 0) < length l ⟶ l!(Suc ((Suc^^(2 * (Suc k'))) 0)) ∈ V'› using Suc_lessD by blast hence 2:‹(Suc^^(2*(Suc k')+1)) 0 < length l ⟶ l!((Suc^^(2 * (Suc k') + 1)) 0) ∈ V'› by simp from 1 2 show ?case ..
qed
text‹Some lemmas about even and odd numbers.› lemma even_sucpow_even:‹even n = (∃k. n = (Suc^^(2*k)) 0)› by (simp add: dvd_def) lemma odd_sucpow_odd:‹odd n = (∃k. n = Suc ((Suc^^(2*k)) 0))› using oddE by fastforce
text‹
The main part of our proof: if V and V' are a bipartition of g, and if l is a cycle in g which starts in V, then the length of the cycle is even. The length of the cycle is the number of edges, but the cycle is a list of edges, so we have to subtract 1 to obtain it.
› lemma twoParts_all_cycles_even:
assumes ‹twoParts g V V'› and ‹isCycle l g› and ‹l!0 ∈ V› shows ‹even (length l - 1)›
proof -
text‹Edges connect nodes from distinct subsets of the partition› have alt:‹∀ e ∈ edges g. ((fst e) ∈ V ⟶ (snd e) ∈ V') ∧ ((fst e) ∈ V' ⟶ (snd e) ∈ V)› using assms(1) by blast text‹The vertices of the cycle alternate between the two subsets of the partition› have alt1:‹∀ i. Suc i < length l ∧ l!i ∈ V ⟶ l!(Suc i) ∈ V'› using assms(1,2) unfolding isCycle_def isPath_def by fastforce have alt1':‹∀ i. Suc i < length l ∧ l!i ∈ V' ⟶ l!(Suc i) ∈ V› using assms(1,2) unfolding isCycle_def isPath_def by fastforce text‹So we stay in the same subset when skipping a node.› have alt2:‹∀ i. Suc (Suc i) < length l ∧ l!i ∈ V ⟶ l!(Suc (Suc i)) ∈ V› using alt1 alt1' by auto text‹After an even number of steps in the cycle, we get into the starting subset› have evenV:‹∀k::nat. (Suc^^(2*k)) 0 < length l ⟶ l!((Suc^^(2*k)) 0) ∈ V› using assms(3) step2V alt2 by blast text‹And after an odd number of steps in the cycle, we get into the other subset› hence oddV':‹∀k::nat. Suc ((Suc^^(2*k)) 0) < length l ⟶ l!(Suc ((Suc^^(2*k)) 0)) ∈ V'› using assms(3) step2V alt1 by auto text‹A cycle starts and ends at the same vertex› from assms(2) have c:‹l!0 = l!(length l - 1)› unfolding isCycle_def by simp text‹So the lastnode of the cycle is in V› with assms(3) have lastInV:‹l!(length l - 1) ∈ V› by simp text‹We can now prove our theorem:› show ?thesis proof - text‹The proof is by contradiction: assume the length of the cycle is not even› { assume ‹¬even (length l - 1)› text‹So the length is odd and we get \<^term>‹k› such that the length is \<^term>‹2*k+1›› with odd_sucpow_odd obtain k where ‹(length l - 1) = Suc ((Suc^^(2*k)) 0)› by blast text‹But we know that following an odd number of edges leads to a node in V'... › with oddV' have ‹l!(length l - 1) ∈ V'› by simp text‹Which is therefore not in V › with assms(1) have ‹l!(length l - 1) ∉ V› by blast text‹Which contradicts the fact that the last node is in V› with lastInV have False by simp } text‹So, the assumption is false, and the theorem is proved.› thus ?thesis by blast qed
qed
text‹Now, the real theorem: All cycles in a bipartite graph have an even length (number of edges).› lemma bipartite_all_cycles_even:
assumes ‹isBipartite g› and ‹isCycle l g› shows ‹even ((length l) - 1)› (* the number of edges is the number of vertices minus 1 *)
proof -
text‹From the first assumption, get a bipartition of g› from assms(1) obtain V1 and V2 where bip:‹twoParts g V1 V2› unfolding isBipartite_def by blast hence bip':‹twoParts g V2 V1› by blast show ?thesis text‹We have two cases: the first node of the cycle may be in V1 or in V2.› proof (cases ‹l!0 ∈ V1›) case True text‹This case reduces to our previous lemma› from twoParts_all_cycles_even[OF bip assms(2) this] show ?thesis . next case False text‹\<^term>‹l!0› is not in V1, but we have to prove that it is in V2!› from assms(2) have ‹l!0 ∈ vertices g› unfolding isCycle_def using path_in_vertices by fastforce with `l ! 0 ∉ V1` bip have ‹l!0 ∈ V2› by blast text‹And we can now reuse the previous lemma› from twoParts_all_cycles_even[OF bip' assms(2) this] show ?thesis . qed
qed
section‹Second theorem about bipartite graph› text‹
Bipartite graphs are exactly 2-colorable graphs.
› lemma ‹isTwoColorable g = isBipartite g› proof
text‹First, we show \<^term>‹isTwoColorable g ⟹ isBipartite g›› { assume ‹isTwoColorable g› text‹Get the coloring function \<^term>‹f›› from isTwoColorable_def this obtain f::‹nat ⇒ bool› where h:‹∀ e ∈ edges g. f (fst e) ≠ f (snd e)› by blast text‹Define the subsets V1 and V2 of same color nodes.› define V1 V2 where ‹V1 = {v. f v} ∩ vertices g› and ‹V2 = {v. ¬f v} ∩ vertices g› text‹And show that they form a bipartition of g.› have ‹twoParts g V1 V2› using edges_link_vertices h V1_def V2_def by auto hence ‹isBipartite g› using isBipartite_def by blast } thus ‹isTwoColorable g ⟹ isBipartite g› using isBipartite_def by simp text‹First, we show \<^term>‹isBipartite g ⟹ isTwoColorable g›› { assume ‹isBipartite g› text‹Get the bipartition of g› from isBipartite_def this obtain V1 and V2 where h:‹twoParts g V1 V2› by auto text‹Then define a bicoloring function based on V1 and V2.› define f where ‹f = (λn. n ∈ V1)› text‹and show that the graph is 2-colorable.› from h have ‹∀e ∈ edges g. f (fst e) ≠ f (snd e)› using f_def by blast hence ‹∃f::nat ⇒ bool. ∀e ∈ edges g. f (fst e) ≠ f (snd e)› by blast } thus ‹isBipartite g ⟹ isTwoColorable g› using isTwoColorable_def by simp
qed
section‹A property of DAGs› text‹
We want to show that in any directed acyclic graph, there is at least one vertex that has no incoming edge. First, we prove by induction that in a non-empty graph where all vertices have at least an incoming edge, there are directed paths of arbitrary length.
› lemma arbitrary_length_chain_suc:
assumes ‹∀v ∈ vertices g. ∃e ∈ edges g. v = snd e› and ‹vertices g ≠ {}› shows ‹∃l. length l = Suc (Suc n) ∧ isDirectedPath l g›
proof (induction n)
case 0 text‹Build a path of length one (two vertyices).› from assms(2) obtain node where node_def:‹node ∈ vertices g› by blast with assms(1) obtain edge where edge_def:‹edge ∈ edges g ∧ node = snd edge› by blast define prev where ‹prev = fst edge› have ‹prev ∈ vertices g› using prev_def edge_def by (simp add: edges_link_vertices) hence ‹isDirectedPath [prev, node] g› unfolding isDirectedPath_def using node_def edge_def prev_def by auto thus ?case by force
next
case (Suc k) text‹Here, we have to extend a directed path using the first assumption› from Suc.IH obtain ll where llprop:‹length ll = Suc (Suc k) ∧ isDirectedPath ll g› by blast text‹ For this, we consider the first vertex of the path, get an incoming edge to this vertex, and extend the path with the first extremity of this edge. › hence ‹ll!0 ∈ vertices g› using dpath_in_vertices by fastforce with assms(1) obtain e where exarc:‹e ∈ edges g ∧ ll!0 = snd e› by blast define lll where ‹lll = (fst e)#ll› with llprop have ‹length lll = Suc (Suc (Suc k)) ∧ isDirectedPath lll g› using Suc isDirectedPath_def edges_link_vertices exarc less_Suc_eq_0_disj by auto thus ?case by blast
qed
corollary arbitrary_length_chain:
assumes ‹∀v ∈ vertices g. ∃e ∈ edges g. v = snd e› and ‹vertices g ≠ {}› and ‹n > 1› shows ‹∃l. length l = n ∧ isDirectedPath l g›
proof -
from assms(3) have ‹∃k. n = Suc (Suc k)› using less_imp_Suc_add by fastforce thus ?thesis using arbitrary_length_chain_suc using assms(1,2) by blast
qed
subsection‹Some theorems about lists and finite sets› text‹
A list of items from a finite set which is longer that the cardinal of the set has repeated elements.
› lemma biglist_from_set_repeat:
assumes ‹finite s› and ‹set l ⊆ s› and ‹length l > card s› shows ‹∃i j. i < length l ∧ j < length l ∧ i ≠ j ∧ l!i = l!j› by (metis assms antisym_conv2 card_length card_mono distinct_card distinct_conv_nth le_less_trans)
text‹
A list of items from a finite set which is longer that the cardinal of the set has an element that appears again later in the list.
› corollary biglist_from_set_repeat_later:
assumes ‹finite s› and ‹set l ⊆ s› and ‹length l > card s› shows ‹∃i j. i < length l ∧ j < length l ∧ i < j ∧ l!i = l!j› by (metis assms biglist_from_set_repeat not_less_iff_gr_or_eq)
subsection‹Sublists and their properties› text‹
The sublist of l composed of item i through j included.
› definition ‹sublist l i j ≡ drop i (take (Suc j) l)›
text‹Examples›
value ‹sublist [0::nat,1,2,3,4,5] 0 2› value ‹sublist [0::nat,1,2,3,4,5] 3 5›
text‹The length of a sublist:› lemma sublist_length:
assumes ‹i < j› and ‹j < length l› shows ‹length (sublist l i j) = (Suc j) - i› unfolding sublist_def by (simp add: Suc_leI assms(2) min.absorb2)
text‹Position of the items of a sublist in the original list:› lemma sublist_idx:
assumes ‹i < j› and ‹j < length l› shows ‹k < (Suc j) - i ⟹ (sublist l i j)!k = l!(k+i)› unfolding sublist_def by (metis (no_types, hide_lams) add.commute assms length_take lessI less_diff_conv less_le min.absorb2 min_less_iff_conj nth_drop nth_take)
text‹A sublist does not contain items that are not in the original list:› lemma sublist_subset:
‹set (sublist l i j) ⊆ set l› unfolding sublist_def by (metis dual_order.trans set_drop_subset set_take_subset)
subsection‹The theorem› text‹
In a non-empty directed acyclic graph, there is at least one vertex without incoming edge.
› lemma dag_root_vertex:
assumes ‹isDAG g› and ‹vertices g ≠ {}› and ‹finite (vertices g)› shows ‹∃v ∈ vertices g. ∀e ∈ edges g. v ≠ (snd e)›
proof -
text‹Assume all vertices have at least an incoming edge.› { assume contr:‹∀v ∈ vertices g. ∃e ∈ edges g. v = snd e› text‹Then, build a list of vertices longer that the number of vertices in the graph.› define n where ‹n = Suc (card (vertices g))› hence ‹n > 1› by (simp add: assms(2,3) card_gt_0_iff) from arbitrary_length_chain[OF contr assms(2) this] obtain l where lp:‹length l = n ∧ isDirectedPath l g› by blast text‹This list necessarily contains the same vertex twice.› hence ‹∃i j. i < length l ∧ j < length l ∧ i < j ∧ l!i = l!j› using biglist_from_set_repeat_later[OF assms(3)] n_def by (metis dpath_in_vertices lessI lp) from this obtain i and j where ij:‹i < length l ∧ j < length l ∧ i < j ∧ l!i = l!j› by blast hence iltj:‹i < j› and jltlen:‹j < length l› and ijsame:‹l!i = l!j› by simp+ text‹The sublist starting and ending at this repeated vertex is a cycle.› define cy where cyp:‹cy = sublist l i j› from cyp iltj have lcy:‹length cy - 1 + i = j› using sublist_length[OF iltj jltlen] by auto from cyp sublist_idx[OF iltj jltlen] have cy_offet:‹∀k < (Suc j) - i. cy!k = l!(k+i)› by blast from sublist_length[OF iltj jltlen] iltj cyp have ‹length cy > 1› by simp moreover from cyp ijsame sublist_idx[OF iltj jltlen] sublist_length[OF iltj jltlen] iltj have ‹cy!0 = cy!(length cy -1)› by auto moreover from lp cyp have ‹set cy ⊆ vertices g› using sublist_subset dpath_in_vertices by fastforce moreover from lp have ‹∀i. Suc i < length l ⟶ (l ! i, l ! Suc i) ∈ edges g› unfolding isDirectedPath_def by blast with cyp sublist_idx[OF iltj jltlen] have ‹∀k. Suc k < length cy ⟶ (cy ! k, cy ! Suc k) ∈ edges g› by (simp add: add.commute sublist_def) ultimately have ‹isDirectedCycle cy g› using ij lp unfolding isDirectedCycle_def isDirectedPath_def by simp text‹But DAGs have by definition no cycle.› with assms(1) have False unfolding isDAG_def by simp text‹So the initial assumption is false, and the theorem is proved.› } thus ?thesis by blast
qed
section‹Topoligical orders and DAGs› text‹DAGs are exactly graphs that have a topological order›
subsection‹Some lemmas about minimal elements›
text‹A non empty set of natural numbers has a minimal element.› lemma not_empty_set_min:
assumes ‹(S::(nat set)) ≠ {}› shows ‹∃m::nat ∈ S. ∀x ∈ S. m ≤ x›
by (metis (full_types) Collect_empty_eq Collect_mem_eq assms exists_least_iff le_less_linear)
text‹A non empty list of natural numbers has a minimal element.› lemma not_empty_list_min:
assumes ‹l ≠ []› shows ‹∃i < length (l::'a list). ∀j < length l. (f::('a⇒nat)) (l!i) ≤ f (l!j)›
proof -
have ‹∃x ∈ f ` (set l). ∀y ∈ f ` (set l). x ≤ y› by (metis assms not_empty_set_min empty_is_image set_empty) thus ?thesis by (metis (full_types) image_iff in_set_conv_nth)
qed
subsection‹Topological orders› text‹
A topological order is compatible with the directed edges of a graph.
› definition isTopologicalOrder :: ‹(vertex ⇒ nat) ⇒ graph ⇒ bool› where
‹isTopologicalOrder f g ≡ inj f ∧ (∀e ∈ edges g. f (fst e) < f (snd e))›
definition hasTopoOrder where
‹hasTopoOrder g ≡ (∃f. isTopologicalOrder f g)›
subsection‹A DAG has a topological order›
text‹
The proof is by induction on the number of vertices in the graph. Since the cardinal of an infinite set in Isabelle/HOL is 0, we have to add the assumption that our graphs have a finite number of vertices in order to handle the base case.
› lemma DAG_n_thus_topoOrder:
‹⟦finite (vertices g); isDAG g; card (vertices g) = n⟧ ⟹ hasTopoOrder g›
proof (induction n arbitrary: g)
case 0 text‹An empty graph has no vertex, so any injective function is a topological order.› thus ?case unfolding hasTopoOrder_def isTopologicalOrder_def by (metis card_0_eq edges_link_vertices(1) ex_in_conv inj_of_nat)
next
case (Suc n) thus ?case proof (cases ‹n = 0›) case True text‹Induction step for a graph with one vertex.› with Suc have card_1:‹card (vertices g) = 1› by linarith text‹The only possible edge is a loop on the unique vertex.› hence edge_loop:‹∀ e ∈ edges g. fst e = snd e› by (metis card_1_singletonE edges_link_vertices singletonD) text‹Which is not possible in a DAG.› have ‹edges g = {}› proof - { assume ‹∃e. e ∈ edges g› from this obtain e where e_edge:‹e ∈ edges g› by blast with edge_loop have loop_e:‹fst e = snd e› by simp define ll where ‹ll = [fst e, snd e]› hence ‹length ll > 1› by simp moreover from ll_def have ‹ll!0 = ll!(length ll - 1)› using loop_e by simp moreover have ‹set ll ⊆ vertices g› using ll_def e_edge edges_link_vertices by simp moreover have ‹(∀i. Suc i < length ll ⟶ (ll ! i, ll ! Suc i) ∈ edges g)› by (simp add: e_edge ll_def) ultimately have ‹∃l. isDirectedCycle l g› unfolding isDirectedCycle_def isDirectedPath_def by blast hence False using Suc.prems(2) unfolding isDAG_def by simp } thus ?thesis by blast qed thus ?thesis unfolding hasTopoOrder_def isTopologicalOrder_def using inj_of_nat by blast next case False text‹Induction step for a graph with more than one vertex.› text‹Assume we have a DAG with \<^term>‹Suc n› vertices.› { fix gg assume gg_dag:‹isDAG gg› and gg_card:‹card (vertices gg) = Suc n› from gg_card ‹n ≠ 0› have gg_not_empty:‹vertices gg ≠ {}› by auto from gg_card have gg_finite:‹finite (vertices gg)› using ‹n ≠ 0› card_infinite by force text‹From a previous theorem, we have a vertex without incoming edge.› from dag_root_vertex[OF gg_dag gg_not_empty gg_finite] obtain root where root_def:‹root ∈ vertices gg ∧ (∀e ∈ edges gg. root ≠ snd e)› by blast text‹We now define a subgraph by removing this root vertex› define sv::‹vertex set› where ‹sv = vertices gg - {root}› define se::‹edge set› where ‹se = {e. e ∈ edges gg ∧ (fst e) ≠ root}› hence subgraph:‹se ⊆ edges gg› by blast have ‹se ⊆ sv × sv› using root_def sv_def se_def using edges_link_vertices by fastforce hence sg_rep:‹(sv, se) ∈ {(V, E). E ⊆ V × V}› by simp define sg::‹graph› where ‹sg = Abs_graph (sv, se)› have sg_vert:‹vertices sg = sv› using sg_def Abs_graph_inverse[OF sg_rep] by simp have sg_edge:‹edges sg = se› using sg_def Abs_graph_inverse[OF sg_rep] by simp text‹This subgraph is also a DAG.› have sg_dag:‹isDAG sg› using dag_subgraph[OF gg_dag] subgraph sg_edge by simp have sg_card:‹card (vertices sg) = n› using gg_card sg_vert sv_def root_def by (simp add: gg_finite) with ‹n ≠ 0› have ‹finite (vertices sg)› using card_infinite by fastforce text‹With the induction hypothesis, we have a topological order on this subgraph.› from Suc.IH[OF this sg_dag sg_card] obtain f where f_def:‹isTopologicalOrder f sg› unfolding hasTopoOrder_def by blast text‹ We use this order to build an order on the original graph by shifting the rank of all vertices of the subgraph by one, and by setting the root as the minimal element. › define f' where ‹f' = (Suc ∘ f)(root:=0)› have ‹inj f› using f_def isTopologicalOrder_def by simp hence ‹inj f'› using f'_def by (metis (no_types, lifting) comp_apply fun_upd_apply injD injI inj_Suc nat.distinct(1)) moreover have ‹(∀e ∈ edges gg. f' (fst e) < f' (snd e))› using isTopologicalOrder_def f'_def f_def root_def se_def sg_edge by auto ultimately have ‹isTopologicalOrder f' gg› unfolding isTopologicalOrder_def by simp hence ‹hasTopoOrder gg› using hasTopoOrder_def by blast } thus ?thesis using Suc.prems(2,3) by blast qed
qed
text‹
This corollary removes the assumption on the size of the graph, which was used only for the induction.
› corollary DAG_thus_topoOrder:
‹⟦finite (vertices g); isDAG g⟧ ⟹ hasTopoOrder g› using DAG_n_thus_topoOrder by blast
text‹
We can now show that (finite) graphs with a topological order are exactly (finite) DAGs.
› lemma topo_order_dag:
assumes ‹finite (vertices g)› shows ‹hasTopoOrder g = isDAG g›
proof
text‹First, show that if a graph admits a topological order, it is a DAG.› { assume ‹hasTopoOrder g› from this obtain f::‹vertex⇒nat› where topo:‹isTopologicalOrder f g› unfolding hasTopoOrder_def by blast have ‹isDAG g› proof - text‹The proof is by contradiction: we assume it is not a DAG and derive False.› { assume contr:‹¬isDAG g› text‹If the graph is not a DAG, it has a directed cycle.› hence ‹∃l. isDirectedCycle l g› unfolding isDAG_def by simp from this obtain l where cycle:‹isDirectedCycle l g› by blast text‹This cycle has a minimal element according to the topological order› with not_empty_list_min have ‹∃i < length l. ∀j < length l. f (l!i) ≤ f (l!j)› by (metis cycle isDirectedCycle_def isDirectedPath_def less_numeral_extra(2) list.size(3)) from this obtain i where i_def:‹i < length l ∧ (∀j < length l. f (l!i) ≤ f (l!j))› by blast have False proof (cases ‹i = 0›) case True text‹If the minimal element is the first one in the cycle, it is also the last one› define i' where ‹i' = (length l -1)› with cycle have cycle_loop:‹l!i' = l!i› unfolding isDirectedCycle_def by (simp add:‹i= 0›) from i'_def cycle have ‹i' > 0› unfolding isDirectedCycle_def isDirectedPath_def by simp text‹So the two last vertices in the cycle form an edge› from this obtain k where k_def:‹i' = Suc k› using old.nat.exhaust by auto with cycle have ‹(l!k, l!i') ∈ edges g› unfolding isDirectedCycle_def isDirectedPath_def by (simp add: i'_def) text‹According to the topological order, the last element is larger that the previous one› hence fk_less:‹f (l!k) < f (l!i')› using topo unfolding isTopologicalOrder_def by auto text‹Which contradicts the fact that it is the minimal element in the cycle.› moreover from cycle_loop i_def have ‹∀j < length l. f (l!i') ≤ f (l!j)› by simp moreover have ‹k < length l› using i'_def k_def by linarith ultimately have False using leD by blast thus ?thesis . next case False text‹If the minimal element is not the first one in the cycle, we consider the previous one› from this obtain k where k_def:‹i = Suc k› using old.nat.exhaust by auto with cycle have ‹(l!k, l!i) ∈ edges g› using i_def unfolding isDirectedCycle_def isDirectedPath_def by blast text‹Which is therefore smaller than the minimal element, hence the contradiction.› hence ‹f (l!k) < f (l!i)› using topo unfolding isTopologicalOrder_def by auto with i_def k_def have False using Suc_lessD leD by blast thus ?thesis . qed } thus ?thesis by blast qed } thus ‹hasTopoOrder g ⟹ isDAG g› . text‹For the other implication, we use the lemma proved by induction.› { assume ‹isDAG g› from DAG_thus_topoOrder[OF assms(1) this] have ‹hasTopoOrder g› . } thus ‹isDAG g ⟹ hasTopoOrder g› .
qed
section ‹k-stable and k-vertex cover›
definition is_k_stable
where ‹is_k_stable g s k ≡ card s ≥ k ∧ s ⊆ vertices g ∧ (∀ e ∈ edges g. ¬((fst e) ∈ s ∧ (snd e) ∈ s))›
definition is_k_vertexcover where ‹is_k_vertexcover g c k ≡
card c ≤ k ∧ c ⊆ vertices g ∧ (∀ e ∈ edges g. ((fst e) ∈ c ∨ (snd e) ∈ c))›
lemma stable_vcover_duality:
assumes ‹finite (vertices g)› and ‹s ⊆ vertices g› and ‹k ≤ card (vertices g)› shows ‹is_k_stable g s k = is_k_vertexcover g (vertices g - s) (card (vertices g) - k)›
proof
{ assume h:‹is_k_stable g s k› let ?c = ‹(vertices g) - s› from h have ‹card s ≥ k› using is_k_stable_def by simp hence ‹card ?c ≤ card (vertices g) - k› using assms h is_k_stable_def by (metis card_Diff_subset diff_le_mono2 rev_finite_subset) moreover from h have ‹s ⊆ vertices g› using is_k_stable_def by simp hence ‹?c ⊆ vertices g› by simp moreover from h have ‹∀ e ∈ edges g. ¬((fst e) ∈ s ∧ (snd e) ∈ s)› using is_k_stable_def by simp hence ‹∀ e ∈ edges g. ((fst e) ∈ ?c ∨ (snd e) ∈ ?c)› using edges_link_vertices by auto ultimately have ‹is_k_vertexcover g ?c (card (vertices g) - k)› using is_k_vertexcover_def by simp } thus ‹is_k_stable g s k ⟹ is_k_vertexcover g (vertices g - s) (card (vertices g) - k)› . { assume h:‹is_k_vertexcover g (vertices g - s) (card (vertices g) - k)› from h have ‹card (vertices g - s) ≤ card (vertices g) - k› using is_k_vertexcover_def by simp hence ‹card (vertices g) - card s ≤ card (vertices g) - k› using assms by (simp add: card_Diff_subset finite_subset) hence ‹card s ≥ k› using assms by simp moreover from h have ‹s ⊆ vertices g› using is_k_vertexcover_def using assms(2) by blast moreover from h have ‹∀ e ∈ edges g. (fst e) ∈ ((vertices g) - s) ∨ (snd e) ∈ ((vertices g) - s)› using is_k_vertexcover_def by simp hence ‹∀ e ∈ edges g. ((fst e) ∉ s ∨ (snd e) ∉ s)› by blast ultimately have ‹is_k_stable g s k› using is_k_stable_def by simp } thus ‹is_k_vertexcover g (vertices g - s) (card (vertices g) - k) ⟹ is_k_stable g s k› .
qed
(*<*) end (*>*) (:endbrush:)
Réduction du problème SubsetSum au Knapsack Réduction SubsetSum
(:brush=isabelle:) theory knapsack imports Main
begin text ‹
Reducing the subset sum problem to the knapsack problem.
›
text ‹
The subset sum problem: find a subset of [1..n] of sum t
› definition isSubsetSum where
‹isSubsetSum n (a::nat⇒int) s t ≡ s ⊆ {i. 1 ≤ i ∧ i ≤ n} ∧ (∑i∈s. a i) = t›
text ‹
The knapsack problem: find k items among n with total weight ≤ B and value at least V
› definition isKnapsack where ‹isKnapsack (n::nat) (v::nat⇒int) (w::nat⇒int) (B::int) (V::int) (k::nat set) ≡
(k ⊆ {i. 1 ≤ i ∧ i ≤ n}) ∧ (∑i∈k. w i) ≤ B ∧ (∑i∈k. v i) ≥ V›
text ‹
Solving a particular form of the knapsack problem solves the subset sum problem.
› lemma ‹isSubsetSum n a s t = isKnapsack n a a t t s› proof
{ assume h:‹isSubsetSum n a s t› hence ‹(∑i∈s. a i) = t› using isSubsetSum_def by simp hence ‹(∑i∈s. a i) ≤ t› and ‹(∑i∈s. a i) ≥ t› by simp+ moreover from h have ‹s ⊆ {i. 1 ≤ i ∧ i ≤ n}› using isSubsetSum_def by simp ultimately have ‹isKnapsack n a a t t s› using isKnapsack_def by simp } thus ‹isSubsetSum n a s t ⟹ isKnapsack n a a t t s› . { assume h:‹isKnapsack n a a t t s› hence ‹(∑i∈s. a i) ≤ t› and ‹(∑i∈s. a i) ≥ t› using isKnapsack_def by simp+ moreover from h have ‹s ⊆ {i. 1 ≤ i ∧ i ≤ n}› using isKnapsack_def by simp ultimately have ‹isSubsetSum n a s t› using isSubsetSum_def by simp } thus ‹isKnapsack n a a t t s ⟹ isSubsetSum n a s t› .
qed
end (:endbrush:)