HyPre.util.PrefixExt

From HyPre Require Export
  PreSuffix
  Safety
  VectorExtra.

Export Veclist.

Section with_X.
  Context {X : Type}.

  Definition partial_prefix {k : nat} (v v' : Vector.t (list X) k) : Prop
    := exists i, v [[i]] = v' [[i]] /\ veclist_prefix v v'.

  Definition prefix_ext {k : nat} (P : Vector.t (list X) k -> Prop) : Vector.t (list X) k -> Prop
    := (fun xt => exists yt, partial_prefix yt xt).

  Definition prefix_ext2 (P : list X -> list X -> Prop) : list X -> list X -> Prop
    := fun xl yl => (exists xl', prefix xl' xl /\ P xl' yl)
                 \/ (exists yl', prefix yl' yl /\ P xl yl').

  Lemma prefix_ext2_twice (P : list X -> list X -> Prop)
    : P nil nil -> forall x y, prefix_ext2 (prefix_ext2 P) x y.
  Proof.
    intros.
    left.
    exists nil.
    split.
    - eapply prefix_nil.
    - right.
      exists nil.
      split.
      + eapply prefix_nil.
      + assumption.
  Qed.

End with_X.