Referring to the data declaration in the proof of a subtype

Stream: new members

[Oleks]

I am trying to define a DAG as a subtype of a homebrewed directed graph implementation (as an exercise to learn Lean):

abbrev NodeId := Nat

deriving
  instance
    BEq, Hashable, Repr
  for
    NodeId

structure DirectedGraph where
  nodes : Std.HashMap NodeId (List NodeId)

def childRel (dg : DirectedGraph) : NodeId → NodeId → Prop :=
  λ parent child => match dg.nodes[parent]? with
  | some children => child ∈ children
  | none => false

def descendantRel (dg : DirectedGraph) : NodeId → NodeId → Prop :=
  Relation.TransGen (childRel dg)

def acyclic (dg : DirectedGraph) : Prop :=
  ∀ n, ¬descendantRel dg n n

structure DirectedAcyclicGraph extends DirectedGraph where
  acyclic {this} : acyclic this

However, when I go on to implement an empty function, I fail to see how I can leverage the fact that nodes is an empty HashMap in the proof of acyclic:

def empty : DirectedAcyclicGraph :=
  { nodes := Std.HashMap.emptyWithCapacity,
    acyclic := by
      intro g
      have h_nodes_empty : g.nodes = Std.HashMap.emptyWithCapacity := by
        rfl
        /-- error:
        tactic 'rfl' failed, the left-hand side
          g.nodes
        is not definitionally equal to the right-hand side
          Std.HashMap.emptyWithCapacity
        --/
}

[Kyle Miller]

When you write acyclic {this} : acyclic this, this does not refer to the structure being defined, you accidentally have "all directed graphs are acyclic"

[Kyle Miller]

Hover over the acyclic field in the structure to see what type it has

[Kyle Miller]

It's possible to refer to the parent using the projection field for that parent. The default name puts to in front:

structure DirectedAcyclicGraph extends DirectedGraph where
  acyclic : acyclic toDirectedGraph

[Kyle Miller]

You can see it in the local context.