[isabelle] adjacent facets

[Michal Wallace]

I'm stuck on something that feels like it ought to be easy... (again :D)

From "HOL-Analysis.Polytope", we have that a polytope is a bounded

polyhedron, and so it's the intersection of a bunch of half-hyperspaces,
and its facets are polytopes lying in the corresponding hyperplanes.

Assume F is a facet of a polytope T, embedded in hyperplane H, and E is a
facet of F, embedded in hyperplane h.

Clearly h⊂H, and also there's another facet F' of T embedded in another
hyperplane H' such that h⊂H', and therefore F and F' are adjacent facets.

It's easy to convince Isabelle that h⊂H, and it's easy enough to obtain the
set of hyperplanes that bound T... But I don't even know how to begin to
prove that (exactly) one of them other than H intersects H at h.

Part of my problem is that I'm working through a learning curve for
Isabelle and a separate learning curve for analysis, and I'm not sure which
one I'm struggling with at any given time.

Can anyone offer some advice here? Even just how to break this problem down
into smaller steps?

Here's what I have so far:

theory Adjacent
imports Main "HOL-Analysis.Polytope"begin
default_sort euclidean_space
section "adjacency"
definition adjacent :: "'a set ⇒ 'a set ⇒ bool" where
"adjacent x y ≡ x≠y ∧ (∃f. f facet_of x ∧ f facet_of y)"
lemma adjacent_facets_exist:
assumes T:"polytope T" "aff_dim T > 0"
and F:"F facet_of T" and E:"E facet_of F"
shows "∃!F'. F'≠F ∧ (E facet_of F') ∧ (F' facet_of T)"
― ‹Every edge of a polygon shares a vertex with another edge, every
face of a 3d polytope shares an edge with another face, etc.›proof
define dimF where dimF:"dimF = aff_dim F"
define dimE where dimE:"dimE = aff_dim E"
have "dimE = dimF-1" using F dimF E dimE facet_of_def by auto

― ‹Obtain the dimF hyperplane H containing F and the dimE hyperplane
h containing E›
from T have phT: "polyhedron T" using polytope_imp_polyhedron by auto
with F obtain H A B where h: "H = {x. A ∙ x = B} ∧ F = T ∩ H"
by (metis facet_of_polyhedron)
from F have phF: "polyhedron F" using phT facet_of_def
face_of_polyhedron_polyhedron by auto
with E obtain h a b where h: "h = {x. a ∙ x = b} ∧ E = F ∩ h"
by (metis facet_of_polyhedron)

― ‹The only reason E is a facet is that F is bounded. That boundary
must have been inherited from the boundaries of T, but I don't know
how to show it. GRRR...›

oops
end

[Michal Wallace]

Of course, right after I finally gave up and asked for help, a (partial)
solution (and/or red herring)
popped into my head.... I still have no idea how to formalize it, though.

Suppose I find a point P in h (so on the same hyperplane as facet F), but
on the other side of E.
Now I can draw a line segment between P and some point R in F and it will
intersect E. (Assume
it intersects somewhere in the middle, and not at the extreme points of E.)

Then, if I have a point Q in between E and R, it must be outside F...
And because polytope T is convex, R must be outside T.

(Perhaps I need to show that convex implies that no two facets fall in the
same hyperplane, but I think I can manage this...)

So now, if I have a third point C at the center of T (thus not in F), and I
draw a line segment
between C and the external point R, there must be a portion of the segment
that's
inside T and a portion that's outside, and so there must be another face of
T that's
getting intersected.

In fact, if I extend the line segment PR past R out to infinity, then every
point in between
has this same characteristic: a line segment between it and C must
intersect some face of T.

As I bring the point Q closer and closer to E, then my line segment CQ will
eventually intersect the face adjacent to F.

This seems like progress, but I'm still essentially where I started: I know
in my head that
some hyperplane supporting T has a particular property, but i have no idea
how I might
convince Isabelle to believe me.

OTOH, this seems like I'm wandering closer to what "Analysis" is actually
all about,
so maybe there are already some places to look in the library for
inspiration, if only I
know what to look for.

