Data.Fix and a tricky termination proof

Stream: general

[Harry Goldstein]

a Hi all. I'm playing around with a way to encode Fix for types. (I see Mathlib has Fix, but I don't think that'd work if I wanted to actually run the fixed point? I want something like Data.Fix in Haskell.) I have the following so far, which seems like it should be a good start, but there are a couple of issues:

class DataFix (fixF : Type) where
  f : Type → Type
  instFunctorF : Functor f
  instMembershipF : Membership fixF (f fixF)
  unfoldStep : fixF → f fixF
  foldStep : f fixF → fixF

def DataFix.base (fixF : Type) [DataFix fixF] : Type → Type := DataFix.f fixF

instance DataFix.instFunctorBase [DataFix fixF] : Functor (base fixF) := DataFix.instFunctorF

class LawfulDataFix (fixF : Type) extends DataFix fixF where
  unfoldStep_foldStep_id : Function.LeftInverse foldStep unfoldStep
  foldStep_unfoldStep_id : Function.RightInverse foldStep unfoldStep
  unfoldStep_size : x ∈ unfoldStep y → sizeOf x < sizeOf y

def DataFix.fold [LawfulDataFix fixF] (alg : base fixF β → β) (x : fixF) : β :=
  (alg ∘ Functor.map (fold alg) ∘ unfoldStep) x
termination_by sizeOf x
decreasing_by
  -- apply LawfulDataFix.unfoldStep_size
  sorry

The first issue is that I'm not sure about the best way to say "when you call Functor.map on this, everything you find will be smaller" — I'm currently encoding it with Membership but I doubt that's correct. But there's also a more basic issue, which is that I don't actually know how to access my assumptions about fixF in the decreasing_by proof. Any advice, either about the mechanics or about the broader modeling question, would be much appreciated.

EDIT: I managed to get it to work with PFunctor, which makes a lot of sense in retrospect.