The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

Hi all!

I have a problem very similar to that of Jacques-Henri Jourdan, which
he asked about on the list four days ago:

https://sympa.inria.fr/sympa/arc/coq-club/2013-07/msg00108.html

I've tried to figure it out by myself, but it's slow going. I could
use some help.

Take this simplified example of my own situation:

Inductive Test1 := t1list : list Test2 -> Test1
with      Test2 := t2item : Test1 -> Test2.

Now I want to define a simple property on it, such as:

Require Import Coq.Lists.List.
Fixpoint short_lists1 t : Prop :=
  match t with t1list lst =>
    length lst < 10  /\
    Forall (fun t2 => short_lists2 t2) lst
  end
with short_lists2 t : Prop :=
  match t with t2item t1 => short_lists1 t1 end.

Coq won't accept it, because I'm attempting structural reduction
through both `Test1` and `list`. (Note that I kept my example mutually
recursive because if I leave it out, any solution I find may or may
not work for my actual problem.)

(1)  Most of what I've tried has been based on Daniel Schepler answer
to Jacques-Henri. He supplied a custom recursion principle. This lead
me to believe that perhaps Coq uses `mylist_rect` (or `mylist_rec`) to
check structural reduction by the `short_lists1` function.
Jacques-Henri seemed satisfied with the answer (though he mentions a
drawback). I myself, however, still cannot get his `short_lists1`
function accepted by Coq. What am I missing?

(2)  Assuming that a custom recursion scheme is the solution, how
would you define one for my example above? I tried doing it manually
(and will continue to try), but could it perhaps be done by using
`Scheme` and friends (Chapter 13 of the manual)? That feels like it
would be more elegant.

Any advice would be appreciated!

--
www.mhelvens.net