# Syntax of GCP

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 base wp.states.

## Syntax

Unset Elimination Schemes.
Inductive cmd :=
| Skip
| Assn (a : action)
| Seq (s t : cmd)
| Case (G : seq (guard * cmd))
| Do (G : seq (guard * cmd)).
Set Elimination Schemes.

Definition gc := seq (guard * cmd).

## Induction Principle

Section GCInduction.
Variables (P : cmd -> Prop) (Q : gc -> Prop).

Hypothesis p_skip : P Skip.
Hypothesis p_assn : forall a, P (Assn a).
Hypothesis p_seq : forall s t, P s -> P t -> P (Seq s t).
Hypothesis p_case : forall G, Q G -> P (Case G).
Hypothesis p_do : forall G, Q G -> P (Do G).

Hypothesis q_nil : Q [::].
Hypothesis q_cons : forall b s G, P s -> Q G -> Q ((b,s) :: G).

Definition gc_ind' (F : forall s, P s) : forall G, Q G :=
fix rec G := match G return Q G with
| [::] => q_nil
| (b,s) :: G => q_cons b (F s) (rec G)
end.

Fixpoint cmd_ind' (s : cmd) : P s :=
match s with
| Skip => p_skip
| Assn e => p_assn e
| Seq s t => p_seq (cmd_ind' s) (cmd_ind' t)
| Case G => p_case (gc_ind' cmd_ind' G)
| Do G => p_do (gc_ind' cmd_ind' G)
end.

Definition gc_ind : (forall s, P s) /\ (forall G, Q G) :=
conj cmd_ind' (gc_ind' cmd_ind').

End GCInduction.

## Decidable equality on terms

Section CmdEqType.

Definition all2 {T} (e : T -> T -> bool) := fix rec (xs ys : seq T) : bool :=
match xs, ys with
| x :: xr, y :: yr => e x y && rec xr yr
| [::], [::] => true
| _, _ => false
end.

Fixpoint cmd_eq (s t : cmd) : bool :=
match s, t with
| Assn e1, Assn e2 => (e1 == e2)
| Skip, Skip => true
| Seq s1 s2, Seq t1 t2 => cmd_eq s1 t1 && cmd_eq s2 t2
| Case G1, Case G2
| Do G1, Do G2 => all2 (fun (p q : guard * cmd) => (p.1 == q.1) && cmd_eq p.2 q.2) G1 G2
| _, _ => false
end.

Lemma all2P T (e : T -> T -> bool) :
(forall x y, reflect (x = y) (e x y)) ->
(forall xs ys, reflect (xs = ys) (all2 e xs ys)).
Proof.
move => r. elim=> [|x xr ih] [|y yr];
by apply: (iffP idP) => //=[/andP|] -[/r->/ih->].
Defined.

Lemma injP T1 T2 (f : T1 -> T2) x y b :
injective f -> reflect (x = y) b -> reflect (f x = f y) b.
Proof. move=> i r. by apply: iffP r _ _ => [->|/i->]. Qed.

Lemma cmd_eqP :
Equality.axiom cmd_eq.
Proof.
hnf; fix ih 1 => -[|a1|s1 s2|G1|G1] [|a2|t1 t2|G2|G2] /=;
exact: (iffP idP) || (apply: injP eqP => x y [] //) ||
(apply: iffP andP _ _ => -[/ih->/ih->] //) ||
apply: injP => [x y []//|]; apply: all2P => -[a1 b1][a2 b2]/=;
by apply: (iffP idP) => [/andP|] [/eqP->/ih->].
Qed.

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

End CmdEqType.

## Specialized induction principle

Section CmdInduction.

Variables (P : cmd -> Prop).

Implicit Types (s t : cmd) (G : gc) (b : guard).

Hypothesis p_skip : P Skip.
Hypothesis p_assn : forall a, P (Assn a).
Hypothesis p_seq : forall s t, P s -> P t -> P (Seq s t).
Hypothesis p_case : forall G, (forall b s, (b,s) \in G -> P s) -> P (Case G).
Hypothesis p_do : forall G, (forall b s, (b,s) \in G -> P s) -> P (Do G).

Lemma cmd_ind : forall s, P s.
Proof.
suff: (forall s, P s) /\ (forall G b s, (b,s) \in G -> P s) => [[//]|].
apply: gc_ind => // b s G ihs ihG b' s'.
rewrite inE => /orP[/eqP[_ ->//]|]. exact: ihG.
Qed.

End CmdInduction.