follows_assoc.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 -> Prop) : trace -> trace -> Prop :=
| 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 -> Prop) : trace -> Prop :=
fun tr => exists tr', p1 tr' /\ follows p2 tr' tr.

(** 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 -> Prop) (tr0 tr1: trace)
 (h: follows (append p0 p1) tr0 tr1) : trace -> Prop :=
| 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 H2. 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 H2. 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 H2. inversion H3. 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.

Definition ex_midpoint :=
forall p0 p1 tr0 tr1 (h: follows (append p0 p1) tr0 tr1),
exists tr, midpoint h tr.

(** Reduce our key property to showing that midpoints exist. *)
Lemma ex_midpoint_append_assoc_R:
  ex_midpoint ->
  append_assoc_R. 
Proof.
move => Hex p1 p2 p3 tr0 h1.  move: h1 => [tr1 [h1 h2]].
case: (Hex p2 p3 tr1 tr0 h2) => tr Hmid.
exists tr. split.
- exists tr1; split => //.
  exact: (midpoint_before Hmid).
- exact: (midpoint_after Hmid).
Qed.

(** Direct proof via coinduction just doesn't work. *)
Lemma ex_midpoint_direct : ex_midpoint.
Proof.
Fail cofix CIH.
Abort.

(** We escape to using classical epsilon. *)
From Coq Require Import ClassicalEpsilon.

(** Some boilerplate. **)
Definition follows_dec : forall p tr0 tr1 (h: follows p tr0 tr1),
 { tr & { a | tr0 = Tnil a /\ hd tr = a /\ p tr } } +
 { tr & { tr' & { b | tr0 = Tcons b tr /\ 
  tr1 = Tcons b tr' /\ follows p tr tr'} } }.
Proof.
intros.
destruct tr0.
- left; exists tr1; exists b. by inversion h; subst.
- destruct tr1.
  * left. exists (Tnil b). exists b. by inversion h; subst.
  * right. exists tr0. exists tr1. exists b0. by inversion h; subst.
Defined.

(** Coinductive function that finds midpoints using the 
constructive indefinite description axiom. *)
CoFixpoint midp (p0 p1: trace -> Prop) tr0 tr1
 (h: follows (append p0 p1) tr0 tr1) : trace :=
match follows_dec h with
| inl (existT tr (exist a (conj _ (conj _ H)))) =>
  let: exist x _ := constructive_indefinite_description _ H in x
| inr (existT tr (existT tr' (exist b (conj _ (conj _ H))))) =>
  Tcons b (@midp _ _ _ _ H)
end.

(** Function [midp] finds what we want. *)
Lemma midpoint_midp : forall (p0 p1: trace -> Prop) tr0 tr1
 (h : follows (append p0 p1) tr0 tr1),
 midpoint h (midp h).
Proof.
cofix CIH.
dependent inversion h; subst.
- rewrite [midp _]trace_destr /=.
  case (constructive_indefinite_description _ _) => /=.
  move => x [a1 hm].
  by apply midpoint_nil => //; destruct x.
- 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.

(** Truncate to existence statement. *)
Lemma ex_midpoint_ClassicalEpsilon : ex_midpoint.
Proof.
move => p0 p1 tr0 tr1 h.
exists (midp h).
exact: midpoint_midp.
Qed.

(** Classical epsilon success. *)
Lemma append_assoc_R_ClassicalEpsilon :
 append_assoc_R.
Proof.
exact: (ex_midpoint_append_assoc_R ex_midpoint_ClassicalEpsilon).
Qed.