Any thoughts?

Thanks... :)

Post by Michal Wallace
I'm stuck on something that feels like it ought to be easy... (again :D)
From "HOL-Analysis.Polytope", we have that a polytope is a bounded
polyhedron, and so it's the intersection of a bunch of half-hyperspaces,
and its facets are polytopes lying in the corresponding hyperplanes.
Assume F is a facet of a polytope T, embedded in hyperplane H, and E is a
facet of F, embedded in hyperplane h.
Clearly h⊂H, and also there's another facet F' of T embedded in another
hyperplane H' such that h⊂H', and therefore F and F' are adjacent facets.
It's easy to convince Isabelle that h⊂H, and it's easy enough to obtain
the set of hyperplanes that bound T... But I don't even know how to begin
to prove that (exactly) one of them other than H intersects H at h.
Part of my problem is that I'm working through a learning curve for
Isabelle and a separate learning curve for analysis, and I'm not sure which
one I'm struggling with at any given time.
Can anyone offer some advice here? Even just how to break this problem
down into smaller steps?
theory Adjacent
imports Main "HOL-Analysis.Polytope"begin
default_sort euclidean_space
section "adjacency"
definition adjacent :: "'a set ⇒ 'a set ⇒ bool" where
"adjacent x y ≡ x≠y ∧ (∃f. f facet_of x ∧ f facet_of y)"
assumes T:"polytope T" "aff_dim T > 0"
and F:"F facet_of T" and E:"E facet_of F"
shows "∃!F'. F'≠F ∧ (E facet_of F') ∧ (F' facet_of T)"
― ‹Every edge of a polygon shares a vertex with another edge, every face of a 3d polytope shares an edge with another face, etc.›proof
define dimF where dimF:"dimF = aff_dim F"
define dimE where dimE:"dimE = aff_dim E"
have "dimE = dimF-1" using F dimF E dimE facet_of_def by auto
― ‹Obtain the dimF hyperplane H containing F and the dimE hyperplane h containing E›
from T have phT: "polyhedron T" using polytope_imp_polyhedron by auto
with F obtain H A B where h: "H = {x. A ∙ x = B} ∧ F = T ∩ H"
by (metis facet_of_polyhedron)
from F have phF: "polyhedron F" using phT facet_of_def face_of_polyhedron_polyhedron by auto
with E obtain h a b where h: "h = {x. a ∙ x = b} ∧ E = F ∩ h"
by (metis facet_of_polyhedron)
― ‹The only reason E is a facet is that F is bounded. That boundary must have been inherited from the boundaries of T, but I don't know how to show it. GRRR...›
oops
end

[Michal Wallace]

Update: I worked out an informal proof that describes how to identify an
adjacent facet of a polytope.
Now (other than cleaning up my inevitable mistakes and oversights) I just
need to figure out how to express it in Isabelle.

Basically, I'm going to approach this by induction on the number of
supporting hyperplanes that aren't in a "discarded" set:

- If I'm down to one hyperplane, I'm pretty sure I can prove it's the one
I want.
- If I find the hyperplane containing adjacent facet along the way,
that's good, too.
- Otherwise, I look at a potential candidate, throw it out, and then
recurse.

So far, induction rules in Isabelle are a bit mysterious to me, so my next
stop is to review the docs and
code for induction, to try and understand how to make a custom induction
rule for this.

Does anyone know of an example proof that does anything similar to this?

Thanks!


( work-in-progress psuedo-proof follows )


(* known facts:
polytope T is defined by a finite number of half-spaces, each defined
by a hyperplane containing exactly one facet. *)


lemma adjacent_face:
assumes "polytope T"
and "H in halfspaces_of T" and "HP = defining-hyperplane-of H"
and "F facet-of T" and "E facet_of F" and "E in HP"

and "P in HP" and "P is outside T"
and "(P,F) convex-through E"
(* That is, a line segment from P to any point inside F intersects
E.
I'm calling this "P convex with F through E", because I don't
know a better term yet. *)

