Serializing Prop-valued fields in Lean structures

Stream: new members

[Nicholas Phair]

Hi all,

I’m using Lean to model parts of a software system. I have stateful components with specifications that describe how they relate to each other, and each component has state-transforming actions with pre- and postconditions to describe their intended behavior - though these pre/postconditions won’t necessarily be proven within Lean itself.

What I’d like to do is serialize these specifications (including the Prop-valued pre/post conditions) so that they can be exported - for example, as JSON - and potentially used in an external tool or even as input to an LLM for refinement.

Here’s a simplified version and example of what one of what these definitions looks like:

structure Action where
  name           : String
  argTypes    : Signature
  retTipe        : Tipe
  stateTypes : Signature
  pre  : Valuation argTypes → Valuation stateTypes → Prop
  post : (st st' : Valuation stateTypes) → (sg : Valuation argTypes) → interpTipe retTipe → Prop

def turnOn : Action := {
  name := "turnOn"
  argTypes := Signature.empty
  retTipe := Tipe.unit
  -- Assume the action’s state includes two boolean fields:
  --   isOn      : Tipe.bool
  --   isPowered : Tipe.bool
  stateTypes := stateSpace
  pre := fun _ _ => True
  -- st is the input state, st' is the output state
  post := fun st st' _ _ =>
    st' stateSpace.isOn = true ∧
    st' stateSpace.isPowered = st stateSpace.isPowered
}

As far as I understand, types and proofs don’t have runtime representations, so I’d probably need to use meta-programming to extract these Prop fields.

Has anyone done something similar or can suggest how/if we can serialize Prop fields like this?

Thanks!
Nick

[Aaron Liu]

Why do these conditions need to be Prop

[Nicholas Phair]

In this example they may not need to be. We have a version that avoids them. But in the general case I think it would be useful to be able to dump some representation of a Prop. It would be good context to a human, or llm, who may want to generate code for this.

[Aaron Liu]

then you can't do it at runtime since they have no runtime representation

[Aaron Liu]

and Props don't really have a "normal form" either so if I give you a Prop how do you decide how to print it

[Nicholas Phair]

I see, I thought that might be the case, thank you.

I suppose you might you be able to get something printable using Lean.PrettyPrinter.ppExpr. There would be constraints here (e.g., the expression would have to be constant).

[Nicholas Phair]

And without a clear "normal form" the output would vary a lot.