The Coq mailing list

[Celia Picard <celia.picard AT irit.fr>]

Hi,
I am a PhD student in Toulouse, doing my research with Ralph Matthes.
I have spent the last months trying to solve a problem very similar to 
the one presented in this thread.
We have come up with a solution. I have extracted here only the elements 
needed to solve this particular example.

Set Implicit Arguments.

(* First of all, I need a finite set of elements.
 I use the well-known definition of Fin by Mc Bride & Mc Kinna *)

Inductive Fin: nat -> Set :=
   first k : Fin (S k)
 | succ k: Fin k -> Fin (S k).

(* By the way, we have a proof of injectivity of Fin that looks a bit 
complicated.
   Is there a well-known (easier) proof of Fin n = Fin m ->  n = m ? *)

(* Then I define a function from that finite set to the types of 
elements we want*)

Definition ilistn (T: Set) (n:nat) := Fin n -> T.

(* And I finally define a tuple made of this function and the
 cardinality of its definition set *)
Definition ilist(T:Set) := {n:nat & ilistn T n}.

(* These 2 functions are just redefinition of projections on ilist*)
Definition lgti(T: Set)(i: ilist T): nat:= projS1 i.

Definition fcti(T: Set)(i: ilist T): ilistn T (lgti i) := projT2 i.

(* Last thing needed for this example is an equivalent for map.
 On ilists, it actually corresponds to a composition of functions. *)
Definition imap(T U:Set) (f:T->U) (l:ilist T): ilist U :=
existS (ilistn U) (lgti l) (fun i => f (fcti l i)).

(* Finally, I can define T and f *)
CoInductive T: Set :=
| A : T -> T
| B : ilist T -> T.

CoFixpoint f (t : T) : T :=
match t with
| A t1' => A (f t1')
| B t1s => B (imap f t1s)
end.

I hope this will help, although it can only solve problems of mixed 
induction and co-induction dealing with lists.
Best,
Celia


Edsko de Vries wrote:
> Hi,
>
> This is related to my previous question, but a lot simpler (hopefully 
> I didn't simplify the problem too much). I don't understand how to
> mix induction and coinduction in Coq. Here is a *very* simple example:
>
> Require Import List.
>
> CoInductive T : Set :=
>   | A : T -> T
>   | B : list T -> T.
>
> CoFixpoint f (t : T) : T :=
>   match t with
>   | A t1' => A (f t1')
>   | B t1s => B (map f t1s)
>   end.
>
> This definition of [f] seems ok to me, but is rejected as not guarded 
> because the recursive argument appears as argument to a function (in 
> this case, map). How should one define functions and data types like 
> this? (I don't care if I have to redefine list; I'm only using list as 
> an example -- the loss of the use of library functions is not an issue.)
>
> Thanks,
>
> Edsko
>
> PS. I seem to recall that a question like this came up before, but I 
> can't find it.