computed/cached fields

Stream: lean4

[Chris B]

Sometimes it would be nice to compute and effectively cache a value that's derived from a structure's earlier fields. In the past I've broken up the structure like this:

structure S where
  a : A
  b : B

def S.def1 : S -> C := ..
def S.def2 : S -> D := ..

structure WellFormedS extends S where
  c : C
  d : D
  hc : c = toS.def1
  hd : d = toS.def2

But this can be cumbersome if you have more than one stage you want to go through. Writing an alternate constructor that requires c and d to be defined properly is another way to do it, but you don't end up having the equalities on hand without some extra plumbing, and having c : Option C, where def1 caches the value has sort of the same issue, and def1 isn't visible to the structure definition, so you can't restrict the type of C.

If anyone's worked with alternate solutions to this kind of thing and has thoughts on better/worse ways to go about this, I would appreciate your insights.

[Gabriel Ebner]

I've been using this:

instance [Hashable α] (p : α → Prop) : Hashable (Subtype p) where
  hash x := hash x.1

def Cached {α : Type _} (a : α) := { b // b = a }

instance {a : α} : DecidableEq (Cached a) :=
  fun ⟨x, hx⟩ ⟨y, hy⟩ => Decidable.isTrue (by cases hx; cases hy; rfl)

instance {a : α} : Hashable (Cached a) where
  hash x := 0

instance {a : α} : Repr (Cached a) where
  reprPrec x := Repr.addAppParen "cached _"

instance {a : α} : Subsingleton (Cached a) :=
  ⟨by intro ⟨x, h⟩; cases h; intro ⟨y, h⟩; cases h; rfl⟩

instance {a : α} : CoeHead (Cached a) α where
  coe x := x.1

def cached (a : α) : Cached a :=
  ⟨a, rfl⟩

instance {a : α} : Inhabited (Cached a) where
  default := cached a

@[simp] theorem cached_val (a : α) (b : Cached a) : (b : α) = a := b.2

[Gabriel Ebner]

You can then just write c := cached (... a ... b).

[Chris B]

@Gabriel Ebner That's a good idea, thanks for your input. Is there a rule of thumb to determine when/whether a declaration like this will be kept alive/cached in a compiled Lean program?

[Gabriel Ebner]

You need to manually pass the cached fields around, if you don't do that it will be recomputed.

[Chris B]

Ok, thank you.