Library prefix

Require Export List. Export ListNotations.
Require Export prog.
Require Import seq.

Inductive prefix {A} : list A → list A → Prop :=
  | PR_nil : ∀ l, prefix [] l
  | PR_after : ∀ l1 l2 x, prefix l1 l2 → prefix (x::l1) (x::l2).

Lemma prefix_refl : ∀ A (l:list A),
  prefix l l.
Proof.
  intros. induction l. apply PR_nil.
  apply PR_after. exact IHl.
Qed.

Lemma prefix_irrefl : ∀ A (l1 l2:list A),
  prefix l1 l2 → prefix l2 l1 → l1 = l2.
Proof.
  intros.
  induction H as [l | l1' l2' x]. inversion H0. reflexivity.
  inversion H0. rewrite IHprefix. reflexivity. assumption.
Qed.

Lemma prefix_trans : ∀ A (l1 l2 l3:list A),
  prefix l1 l2 → prefix l2 l3 → prefix l1 l3.
Proof.
  intros. revert l1 H.
  induction H0; intros.
  - inversion H. apply PR_nil.
  - inversion H. apply PR_nil. apply PR_after. apply IHprefix; assumption.
Qed.

Lemma prefix_length : ∀ {A} (l1 l2 : list A),
  prefix l1 l2 → length l1 ≤ length l2.
Proof.
  intros. induction H.
  - apply le_0_n.
  - simpl. apply le_n_S. assumption.
Qed.

Lemma prefix_single : ∀ A x (l1 l2 : list A),
  prefix (x::l1) (x::l2) ↔ prefix l1 l2.
Proof.
  split; intros.
  - inversion H. assumption.
  - apply PR_after. assumption.
Qed.

Inductive prefix_prog : prog → prog → Prop :=
  | PP_nil : ∀ p, prefix_prog {{}} p
  | PP_after : ∀ p1 p2 s, prefix_prog p1 p2 → prefix_prog (s;;p1) (s;;p2).

Lemma prefix_prog_refl : ∀ p,
  prefix_prog p p.
Proof.
  intros. induction p. apply PP_nil.
  apply PP_after. exact IHp.
Qed.

Lemma prefix_prog_irrefl : ∀ p1 p2,
  prefix_prog p1 p2 → prefix_prog p2 p1 → p1 = p2.
Proof.
  intros.
  induction H as [p | p1' p2' s]. inversion H0. reflexivity.
  inversion H0. rewrite IHprefix_prog. reflexivity. assumption.
Qed.

Lemma prefix_prog_trans : ∀ p1 p2 p3,
  prefix_prog p1 p2 → prefix_prog p2 p3 → prefix_prog p1 p3.
Proof.
  intros. revert p1 H.
  induction H0; intros.
  - inversion H. apply PP_nil.
  - inversion H. apply PP_nil. apply PP_after. apply IHprefix_prog; assumption.
Qed.

Lemma prefix_prog_single : ∀ p1 p2 s,
  prefix_prog (s;;p1) (s;;p2) ↔ prefix_prog p1 p2.
Proof.
  split; intros.
  - inversion H. assumption.
  - apply PP_after. assumption.
Qed.

Lemma prefix_prog_app : ∀ p q,
  prefix_prog p (p+;+q).
Proof.
  intros. induction p.
  - apply PP_nil.
  - simpl. apply PP_after. assumption.
Qed.

Lemma prefix_prog_intro : ∀ p q,
  prefix_prog p q ↔ ∃ r, q = p +;+ r.
Proof.
  split; intros.
  - induction H.
    + ∃ p. reflexivity.
    + inversion IHprefix_prog as [r H0].
      ∃ r. simpl. rewrite <- H0. reflexivity.
  - inversion H as [r H0]. rewrite H0. apply prefix_prog_app.
Qed.