Any low hanging fruits related to SimpleGraph?

Stream: graph theory

[Lessness]

The title. I want to prove something for training purposes about simple graphs (and too lazy to browse Mathlib documentation, at least right now :sweat_smile:).

Cheers! :tea:

[Shreyas Srinivas]

I don't know how low this is, but given that a formulation already exists in Isabelle: Berge's Lemma

[Lessness]

Oh, thank you! Will try doing it.

[Lessness]

Do you know where to find the Isabelle proof of Berge's Lemma? I only found the arXiv publication here. It states that their proof was different from standard proof and shorter than it.

[Shreyas Srinivas]

They describe their shorter proof there. I thought there was an AFP entry for it. I'll ask the author.

[Lessness]

Thank you!

[Lessness]

Does this formulation of Berge's Lemma makes sense?

import Mathlib.Init.Function
import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Finsubgraph
import Mathlib.Combinatorics.SimpleGraph.Connectivity


def IsMaximum {V} {G: SimpleGraph V} {M: SimpleGraph.Finsubgraph G} (H: M.val.IsMatching): Prop :=
  forall (M': SimpleGraph.Finsubgraph G) (H': M'.val.IsMatching),
  exists (f: M'.val.verts -> M.val.verts), Function.Injective f

mutual
  def AlternatingWalkFalse {V} {G: SimpleGraph V} (M: SimpleGraph.Finsubgraph G) {x y: V}: SimpleGraph.Walk G x y -> Prop
  | SimpleGraph.Walk.nil => True
  | @SimpleGraph.Walk.cons _ _ x' y' _ _ p => (M.val.Adj x' y' -> False) /\ AlternatingWalkTrue M p
  def AlternatingWalkTrue {V} {G: SimpleGraph V} (M: SimpleGraph.Finsubgraph G) {x y: V}: SimpleGraph.Walk G x y -> Prop
  | SimpleGraph.Walk.nil => True
  | @SimpleGraph.Walk.cons _ _ x' y' _ _ p => M.val.Adj x' y' /\ AlternatingWalkFalse M p
end

def AugmentingPath {V} {G: SimpleGraph V} (M: SimpleGraph.Finsubgraph G) {x y: V} (P: SimpleGraph.Path G x y): Prop :=
  (Set.Mem x M.val.verts -> False) /\
  (Set.Mem y M.val.verts -> False) /\
  AlternatingWalkFalse M P.val

theorem Berge's_lemma {V} {G: SimpleGraph V} {M: SimpleGraph.Finsubgraph G} (H: M.val.IsMatching):
  IsMaximum H <-> (forall (x y: V) (P: SimpleGraph.Path G x y), AugmentingPath M P -> False) := by
  sorry

[Lessness]

Especially definition of IsMaximum which, probably, could be defined in some better way.

[Shreyas Srinivas]

So first a little bit of notational clean up:

import Mathlib


def IsMaximum {V} {G: SimpleGraph V} {M: SimpleGraph.Finsubgraph G} (_: M.val.IsMatching): Prop :=
  ∀ (M': SimpleGraph.Finsubgraph G), M'.val.IsMatching →
    ∃ (f: M'.val.verts -> M.val.verts), Function.Injective f

mutual
  def AlternatingWalkFalse {V} {G: SimpleGraph V} (M: SimpleGraph.Finsubgraph G) {x y: V}: SimpleGraph.Walk G x y -> Prop
  | SimpleGraph.Walk.nil => True
  | @SimpleGraph.Walk.cons _ _ x' y' _ _ p => (M.val.Adj x' y' -> False) ∧ AlternatingWalkTrue M p
  def AlternatingWalkTrue {V} {G: SimpleGraph V} (M: SimpleGraph.Finsubgraph G) {x y: V}: SimpleGraph.Walk G x y -> Prop
  | SimpleGraph.Walk.nil => True
  | @SimpleGraph.Walk.cons _ _ x' y' _ _ p => M.val.Adj x' y' ∧  AlternatingWalkFalse M p
end

def AugmentingPath {V} {G: SimpleGraph V} (M: SimpleGraph.Finsubgraph G) {x y: V} (P: SimpleGraph.Path G x y): Prop :=
  (x ∉ M.val.verts) ∧  (y ∉ M.val.verts) ∧
  AlternatingWalkFalse M P.val

theorem Berge's_lemma {V} {G: SimpleGraph V} {M: SimpleGraph.Finsubgraph G} (H: M.val.IsMatching):
  IsMaximum H ↔ (∀ (x y: V) (P: SimpleGraph.Path G x y), AugmentingPath M P → False) := by
  sorry

[Shreyas Srinivas]

Secondly, I am not sure how Berge's theorem applies to infinite graphs, but this is partly because I have not touched this area in a long time. The proof that I mentioned works naturally for the case of finite graphs. SimpleGraph V is not finite by default

[Yaël Dillies]

You can always just assume Finite V.

[Shreyas Srinivas]

Yeah that's what I wanted to say

[Shreyas Srinivas]

Further, when you limit yourself to finite graphs (perhaps with Finite or Finset), you can use the cardinality based definition of maximum matching

[Shreyas Srinivas]

And then consider the definition of augmenting path

[Shreyas Srinivas]

It it based on alternating walks.

[Shreyas Srinivas]

which need not terminate even in finite graphs

[Shreyas Srinivas]

Also, I am not sure why you are calling IsMaximum on a proof that M is a matching without using the proof.

[Lessness]

Aren't walks basically a finite list, which always terminate? Or I'm misunderstanding something.

[Lessness]

Shreyas Srinivas said:

Also, I am not sure why you are calling IsMaximum on a proof that M is a matching without using the proof.

Fixed.

[Shreyas Srinivas]

A walk can loop indefinitely.

[Shreyas Srinivas]

unlike a path.

[Shreyas Srinivas]

A path requires a sequence of distinct vertices which form a walk. walks don't have the distinctness requirement.

[Shreyas Srinivas]

An alternating walk which is looping at the end won't be augmenting.

[Lessness]

One can't define infinitely long walk, as I believe, even if there are loops. At least in Lean it will be finite, as inductive datatypes do.

[Shreyas Srinivas]

No it is not just about infinite walks. Berge's theorem holds for augmenting paths, not augmenting walks.

[Shreyas Srinivas]

An augmenting walk can loop back to the beginning and it will meet the definition of an augmenting walk (be alternating with both endpoints unmatched). But augmenting the matching with this path will not give you a larger matching.

[Lessness]

def AugmentingPath {V} [Finite V] {G: SimpleGraph V} (M: SimpleGraph.Subgraph G) {x y: V} (P: SimpleGraph.Path G x y): Prop :=
  x ∉ M.verts ∧ y ∉ M.verts ∧ AlternatingWalkFalse M P.val

Here I have P: SimpleGraph.Path G x y, so that should be okay, imho. :thinking:

[Shreyas Srinivas]

yes that should work

[Lessness]

Lessness said:

Shreyas Srinivas said:

Also, I am not sure why you are calling IsMaximum on a proof that M is a matching without using the proof.

Fixed.

Fixed it back (and changed Finsubgraph to simply Subgraph).

def IsMaximum {V} [Finite V] {G: SimpleGraph V} {M: SimpleGraph.Subgraph G} (_: M.IsMatching): Prop :=
  ∀ (M': SimpleGraph.Subgraph G), M'.IsMatching →
  ∃ (f: M'.verts -> M.verts), Function.Injective f

Imho, if I remove both M.IsMatchingit goes wrong. I need these hypothesis to talk specifically about Matchings, not some general subgraph.

[Lessness]

It's similar to this:

def IsMaximum' {V} [Finite V] {G: SimpleGraph V} (H: { M: SimpleGraph.Subgraph G // M.IsMatching }): Prop :=
  ∀ (H': { M': SimpleGraph.Subgraph G // M'.IsMatching }),
  ∃ (f: H'.val.verts -> H.val.verts), Function.Injective f

[Shreyas Srinivas]

A simpler way to do that is to attach the matching condition to the body of the definition.

[Shreyas Srinivas]

Because you don't have to destructure the object of the subtype all the time.

[Lessness]

Current version is such:

import Mathlib

def IsMaximum {V} {G: SimpleGraph V} {M: SimpleGraph.Subgraph G} (_: M.IsMatching): Prop :=
  ∀ (M': SimpleGraph.Subgraph G), M'.IsMatching →
  M'.support.ncard ≤ M.support.ncard

mutual
  def AlternatingWalkFalse {V} {G: SimpleGraph V} (M: SimpleGraph.Subgraph G) {x y: V}: SimpleGraph.Walk G x y → Prop
  | SimpleGraph.Walk.nil => True
  | @SimpleGraph.Walk.cons _ _ x' y' _ _ p => ¬ M.Adj x' y' ∧ AlternatingWalkTrue M p
  def AlternatingWalkTrue {V} {G: SimpleGraph V} (M: SimpleGraph.Subgraph G) {x y: V}: SimpleGraph.Walk G x y → Prop
  | SimpleGraph.Walk.nil => True
  | @SimpleGraph.Walk.cons _ _ x' y' _ _ p => M.Adj x' y' ∧ AlternatingWalkFalse M p
end

def AugmentingPath {V} {G: SimpleGraph V} (M: SimpleGraph.Subgraph G) {x y: V} (P: SimpleGraph.Path G x y): Prop :=
  x ∉ M.support ∧ y ∉ M.support ∧ AlternatingWalkFalse M P.val

theorem Berge's_lemma {V} [Finite V] {G: SimpleGraph V} {M: SimpleGraph.Subgraph G} (H: M.IsMatching):
  IsMaximum H ↔ (∀ (x y: V) (P: SimpleGraph.Path G x y), ¬ AugmentingPath M P) := by
  sorry

[Lessness]

Will start tinkering with proving this lemma now.

[Shreyas Srinivas]

are you comfortable with mutually inductive definitions?

[Shreyas Srinivas]

Personally I am not.

[Lessness]

It was the easiest way (for me) to define the AugmentingPath. I believe I have no problems with mutual definitions.

Do you have some better suggestion?

[Kyle Miller]

I'd say feel free to use the mutually inductive definitions if you have no problems proving things about them, at least for the experience.

[Kyle Miller]

You can also make the False/True suffixes be an actual Bool argument to a single definition

[Kyle Miller]

I've found before that alternating walks are a real pain to deal with. My last attempt, I made a custom inductive type for them along with maps to plain Walks, since that way you can do cases on the alternating walk and make progress without needing to wrestle with unfolding a definition. https://github.com/leanprover-community/mathlib/blob/a5c872475ef4a299a616d5eb1fc6723128741158/src/hamiltonian2.lean#L458

[Lessness]

Kyle Miller said:

You can also make the False/True suffixes be an actual Bool argument to a single definition

Great idea! Done.

[Shreyas Srinivas]

you might benefit here from an index which tracks the path length

[Lessness]

What did I do wrong here? Or, probably better question, what should I use instead of SimpleGraph.Subgraph.degree?

import Mathlib

#check SimpleGraph.Subgraph.degree

def aux0 {V} [Finite V] {G: SimpleGraph V} {M: G.Subgraph}:
  ∀ (x: V), x ∈ M.verts → M.degree x ≤ 2 := by
    sorry

It gives me an error: failed to synthesize instance Fintype ↑(SimpleGraph.Subgraph.neighborSet M x).

[Yaël Dillies]

Replace [Finite V] by [Fintype V] [DecidableEq V]

[Lessness]

Thank you!

[Lessness]

Another possible option is, I believe, such:

import Mathlib

def aux0 {V} {G: SimpleGraph V} {M: G.Subgraph}:
  ∀ (x: V), x ∈ M.verts → (M.neighborSet x).ncard ≤ 2 := by
    sorry

[Yaël Dillies]

Please don't use ncard when you know the set is finite. This is going to prove painful further down the line.

[Lessness]

Oh, thank you

[Shreyas Srinivas]

I am still not sure that using functions with junk values won't result in proving statements that look wrong (emphasis on 'look') and mess with people's minds.

[Shreyas Srinivas]

At least in graph theory, the correct default can vary according to the problem.

[Lessness]

Hmm, it still don't work for me. Lean still announces that it can't synthesize the instance. :(
Does it work for you?

import Mathlib

def aux0 {V} [Fintype V] [DecidableEq V] {G: SimpleGraph V} (M: G.Subgraph):
  ∀ (x: V), x ∈ M.verts → M.degree x ≤ 2 := by
    sorry

[Kyle Miller]

You probably need [DecidableRel G.Adj] (I take that back, it's unclear which decidability assumption is needed/best)

[Kyle Miller]

I think this instance is the one that's not firing because you don't have enough assumptions to get that DecidablePred instance

[Kyle Miller]

Shreyas Srinivas said:

I am still not sure that using functions with junk values won't result in proving statements that look wrong (emphasis on 'look') and mess with people's minds.

If you've got a concrete example of this causing an issue in one of your mathlib formalization projects, then feel free to create a new topic explaining it!

[Lessness]

What's solution to this? Defining necessary instances by hand?

Anyway, reading/learning about type classes now in "Theorem Proving in Lean 4"... with hope to solve the problem myself, maybe.

[Lessness]

This works.

import Mathlib

def aux0 {V} [Fintype V] {G: SimpleGraph V} (M: G.Subgraph) [DecidableRel M.Adj]:
  ∀ (x: V), x ∈ M.verts → M.degree x ≤ 2 := by sorry

[Lessness]

Yes, some progress! :sweat_smile: :partying_face:

Did long proof (probably could be shortened very much when I get more experience) of the lemma

def aux0 {V} {G: SimpleGraph V} {M1 M2: G.Subgraph} (H1: M1.IsMatching) (H2: M2.IsMatching):
  let S := M1.SymmDiff M2
  ∀ (x: V), x ∈ S.verts → (S.neighborSet x).encard ≤ 2

[Lessness]

Any hints how to approach lemma aux1?
It's here at Github.

[Shreyas Srinivas]

404 on that link for me

[Lessness]

Ow, sorry, yes, it's still private. One minute.

[Lessness]

Fixed the link

[Lessness]

I probably should at first prove that for all graphs with maximum vertex degree 2 there is only three types of connected components... and then use this information to prove their properties for the symmetrical difference of two matchings.

[Shreyas Srinivas]

On my phone right now, but isn't aux0 a theorem?

[Lessness]

Yes. Changed def to theorem.

[Lessness]

Simplified aux1 formulation to such:

theorem aux1 {V} {G: SimpleGraph V} (M: G.Subgraph):
  (∀ (x: V), x ∈ M.verts → (M.neighborSet x).encard ≤ 2) →
  ∀ (c: M.coe.ConnectedComponent),
  ∃ (x y: V) (W: G.Walk x y), W.IsTrail ∧ W.toSubgraph = (⊤: G.Subgraph).induce c.supp := by sorry

If I manage to prove this (big if), then the three types of connected components should be easy to prove. Just reason about the length and equality or inequality of the endpoints.

[Lessness]

It seems I need to exclude possibility of infinitely big connected components, otherwise it will be impossible to prove the theorem aux1. What's the best way to do that?
Finite V, Finite M.verts or maybe even Finite M.support?

[Lessness]

I chose to use Finite V, as it seemed the best (subjectively) to me.

[Mauricio Collares]

Quoting Yaël's advice:

Yaël Dillies said:

Replace [Finite V] by [Fintype V] [DecidableEq V]

[Mauricio Collares]

I understand this is not exactly what you're asking, but it just seemed relevant

[Lessness]

Right, yes.

[Lessness]

Thank you!

[Lessness]

In need of suggestions/hints for proof of theorem aux1... Thanks in advance.

Graph theory is harder than it seems at the first sight. :sweat_smile:

[Lessness]

Lessness said:

It's here at Github.

[Kevin Buzzard]

Lessness said:

Graph theory is harder than it seems at the first sight. :sweat_smile:

Yup, Lean even had perfectoid spaces before it had graphs!

[Lessness]

Interesting!

[Shreyas Srinivas]

As a first simplification, after you have all the finiteness conditions, don't use encard. This is only going to add extra steps.

[Shreyas Srinivas]

For further help I will have to play with the proof first.

[Lessness]

Ok, so the first step is to get rid of the encard. That I can do.

[Kyle Miller]

I feel like encard is the least of your worries -- all you need is some lemma that can go back and forth between (M.neighborSet x).encard ≤ 2 and some other convenient representation, and applying that lemma is hardly a step compared to a full proof of aux1.

Do you have a paper proof yet of aux1, one where you don't cheat and use your intuition about how obvious it is? I find that's usually the biggest problem... Lots of this stuff is a lot more technical than you might think.

[Shreyas Srinivas]

You might benefit from just plugging in the interval_cases version of that claim namely that the degree of x is 0, 1, or 2

[Kyle Miller]

One argument I can see is that you do induction on the number of edges of M, build up theory for what happens to connected components when you add/delete edges, and then argue that if the edge is joining the connected components then the trails from each connected component's trail must start/end at the vertices being joined since those vertices must be degree <= 1, and so you can join them to make the trail for the joined connected component.

[Shreyas Srinivas]

Then you have a separate theorem to prove that a connected graph in which all nodes have degree exactly 2 is a cycle.

[Shreyas Srinivas]

Then a slight generalisation says " if G is a connected graph with all its vertices having degrees 1 or 2, then it is a cycle or a path"

[Kyle Miller]

I forgot to handle the case of an edge that isn't a bridge between connected components -- in that case you argue you can just extend the trail for the connected-component-without-the-edge by the edge. Incidentally that's a cycle, but the fact it's a cycle isn't so important for the proof.

[Shreyas Srinivas]

Shreyas Srinivas said:

Then a slight generalisation says " if G is a connected graph with all its vertices having degrees 1 or 2, then it is a cycle or a path"

These are simpler theorems that are show that a graph is one of so many kinds.

[Shreyas Srinivas]

Then extend them to subgraphs

[Shreyas Srinivas]

(This is a trivial step)

[Shreyas Srinivas]

Okay I now see Kyle's message (thanks zulip's android app). His argument is useful for applying the lemmas I described in the subgraphs while handling the connected component related details.

[Lessness]

OK, you were right that getting rid of S.encard <= 2 will be easy.
Proved that

theorem encard_aux1 {V} (S: Set V) (H: S.encard ≤ 2):
  S = ∅ ∨ (∃ x, S = {x}) ∨ (∃ x y, x ≠ y ∧ S = {x, y})

[Kyle Miller]

(And because getting rid of it is easy, it's harmless keeping it in the definition.)

[Shreyas Srinivas]

I just think it becomes a tedious distraction

[Lessness]

It's harmless distraction right now thanks to the theorem (encard_aux1), I believe. Now looking forward the hardest part.

Will make some kind of paper proof for the start, maybe.
I like to tinker directly in a proof assistant, without doing paper proofs, but that works only for simplest situations, probably. Must get rid of this habit.

[Lessness]

Now reading your suggestions and hints, thank you all!

[Kyle Miller]

For aux1, another strategy, rather than futzing too much with connected components, is to reduce to the case that M is connected somehow (going to a connected component, you still have the same degree condition, with the same degrees), and then prove by contradiction. You want to prove that given "forall x y : V and W : G.walk x y, then if W.toSubgraph is equal to the subgraph, then W is not a trail" you can prove False. Since G is finite, there must be some walk W such that W.toSubgraph is equal to the subgraph. So then take a least-length such walk. This is not a trail by assumption. Now it's a simple matter of combinatorics :wink: (More seriously, you use this to somehow argue you have a vertex of degree at least three, and if there isn't one, to argue that your walk is not of least length.)

[Shreyas Srinivas]

How can M be connected? It is a matching

[Kyle Miller]

Not in aux1. (@Lessness There seems to be a bug in the aux1 statement. Do you mean M.induce c.supp rather than (⊤: G.Subgraph).induce c.supp?)

[Lessness]

Ouw. Have to check definition of induce, but it's possible that I have made a bug.

[Kyle Miller]

(⊤: G.Subgraph).induce c.supp gives you the induced subgraph relative to G itself, and it might have more edges than M.induce c.supp (in particular, edges outside of M). If you want c-as-a-subgraph, then since c : M.coe.ConnectedComponent, it seems that M.induce c.supp is capturing the intent.

(Side note: at some point I was working on building up API around the set of connected components as subgraphs -- maybe I'll try to find it again and see if it's worth salvaging.)

[Lessness]

Yes, it seems that M.induce c.supp is the right, not what I had for now.

[Lessness]

The first part of aux1 - where the connected component has node with degree 0 - is proven (with some ugly proof, imho)
Here

That's some progress :partying_face:

[Lessness]

Erm, should probably restructure the proof somewhat... I mean, prove that connected component with some node of degree zero is trail. In different theorem.
Then look at connected components with some node of degree 1 (all nodes has degree 1 or 2). Probably another separate theorem.
And then the final theorem where all nodes has degree of 2.

Then combine them into one - the current formulation of aux1.

[Lessness]

Restructuring done.

Now I have two theorems with sorry and aux1 proved assuming these two are correct and will be proved too.

theorem aux1_subcase_2 {V} {G: SimpleGraph V} (M: G.Subgraph):
  ∀ (x: V) (H: x ∈ M.verts) (H0: ∃ (y: V), M.neighborSet x = {y}),
  ∃ (z: V) (W: G.Walk x z), W.IsTrail ∧
  W.toSubgraph = M.induce (M.coe.connectedComponentMk ⟨x, H⟩).supp := by
    sorry

theorem aux1_subcase_3 {V} {G: SimpleGraph V} (M: G.Subgraph):
  ∀ (c: M.coe.ConnectedComponent)
  (H: ∀ x, x ∈ c.supp → ∃ x1 x2, x1 ≠ x2 ∧ M.neighborSet x = {x1, x2}),
  ∃ (x: V) (W: G.Walk x x), W.IsCycle ∧ W.toSubgraph = M.induce c.supp := by
    sorry

[Peter Nelson]

encard is the correct generality for that lemma - any connected graph with maximum degree at most 2 is a cycle or (possibly infinite) path.

[Lessness]

Hello, currently I'm trying to prove the theorem about graph with max degree 2 and got stuck a bit.
In this case I'm going to ask for some help.

At the file Berge.lean, line 640, I have commented at the place.
Part of the proof state:

W_1: SimpleGraph.Walk (SimpleGraph.Subgraph.coe (SimpleGraph.Subgraph.deleteVerts M {↑v}))
  { val := x_2, property := (_ : x_2 ∈ M.verts \ {↑v}) } { val := u, property := H7 }
H12: u ∈ M.verts
⊢ SimpleGraph.Walk (SimpleGraph.Subgraph.coe M) { val := x_2, property := (_ : x_2 ∈ M.verts) }
  { val := u, property := H12 }

Here I want to do induction on W_1 and construct Walk in the subgraph M using parts of W_1. But the induction doesn't work and I can't find a way to fix that (for now).
The error message is:

index in target's type is not a variable (consider using the `cases` tactic instead)
  { val := x_2, property := (_ : x_2 ∈ M.verts \ {↑v}) }

[Shreyas Srinivas]

How are you calling induction?

[Lessness]

induction W_1... are there other ways, too?

[Lessness]

Probably the simple induction isn't going to work even after generalizing a bit. Something to think about.

Taking a pause because Monday means studying other stuff and tests at university.

[Shreyas Srinivas]

I am sorry I forgot about this entirely

[Shreyas Srinivas]

I was reading the hitchhikers guide to logical verification and came across this exact issue

[Shreyas Srinivas]

Page 92

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

The simplest trick (not described there explicitly) is to take whatever expression lean is complaining about as not a variable (say e), and use the set tactic from mathlib to assign a new variable to it.

[Shreyas Srinivas]

set x:=e with h will assign a variable x to expression e, replace all occurrences of e with x in all hypothesis and the goal and insert an equality h: x=e in your hypothesis, which you can use for rw

[Kyle Miller]

Yeah, set or generalize are tricks for this index problem

[Lessness]

Thank you! I managed to prove auxiliary lemma to use instead of set or generalize, but next time will try them out too.

[Lessness]

Anyway, I'm abandoning this Berge's lemma for now (probably at least for two and half months... I have exams at university during January and, if anything goes successfully, then will return to this).

I believe that anything up to formulation of aux_experiment and the Berge's_lemma at the end is good enough to use for someone who is interesting finishing what I started (if there's anyone, of course). I will be glad to learn from this person, if that happens. :)

Sorry! And cheers!

[Kyle Miller]

Ah well, I hope you had fun struggling with simple graphs, and I hope to see you back!

(These might be low-hanging fruit, but there's something about combinatorial objects where, you can see the fruit, you can see that you can reach the fruit, but somehow you're not allowed to just go and pick it. There's always some additional complexity you have to sort out first... It's not quite the same, but I'm suddenly reminded of that hilarious babel fish puzzle in the old The Hitchhiker's Guide To The Galaxy text adventure game.)

To remind myself where you are so far, I think you've got it here