Library GCSyntax

Syntax of GC

The syntax of GC is described by a nested inductive type, for which there is little built-in support in Coq. We manually derive an induction principle for GC and show that equality on GC terms is decidable.
Require Import Facts States.
Set Implicit Arguments.

Module GCSyntax (Sigma : State).
Export Sigma.


Inductive cmd :=
| Skip
| Assn (a : action)
| Seq (s t : cmd)
| Case (G : seq (guard × cmd))
| Do (G : seq (guard × cmd)).
Definition gc := seq (guard × cmd).

Induction Principle

Section GCInduction.
Variables (P : cmdProp) (Q : gcProp).

Hypothesis p_skip : P Skip.
Hypothesis p_assn : a, P (Assn a).
Hypothesis p_seq : s t, P sP tP (Seq s t).
Hypothesis p_case : G, Q GP (Case G).
Hypothesis p_do : G, Q GP (Do G).

Hypothesis q_nil : Q [::].
Hypothesis q_cons : b s G, P sQ GQ ((b,s) :: G).

Definition gc_ind´ (F : s, P s) : G, Q G :=
  fix rec G := match G return Q G with
  | [::]q_nil
  | (b,s) :: Gq_cons b (F s) (rec G)

Fixpoint cmd_ind (s : cmd) : P s :=
  match s with
  | Skipp_skip
  | Assn ep_assn e
  | Seq s tp_seq (cmd_ind s) (cmd_ind t)
  | Case Gp_case (gc_ind´ cmd_ind G)
  | Do Gp_do (gc_ind´ cmd_ind G)

Definition gc_ind : ( s, P s) ( G, Q G) :=
  conj cmd_ind (gc_ind´ cmd_ind).

End GCInduction.

Decidable equality on terms

Section CmdEqType.

Definition all2 {T} (e : TTbool) := fix rec (xs ys : seq T) : bool :=
  match xs, ys with
  | x :: xr, y :: yre x y && rec xr yr
  | [::], [::]true
  | _, _false

Fixpoint cmd_eq (s t : cmd) : bool :=
  match s, t with
  | Assn e1, Assn e2 ⇒ (e1 == e2)
  | Skip, Skiptrue
  | Seq s1 s2, Seq t1 t2cmd_eq s1 t1 && cmd_eq s2 t2
  | Case G1, Case G2
  | Do G1, Do G2all2 (fun p q(p.1 == q.1) && cmd_eq p.2 q.2) G1 G2
  | _, _false

Lemma all2P T (e : TTbool) :
  ( x y, reflect (x = y) (e x y)) →
  ( xs ys, reflect (xs = ys) (all2 e xs ys)).

Lemma injP T1 T2 (f : T1T2) x y b :
  injective freflect (x = y) breflect (f x = f y) b.

Lemma cmd_eqP :
  Equality.axiom cmd_eq.

Canonical cmd_eqMixin := EqMixin cmd_eqP.
Canonical cmd_eqType := Eval hnf in EqType cmd cmd_eqMixin.

End CmdEqType.

End GCSyntax.