Library prog

Based on some ideas and some code of tutorial on Coq by Pierce and al. Software Foundations. The license of the software is not strict, but the license must be included, cf. SF-LICENSE.

This file defines the language used, namely arithmetic expressions aexp, boolean expressions bexp, statements stmt and programs prog.

Require Export sflib.

Inductive id : Type :=
  Id : nat → id.

Lemma eq_id_dec : ∀ (i1 i2:id),
  {i1 = i2 } + {i1 ≠ i2 }.
Proof.
  intros. destruct i1, i2.
  destruct (Nat.eq_dec n n0).
  left; subst; reflexivity.
  right. injection. assumption.
Defined.

Inductive aexp : Type :=
  | A_num : nat → aexp
  | A_id : id → aexp
  | A_plus : aexp → aexp → aexp
  | A_minus : aexp → aexp → aexp
  | A_mult : aexp → aexp → aexp.

Tactic Notation "aexp_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "A_num" | Case_aux c "A_id" | Case_aux c "A_plus"
  | Case_aux c "A_minus" | Case_aux c "A_mult" ].

Inductive id_inR_aexp : aexp → id → Prop :=
  | IIA_id : ∀ i, id_inR_aexp (A_id i) i
  | IIA_plus_l : ∀ i, ∀ a1 a2, id_inR_aexp a1 i →
      id_inR_aexp (A_plus a1 a2) i
  | IIA_plus_r : ∀ i, ∀ a1 a2, id_inR_aexp a2 i →
      id_inR_aexp (A_plus a1 a2) i
  | IIA_minus_l : ∀ i, ∀ a1 a2, id_inR_aexp a1 i →
      id_inR_aexp (A_minus a1 a2) i
  | IIA_minus_r : ∀ i, ∀ a1 a2, id_inR_aexp a2 i →
      id_inR_aexp (A_minus a1 a2) i
  | IIA_mult_l : ∀ i, ∀ a1 a2, id_inR_aexp a1 i →
      id_inR_aexp (A_mult a1 a2) i
  | IIA_mult_r : ∀ i, ∀ a1 a2, id_inR_aexp a2 i →
      id_inR_aexp (A_mult a1 a2) i.

Inductive bexp : Type :=
  | B_true : bexp
  | B_false : bexp
  | B_eq : aexp → aexp → bexp
  | B_le : aexp → aexp → bexp
  | B_not : bexp → bexp
  | B_and : bexp → bexp → bexp.

Tactic Notation "bexp_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "B_true" | Case_aux c "B_false" | Case_aux c "B_eq"
  | Case_aux c "B_le" | Case_aux c "B_not" | Case_aux c "B_and" ].

Inductive id_inR_bexp : bexp → id → Prop :=
  | IIB_eq_l : ∀ a1 a2 i, id_inR_aexp a1 i → id_inR_bexp (B_eq a1 a2) i
  | IIB_eq_r : ∀ a1 a2 i, id_inR_aexp a2 i → id_inR_bexp (B_eq a1 a2) i
  | IIB_le_l : ∀ a1 a2 i, id_inR_aexp a1 i → id_inR_bexp (B_le a1 a2) i
  | IIB_le_r : ∀ a1 a2 i, id_inR_aexp a2 i → id_inR_bexp (B_le a1 a2) i
  | IIB_not : ∀ b i, id_inR_bexp b i → id_inR_bexp (B_not b) i
  | IIB_and_l : ∀ b1 b2 i, id_inR_bexp b1 i → id_inR_bexp (B_and b1 b2) i
  | IIB_and_r : ∀ b1 b2 i, id_inR_bexp b2 i → id_inR_bexp (B_and b1 b2) i.

Definition label := nat.

Inductive prog : Type :=
  | P_nil : prog
  | P_cons : stmt → prog → prog
with stmt :=
  | S_skip : label → stmt
  | S_ass : label → id → aexp → stmt
  | S_if : label → bexp → prog → prog → stmt
  | S_while : label → bexp → prog → stmt
  | S_assert : label → bexp → label → stmt.

Scheme prog_mutual_ind := Induction for prog Sort Prop
  with stmt_mutual_ind := Induction for stmt Sort Prop.

Scheme prog_mutual_rect := Induction for prog Sort Type
  with stmt_mutual_rect := Induction for stmt Sort Type.

Tactic Notation "prog_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "P_nil" | Case_aux c "P_cons" | Case_aux c "S_skip"
  | Case_aux c "S_ass" | Case_aux c "S_ifb" | Case_aux c "S_while"
  | Case_aux c "S_assert" ].

Notation "'SKIP' << l >>" :=
  (S_skip l) (at level 60).
Notation "x '::=' a << l >>" :=
  (S_ass l x a) (at level 60).
Notation "'WHILE' << l >> b 'DO' c 'END'" :=
  (S_while l b c) (at level 80, right associativity).
Notation "'IFB' << l >> b 'THEN' c2 'ELSE' c3 'FI'" :=
  (S_if l b c2 c3) (at level 80, right associativity).
Notation "'ASSERT' << l >> b =>> l1" :=
  (S_assert l b l1) (at level 80, right associativity).

Notation "s ;; p" := (P_cons s p)
                     (at level 60, right associativity).
Notation "{{ }}" := P_nil.
Notation "{{ p ; .. ; q }}" := (P_cons p .. (P_cons q {{}}) ..).

Fixpoint app_prog (p1 p2 : prog) :=
  match p1 with
  | {{}} ⇒ p2
  | s;;p ⇒ s;;(app_prog p p2 )
  end.

Notation "x +;+ y" := (app_prog x y)
                      (right associativity, at level 60).