tactics for unfolding parameters defined in structure

Stream: metaprogramming / tactics

[Bach Hoang]

Hi,

I have a question about how to unfold the parameters that is already defined in the structure. Right now I have a type that is built by structure as follow :

structure State where
  labels     : String
  val_labels : List String
  typeMap    : List (String × Type)
  type       : String → Type := fun s =>
    match typeMap.find? (fun p => p.fst = s) with
    | some (_, ty) => ty
    | none => Unit
  val        : List ((s : String) × type s)
  lemma_1    : ∀ x ∈ val, ∃ y ∈ typeMap, x.fst = y.fst
  lemma_2    : ∀ x ∈ typeMap, ∃ y ∈ val, x.fst = y.fst

And right now, I have a result that I need to prove, similar to below

theorem result (X : State) (name : String) : X.type name = Unit := by sorry

, which will require me to unfold the function "type" in State type. But I have tried multiple tactics, including simp, unfold, delta, and they does not reveal the "type" function inside State.

Can you suggest what should I do to resolve this problem ? Thanks

[Aaron Liu]

You can set the type field to whatever you want, it doesn't have to be what you put down

[Aaron Liu]

For example here I override the default value with my own implementation

example : State where
  labels := "dummy_labels"
  val_labels := ["label_zero", "label_one"]
  typeMap := [("type_zero", Nat), ("type_one", Int × Bool), ("type_two", Unit)]
  type := fun _ => Nat
  val := [⟨"type_zero", 17⟩, ⟨"type_two", 8⟩, ⟨"type_one", 777⟩, ⟨"type_one", 42⟩]
  lemma_1 := by decide
  lemma_2 := by decide

[Kyle Miller]

What you need is a feature that doesn't exist, but I hope it will at some point since many people tend to get confused about default values, and there's good reason to be able to define some fields while defining others.

This is what the not-yet-existing feature would look like:

structure State where
  labels     : String
  val_labels : List String
  typeMap    : List (String × Type)
  let type   : String → Type := fun s =>
    match typeMap.find? (fun p => p.fst = s) with
    | some (_, ty) => ty
    | none => Unit
  val        : List ((s : String) × type s)
  lemma_1    : ∀ x ∈ val, ∃ y ∈ typeMap, x.fst = y.fst
  lemma_2    : ∀ x ∈ typeMap, ∃ y ∈ val, x.fst = y.fst

[Kyle Miller]

It's possible to simulate this by breaking the structure definition into two:

structure PreState where
  labels     : String
  val_labels : List String
  typeMap    : List (String × Type)

def PreState.type (st : PreState) (s : String) : Type :=
  match st.typeMap.find? (fun p => p.fst = s) with
  | some (_, ty) => ty
  | none => Unit

structure State extends PreState where
  val        : List ((s : String) × toPreState.type s)
  lemma_1    : ∀ x ∈ val, ∃ y ∈ typeMap, x.fst = y.fst
  lemma_2    : ∀ x ∈ typeMap, ∃ y ∈ val, x.fst = y.fst