Library ConCert.Execution.ChainedList

(* This file implements a 'chained list'. This can essentially be
thought of as the proof-relevant transitive reflexive closure of
a relation. That is, each link (element) has a "from" point that
must match the previous element's "to" point. *)
From ConCert.Utils Require Import Automation.
Section ChainedList.
  Context {Point : Type} {Link : Point -> Point -> Type}.

  Inductive ChainedList : Point -> Point -> Type :=
    | clnil : forall {p}, ChainedList p p
    | snoc : forall {from mid to},
        ChainedList from mid -> Link mid to -> ChainedList from to.

  Fixpoint clist_app
            {from mid to}
            (xs : ChainedList from mid)
            (ys : ChainedList mid to) : ChainedList from to :=
    match ys with
    | clnil => fun xs => xs
    | snoc ys' y => fun xs => snoc (clist_app xs ys') y
    end xs.

  Infix "++" := clist_app (right associativity, at level 60).

  Definition clist_prefix
            {from mid to}
            (prefix : ChainedList from mid)
            (full : ChainedList from to) : Prop :=
    exists suffix, full = prefix ++ suffix.

  Definition clist_suffix
            {from mid to}
            (suffix : ChainedList mid to)
            (full : ChainedList from to) : Prop :=
    exists prefix, full = prefix ++ suffix.

  Infix "`prefix_of`" := clist_prefix (at level 70).
  Infix "`suffix_of`" := clist_suffix (at level 70).

  Section Theories.
  Lemma app_clnil_l {from to} (xs : ChainedList from to) :
    clnil ++ xs = xs.
  Proof. induction xs; auto; cbn; solve_by_rewrite. Qed.

  Lemma clist_app_assoc
        {c1 c2 c3 c4}
        (xs : ChainedList c1 c2)
        (ys : ChainedList c2 c3)
        (zs : ChainedList c3 c4) :
    xs ++ ys ++ zs = (xs ++ ys) ++ zs.
  Proof. induction zs; intros; auto; cbn; solve_by_rewrite. Qed.
  End Theories.

  Lemma prefix_of_app
        {from mid to to'}
        {prefix : ChainedList from mid}
        {xs : ChainedList from to}
        {suffix : ChainedList to to'} :
    prefix `prefix_of` xs ->
    prefix `prefix_of` xs ++ suffix.
  Proof.
    intros [ex_suffix ex_suffix_eq_app].
    exists (ex_suffix ++ suffix).
    rewrite clist_app_assoc; congruence.
  Qed.
End ChainedList.

Declare Scope clist_scope.
Delimit Scope clist_scope with trace.
Bind Scope clist_scope with ChainedList.
Infix "++" := clist_app (right associativity, at level 60) : clist_scope.

Infix "`prefix_of`" := clist_prefix (at level 70) : clist_scope.
Infix "`suffix_of`" := clist_suffix (at level 70) : clist_scope.

Arguments ChainedList : clear implicits.