General strategy for theorems about complicated definitions

Stream: lean4

[Jannis]

Hi!
So I'm writing some very basic graph theory proofs, but my definitions are getting a bit tangled to the point that I have relatively complicated definitions e.g. for Path.append:

def Path.append
  (p1 : Path graph) (p2 : Path graph)
  (hp1 : p1.IsBetween u v) (hp2 : p2.IsBetween v w)
  (hvOnlyCommon : OnlyCommon v p1 p2) :
    { p : Path graph // p.IsBetween u w ∧ p.length = p1.length + p2.length - 1 } := by ...

As you can see, I modeled some properties of the return value of Path.append through the use of a subtype.
I think modeling Path.IsBetween u w with the subtype is fine, but I am not happy with having to model the length properties in there too.

This leads me to my first question: It's surely not idiomatic to just prove everything about a definition inside the definition itself and then have the proven theorems be properties of the subtype like I did, right?

Let me now explain, why I even chose to put the length properties in the subtype.
This is because my Path.append definition has to do a bit of work to actually append the paths (orient the given paths, which are basically lists of vertices).
I tried proving the length properties from an external theorem, but I couldn't get that to work, because unfolding Path.append (and Path.length) lead to something I couldn't really work with:

⊢ (↑(match ⟨op1, hop1⟩ with
          | ⟨op1, ⋯⟩ =>
            match p2.orient hp2 with
            | ⟨op2, ⋯⟩ =>
              ⟨{
                  walk :=
                    { vertices := op1.walk.vertices ++ op2.walk.vertices.tail, isNonempty := ⋯,
                      hasAdjacentVertices := ⋯ },
                  isNonRepeating := ⋯ },
                ⋯⟩)).walk.vertices.length =
  p1.walk.vertices.length + p2.walk.vertices.length - 1

This leads me to my second question: Is there some way of simplifying this goal state? That would enable me to actually prove properties such as the length properties in external theorems, which I think would be more idiomatic as the properties of definitions like Path.append would then be extensible from the outside.

[Jannis]

So I actually managed to prove the length properties from an external theorem now:

theorem path_append_length
  (p1 : Path graph) (p2 : Path graph)
  (hp1 : p1.IsBetween u v) (hp2 : p2.IsBetween v w)
  (hvOnlyCommon : OnlyCommon v p1 p2) :
    (let p := (p1.append p2 hp1 hp2 hvOnlyCommon).val
    p.length = p1.length + p2.length - 1) := by
  simp [Path.append, Path.length]
  obtain ⟨_, _, _, _⟩ := p1.orient hp1
  obtain ⟨_, _, _, _⟩ := p2.orient hp2
  have : p2.walk.vertices.length > 0 := List.length_pos_of_ne_nil p2.walk.isNonempty
  grind

This now leaves only my first question to be answered.

[Max Nowak 🐉]

It generally makes more sense to first implement the function itself, and then prove properties about it. When you define addition on numbers, you don't have a type add : Nat -> Nat -> { res : Nat // is commutative and all the other properties } either.

[Max Nowak 🐉]

If you often handle objects like "path from A to B", then you can still define a helper after defining append and after proving properties about it. Something like def PathBetween (a b : Vertex) : Type := { p : Path // ... }, and then define some convenience combinators, like def PathBetween.append (p1 : PathBetween A B) (p2 : PathBetween B C) : PathBetween A C := ...