Zulip Chat Archive

Stream: lean4

Topic: computed/cached fields


Chris B (Feb 25 2022 at 18:51):

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 (Feb 25 2022 at 19:51):

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 (Feb 25 2022 at 19:51):

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

Chris B (Feb 26 2022 at 02:13):

@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 (Feb 28 2022 at 13:43):

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

Chris B (Feb 28 2022 at 15:10):

Ok, thank you.


Last updated: Dec 20 2023 at 11:08 UTC