(* 'discarded' is a set of half-spaces of T that we know are not
adjacent to F.
Since it's proven that the total number of facets is finite, we
can use induciton the number of remaining candidates. *)
and "discarded SUBSET half-spaces-of T"
(* also nothing in the discard pile can be an adjacent facet we've
overlooked *)
and "FORALL x:discarded. p:x | x=H | ~(E SUBSET (T INTERSECT
(definining-hyperplane-of H)))"

(* also we only care about the hyperplanes that cut P off from T, so
just to simplify things: *)
and "FORALL h:halfspaces_of T. p:h ==> h:discarded"

and "N = card(halfspaces_of T) - card(discarded)"

obtains F' where "F'~=F" and "F' facet_of T" and "E facet_of F'"

by (induction N)

- because P is in H but outside T, there must be an H' where H'
halfspace_of T
with corresponidng hyperplane HP', where HP' intersects HP, cutting P
off from T.
- obtain such H' HP' (* I can already do this much *)

- if N=1 then THE F' where (F' facet_of T & F' SUBSET HP') must be
adjacent to F
proof (* adjacent faces must exist, or else there'd be a 'hole'
in the boundary of the polytope, and polytopes are bounded
by definition. Since F' is the last possible face it could be,
it must be the one we're looking for.

Ideally, this fact would be sufficient to show that the
adjacent facet
exists, and I wouldn't need to do any induction to obtain it,
but if
there are multiple faces, it's always possible that no matter
how
close P gets to E, any facet cutting it off from P could fail
to be
adjacent to F because there's some other tiny facet in between.
But, with only 1 possible facet left, it has to be the one
closing
the gap.

*) sorry

- if N > 1 then the face adjacent with F through E is in (facets
T)-(discarded)
we already have obtained F' and correspoinding H', so evaluate it:

