Dependent pattern matching and specializing a function

Using Coq
1

I have the following constructor:

PInput
  : ∀ {m : MType} {c : SType}
  , (Message  m → Message (Channel c) → Process)
  → Message (Channel (Receive m c))
  → Process

How can I pattern match on m, and depending on the case, get a specialized (Message m → Message (Channel c) → Process)?

Thank you!

2

Use an annotation on the match to get the return type you want. This is the convoy pattern. Something like

Definition PInput : ∀ {m : MType} {c : SType},
  (Message  m → Message (Channel c) → Process)
  → Message (Channel (Receive m c))
  → Process :=
  match m as m' return (Message m' -> Message (Channel c) -> Process) -> Message (Channel (Receive m' c)) -> Process with
  | (* constructor *) => fun f M -> (* do something with f and M to get a Process *)
  | (* ... *) => fun f M -> (* ... *)
  end.

Here we’ve used the convoy pattern to refine the types of both arguments to the function, since both of their types were dependent on m.

1 Like
3

Thank you! I think I’m finally getting my head around dependent pattern matching in Coq :slight_smile: