Require Import Facts States.
Set Implicit Arguments.
Unset Strict Implicit.

Module GCSyntax (Sigma : State).
Export Sigma.

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).

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

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

Hypothesis q_nil : Q [::].
Hypothesis q_cons : ∀ b s G, P s → Q G → Q ((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) :: 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 : (∀ s, P s) ∧ (∀ G, Q G) :=
  conj cmd_ind (gc_ind´ cmd_ind).

End GCInduction.

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 ⇒ (p.1 == q.1) && cmd_eq p.2 q.2) G1 G2
  | _, _ ⇒ false
  end.

Lemma all2P T (e : T → T → bool) :
  (∀ x y, reflect (x = y) (e x y)) →
  (∀ 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.

End GCSyntax.