making coersions

Stream: new members

[Paul Rowe]

I have a situation where I want to extend a structure with an additional proof that its partial function is in fact total. I don't want to create a whole new structure because I want to view it as an instance of the more general structure and use all the existing definitions for it.

structure process_model (C S : Type) :=
(P : C → C → Prop)
(c0 : C)
(O : C → option S)
(T : S → S → Prop)
(compat : (transfer P O) = T)

structure gt_process_model (C S : Type) extends process_model C S :=
(total : ∀ c, ∃ s, O c = s)

def incorrect (K : process_model C S) (R : gt_process_model C S) : Prop :=
(∃ s, m_reach_state K s ∧ ¬(@m_reach_state R s))

The problem with the above is that R is of the wrong type in the final definition. I could explicitly define the coersion that forgets the totality of O, but I don't have a good grasp for how coersions work.

If I declare gt_process_model as an instance of process_model Lean complains that process_model is not a class (obviously true). But when I simply declare it as a class, all sorts of other definitions start breaking. What do I need to do to get Lean to let me write something like

def incorrect (K : process_model C S) (R : gt_process_model C S) : Prop :=
(∃ s, m_reach_state K s ∧ ¬(@m_reach_state ↑R s))

[Paul Rowe]

Ok, I figured something out. It works if I define an instance of has_lift_t as follows:

instance gtpm_lift (C S : Type) :
has_lift_t (gt_process_model C S) (process_model C S) :=
⟨λ R, {P := R.P, c0 := R.c0, O := R.O, T := R.T, compat := R.compat }⟩

Type class inference needs a little help my final definition, but it works once I explicitly elaborate the types:

def incorrect (K : process_model C S) (R : gt_process_model C S) : Prop :=
(∃ s, m_reach_state K s ∧ ¬(@m_reach_state C S ↑R s))

[Kyle Miller]

Paul Rowe said:

instance gtpm_lift (C S : Type) :
has_lift_t (gt_process_model C S) (process_model C S) :=
⟨gt_process_model.to_process_model⟩

I can't check it right now, but you could probably use coercion function that extends defines for you here.

[Paul Rowe]

Would that be R.to_process_model in this case? Is there a less verbose notation? I am starting to run into problems with my approach. Lean seems to be getting confused about the access functions. Or rather, I'm the one who's confused and I can't figure out what Lean wants me to think. :)

Edit: using R.to_process_model looks promising so far. But it's so clunky to type and read. That's why I'm looking for a slicker notation.

[Kyle Miller]

It can be a bit of a surprise that all extends does for structures is to create a totally new type that happens to also include the fields of the original structure (while defining a to_X function to cast it to the supertype). You might need to define a bunch of lemmas (which you can mark with @[simp]) to rewrite access functions on the gt_process_model to ones on the to_process_model version to keep confusion under control.

(The extends keyword seems to work in a slightly different way for classes, since it seems to define an instance for you, too.)

[Kyle Miller]

I'm not sure what the best way of dealing with this is -- it's just something I might try if I wanted to use extends for structures.

[Paul Rowe]

Thanks. That helps me a lot. It does seem like a shame that it's not somehow simpler all around. I'll have to play around more with classes and instances to see what mode works best for me.

I appreciate the help!

[Kyle Miller]

I think the issue is that type inference in the presence of subtype relationships for records ends up being tricky, so Lean doesn't support it, but I'm not sure what the problem is exactly.