follows_assoc_set.v

(** SSReflect boilerplate. *)
From Coq Require Import ssreflect.
Set SsrOldRewriteGoalsOrder.
Set Asymmetric Patterns.
Set Bullet Behavior "None".
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(** Traces as lazy lists of booleans. *)
CoInductive trace : Set :=
| Tnil : bool -> trace
| Tcons : bool -> trace -> trace.

(** The usual coinductive decomposition boilerplate. *)
Definition trace_decompose (tr: trace): trace :=
match tr with
| Tnil b => Tnil b
| Tcons b tr' => Tcons b tr'
end.

Lemma trace_destr: forall tr, tr = trace_decompose tr.
Proof. case => //=. Qed.

(** Trace heads. *)
Definition hd tr :=
match tr with
| Tnil b => b
| Tcons b tr0 => b
end.

(** Key predicate which holds for two traces when the first is a
prefix of the second, and [p] holds for the suffix. *)
CoInductive follows (p : trace -> Set) : trace -> trace -> Set :=
| follows_nil : forall b tr,
   hd tr = b ->
   p tr ->
   follows p (Tnil b) tr
| follows_delay: forall b tr tr',
   follows p tr tr' ->
   follows p (Tcons b tr) (Tcons b tr').

(** There is a prefix for which [p1] holds. *)
Definition append (p1 p2: trace -> Set) : trace -> Set :=
fun tr => { tr' & (p1 tr' * follows p2 tr' tr)%type }.

(** The key property we want to prove about [append]. *)
Definition append_assoc_R := 
forall p1 p2 p3 tr, (append p1 (append p2 p3)) tr -> 
 (append (append p1 p2) p3) tr.

(** Useful predicate for proving [append_assoc_R]. *) 
CoInductive midpoint (p0 p1: trace -> Set) (tr0 tr1: trace)
 (h: follows (append p0 p1) tr0 tr1) : trace -> Set :=
| midpoint_nil : forall tr,
   tr0 = Tnil (hd tr1) ->
   p0 tr ->
   follows p1 tr tr1 ->
   midpoint h tr
| midpoint_delay : forall tr2 tr3
  (h1: follows (append p0 p1) tr2 tr3) b tr',
   tr0 = Tcons b tr2 ->
   tr1 = Tcons b tr3 ->
   @midpoint p0 p1 tr2 tr3 h1 tr' ->
   midpoint h (Tcons b tr').

(** First useful fact about midpoints. *)
Lemma midpoint_before: forall p0 p1 tr0 tr1 
 (h: follows (append p0 p1) tr0 tr1) tr',
 midpoint h tr' -> follows p0 tr0 tr'.
Proof.
cofix COINDHYP. dependent inversion h. move => {tr H0}.
- move: tr1 b tr0 h e a H. case. 
  - move => st0 st1 tr0 h1 h2 h3 h4. simpl in h2.  
    move => tr' hm.
    inversion hm; subst => {hm}; last by inversion H.
    destruct h3. destruct p. inversion h1. 
    subst. apply follows_nil; last by [].
    by inversion H1.
  - move => st0 tr0 st1 tr1 h1 h2 h3 h4. simpl in h2.
    move => tr' hm.
    inversion hm; subst => {hm}; last by inversion H.
    destruct h3. destruct p. inversion h1.
    subst. apply follows_nil; last by []. by inversion H1. 
- subst.
  move => tr0 hm.
  destruct tr0; first by inversion hm.
  inversion hm; subst => {hm}; first by inversion H.
  inversion H1; subst => {H1}.
  inversion H2; subst => {H2}.
  apply follows_delay. 
  by have := COINDHYP _ _ _ _ h1; apply. 
Qed.

(** Second useful fact about midpoints. *)
Lemma midpoint_after: forall p0 p1 tr0 tr1
 (h: follows (append p0 p1) tr0 tr1) tr',
 midpoint h tr' -> follows p1 tr' tr1.
Proof.
cofix COINDHYP. dependent inversion h. move => {tr H0}.
- move: tr1 b tr0 h e a H. case. 
  * move => st0 st1 tr0 h1 h2 h3 h4. simpl in h2. move => tr' hm.
    inversion hm; subst => {hm}; last by inversion H.
    destruct tr'; last by inversion H. destruct h3.
    destruct p. inversion H1. subst.
    apply follows_nil; last by []. by inversion H1. 
  * move => st0 tr0 st1 tr1 h1 h2 h3 h4. simpl in h2.
    move => tr' hm. by inversion hm; last by inversion H.
- subst. 
  move => tr0 hm.
  destruct tr0; first by inversion hm.
  inversion hm; subst => {hm}; first by inversion H.
  inversion H1; subst => {H1}.
  inversion H2; subst.
  apply follows_delay.
  by have := COINDHYP _ _ _ _ h1; apply. 
Qed.

(** Function [midp] finds what we want. *)
CoFixpoint midp (p0 p1: trace -> Set)  (tr0 tr1: trace)
 (h: follows (append p0 p1) tr0 tr1): trace :=
match h with
| follows_nil _ _ _ h1 => let: existT tr2 h2 := h1 in tr2
| follows_delay st tr2 tr3 h1 => Tcons st (midp h1)
end.

Lemma midpoint_midp : forall (p0 p1: trace -> Set) tr0 tr1
 (h : follows (append p0 p1) tr0 tr1),
 midpoint h (midp h).
Proof.
cofix CIH.
dependent inversion h; subst.
- rewrite [midp _]trace_destr /=.
  by destruct a,p,x => //=; apply midpoint_nil.
- rewrite [midp _]trace_destr /=.
  exact: (@midpoint_delay p0 p1 (Tcons b tr) (Tcons b tr') 
   (follows_delay b f) tr tr' f b (midp f)).
Qed.

(* Set success. *)
Lemma append_assoc_R_Set :
 append_assoc_R.
Proof.
move => p1 p2 p3 tr0 h1.  move: h1 => [tr1 [h1 h2]].
exists (midp h2). split.
- have Hs := midpoint_before (midpoint_midp h2).
  by exists tr1.
- exact: midpoint_after (midpoint_midp h2).
Qed.