Proving existence statements about coinductive types constructively

As anyone who has worked with Coq’s machinery for coinduction and corecursion knows, the limitations of the cofix operator and the guardedness condition can easily get in the way of progress. However, these limitations appear to me to be particularly difficult to surpass when trying to prove statements of existence (of some term with coinductive type, which satisfies some coinductive predicate).

Specifically, when proving existence inductively (or building a sig type), the usual pattern is to:

  • obtain some value from the inductive hypothesis
  • massage this value in some way to build the “final” value, and apply the exists tactic on this value.

Unfortunately, this pattern is largely incompatible with the coinductive guard condition, which requires the coinductive call to be guarded by a constructor: we might not be able to apply the constructor until we have massaged our value.

To get around this, people usually define standalone corecursive functions that return the required value explicitly. Nevertheless, this is not always convenient if we have types that live in Prop, and then my current solution is to resort to using the classical epsilon.

My general question is: is there some general pattern for dealing with coinductive existence proofs constructively when Props are involved?

To make this question more concrete, consider the Coq code below which resorts to classical epsilon to prove a seemingly simple property (append_assoc_R) of coinductive types. Does this property have a nice constructive proof?

(See also the gist with the code, which should work on Coq 8.10 and later.)

(** 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.

Simon Hudon points out on Coq’s Zulip chat that essentially equivalent results can be obtained constructively by switching follows to be in Set (or Type) rather than Prop. This means that no “truncated” existence statement needs to be proven to get append_assoc_R, but also that the usual benefits of Prop disappear, such as impredicativity.

For comparison purposes, the resulting code could look like below.

(See also the gist with the code, which should work on Coq 8.10 and later.)

(** 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.