Library seq

Basic properties of the concatenation of programs app_prog.

Require Export prog.

Lemma seq_assoc : ∀ p q r,
  p +;+ q +;+ r = (p +;+ q ) +;+ r.
Proof.
  intros. induction p.
  + reflexivity.
  + simpl. rewrite IHp. reflexivity.
Qed.

Lemma seq_nil_l : ∀ p,
  {{}} +;+ p = p.
Proof.
  intros; trivial.
Qed.

Lemma seq_nil_r : ∀ p,
  p +;+ {{}} = p.
Proof. intros; induction p.
  + reflexivity.
  + simpl. rewrite IHp. reflexivity.
Qed.

Lemma app_prog_cons : ∀ s p1 p2,
  (s ;;p1 )+;+p2 = s ;;p1 +;+p2.
Proof.
  intros. reflexivity.
Qed.