start on a proof of the polyhedron formula

Poly100.thy

(* 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

(* ------------------------------------------------------------------------ *)
section ‹Vocabulary (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"

(* ------------------------------------------------------------------------ *)
section ‹Simplex 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 -
  ― ‹‹C1› is 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 from ‹C1› that isn't in F, and call the remaining set ‹C›.›
  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 that ‹F› and ‹C› together 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 of ‹C›
        are the extreme points of an ‹n-1› dimensional 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 C ‹A ∈ C1› ‹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, a ‹facet_of› and a ‹convex hull› are 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 S ‹A ∈ C1› ‹A ∉ F› ‹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 drop ‹aff_dim C› by 1. But we already know ‹F⊆convex hull C›, and (although we
          haven't proven it here), ‹aff_dim C = aff_dim F›. So if there were any point ‹p∈C ∧ p∉F›,
          we would also have ‹aff_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) S ‹A ∈ C1› ‹A ∉ F› ‹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


text ‹The proof above was a lot of work. I wanted to generalize it to arbitrary faces, which
      made me realize that the set ‹C› in 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 as ‹C›, I decided it probably stood for ‹corners›, 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')


text ‹Once 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





subsection ‹Count of faces›

text ‹We will show that ‹k d_face_count S = (n+1) choose (k+1)› for all ‹n 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)



subsection ‹mapping 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 define ‹is_simplex› and 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

(* ------------------------------------------------------------------------ *)
section ‹The 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)"

text ‹For example, in a triangle, we have:

    k | n  |‹x⇩n›|
    --+----+----+------------
    0 | -1 | 1  | empty face
    1 |  0 | 3  | vertices
    2 |  1 | 3  | edges
    3 |  2 | 1  | surface

The alternating sum of ‹x⇩n› (and therefore the Euler characteristic) is:  -(1) + 3 - 3 + 1 = 0›



subsection ‹The empty face›

text ‹The 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

subsection ‹Euler characteristic for an n-Simplex.›


text ‹From all the simplex work above, we have a bijection between
faces of an n-simplex and subsets of its n+1 corners.›

text ‹There are (n+1 choose k) ways to select k corners, so there are
(n+1 choose k) distinct faces with aff_dim (k-1).›

text ‹When we plug these numbers into the Euler relation, we get a sequence that
always sums to 0.›

text ‹However, we have a small off-by-one error to contend with:
  @{thm Binomial.choose_alternating_sum} requires ‹n>0› when it would
  really apply to ‹n≥0›... So we have to prove the 0 case separately.›

text ‹This 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


section ‹Simplication›

text ‹v. To make a system more complex so that the use of the system is easier or simpler.›

text ‹In this case, I'm also using the word to mean the process of forming a simplical complex
or triangulation.›

text ‹Note 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›.›


text ‹We define the concept of a cutting a polyhedron (really any ordered set) into two parts:›

text ‹In 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 {} " |
›

subsection ‹Tverberg's Method›

text ‹Adapted from ∗‹How to cut a convex polytope into simplices› by 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

section ‹Euler 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

›

text ‹Now 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

(* ------------------------------------------------------------------------ *)
section ‹The Polyhedron Formula›
(* ------------------------------------------------------------------------ *)
text ‹The 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

(* ------------------------------------------------------------------------ *)
section ‹The Platonic Solids›
(* ------------------------------------------------------------------------ *)

text ‹There 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 inequality ‹iq0› in 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 into ‹iq0›, 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

text ‹So 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, ‹s≥3›, ‹m≥3›, and ‹E>0› can be derived from more basic facts. I will
  have to study Polytope.thy a bit more.›


(* ------------------------------------------------------------------------ *)
section ‹Pick's Theorem›
(* ------------------------------------------------------------------------ *)

text ‹Another 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=0 ⟶ E=3  (a single triangle)
       E' = 3*I' + 2*B' - 3
       E' = 3*0  + 2*3  - 3

  1. I'=I+1 ⟶ E'=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
                                 moves ‹X≥0› old 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

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

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 thanks! I'll give that a try for the next version!

@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. :)