RIS.subword: the subword ordering on words.

Set Implicit Arguments.

Require Import tools.

Section subword.
  Context {A : Set}.

  Reserved Notation " u ⊑ v " (at level 80).

  Fixpoint subword (u v : list A) :=
    match u with
    | [] ⇒ True
    | a::u ⇒ match v with
             | [] ⇒ False
             | b::v ⇒ (a = b ∧ u ⊑ v) ∨ (a::u ⊑ v)
             end
    end
  where " u ⊑ v " := (subword u v).

  Global Instance subword_cons_Proper a :
    Proper (subword ==> subword) (cons a).

  Global Instance subword_PreOrder : PreOrder subword.

  Lemma subword_length u v : u ⊑ v → ⎢u⎥ ≤ ⎢v⎥.

  Global Instance subword_leq_length : Proper (subword ==> le) (@length A).

  Global Instance subword_PartialOrder : PartialOrder eq subword.

  Lemma subword_app_r u v : v ⊑ u++v.

  Global Instance subword_app : Proper (subword ==> subword ==> subword) (@app A).

  Lemma subword_nil u : [] ⊑ u.
  Lemma subword_cons u a : u ⊑ a::u.

End subword.
Infix " ⊑ " := subword (at level 80).