The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

The example that you are studying is the example of infinite
repetition of a word in a stream.  It appears a similar example is
given in the book "Interactive Theorem Proving and Program
Development, CoqArt..., Springer Verlag" that Pierre Castéran and I
published a few months ago, our functions are called LAppend (for your
iconc) and omega (for your loop).  However, you will notice that our
omega is a co-recursive function and your loop is a CoInductive
relation.  Also our omega does not mimick exactly your loop, because
omega relies on a "general_omega" function instead of relying on
LAppend.  This change of structure makes the proofs easier.  You can
check our examples on the internet site (chapter 13 deals with
co-inductive objects).

http://www.labri.fr/Perso/~casteran/CoqArt/index.html,

In your setting, one can try to perform proofs containing recursions 
on words that have the "fleche" property, but there is a problem.  if 
we consider the words abc and bc, the latter is a sub-word of the 
former, but "loop abc s" means s is abcabcabcabcabc while "loop bc s'"
means s' is bcbcbcbcbc  and it appears obviously that s' is not a 
"sub-sequence" of s'.  For this reason I propose changing the 
statement to prove to the following one:

Lemma tutu : forall s m n, loop m s -> ifleche (iconc n s).

and reasoning by co-induction over the proof of "loop m s" is 
possible, the reasoning step goes one constructor at a time, so that
the "usual" structure of co-inductive proofs is preserved.  Because we
quantified over n, we do not need to have arbitrary deep recursion, 
and "well-founded co-recursion", as you call it, is not needed.  The 
lesson here is that the statement that you proposed was not general 
enough: when you have a problem, try to become more abstract.

Of course, in the end we do not get exactly what you wanted, because
tata requires that we prove "ifleche s" and we only proved
"ifleche (iconc n s)", this is were we replace your "ifleche_trans" 
by another recursive theorem, which states the same thing the other 
way around:

Lemma toto : forall m s, ifleche (iconc m s) -> ifleche s.

This one is proved by conventional induction over m, if there was a 
need for "well-founded recursion" it could be used in this theorem (I 
am currently working on an example that mixes well-founded recursion 
and co-recursion, but I will make it public later when I have ironed 
out the details).  And then we can conclude with the theorem you 
requested.  It is remarkable that the theorem I used is inverse to the
theorem you wanted to use.  Maybe this comes of the fact that 
co-recursion forces you to always look the other way around.

The full proof text is given as an attachment, it has been checked with
Coq-8.0 (Apr 2004), I removed theorems ifleche_trans and fleche_all that
were not used in my attempt.

Yves
CoInductive sbool : Set := cb : bool -> sbool -> sbool.

CoInductive ifleche : sbool -> Set :=
  ci : forall b s, ifleche s -> ifleche (cb b s) .

Inductive mot1 : Set :=
  | u1 : bool -> mot1
  | c1 : bool -> mot1 -> mot1.

Inductive fleche : mot1 -> Set :=
  | fu1 : forall b, fleche (u1 b)
  | fc1 : forall b m, fleche m -> fleche (c1 b m).

Fixpoint iconc (m : mot1) (s : sbool) {struct m} : sbool :=
  match m with
  | u1 b => cb b s
  | c1 b m => cb b (iconc m s)
  end.

CoInductive loop (m : mot1) : sbool -> Set :=
  | lp : forall s, loop m s -> loop m (iconc m s).

Lemma tutu : forall s m n, loop m s -> ifleche (iconc n s).
intros s m; generalize s; clear s.
cofix tata.
intros s n; case n; simpl.
intros b l; apply (ci b).
case l; clear s l.  (* Here is a clever step, a case analysis on a proof *)
intros s l; apply tata; assumption.
intros b n' l; apply (ci b).
apply tata; assumption.
Qed.

Lemma toto : forall m s, ifleche (iconc m s) -> ifleche s.
induction m; simpl; intros s i; inversion i; auto.
Qed.

Lemma tata : forall s m, loop m s -> ifleche s.
intros s m l; apply (toto m); apply tutu with m.
assumption.
Qed.