- then show ?thesis
proof (cases "E is a subset of HP'")
case True:
- thus F and F' are adjacent by shared facet E, and we have what we
were looking for.
proof (* face E is in both hyperplanes, and no two facets can be
in the same hyperplane. *)
(* so... this is what we were looking for. *) sorry
case False:
- then HP' does not contain E
- then either HP' is a supporting hyperplane of E, OR they are
completely disjoint
(* HP' can't intersect E somewhere in the middle, because that
would remove
part of E from T and we know E is a subset of T *)
- either way, this isn't the face we're looking on, so recurse on
(discarded insert H')

[José Manuel Rodriguez Caballero]

Post by Michal Wallace
Part of my problem is that I'm working through a learning curve for
Isabelle and a separate learning curve for analysis, and I'm not sure which
one I'm struggling with at any given time.

This happens because you began with a very advanced topic. That is not a
good strategy from a pedagogical point of view. It was better to do one
thing at the time. If your goal is to prove Euler's formula in for
polytopes, try to prove easier versions first and go increasing the
complexity step by step. Your intuition about this particular problem will
increase with practice. So, I recommend you to follow the following
learning process:

1. Proof Euler's formula for graphs as an exercise of initiation. Use
graph duality:

2. Generalize your proof to any CW-complex (these are generalizations of
graphs). To implement this one in Isabelle/HOL require more coffee than the
graph theoretical version, but it is conceptually simpler than its
particular case for the polytopes.
3. Prove the Euler's formula as a corollary of your result for
CW-complex. You can reduce your proof to the case of the hypercube, because
any polytope is topologically equivalent to a hypercube. For the hypercube,
Euler formula is just a calculation that you can carry out by induction on
the dimension.

There is some wisdom about proving theorems from Alexander Grothendieck
that could be useful for computer scientists and programmers (I hope
someday some will write a book entitled Grothendieck for computer
scientists.). According to Grothendieck, it is easier to prove an abstract
theorem than a concrete one, because in abstraction you only deal with the
essential parts of the theorem whereas in the concrete case there are too
many details.

Kind Regards,
Jose M.

[Michal Wallace]

On Sat, Aug 25, 2018 at 1:31 PM José Manuel Rodriguez Caballero <
***@gmail.com> wrote:

This happens because you began with a very advanced topic. That is not a

Post by José Manuel Rodriguez Caballero

Post by José Manuel Rodriguez Caballero
good strategy from a pedagogical point of view. It was better to do one
thing at the time. If your goal is to prove Euler's formula in for
polytopes, try to prove easier versions first and go increasing the
complexity step by step. Your intuition about this particular problem will
increase with practice. So, I recommend you to follow the following

1. Proof Euler's formula for graphs as an exercise of initiation. Use
graph duality: http://youtu.be/-9OUyo8NFZg
This is a nice proof. I'm not convinced it's any easier to formalize, but

it might be... I'm willing to give this a shot.

There's a good start on graph theory in the AFP:
https://www.isa-afp.org/entries/Graph_Theory.html It's based on directed
graphs, but allows modelling undirected graphs as bi-directed graphs.
It looks like it defines spanning trees, and cycles, but I'd have to define
faces and duals... Maybe that won't be hard?

Post by José Manuel Rodriguez Caballero
1. Generalize your proof to any CW-complex (these are generalizations
of graphs). To implement this one in Isabelle/HOL require more coffee than
the graph theoretical version, but it is conceptually simpler than its
particular case for the polytopes.
Okay, but I don't understand what CW-complex is. I don't understand any of

the following terms yet: homotopy, closed ball, attaching map, covered,
Hausdorf space, homeomorphism, boundary... Those are just from the first
two paragraphs on the wikipedia description. I do believe you when you say
that it's easier to express these ideas with CW complexes, but...

In a way, this *seems* like it's sort of like saying: the program I want to
write in C would be easier to express in ML, but I only have access to a C
compiler, so in order to express things in that nice elegant way, I have to
first implement ML in C...

Once the cost of implementing ML (or CW) is added to the budget, the "hard"
way probably turns out to be quicker.

Am I wrong about this? Is there an introductory book about CW complexes
that defines everything step by step that I could follow? Or...
alternatively, do you see this stuff already existing under different names
in Isabelle? Or... Do you feel like writing a CW-complex theory? :D

(To be fair, the available language for discussing polytopes in Isabelle is
turning out to be pretty limited, too, but at least I have vague memories
of high school geometry to fall back on... )

Post by José Manuel Rodriguez Caballero
1. Prove the Euler's formula as a corollary of your result for
CW-complex. You can reduce your proof to the case of the hypercube, because
any polytope is topologically equivalent to a hypercube. For the hypercube,
Euler formula is just a calculation that you can carry out by induction on
the dimension.
Let's say I get this far...

How can I demonstrate that a polytope has connected edges, the way a graph
(or presumably a CW complex) does?

To me this means that two edges share a vertex, or two faces share an edge,
and so on in higher dimensions... Which is to say that they are adjacent,
and we're back to my original question: how to show that such things exist?

Post by José Manuel Rodriguez Caballero
There is some wisdom about proving theorems from Alexander Grothendieck
that could be useful for computer scientists and programmers (I hope
someday some will write a book entitled Grothendieck for computer
scientists.). According to Grothendieck, it is easier to prove an abstract
theorem than a concrete one, because in abstraction you only deal with the
essential parts of the theorem whereas in the concrete case there are too
many details.

I like this idea, and in fact, I've found myself reusing it repeatedly
already: in proving the polyhedron formula for simplices, I wound up giving
names to all sorts of things that were being referred to implicitly (like
vertices and d-faces and whatnot).

Yesterday I hit on the idea of giving a name to the halfspaces of a
polytope, and was able to show that if a point exists in one half-space but
isn't inside the polyhedron, then there must be a half-space that doesn't
contain it (and thus at least one facet separating it from the polytope)...
I think with this I can eventually show that there's some sequence of
intersecting hyperplanes connecting this new face from the one in the first
hyperplane, (and therefore the Nth face in the sequence is adjacent to the
Nth+1), but I'm not quite there yet...

[Michal Wallace]

So, just to finish the story... I found an extremely unsatisfying proof
that an adjacent
facet exists for any facet of a facet. I still don't know how to prove it's
unique.
(Maybe that's not actually the case in higher dimensions?)

Anyway:

section‹Adjacent facets›
definition adjacent_by :: "'a set ⇒ 'a set ⇒ 'a set ⇒ bool"
("_ _ adjacent'_by _" [60,60,60] 65) where
"x y adjacent_by f ≡ x≠y ∧ f facet_of x ∧ f facet_of y"
definition adjacent :: "'a set ⇒ 'a set ⇒ bool" where
"adjacent x y ≡ (∃f. x y adjacent_by f)"
lemma adjacent_facet_exists:
assumes T:"polytope T"
and F:"F facet_of T" and E:"E facet_of F"
shows "∃F'. F F' adjacent_by E"
― ‹Every edge of a polygon shares a vertex with another edge, every
face of a 3d polytope shares an edge with another face, etc.›proof -
from T have phT: "polyhedron T" using polytope_imp_polyhedron by auto
from F E have E0:"E face_of T" using face_of_trans
facet_of_imp_face_of by blast
moreover have E1:"E ≠ {} ∧ E≠T " using E F facet_of_def by auto
ultimately have E2:"E = ⋂{F'. F' facet_of T ∧ E ⊆ F'}"
using phT face_of_polyhedron by blast
then obtain Fs where Fs:"Fs = {F'. F' facet_of T ∧ E ⊆ F'} ∧ E=⋂Fs" by auto
then obtain F' where F':"F'∈Fs ∧ F'≠F"
by (metis E Inf_greatest facet_of_imp_subset facet_of_irrefl
order_refl subset_antisym)
hence "E facet_of F'"
by (smt Collect_mem_eq Collect_mono_iff E F Fs E0 E1 E2
equalityE face_of_face facet_of_def facet_of_imp_face_of le_Inf_iff)
hence "F'≠F ∧ (E facet_of F') ∧ (F' facet_of T)" using F' Fs by blast
then show ?thesis using adjacent_by_def using E by blastqed

[José Manuel Rodriguez Caballero]

Post by Michal Wallace
So, just to finish the story... I found an extremely unsatisfying proof
that an adjacent
facet exists for any facet of a facet. I still don't know how to prove it's
unique.
(Maybe that's not actually the case in higher dimensions?)

You could avoid your problem using the following approach:
1- the Euler characteristic is a topological invariant, i.e., it is
invariant under homeomorphisms.
2- any polytope is homeomorphic to an hypercube.
3- the Euler characteristic of a hypercube is 1.

Notice that:

A 0-cube is just a point. So, its Euler characteristic is 1 = 1.

A 1-cube is a segment. Notice that a segment has 2 vertices and 1 edge. So,
its Euler, characteristic is 2 - 1 = 1.

In the case of a 2-cube (a square), you have 4 vertices, 4 edges and 1
face. So, its Euler characteristic is 4 - 4 + 1 = 1.

the general proof is by induction on the dimension.

Definition of Euler Characteristic for this purpose:
http://applet-magic.com/eulerpoincare4.htm

Kind Regards,
José M.

[José Manuel Rodriguez Caballero]

Post by Michal Wallace
So, just to finish the story... I found an extremely unsatisfying proof
that an adjacent
facet exists for any facet of a facet. I still don't know how to prove it's
unique.
(Maybe that's not actually the case in higher dimensions?)

The proof is as follows:
1. This is true for an n-dimensional simplex (just proceed by induction on
the dimension).
2. Any polytope can be expresses as a union of adjacent simplexes.

Imagine a square A B C D draw from A to B to C to D and then to A again.
For example, given the 1-face AB, you want to prove that there is a 1-face
which is adjacent to AB (in this case AC or BD are the answers).

Divide the square A B C D into two triangles A B D and C B D. Notice that
A B is adjacent to B D by definition. Also, C B is adjacent to A B by
definition.

For more information about simplicial complexes:
https://en.wikipedia.org/wiki/Simplicial_complex

If you want to visualice higher dimensions, you need to see pictures of
higher dimensional objects in the plane, close your eyes and try to
reconstruct the picture in your head. It require some practice, but it
work! Here is an introduction to visualization of higher dimensions:

Sidis was able to visualize the four dimension when he was a child, during
his PhD at Harvard: https://www.sidis.net/

Kind Regards,
José M.