Create a gist now

Instantly share code, notes, and snippets.

Embed
What would you like to do?
start on a proof of the polyhedron formula
(* Isar Proofs (eventually) for three theorems from http://www.cs.ru.nl/~freek/100/
#13 Polyhedron Formula (F + V - E = 2)
#50 The Number of Platonic Solids
#92 Pick's theorem
*)
theory Poly100
imports Main "HOL.Binomial" "HOL-Analysis.Polytope"
begin
(* ------------------------------------------------------------------------ *)
sectionVocabulary (Syntax helpers)
(* ------------------------------------------------------------------------ *)
definition d_faces ("(_ d'_faces _)" [85,85] 80) where
"n d_faces p = {f. f face_of p ∧ aff_dim f = n}"
definition d_face_count ("(_ d'_face'_count _)" [85,85] 80) where
"n d_face_count p = card(n d_faces p)"
definition verts where "verts p = 0 d_faces p"
definition edges where "edges p = 1 d_faces p"
definition surfs where "surfs p = 2 d_faces p"
definition facets where "facets p = (aff_dim p -1) d_faces p"
(* ------------------------------------------------------------------------ *)
sectionSimplex Theory.
(* ------------------------------------------------------------------------ *)
lemma facet_of_simplex_simplex:
assumes "n simplex S" "F facet_of S" "n≥0"
shows "(n-1) simplex F"
― ‹Polytope.thy defines @{thm simplex_insert_dimplus1} which demonstrates that you can
add an affine-independent point to a simplex and create a higher-dimensional simplex
(e.g: adding a point off the plane to a triangle yields a tetrahedron.) This lemma
lets us work in the opposite direction, to show each n-dimensional simplex is
composed of (n-1) simplices.
proof -
― ‹‹C1is the set of affine-independent vertices required by @{const simplex}.
obtain C1 where C: "finite C1" "¬(affine_dependent C1)" "int(card C1) = n+1"
and S: "S = convex hull C1" using assms unfolding Polytope.simplex by force
― ‹Isolate the vertex fromC1that isn't in F, and call the remaining setC.
then obtain A where "A∈C1" and "A∉F"
by (metis affine_dependent_def affine_hull_convex_hull assms(2)
facet_of_convex_hull_affine_independent_alt hull_inc)
then obtain C where "C = C1 - {A}" by simp
― ‹Finally, show thatFandCtogether meet the definition of an (n-1) simplex.
show ?thesis unfolding Polytope.simplex
proof (intro exI conjI)
― ‹The first couple statements show that the remaining vertices ofC
are the extreme points of ann-1dimensional simplex. These all follow
trivially from the idea that we're just removing one vertex from a set that
already had the required properties.
show "finite C" by (simp add: C(1)C = C1 - {A})
show "¬ affine_dependent C" by (simp add: C(2)C = C1 - {A}affine_independent_Diff)
show "int (card C) = (n-1) + 1"
using CAC1› ‹C = C1 - {A}affine_independent_card_dim_diffs by fastforce
show "F = convex hull C"
― ‹This is the tricky one. Intuitively, it's obvious that once we removed vertex A,
there's one facet left, and it's the simplex defined by the remaining vertices.
It's not obvious (to me, anyway) exactly how to derive this fact from the definitions.
Thankfully, as long as we point her in the right direction, Isabelle is happy to work
through the details of proofs that would normally be left as an exercise for the reader.
proof
― ‹Briefly, afacet_ofand aconvex hullare both sets, so to prove equality, we just
show that each is a subset of the other. Sledgehammer found a proof for the first
statement in a matter of seconds.
show "F ⊆ convex hull C"
by (metis C(2) Diff_subset SAC1› ‹AF› ‹C = C1 - {A}assms(2)
facet_of_convex_hull_affine_independent hull_inc hull_mono insert_Diff subset_insert)
next
― ‹The opposite direction was harder to prove. My plan had been to convince Isabelle
that since C is the minimal set of affine-independent vertices, then removing any one
would dropaff_dim Cby 1. But we already knowFconvex hull C, and (although we
haven't proven it here),aff_dim C = aff_dim F. So if there were any pointpCpF,
we would also haveaff_dim C < aff_dim F, and hence a contradiction. The facts
referenced by these sledgehammer-generated proofs suggest it found a way to derive
a similar idea, but directly, without resorting to proof by contradicition.
have"C ⊆ F"
by (metis C(2) SAC1› ‹AF› ‹C = C1 - {A}assms(2)
facet_of_convex_hull_affine_independent hull_inc insertE insert_Diff subsetI)
thus "convex hull C ⊆ F"
by (metis C(2) S assms(2) convex_convex_hull facet_of_convex_hull_affine_independent hull_minimal)
qed
qed
qed
textThe proof above was a lot of work. I wanted to generalize it to arbitrary faces, which
made me realize that the setCin the definition of @{thm simplex} corresponds to
the union of all vertex faces. (A vertex in polytope-land is a set containing one point,
but simplices are defined in terms of the points themselves). So I found it helpful
to create a definition that mirrors the definition of @{thm simplex}, but lets me
assign a name to set of these points themselves. Since @{thm simplex} refers to this
set asC, I decided it probably stood forcorners, and so...
definition corners_of ("_ corners'_of _" [80, 80] 85) where
"C corners_of S ≡ finite C ∧ (¬affine_dependent C) ∧
(int(card C) = aff_dim S + 1) ∧
(S=convex hull C)"
definition corners where
"corners S = (THE C. C corners_of S)" if "n simplex S"
context
fixes n :: int
and S :: "'a::euclidean_space set"
assumes nS: "n simplex S" and "n≥-1"
begin
lemma corners_exist:
shows "∃C. C corners_of S"
unfolding corners_of_def
using Polytope.simplex aff_dim_simplex nS by blast
lemma corners_equiv:
assumes "C0 corners_of S" and "C1 corners_of S"
shows "C0 = C1"
unfolding simplex_def corners_of_def
by (metis assms corners_of_def extreme_point_of_convex_hull_affine_independent subsetI subset_antisym)
lemma corners_unique:
shows "∃!C. C corners_of S"
using nS corners_exist corners_equiv by blast
lemma corners_are_corners_of:
"(C = corners S) ≡ C corners_of S"
by (smt nS corners_def corners_unique theI')
textOnce we have a name for these points, metis is able able to untangle th
different terminologies used in the definition of polytopes, faces, and
simplices, and show what we really wanted to say with much less manual work:
lemma face_of_simplex_simplex:
assumes F: "F face_of S" and k: "aff_dim F = k"
shows "k simplex F"
proof -
from nS obtain SC where SC: "SC corners_of S" using corners_of_def simplex_def
by (metis (no_types, hide_lams) aff_dim_affine_independent
aff_dim_convex_hull aff_independent_finite)
with F obtain FC where FC: "FC corners_of F"
by (metis (no_types, hide_lams) aff_dim_affine_independent
aff_dim_convex_hull aff_independent_finite
affine_independent_subset corners_of_def
face_of_convex_hull_affine_independent)
thus "k simplex F" by (metis FC corners_of_def k simplex_def)
qed
subsectionCount of faces
textWe will show thatk d_face_count S = (n+1) choose (k+1)for alln simplex S,
as there are (n+1) corners, and each k-dimensional face encloses (k+1) of them.
subsubsection "correspondence between faces and sets of corners"
lemma sub_corners_simplex_face:
― ‹Any subset of the corners of a simplex is sufficient to form a new simplex.
assumes C: "C ⊆ corners S" and k: "int(card C) = k+1"
obtains F where "F = convex hull C" and "F face_of S" and "k simplex F"
proof
obtain C1 where C1: "C1 corners_of S" using corners_exist by auto
from C1 have CC1: "C ⊆ C1" by (metis C corners_def corners_unique nS theI)
let ?F = "convex hull C"
show 0: "?F = convex hull C" by simp
thus 1: "?F face_of S" using C1 CC1 corners_of_def
by (metis face_of_convex_hull_affine_independent)
show 2: "k simplex ?F" unfolding simplex_def
proof (intro exI conjI)
show "¬ affine_dependent C"
using C1 CC1 affine_independent_subset corners_of_def by blast
show "int (card C) = k + 1" by (fact k)
show "?F = convex hull C" by (fact 0)
qed
qed
lemma ex1_corresponding_face:
assumes C: "C ⊆ corners S"
shows "∃!F. F = convex hull C ∧ F face_of S ∧ (int(card C)-1) simplex F"
proof -
let ?k = "(int(card C)-1)"
have "card C = ?k+1" by auto
with C obtain F where "F = convex hull C ∧ F face_of S ∧ ?k simplex F"
using sub_corners_simplex_face by blast
thus ?thesis by blast
qed
definition corresponding_face where
"corresponding_face C ≡ (THE F. F = convex hull C ∧ F face_of S ∧ (int(card C)-1) simplex F)"
if "C ⊆ corners S"
lemma corresponding_face:
assumes "C ⊆ corners S"
shows "(F = corresponding_face C) ≡
(F = convex hull C ∧ F face_of S ∧ (int(card C)-1) simplex F)"
using assms corresponding_face_def ex1_corresponding_face
by (smt the_equality)
subsubsection "More simplex helpers."
text "Here are few lemmas I thought I'd need while I was building up to the proof above."
lemma card_simplex_corners0:
assumes S: "n simplex S" and C: "C corners_of S"
shows "int(card C) = n+1"
― ‹Once I defined corresponding corners, metis can figure this out on its own.
proof -
from S have "aff_dim S = n" by (simp add: aff_dim_simplex)
thus "int(card C) = n + 1" using corners_of_def C by auto
qed
lemma simplex_corners_of_face:
assumes "n simplex S" and F: "F face_of S"
and SC: "SC corners_of S" and FC: "FC corners_of F"
shows "FC ⊆ SC"
proof
fix x assume "x∈FC"
with F FC SC show "x∈SC" using corners_of_def
by (metis (full_types) extreme_point_of_face
extreme_point_of_convex_hull_affine_independent)
qed
lemma simplex_face_of_corners:
assumes "n simplex S"
and "SC corners_of S" and "FC corners_of F"
and "FC ⊆ SC"
shows "F face_of S"
by (metis assms(2) assms(3) assms(4) corners_of_def face_of_convex_hull_affine_independent)
lemma obtain_corners:
assumes "n simplex S"
obtains C where "C corners_of S"
by (metis (no_types, hide_lams) aff_dim_affine_independent aff_dim_convex_hull aff_independent_finite assms corners_of_def simplex_def)
lemma corners_face_equiv:
assumes "SC corners_of S" and "FC corners_of F"
shows "(FC ⊆ SC ∧ int(card FC) = k+1)
≡ (F face_of S ∧ aff_dim F = k)"
by (smt nS assms corners_of_def simplex_corners_of_face simplex_face_of_corners)
subsectionmapping a set of corners to its corresponding face
lemma simplex_self_face:
― ‹Any simplex is a face of itself.
"S face_of S" using nS convex_simplex face_of_refl by auto
lemma n_simplex_only_n_face:
― ‹The only n dimensional face of an n simplex S is S itself.
shows "n d_faces S = {S}"
proof
let ?F = "n d_faces S"
have "?F ⊆ {f. f face_of S ∧ aff_dim f = n}" using d_faces_def by auto
hence "?F ⊆ {f. f face_of S}" by auto
thus "?F ⊆ {S}" by (smt nS aff_dim_simplex convex_simplex
d_faces_def face_of_aff_dim_lt insertCI mem_Collect_eq simplex_def subsetI)
show "{S} ⊆ n d_faces S"
using nS simplex_self_face aff_dim_simplex d_faces_def by blast
qed
subsection "---- proven simplex stuff but probably garbage ------"
lemma ex1_face_corners:
assumes "F face_of S"
shows "∃!c. c = corresponding_corners F"
by simp
lemma unique_face:
assumes "F face_of S" and "c0 corners_of F" and "c1 corners_of F"
shows "c0 = c1"
using Poly100.corners_equiv assms face_of_simplex_simplex simplex_dim_ge by blast
lemma unique_corners:
assumes "C ⊆ corners S"
and "F0 face_of S ∧ F0 = convex hull C"
and "F1 face_of S ∧ F1 = convex hull C"
and "F face_of S" and "c0 corners_of F" and "c1 corners_of F"
shows "c0 = c1"
using Poly100.corners_equiv assms face_of_simplex_simplex simplex_dim_ge by blast
subsection "---- unproven simplex stuff ------"
lemma corner_face_equiv:
assumes "SC corners_of S"
and "c0 ⊆ SC" and "f0 = corresponding_face c0"
and "c1 ⊆ SC" and "f1 = corresponding_face c1"
shows "c0 = c1 ⟷ f0 = f1"
proof
show "c0 = c1 ⟹ f0 = f1" by (simp add: assms(3) assms(5))
show "f0 = f1 ⟹ c0 = c1"
using nS assms
corners_def corners_of_def Poly100.corners_unique
corresponding_face ex1_corresponding_face the_equality
by (metis (no_types, lifting)
simplex_dim_ge
aff_dim_affine_independent aff_dim_convex_hull
aff_independent_finite affine_independent_subset)
qed
⌦‹
― ‹TODO: make this proof explicit. it takes a really long time to run.
lemma exists_corresponding_corners:
assumes "F face_of S"
shows "∃!C. C ⊆ corners S ∧ F = corresponding_face C"
using nS assms simplex_dim_ge
face_of_simplex_simplex simplex_corners_of_face
corners_def corners_of_def Poly100.corners_unique
corresponding_face unique_corresponding_face the_equality
aff_dim_affine_independent aff_dim_convex_hull
aff_independent_finite affine_independent_subset
by (metis (no_types, lifting))
⌦‹ recall:
"corresponding_face C ≡ (THE F. F = convex hull C ∧ F face_of S ∧ (int(card C)-1) simplex F)"
if "C ⊆ corners S"
definition corresponding_corners0 where
"corresponding_corners0 F ≡ (THE C. F = corresponding_face C)"
if "F face_of S"
definition corresponding_corners1 where
"corresponding_corners1 F ≡ (THE C. C ⊆ corners S ∧ F = convex hull C)"
if "F face_of S"
definition corresponding_corners where
"corresponding_corners F ≡ (THE C. C ⊆ corners S ∧ F = corresponding_face C)"
if "F face_of S"
lemma unique_aff_dim_convex_hull:
assumes 0: "¬affine_dependent C0"
and 1: "¬affine_dependent C1"
and 2: "convex hull C0 = convex hull C1"
and 3: "aff_dim C0 = aff_dim C1"
shows "C0 = C1"
by (metis 0 1 2 subsetI subset_antisym
extreme_point_of_convex_hull_affine_independent)
lemma simplex_face_equiv:
assumes F: "F face_of S"
and "C0 ⊆ corners S"
and "C1 ⊆ corners S"
and "convex hull C0 = convex hull C1"
shows "C0 = C1"
using nS assms unique_aff_dim_convex_hull face_of_simplex_simplex
by (metis aff_dim_convex_hull affine_independent_subset corners_are_corners_of corners_of_def)
― ‹this parallels @{thm ex1_corresponding_face}
lemma ex1_corresponding_corners:
assumes F: "F face_of S"
shows "∃!C. C ⊆ corners S ∧ F = corresponding_face C"
proof -
obtain FC where FC: "FC ⊆ corners S ∧ F = convex hull FC"
using nS F face_of_simplex_simplex
by (metis (no_types, lifting) aff_dim_affine_independent
aff_dim_convex_hull aff_independent_finite assms
corners_def corners_of_def corners_unique
simplex_corners_of_face simplex_def the_equality)
obtain FC' where CF: "FC' ⊆ corners S ∧ F = corresponding_face FC'"
using FC corresponding_face by auto
thus "∃!C. C ⊆ corners S ∧ F = corresponding_face C"
by (metis corner_face_equiv corners_def corners_unique nS the_equality)
qed
lemma corresponding_corners:
assumes F: "F face_of S"
shows "(C = corresponding_corners F)
≡ (C ⊆ corners S ∧ F = corresponding_face C)"
using nS F
by (smt corners_def
Poly100.corners_exist corners_unique
corresponding_corners_def ex1_corresponding_corners
corresponding_face simplex_dim_ge the_equality)
lemma corner_face_inj:
assumes C0: "C0 ⊆ corners S" and F0: "F0 = corresponding_face C0"
and C1: "C1 ⊆ corners S" and F1: "F1 = corresponding_face C1"
shows "C0 = C1 ⟷ F0 = F1"
using nS assms corresponding_corners corresponding_face by metis
lemma corresponding_face_inj:
"inj_on (corresponding_face) {C. C ⊆ corners S}"
using corner_face_equiv corners_are_corners_of inj_on_def by fastforce
lemma corresponding_face_bij:
shows "bij_betw (corresponding_face) {fc. fc ⊆ corners S} {f. f face_of S}"
proof -
let ?ps = "{fc. fc ⊆ corners S}" ― ‹power set of corners
let ?fs = "{f. f face_of S}" ― ‹set of all faces
have 0: "inj_on (corresponding_face) ?ps"
using corner_face_inj inj_on_def by (metis (no_types) mem_Collect_eq)
have 1: "∀f∈?fs. ∃c∈?ps. f = corresponding_face c"
using ex1_corresponding_corners by blast
have 2: "inj_on (corresponding_corners) ?fs"
by (smt corresponding_corners inj_on_def mem_Collect_eq)
have 3: "∀c∈?ps. ∃f∈?fs. c = corresponding_corners f"
by (metis corresponding_corners corresponding_face mem_Collect_eq)
from 0 1 2 3 have "(corresponding_face)`?ps = ?fs"
using corresponding_corners by auto
thus ?thesis using corresponding_face_inj inj_on_imp_bij_betw by fastforce
qed
lemma corresponding_face_card_inj:
assumes C0: "C0 ⊆ corners S ∧ card C0 = n" and F0: "F0 = corresponding_face C0"
and C1: "C1 ⊆ corners S ∧ card C1 = n" and F1: "F1 = corresponding_face C1"
shows "C0 = C1 ⟷ F0 = F1"
using nS assms corresponding_corners corresponding_face by metis
lemma card_corners_and_faces:
shows "card {fc. fc ⊆ corners S} = card {f. f face_of S}"
using bij_betw_same_card corresponding_face_bij by auto
lemma card_simplex_corners:
"card(corresponding_corners S) = n+1"
by (metis nS aff_dim_simplex corresponding_corners corresponding_face
diff_add_cancel simplex_self_face)
lemma corners_are_corresponding:
assumes "F face_of S"
shows "corners F = corresponding_corners F"
by (metis (no_types, hide_lams) Poly100.corners_are_corners_of assms
corners_of_def corresponding_corners corresponding_face nS
simplex_corners_of_face simplex_dim_ge)
lemma corners_of_are_corresponding:
assumes "F face_of S"
shows "FC corners_of F ⟷ FC = corresponding_corners F"
by (metis (full_types) Poly100.corners_are_corners_of Poly100.face_of_simplex_simplex assms corners_are_corresponding nS simplex_dim_ge)
lemma corners_of_face_are_corners:
assumes "F face_of S"
shows "FC = corners F ⟷ FC corners_of F"
by (metis assms corners_of_are_corresponding corners_def face_of_simplex_simplex the_equality)
lemma face_subset_equiv:
"F face_of S ⟷ (∃k. k simplex F ∧ corners F ⊆ corners S)"
― ‹TODO: why doesn't this follow automatically from @{thm corners_face_equiv}
or @{thm corresponding_corners}?
― ‹TODO: maybe I can defineis_simplexand not have to worry about the dimension?
currently, it's required for the second "show" step of the proof
proof
define sc where sc: "sc = corners S"
define fc where fc: "fc = corners F"
from nS sc have sc_of: "sc corners_of S" using corners_of_face_are_corners simplex_self_face by auto
show "F face_of S ⟹ (∃k. k simplex F ∧ fc ⊆ sc)"
proof -
assume F: "F face_of S" define k where k: "k = aff_dim F"
from F fc have "fc corners_of F" using corners_of_face_are_corners by auto
with F sc_of have "fc ⊆ sc" using simplex_corners_of_face using nS by blast
moreover from F k have "k simplex F" using face_of_simplex_simplex by auto
ultimately have "k simplex F ∧ fc ⊆ sc" by auto
thus ?thesis ..
qed
show "(∃k. k simplex F ∧ fc ⊆ sc) ⟹ F face_of S"
by (metis Poly100.corners_are_corners_of corners_of_def ex1_corresponding_face fc sc simplex_dim_ge)
qed
lemma card_corresponding_corners:
assumes "F face_of S"
shows "card(corresponding_corners F) = (aff_dim F)+1"
using assms face_of_simplex_simplex card_simplex_corners
by (metis (no_types, hide_lams) add.commute assms corners_of_are_corresponding corners_of_def )
lemma finite_corners: "finite (corners S)"
using corners_are_corners_of corners_of_def by auto
lemma subset_choose:
assumes "finite X"
shows "card {Y. Y ⊆ X ∧ card(Y) = k} = ((card X) choose k)"
using assms Binomial.n_subsets by auto
lemma card_faces_and_subsets:
"{(f,c). f face_of S ∧ c = corresponding_corners f} =
{(f,c). c ⊆ corners S ∧ f = corresponding_face c }"
by (metis corresponding_corners corresponding_face)
lemma faces_and_subsets_dim:
assumes "k ≥ -1"
shows "(f face_of S ∧ c = corresponding_corners f ∧ aff_dim f = k)
⟷ (c ⊆ corners S ∧ f = corresponding_face c ∧ card c = nat(k+1))"
by (smt aff_dim_simplex assms corresponding_corners corresponding_face int_nat_eq of_nat_eq_iff)
lemma card_faces_and_subsets_dim:
assumes "k ≥ -1"
shows "{(f,c). f face_of S ∧ c = corresponding_corners f ∧ aff_dim f = k}
= {(f,c). c ⊆ corners S ∧ f = corresponding_face c ∧ card c = nat(k+1)}"
using assms card_faces_and_subsets faces_and_subsets_dim by auto
― ‹same as @{thm corresponding_face_bij}, but this time add the cardinality predicates}
lemma corresponding_face_dim_bij:
shows "bij_betw (corresponding_face) {c. c ⊆ corners S ∧ card c = k}
{f. f face_of S ∧ aff_dim f = int(k)-1 }"
proof -
let ?cs = "{c. c ⊆ corners S ∧ card c = k }"
let ?fs = "{f. f face_of S ∧ aff_dim f = int(k)-1 }"
let ?cf = "corresponding_face"
have 0: "inj_on (?cf) ?cs"
using corresponding_face_card_inj inj_on_def
by (metis (mono_tags, lifting) corresponding_face_inj inj_onD inj_onI mem_Collect_eq)
have 1: "∀f∈?fs. ∃c∈?cs. f = ?cf c"
by (smt aff_dim_affine_independent aff_dim_convex_hull aff_dim_simplex
affine_independent_subset corners_are_corners_of
corners_of_def corners_unique corresponding_face
ex1_corresponding_face ex1_corresponding_corners
mem_Collect_eq nat_int)
have 2: "inj_on (corresponding_corners) ?fs"
by (smt corresponding_corners inj_on_def mem_Collect_eq)
have 3: "∀c∈?cs. ∃f∈?fs. c = corresponding_corners f"
using Poly100.faces_and_subsets_dim mem_Collect_eq nS
by (smt aff_dim_simplex corresponding_corners corresponding_face)
from 0 1 2 3 have 4: "(?cf)`?cs = ?fs" using corresponding_corners by auto
hence "inj_on ?cf ?cs ⟹ (?cf)`?cs = ?fs ⟹ bij_betw ?cf ?cs ?fs"
using bij_betw_imageI[of ?cf ?cs ?fs] by simp
with 0 4 show "bij_betw (?cf) ?cs ?fs" by blast
qed
lemma card_simplex_faces:
assumes "k ≥ -1"
shows "k d_face_count S = (nat(n+1) choose nat(k+1))"
proof -
define nc where nc: "nc = nat(k+1)"
have k1nc: "k+1 = nc" using assms nc by auto
have "k d_face_count S = card {f. f face_of S ∧ aff_dim f = k}"
unfolding d_face_count_def d_faces_def ..
also have "... = card {c. c ⊆ corners S ∧ card(c) = nc}"
proof -
have "∀n. card {A. A ⊆ corners S ∧ card A = n} = card {A. A face_of S ∧ aff_dim A = int n - 1}"
using bij_betw_same_card corresponding_face_dim_bij by blast
moreover have "int nc = 1 + k" by (metis add.commute k1nc)
ultimately show ?thesis by simp
qed
also have "... = (card (corners S) choose nc)"
using nc finite_corners Binomial.n_subsets by simp
finally show "k d_face_count S = (nat(n+1) choose nc)"
by (metis card_simplex_corners0 corners_are_corners_of nS nat_int)
qed
end
(* ------------------------------------------------------------------------ *)
sectionThe Euler characteristic for Simplices.
(* ------------------------------------------------------------------------ *)
text "The Euler characteristic is the alternating sum ‹-x⇩-⇩1 + x⇩0 - x⇩1 + x⇩2 … ± x⇩n›
of the number of n-dimensional faces."
definition euler_char where
"euler_char p = (∑k≤nat(aff_dim p+1). (-1::int)^k * (int(k)-1) d_face_count p)"
textFor example, in a triangle, we have:
k | n |xn|
--+----+----+------------
0 | -1 | 1 | empty face
1 | 0 | 3 | vertices
2 | 1 | 3 | edges
3 | 2 | 1 | surface
The alternating sum ofxn(and therefore the Euler characteristic) is: -(1) + 3 - 3 + 1 = 0
subsectionThe empty face
textThe empty set is considered to be a face of any polytope,
and its affine dimension is -1, but we don't actually count
it in the sum.
lemma "S = {} ⟷ aff_dim S = -1"
by (fact Convex_Euclidean_Space.aff_dim_empty)
lemma empty_face_count:
"(-1) d_face_count p = 1"
proof -
let ?F = "(-1) d_faces p"
have "?F = {f. f face_of p ∧ aff_dim f = -1}" by (simp add: d_faces_def)
hence "?F = {f. f face_of p ∧ f = {}}" by (simp add: aff_dim_empty)
hence f: "?F = {{}}" by auto
have "(-1) d_face_count p = card(?F)" by (simp add: d_face_count_def)
with f show "(-1) d_face_count p = 1" by simp
qed
subsectionEuler characteristic for an n-Simplex.
textFrom all the simplex work above, we have a bijection between
faces of an n-simplex and subsets of its n+1 corners.
textThere are (n+1 choose k) ways to select k corners, so there are
(n+1 choose k) distinct faces with aff_dim (k-1).
textWhen we plug these numbers into the Euler relation, we get a sequence that
always sums to 0.
textHowever, we have a small off-by-one error to contend with:
@{thm Binomial.choose_alternating_sum} requiresn>0when it would
really apply ton0... So we have to prove the 0 case separately.
textThis actually worked out okay for me: getting these two cases to
both work out to zero forced me to rework and clarify a whole lot of
the theory behind counting simplex corners.
lemma euler_0simplex_eq0:
assumes "0 simplex S"
shows "euler_char S = 0"
proof -
have neg1: "(-1) d_face_count S = 1"
by (simp add: empty_face_count)
have zero: "0 d_face_count S = 1"
by (simp add: n_simplex_only_n_face assms d_face_count_def)
define N1 where N: "N1 = nat(0+1)"
― ‹Now plug these results into the definition, and calculate.
hence "euler_char S = (∑k≤N1. (-1::int)^k * (int(k)-1) d_face_count S)"
by (metis (full_types) aff_dim_simplex assms euler_char_def)
also have "... = (-1::int)^0 * (int(0)-1) d_face_count S
+ (-1::int)^1 * (int(1)-1) d_face_count S"
using N by simp
finally show "euler_char S = 0" using neg1 zero by simp
qed
lemma euler_nsimplex_eq0:
assumes "n simplex S" "n≥0"
shows "euler_char S = 0"
proof -
define N1 where N1: "N1 = nat(n+1)"
hence "euler_char S = (∑k≤N1. (-1::int)^k * (int(k)-1) d_face_count S)"
using N1 assms aff_dim_simplex assms euler_char_def by blast
also have "... = (∑k≤N1. (-1::int)^k * (N1 choose k))"
using assms N1 card_simplex_faces
by (smt One_nat_def Suc_nat_eq_nat_zadd1 add.right_neutral add_Suc_right int_nat_eq nat_int sum.cong)
finally show "euler_char S = 0"
using N1 Binomial.choose_alternating_sum by (smt assms(2) nat_0_iff neq0_conv sum.cong)
qed
sectionSimplication
textv. To make a system more complex so that the use of the system is easier or simpler.
textIn this case, I'm also using the word to mean the process of forming a simplical complex
or triangulation.
textNote that @{theory "HOL-Analysis.Polytope"} already provides several lemmas for
talking about this idea:
@{thm cell_subdivision_lemma}
@{thm cell_complex_subdivision_exists}
@{thm simplicial_complex_def}
@{thm triangulation_def}
We'll make use of this machinery below, but in particular, we want to set things
up so we can reason inductively about the process, showing that at any step along
the way, some particular property holds.
(We will use this induction-by-triangulation tactic twice in this paper:
first to prove that the euler characteristic is 0 for all polyhedra, and then
later to derive Pick's theorem for the area of a polygon on ‹ℤ⇧2.
textWe define the concept of a cutting a polyhedron (really any ordered set) into two parts:
textIn particular, we want to cut our space (and any unlucky polyhedra that happen to be
in it) by means of a hyperplane. A hyperplane is just the n-dimensional equivalent
of a plane that cuts a 3d space into two halves. (Or a line that cuts a plane, etc.)
TODO: describe inner product, and what this set notation means.
subsection "definitions"
definition is_simplex where
"is_simplex p ≡ (∃n. n simplex p)"
lemma is_simplex [simp]:
"is_simplex p ⟶ (∃n. n simplex p)"
using is_simplex_def by auto
default_sort euclidean_space
typedef (overloaded) 'a Polytope
= "{p::'a set. polytope p}"
using polytope_empty by auto
typedef (overloaded) 'a Simplex
= "{s::'a set. polytope s ∧ is_simplex s}"
using is_simplex_def polytope_sing by fastforce
typedef (overloaded) 'a hyperplane
= "{h::'a set. ∃a b. h = {x. a ∙x = b}}"
by blast
definition cut_of ("_ cut'_of _" [70,70] 75) where
"H cut_of P ≡ ({x∈P. x≤H}, {x∈P. x≥H})"
typedef (overloaded) 'a cut_fn
= "{fn::('a Polytope ⇒ 'a hyperplane). True}"
by blast
typedef (overloaded) 'a simplication
― ‹A list of the actual simplices obtained, and the cuts used to make them.
TODO: add a predicate so that the cuts have to all be adjacent to the simplex obtained.
= "{hsl::('a hyperplane list × 'a Simplex) list. True}"
by blast
⌦‹
fun simplication ("_ simplication _ _" [80,82,80] 85) where
0 : "Q simplication [] = Q {} " |
subsectionTverberg's Method
textAdapted from ∗‹How to cut a convex polytope into simplicesby Helge Tverberg
lemma tv1:
assumes convex:"convex K" and poly:"polytope K" and d:"aff_dim K = d"
fixes F assumes "F ∈ faces K"
shows "is_simplex K ∨ (∃v. v ∈ verts K
∧ (∃F0. F0 ∈ faces K ∧ ¬(v ⊆ F0)
∧ (∃F1. F1 ∈ faces K ∧ ¬(v ⊆ F1) ∧ F0 ≠ F1)))"
proof (cases "d<2")
case True
hence "is_simplex K" using is_simplex_def d poly polytope_lowdim_imp_simplex by fastforce
thus ?thesis ..
next
case False hence "d ≥ 2" by simp thus ?thesis
proof (cases "is_simplex F")
case True
thus ?thesis try0 sorry
next
case False
thus ?thesis try0 sorry
qed
qed
sectionEuler Characteristic for a a general full-dimensional polytope.
― ‹
Now we know the euler characteristic for all simplices. Then, following
Tverberg or Euler or possibly just Polytope.thy, we will show that:
a) the euler characterstic of a polytope = 0 provided it's 0 for
the two sections you get when you slice it with a hyperplane.
b) any polytope can be cut into simplices
textNow we want to show that at each step along the way, the
euler characteristic remains unchange.
Putting these two things together with our proof of the characteristic
for simplices, we can then show that it holds for any polytope.
theorem euler_poincare:
assumes "polytope p" and "aff_dim p = d"
shows "euler_char p = 1"
sorry
(* ------------------------------------------------------------------------ *)
sectionThe Polyhedron Formula
(* ------------------------------------------------------------------------ *)
textThe polyhedron formula is the Euler relation in 3 dimensions.
― ‹
The euler characteristic is 0 for all non-empty simplices,
but (at least for the polyhedron forumla) we will ignore the empty
face and the face that consists of the whole simplex. That's where
the 2 comes from)
locale convex_polyhedron =
fixes p assumes "polytope p" and "aff_dim p = 3"
begin
definition F where "F = card(surfs p)"
definition V where "V = card(verts p)"
definition E where "E = card(edges p)"
theorem polyhedron_formula:
shows "F + V - E = 2"
sorry
end
(* ------------------------------------------------------------------------ *)
sectionThe Platonic Solids
(* ------------------------------------------------------------------------ *)
textThere are exactly five platonic solids. The following theorem enumerates
them by their Schläfli pairs(s,m), using the polyhedron formula above.
theorem (in convex_polyhedron) PLATONIC_SOLIDS:
fixes s::nat ― ‹number of sides on each face
and m::nat ― ‹number of faces that meet at each vertex
assumes "s ≥ 3" ― ‹faces must have at least 3 sides
and "m ≥ 3" ― ‹at least three faces must meet at each vertex
and "E>0"
and eq0: "s * F = 2 * E"
and eq1: "m * V = 2 * E"
shows "(s,m) ∈ {(3,3), (3,4), (3,5), (4,3), (5,3)}"
proof -
― ‹Following Euler, as explained here:
https://www.mathsisfun.com/geometry/platonic-solids-why-five.html
―‹First, redefine F and V in terms of sides and meets:
from eq0 `s≥3` have f: "F = 2*E/s"
by (metis nonzero_mult_div_cancel_left not_numeral_le_zero of_nat_eq_0_iff of_nat_mult)
from eq1 `m≥3` have v: "V = 2*E/m"
by (metis nonzero_mult_div_cancel_left not_numeral_le_zero of_nat_eq_0_iff of_nat_mult)
―‹Next, rewrite Euler's formula as inequalityiq0in those terms:
from polyhedron_formula have "F + V - E = 2" .
with f v have "(2*E/s) + (2*E/m) - E = 2" by simp
hence "E/s + E/m - E/2 = 1" by simp
hence "E * (1/s + 1/m - 1/2) = 1" by argo
with `E>0` have "1/s + 1/m - 1/2 = 1/E"
by (simp add: linordered_field_class.sign_simps(24) nonzero_eq_divide_eq)
with `E>0` have iq0: "1/s + 1/m > 1/2" by (smt of_nat_0_less_iff zero_less_divide_1_iff)
―‹Lower bounds for{s,m}provide upper bounds for{1/s, 1/m}››
with `s≥3` `m≥3` have "1/s ≤ 1/3" "1/m ≤ 1/3" by auto
―‹Plugging these intoiq0, we calculate upper bounds for{s,m}››
with iq0 have "1/s > 1/6" "1/m > 1/6" by linarith+
hence "s < 6" "m < 6" using not_less by force+
―‹This gives us 9 possible combinations for the pair(s,m).
with `s≥3` `m≥3` have "s ∈ {3,4,5}" "m ∈ {3,4,5}" by auto
hence "(s,m) ∈ {3,4,5} × {3,4,5}" by auto
―‹However, four of these fail to satisfy our inequality.
moreover from iq0 have "1/s + 1/m > 1/2" .
hence "(s,m) ∉ {(4,4), (5,4), (4,5), (5,5)}" by auto
ultimately show "(s,m) ∈ {(3,3), (3,4), (3,5), (4,3), (5,3)}" by auto
qed
textSo far, this proof shows that if these relationships between {s,m,F,V} hold,
then a platonic solid must have one of these five combinations for (s,m).
We have not yet shown the converse -- that the five remaining pairs actually do
represent valid polyhedra.
We also haven't shown that eq0 and eq1 actually describe convex polyhedra. These
should be theorems, not assumptions.
Probably even,s3,m3, andE>0can be derived from more basic facts. I will
have to study Polytope.thy a bit more.
(* ------------------------------------------------------------------------ *)
sectionPick's Theorem
(* ------------------------------------------------------------------------ *)
textAnother consequence of Euler's formula is Pick's theorem, which describes
the area of a polygon whose vertices all lie on the integer lattice points of the
plane. (In other words for each vertex, the coordinates x,y on the plane are both
integers.)
We can prove it by triangulating the polygon such that each triangle has 0
interior lattice points, and the boundary of each triangle is a lattice point.
Then, assuming the area of each such triangle is 1/2, we can just divide the
number of faces F by 2. (except one face is the plane itself, so we say A=(F-1)/2.
theorem pick0: "B = 3 ∧ I = 0 ⟶ A = 1/2"
― ‹TODO: prove the area of a primitive triangle is 1/2.
oops
theorem funkenbusch:
fixes I::int and B::int ― ‹number of interior and boundary points
shows "E = 3*I + 2*B - 3"
― ‹informal proof due to Funkenbusch:
"From Euler's Formula to Pick's Formula Using an Edge Theorem"
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.475.919&rep=rep1&type=pdf
(still thinking about how to formalize this.)
The theorem counts the number of edges in the triangularization, inductively.
0. (Base case): B=3, I=0E=3 (a single triangle)
E' = 3*I' + 2*B' - 3
E' = 3*0 + 2*3 - 3
1. I'=I+1E'=E+3 : new interior point subdivides a triangle into 3 parts, adding 3 edges
true because the formula contains the term E = 3*I + ...
2. B'=B+(1-x)E'=E+(2+x) : new boundary point adds 2 edges to boundary. but this also
movesX0old boundary points into the interior, and have to draw
an edge from the new point to each of them, too.
E' = 3*I' + 2*B' - 3
E' = 3*(I+x) + 2*(B+1-x) -3
E' = 3I +3x + 2B + 2 - 2x - 3
E' = 3I + 2B + x - 1
E + (2+x) = 3I + 2B + x - 1
E = 3I + 2B - 3
oops
theorem pick's_theorem:
fixes I::int and B::int ― ‹number of interior and boundary points
and V::int and E::int and F::int ― ‹edges, vertices, and faces (triangles + the plane)
assumes "B≥3" ― ‹So we have a polygon
and euler: "V - E + F = 2" ― ‹Euler's theorem
and verts: "V = I + B" ― ‹Each point has become a vertex in the triangularization graph
and edges: "E = 3*I + 2*B - 3" ― ‹Funkenbusch's edge theorem, above
and area: "A = (F-1)/2" ― ‹coming soon...
shows "A = I + B/2 - 1"
proof -
from euler have "V - E + F = 2" .
with verts have "(I + B) - E + F = 2" by simp
with edges have "(I + B) - (3*I + 2*B - 3) + F = 2" by simp
hence "(I + B) - (3*I + 2*B - 3) + F = 2" by simp
hence "F = 2 * I + B - 1" by simp
hence "F-1 = 2*I + B - 2" by simp
hence "(F-1)/2 = I + B/2 -1" by simp
with area show "A = I + B/2 - 1" by auto
qed
end
@tangentstorm

This comment has been minimized.

Show comment
Hide comment
@tangentstorm

tangentstorm Jul 24, 2018

so: I made a start on enumerating the platonic solids for the list of 100 theorems, but I need some help:
it assumes that I've already proven euler's relation (which is also on the list). I haven't, but ignore that for now. :)

my question is how to approach the three items marked '!HELP!' in the text... they just seem like they ought to be easy to simplify.

NOTE: the plain isar *.thy file is here: https://github.com/tangentstorm/tangentlabs/blob/master/isar/Poly100.thy

Owner

tangentstorm commented Jul 24, 2018

so: I made a start on enumerating the platonic solids for the list of 100 theorems, but I need some help:
it assumes that I've already proven euler's relation (which is also on the list). I haven't, but ignore that for now. :)

my question is how to approach the three items marked '!HELP!' in the text... they just seem like they ought to be easy to simplify.

NOTE: the plain isar *.thy file is here: https://github.com/tangentstorm/tangentlabs/blob/master/isar/Poly100.thy

@dominique-unruh

This comment has been minimized.

Show comment
Hide comment
@dominique-unruh

dominique-unruh Jul 24, 2018

For the "m<=5" I would try the following:
Instead of proving "s<=5", I would prove

have "s<=5" if "1/s + 1/m > 1/2" for s m

From that, you can then conclude both "s<=5" and "m<=5" directly.

(I haven't checked if it all works out.)

dominique-unruh commented Jul 24, 2018

For the "m<=5" I would try the following:
Instead of proving "s<=5", I would prove

have "s<=5" if "1/s + 1/m > 1/2" for s m

From that, you can then conclude both "s<=5" and "m<=5" directly.

(I haven't checked if it all works out.)

@tangentstorm

This comment has been minimized.

Show comment
Hide comment
@tangentstorm

tangentstorm Jul 24, 2018

@dominique-unruh thanks! I'll give that a try for the next version!

Owner

tangentstorm commented Jul 24, 2018

@dominique-unruh thanks! I'll give that a try for the next version!

@tangentstorm

This comment has been minimized.

Show comment
Hide comment
@tangentstorm

tangentstorm Jul 25, 2018

@int-e showed me how to rewrite a huge chunk of the middle section, so the redundancy just went away... I think this is really starting to shape up into something nice. :)

Owner

tangentstorm commented Jul 25, 2018

@int-e showed me how to rewrite a huge chunk of the middle section, so the redundancy just went away... I think this is really starting to shape up into something nice. :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment