Basic graph data structure

Stream: new members

[Hugo Sales Corrêa]

Hi everyone, I'm looking to implement some basic graph algorithms as a means of learning Lean

I decided to start by specifying DiGraphs as subtypes as follows

def DiGraph {u: Nat} : Type :=
    {adj: Array (Array (Fin u)) // u ≤ adj.size}

I'm just trying to guarantee that no vertex will be adjacent to a non-existent vertex.
I got stuck trying to prove minor things,

  variable {u: Nat} (g h: DiGraph (u:=u))

  def emptyDiGraph: DiGraph (u := 0) := ⟨#[], by simp⟩

  def addNode : DiGraph (u:=u) :=
    ⟨g.val.push #[], by
      rw [Array.size_push]
      apply Nat.le_step
      exact g.property
    ⟩
  theorem add_grows_by_one : h = addNode g → g.val.size + 1 = h.val.size := by
    intro hip
    cases g with
    | mk adj prop =>
    cases h with
    | mk nadj nprop =>
      rw [addNode] at hip
      have heq: nadj = adj.push #[] := by
        simp at hip
        sorry
      simp
      rw [heq]
      simp

Right before the sorry, when trying to prove the subgoal heq, the proof state is as follows:

u : ℕ
adj : Array (Array (Fin u))
prop : u ≤ adj.size
nadj : Array (Array (Fin u))
nprop : u ≤ nadj.size
hip : ⟨nadj, nprop⟩ = ⟨adj.push #[], ⋯⟩
⊢ nadj = adj.push #[]

I cannot figure out how to extract the first term from the hip identity to prove this subgoal.
I also got no luck with apply?. What am I missing?

I know this is a basic question, but any help is appreciated, thanks!

[Aaron Liu]

Try using docs#congrArg or the congr() syntax

[Aaron Liu]

I think exact congrArg Subtype.val hip should close your goal.

[Aaron Liu]

cases hip should also work

[Hugo Sales Corrêa]

Solved! Thank you!