The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Fri, Jul 19, 2013 at 7:26 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:

> I think if you define a variant of [Forall] based on recursion instead of
> induction, this will just work, since the termination checking understands
> the former but not the latter.

Aha, indeed! The following seems to work:

Require Import Coq.Lists.List.

Definition ForallRec {B} (P:B->Prop) (l: list B) : Prop :=
  fold_left (fun p b => p /\ (P b)) l True.

Fixpoint short_lists1 t : Prop :=
  match t with t1list lst =>
    length lst < 10  /\
    ForallRec (fun t2 => short_lists2 t2) lst
  end
with short_lists2 t : Prop :=
  match t with t2item t1 => short_lists1 t1 end.

I think this will work for my real-life problem too, so that's good.
;-) Unfortunately, it doesn't improve my understanding of recursion
schemes.

If possible, I'd still like a response to my question (1).

Thanks!

--
www.mhelvens.net