The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 09/17/2011 03:12 PM, 
ldou AT cs.ecnu.edu.cn
 wrote:

>     i'm using Coq to formalize the Sequence Diagram. The following inductive
> type of sequence diagram has been defined:
>    Then i want to define "context" in Coq. According to our concept, a
> context is a sequence diagram with one of its fragment replaced by a special
> symbol x, just like term rewriting. how should i define "context"? any
> suggestions are appreciated.

Pierre's second solution is good, but here is another that I use all
the time to do Wright-Felleisen-style reduction semantics.

A context is just a Coq function:

Definition context : Set := seqDiag -> seqDiag.

... further constrained by the "iscontext" inductive predicate:

Inductive iscontext: context -> Prop :=
  | iscontext_hole:
      iscontext (fun x => x)
  | iscontext_strict_l: forall C s,
      iscontext C -> iscontext (fun x => DStrict (C x) s)
  | iscontext_strict_r: forall s C,
      iscontext C -> iscontext (fun x => DStrict s (C x))
  | iscontext_par_l: forall C s,
      iscontext C -> iscontext (fun x => DPar (C x) s)
  | iscontext_par_r: forall s C,
      iscontext C -> iscontext (fun x => DPar s (C x))
  | iscontext_seq_l: forall C s,
      iscontext C -> iscontext (fun x => DSeq (C x) s)
  | iscontext_seq_r: forall s C,
      iscontext C -> iscontext (fun x => DSeq s (C x)).

In this approach, "filling the hole" (Pierre's "fill d C" function) is
just Coq's function application "C d".  It also makes it slightly easier
to compose contexts, shall you ever need to do that.

Hope this helps,

- Xavier Leroy