The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Hi,

I'm trying to map an object of type A to an object of type X. If A 
references a single object of type B, I don't have a problem, i.e.

CoInductive A : Set :=
  Build_A : B -> A
with B : Set :=
  Build_B : A -> B.

Definition RB := fun a : A => let (RB) := a in RB.
Definition RA := fun b : B => let (RA) := b in RA.

CoInductive X : Set :=
  Build_X : Y -> X
with Y : Set :=
  Build_Y : X -> Y.

Definition SY := fun x : X => let (SY) := x in SY.
Definition SX := fun y : Y => let (SX) := y in SX.

CoFixpoint f(a : A) : X :=
  Build_X (g (RB a))
with g (b : B) : Y :=
  Build_Y (f (RA b)).

Theorem T :
  forall a : A,
     RA (RB a) = a -> {x : X |
        exists y : Y,
           SY x = y /\
           SX y = x}.
Proof.
intros.
exists (f a).
exists (SY (f a)).
split.
reflexivity.
simpl.
rewrite H.
reflexivity.
Qed.

However, if A references a list of B, I'm not sure how to define f. 
Everything that I've tried produces an error.

Require Import List.

CoInductive A : Set :=
  Build_A : list B -> A
with B : Set :=
  Build_B : A -> B.

Definition RB := fun a : A => let (RB) := a in RB.
Definition RA := fun b : B => let (RA) := b in RA.

CoInductive X : Set :=
  Build_X : list Y -> X
with Y : Set :=
  Build_Y : X -> Y.

Definition SY := fun x : X => let (SY) := x in SY.
Definition SX := fun y : Y => let (SX) := y in SX.

CoFixpoint f(a : A) : X := ???

Theorem T :
  forall a : A, forall b : B,
     In b (RB a) /\ a = (RA b) -> {x : X |
        exists y : Y,
           In y (SY x) /\
           SX y = x}.

Any help would be gratefully appreciated. Thanks.

Regards,
Jeff.