The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Hi all,
 there is some (strange?) feature I found with mutual induction.

I don't remember having seen writing about it in this list.
(*******************)

(* Here is a dummy code we know it works *)
Inductive test1 (A: Type): Type :=
| TA: test1 A
| TB: test2 A -> A -> test1 A

with test2 (A: Type): Type :=
| U: test1 A -> test2 A
| V: test2 A.

(* Here is a variation of the previous code
   (which is not isomorphic,
    but we don't care about this criterion here)
   which uses a different parameter for the mutual
   call of test1
   [that is in "U", we call "test1 B" instead of "test1 A"]
*)
Inductive test1 (A: Type): Type :=
| TA: test1 A
| TB: test2 A -> A -> test1 A

with test2 (A: Type): Type :=
| U: forall B, test1 B -> test2 A
| V: test2 A.
(* Again it is accepted, showing the "A" parameter seems
   only important to be shared by all constructors
   of "test1 A", those of "test2 A" shouldn't really
   care about since they can call test1 on something different
   of "A"
*)

(* But what seems strange to me, is that we cannot get rid
   of "A" in test2, since the following code is not accepted
*)
Inductive test1 (A: Type): Type :=
| TA: test1 A
| TB: test2 -> A -> test1 A

with test2: Type :=
| U: forall B, test1 B -> test2
| V: test2.

(**********************************)
Is there any reason I haven't thought of for this behaviour?
Is it to forbide things like "test1 test2"?
(I know this is not the case for the later,
 since we can write
 "test1 (test2 unit)"/"test1 (test2 False)"/"test1 (test2 A)" for any
 A, which would be isomorphic to "test1 test2",
 but I may have missed something)

(**********************************)
(**********************************)
If anyone is interested in having recursion in records,
I found a trick (but I doubt anybody in this list is interested in it,
and it is not very handy):

You cannot use mutual induction with records BUT you can use
 recursion in records, so the following code won't work:
>>>
Inductive llist (A: Type): Type :=
| LNil: llist A
| LCons: ne_llist A -> llist A
with ne_llist (A: Type): Type :=
{head: A; tail: llist A}.
<<<
but the following will:
>>>
Set Implicit Arguments.

Inductive tmp_list (A: Type) : Type :=
| TNil: tmp_list A
| TCons: A -> tmp_list A.

Inductive llist (A: Type) : Type :=
mk_llist {
 head: A;
 tail: tmp_list (llist A)
}.

Definition Llist A := tmp_list (llist A).
<<<
but the coding is not painless:
>>>
Require Import List.

Definition tmp_conv1 (A: Type): llist A -> list A :=
 fix c1 (L: llist A) :=
 match L with
 mk_llist h t => h::(match t with
                     | TNil => nil
                     | TCons x => c1 x
                     end)
 end.

Definition conv1 (A: Type) (L: Llist A): list A :=
 match L with
 | TNil => nil
 | TCons l => tmp_conv1 l
 end.

Definition conv2 (A: Type): list A -> Llist A :=
 fix c2 (l: list A) : Llist A :=
 match l with
 | nil => TNil (llist A)
 | h::t => TCons (mk_llist h (c2 t))
 end.

Goal forall A (l: list A), conv1 (conv2 l) = l.
Proof.
 induction l; simpl; f_equal.
 now unfold conv1 in IHl.
Qed.

Goal forall A (l: Llist A), l = conv2 (conv1 l).
Proof.
 intro A; unfold Llist, conv1.
 destruct l; simpl; f_equal.
 revert l.
 fix 1.
 destruct l; simpl; f_equal.
 destruct tail; simpl; f_equal.
 destruct (Unnamed_thm0 l).
 reflexivity.
Qed.
<<<
I know that in 8.3 there is better syntax for the records, but I
haven't it here, and the mutual recursion with records is always
forbidden (if Classes were recursive, it wouldn't be a matter to
hack records to make them recursive).