100/konigsberg.ml

   1 (* ========================================================================= *)
   2 (* Impossibility of Eulerian path for bridges of Koenigsberg.                *)
   3 (* ========================================================================= *)
   4
   5 let edges = new_definition
   6   `edges(E:E->bool,V:V->bool,Ter:E->V->bool) = E`;;
   7
   8 let vertices = new_definition
   9   `vertices(E:E->bool,V:V->bool,Ter:E->V->bool) = V`;;
  10
  11 let termini = new_definition
  12   `termini(E:E->bool,V:V->bool,Ter:E->V->bool) = Ter`;;
  13
  14 (* ------------------------------------------------------------------------- *)
  15 (* Definition of an undirected graph.                                        *)
  16 (* ------------------------------------------------------------------------- *)
  17
  18 let graph = new_definition
  19  `graph G <=>
  20         !e. e IN edges(G)
  21             ==> ?a b. a IN vertices(G) /\ b IN vertices(G) /\
  22                       termini G e = {a,b}`;;
  23
  24 let TERMINI_IN_VERTICES = prove
  25  (`!G e v. graph G /\ e IN edges(G) /\ v IN termini G e ==> v IN vertices G`,
  26   REWRITE_TAC[graph; EXTENSION; IN_INSERT; NOT_IN_EMPTY] THEN
  27   MESON_TAC[]);;
  28
  29 (* ------------------------------------------------------------------------- *)
  30 (* Connection in a graph.                                                    *)
  31 (* ------------------------------------------------------------------------- *)
  32
  33 let connects = new_definition
  34  `connects G e (a,b) <=> termini G e = {a,b}`;;
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* Delete an edge in a graph.                                                *)
  38 (* ------------------------------------------------------------------------- *)
  39
  40 let delete_edge = new_definition
  41  `delete_edge e (E,V,Ter) = (E DELETE e,V,Ter)`;;
  42
  43 let DELETE_EDGE_CLAUSES = prove
  44  (`(!G. edges(delete_edge e G) = (edges G) DELETE e) /\
  45    (!G. vertices(delete_edge e G) = vertices G) /\
  46    (!G. termini(delete_edge e G) = termini G)`,
  47   REWRITE_TAC[FORALL_PAIR_THM; delete_edge; edges; vertices; termini]);;
  48
  49 let GRAPH_DELETE_EDGE = prove
  50  (`!G e. graph G ==> graph(delete_edge e G)`,
  51   REWRITE_TAC[graph; DELETE_EDGE_CLAUSES; IN_DELETE] THEN MESON_TAC[]);;
  52
  53 (* ------------------------------------------------------------------------- *)
  54 (* Local finiteness: set of edges with given endpoint is finite.             *)
  55 (* ------------------------------------------------------------------------- *)
  56
  57 let locally_finite = new_definition
  58  `locally_finite G <=>
  59      !v. v IN vertices(G) ==> FINITE {e | e IN edges G /\ v IN termini G e}`;;
  60
  61 (* ------------------------------------------------------------------------- *)
  62 (* Degree of a vertex.                                                       *)
  63 (* ------------------------------------------------------------------------- *)
  64
  65 let localdegree = new_definition
  66  `localdegree G v e =
  67         if termini G e = {v} then 2
  68         else if v IN termini G e then 1
  69         else 0`;;
  70
  71 let degree = new_definition
  72  `degree G v = nsum {e | e IN edges G /\ v IN termini G e} (localdegree G v)`;;
  73
  74 let DEGREE_DELETE_EDGE = prove
  75  (`!G e:E v:V.
  76         graph G /\ locally_finite G /\ e IN edges(G)
  77         ==> degree G v =
  78                 if termini G e = {v} then degree (delete_edge e G) v + 2
  79                 else if v IN termini G e then degree (delete_edge e G) v + 1
  80                 else degree (delete_edge e G) v`,
  81   REPEAT STRIP_TAC THEN
  82   REWRITE_TAC[degree; DELETE_EDGE_CLAUSES; IN_DELETE] THEN
  83   SUBGOAL_THEN
  84    `{e:E | e IN edges G /\ (v:V) IN termini G e} =
  85         if v IN termini G e
  86         then e INSERT {e' | (e' IN edges G /\ ~(e' = e)) /\ v IN termini G e'}
  87         else {e' | (e' IN edges G /\ ~(e' = e)) /\ v IN termini G e'}`
  88   SUBST1_TAC THENL
  89    [REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN COND_CASES_TAC THEN
  90     ASM_REWRITE_TAC[IN_ELIM_THM; IN_INSERT] THEN
  91     ASM_MESON_TAC[];
  92     ALL_TAC] THEN
  93   ASM_CASES_TAC `(v:V) IN termini G (e:E)` THEN ASM_REWRITE_TAC[] THENL
  94    [ALL_TAC;
  95     COND_CASES_TAC THENL [ASM_MESON_TAC[IN_SING; EXTENSION]; ALL_TAC] THEN
  96     MATCH_MP_TAC NSUM_EQ THEN REWRITE_TAC[IN_ELIM_THM; localdegree] THEN
  97     REWRITE_TAC[DELETE_EDGE_CLAUSES]] THEN
  98   SUBGOAL_THEN
  99    `FINITE {e':E | (e' IN edges G /\ ~(e' = e)) /\ (v:V) IN termini G e'}`
 100    (fun th -> SIMP_TAC[NSUM_CLAUSES; th])
 101   THENL
 102    [MATCH_MP_TAC FINITE_SUBSET THEN
 103     EXISTS_TAC `{e:E | e IN edges G /\ (v:V) IN termini G e}` THEN
 104     SIMP_TAC[IN_ELIM_THM; SUBSET] THEN
 105     ASM_MESON_TAC[locally_finite; TERMINI_IN_VERTICES];
 106     ALL_TAC] THEN
 107   REWRITE_TAC[IN_ELIM_THM] THEN ASM_REWRITE_TAC[localdegree] THEN
 108   SUBGOAL_THEN
 109    `nsum {e':E | (e' IN edges G /\ ~(e' = e)) /\ (v:V) IN termini G e'}
 110          (localdegree (delete_edge e G) v) =
 111     nsum {e' | (e' IN edges G /\ ~(e' = e)) /\ v IN termini G e'}
 112          (localdegree G v)`
 113   SUBST1_TAC THENL
 114    [ALL_TAC; COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ARITH_TAC] THEN
 115   MATCH_MP_TAC NSUM_EQ THEN SIMP_TAC[localdegree; DELETE_EDGE_CLAUSES]);;
 116
 117 (* ------------------------------------------------------------------------- *)
 118 (* Definition of Eulerian path.                                              *)
 119 (* ------------------------------------------------------------------------- *)
 120
 121 let eulerian_RULES,eulerian_INDUCT,eulerian_CASES = new_inductive_definition
 122  `(!G a. a IN vertices G /\ edges G = {} ==> eulerian G [] (a,a)) /\
 123   (!G a b c e es. e IN edges(G) /\ connects G e (a,b) /\
 124                   eulerian (delete_edge e G) es (b,c)
 125                   ==> eulerian G (CONS e es) (a,c))`;;
 126
 127 let EULERIAN_FINITE = prove
 128  (`!G es ab. eulerian G es ab ==> FINITE (edges G)`,
 129   MATCH_MP_TAC eulerian_INDUCT THEN
 130   SIMP_TAC[DELETE_EDGE_CLAUSES; FINITE_DELETE; FINITE_RULES]);;
 131
 132 (* ------------------------------------------------------------------------- *)
 133 (* The main result.                                                          *)
 134 (* ------------------------------------------------------------------------- *)
 135
 136 let EULERIAN_ODD_LEMMA = prove
 137  (`!G:(E->bool)#(V->bool)#(E->V->bool) es ab.
 138         eulerian G es ab
 139         ==> graph G
 140             ==> FINITE(edges G) /\
 141                 !v. v IN vertices G
 142                     ==> (ODD(degree G v) <=>
 143                          ~(FST ab = SND ab) /\ (v = FST ab \/ v = SND ab))`,
 144   MATCH_MP_TAC eulerian_INDUCT THEN CONJ_TAC THENL
 145    [SIMP_TAC[degree; NOT_IN_EMPTY; SET_RULE `{x | F} = {}`] THEN
 146     SIMP_TAC[NSUM_CLAUSES; FINITE_RULES; ARITH];
 147     ALL_TAC] THEN
 148   SIMP_TAC[GRAPH_DELETE_EDGE; FINITE_DELETE; DELETE_EDGE_CLAUSES] THEN
 149   REPEAT GEN_TAC THEN
 150   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
 151   ASM_SIMP_TAC[GRAPH_DELETE_EDGE] THEN STRIP_TAC THEN
 152   X_GEN_TAC `v:V` THEN DISCH_TAC THEN
 153   MP_TAC(ISPECL [`G:(E->bool)#(V->bool)#(E->V->bool)`; `e:E`; `v:V`]
 154                 DEGREE_DELETE_EDGE) THEN
 155   ANTS_TAC THENL
 156    [ASM_REWRITE_TAC[locally_finite] THEN GEN_TAC THEN DISCH_TAC THEN
 157     MATCH_MP_TAC FINITE_SUBSET THEN
 158     EXISTS_TAC `edges(G:(E->bool)#(V->bool)#(E->V->bool))` THEN
 159     ASM_SIMP_TAC[SUBSET; IN_ELIM_THM];
 160     ALL_TAC] THEN
 161   DISCH_THEN SUBST1_TAC THEN
 162   MP_TAC(ISPECL [`G:(E->bool)#(V->bool)#(E->V->bool)`; `e:E`]
 163          TERMINI_IN_VERTICES) THEN
 164   ASM_REWRITE_TAC[] THEN
 165   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [connects]) THEN
 166   DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
 167   ASM_CASES_TAC `b:V = a` THEN ASM_REWRITE_TAC[] THENL
 168    [REWRITE_TAC[SET_RULE `{a,a} = {v} <=> v = a`] THEN
 169     COND_CASES_TAC THEN ASM_SIMP_TAC[ODD_ADD; ARITH];
 170     ALL_TAC] THEN
 171   ASM_REWRITE_TAC[SET_RULE `{a,b} = {v} <=> a = b /\ a = v`] THEN
 172   COND_CASES_TAC THEN ASM_SIMP_TAC[ODD_ADD; ARITH] THEN ASM_MESON_TAC[]);;
 173
 174 let EULERIAN_ODD = prove
 175  (`!G es a b.
 176         graph G /\ eulerian G es (a,b)
 177         ==> !v. v IN vertices G
 178                 ==> (ODD(degree G v) <=> ~(a = b) /\ (v = a \/ v = b))`,
 179   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 180   DISCH_THEN(MP_TAC o MATCH_MP EULERIAN_ODD_LEMMA) THEN
 181   ASM_SIMP_TAC[FST; SND]);;
 182
 183 (* ------------------------------------------------------------------------- *)
 184 (* Now the actual Koenigsberg configuration.                                 *)
 185 (* ------------------------------------------------------------------------- *)
 186
 187 let KOENIGSBERG = prove
 188  (`!G. vertices(G) = {0,1,2,3} /\
 189        edges(G) = {10,20,30,40,50,60,70} /\
 190        termini G (10) = {0,1} /\
 191        termini G (20) = {0,2} /\
 192        termini G (30) = {0,3} /\
 193        termini G (40) = {1,2} /\
 194        termini G (50) = {1,2} /\
 195        termini G (60) = {2,3} /\
 196        termini G (70) = {2,3}
 197        ==> ~(?es a b. eulerian G es (a,b))`,
 198   GEN_TAC THEN STRIP_TAC THEN
 199   MP_TAC(ISPEC `G:(num->bool)#(num->bool)#(num->num->bool)` EULERIAN_ODD) THEN
 200   REWRITE_TAC[NOT_EXISTS_THM] THEN
 201   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 202   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN ANTS_TAC THENL
 203    [ASM_REWRITE_TAC[graph] THEN GEN_TAC THEN
 204     REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN STRIP_TAC THEN
 205     ASM_REWRITE_TAC[SET_RULE
 206      `{a,b} = {x,y} <=> a = x /\ b = y \/ a = y /\ b = x`] THEN
 207     MESON_TAC[];
 208     ALL_TAC] THEN
 209   ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
 210   SIMP_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 211   ASM_REWRITE_TAC[degree; edges] THEN
 212   SIMP_TAC[TAUT `a IN s /\ k IN t <=> ~(a IN s ==> ~(k IN t))`] THEN
 213   ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
 214   SIMP_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
 215   ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH] THEN
 216   REWRITE_TAC[DE_MORGAN_THM] THEN
 217   REWRITE_TAC[SET_RULE `{x | x = a \/ P(x)} = a INSERT {x | P(x)}`] THEN
 218   REWRITE_TAC[SET_RULE `{x | x = a} = {a}`] THEN
 219   SIMP_TAC[NSUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
 220   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH] THEN
 221   ASM_REWRITE_TAC[localdegree; IN_INSERT; NOT_IN_EMPTY; ARITH] THEN
 222   REWRITE_TAC[SET_RULE `{a,b} = {x} <=> x = a /\ a = b`] THEN
 223   DISCH_THEN(fun th ->
 224    MP_TAC(SPEC `0` th) THEN MP_TAC(SPEC `1` th) THEN
 225    MP_TAC(SPEC `2` th) THEN MP_TAC(SPEC `3` th)) THEN
 226   REWRITE_TAC[ARITH] THEN ARITH_TAC);;
 227
 228 (******
 229
 230 Maybe for completeness I should show the contrary: existence of Eulerian
 231 circuit/walk if we do have the right properties, assuming the graph is
 232 connected; cf:
 233
 234 http://math.arizona.edu/~lagatta/class/fa05/m105/graphtheorynotes.pdf
 235
 236  *****)