The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Dear Adam,

I'm trying to construct the proof of a transformation - please see the attached 
class diagram. Informally, the transformation is as follows:

Map every instance of A to an instance of X.

Map every instance of B to an instance of Y, provided that the instance of A to 
which B is related via R1, is different from the instance of A to which B is 
related via R2.

The diagram also shows an example input model and the corresponding output 
model.

I originally represented the classes as mutually inductive types, but I gather 
that would lead to a model that couldn't be instantiated. (BTW, I eventually 
want to extract a program that implements the transformation.)

In the attached ".v" file, X' is not fully defined because I don't know how to 
construct an X containing a list of Y, in which each Y depends on X.

Thanks.

Regards,
Jeff.

Adam Chlipala wrote:
> Jeff Terrell wrote:
> > However, in the case where X references many Y, I'm not sure how to 
> > define the function.
> >
> > CoInductive X : Set :=
> >    Build_X : nat -> list Y -> X
> > with Y : Set :=
> >    Build_Y : nat -> X -> Y.
>
> This definition type-checks:
>
> CoFixpoint Build_XY (n : nat) (m : nat) : X :=
>   Build_X n (Build_YX m n :: nil)
> with
>   Build_YX (m : nat) (n : nat) : Y := Build_Y m (Build_XY n m).
>
> ...but I'm guessing that this isn't what you're looking for.  Can you 
> explain what you are trying to do in your actual example?  Co-inductive 
> types have many non-intuitive features, and it's quite possible that 
> you'd be better off reformulating your development at a higher level.

Attachment: ab-xy.pdf
Description: Adobe PDF document

(* File : ab-xy.v *)
Require Import List EqNat.

(* Input Model *)
CoInductive A : Set  :=
   Build_A : nat -> list B -> list B -> A
with B : Set := 
   Build_B : nat -> A -> A -> B.

(* A *)
Definition AID := fun a : A => let (AID, _, _) := a in AID.
Definition R1_B := fun a : A => let (_, R1_B, _) := a in R1_B.
Definition R2_B := fun a : A => let (_, _, R2_B) := a in R2_B.

(* B *)
Definition BID := fun b : B => let (BID, _, _) := b in BID.
Definition R1_A := fun b : B => let (_, R1_A, _) := b in R1_A.
Definition R2_A := fun b : B => let (_, _, R2_A) := b in R2_A.

(* Output Model *)
CoInductive X : Set :=
   Build_X : nat -> list Y -> X
with Y : Set :=
   Build_Y : nat -> X -> Y.

(* X *)
Definition XID := fun x : X => let (XID, _) := x in XID.
Definition R3_Y := fun x : X => let (_, R3_Y) := x in R3_Y.

(* Y *)
Definition YID := fun y : Y => let (YID, _) := y in YID.
Definition R3_X := fun y : Y => let (_, R3_X) := y in R3_X.

(* Support *)
Definition Eq_A (a : A) (a' : A) : bool :=
   if beq_nat (AID a) (AID a') then true else false.

(* Fixpoint Build_R3_Y (lb : list B) : list Y :=
   match l with
   | nil => nil
   | b :: lb' =>
   if Eq_A (R1_A b) (R2_A b) then
      Build_R3_Y lb' ?
   else
      Build_Y (BID b) ? :: Build_R3_Y lb' ?
   end. *)

Definition X' (a : A) : X := Build_X (AID a) nil. (* TBD : Build_R3_Y (R1_B 
a) *)

Theorem T :
   forall la : list A, {lx : list X | 
      forall a : A, In a la ->
         exists x : X,
            In x lx /\
            (XID x) = (AID a) /\
            forall b : B, In b (R1_B a) /\ (Eq_A a (R2_A b) = false) ->
               exists y : Y,
                  In y (R3_Y x) /\
                  (YID y) = (BID b) /\
                  (R3_X y) = x}.
Proof.
   intro la.
   induction la as [| a'].
   exists nil.
   intros a H.
   elim H.

   destruct IHla as (lxw).
   exists (X' a' :: lxw).
   intros a H1.
   exists (X' a').
   split.
   simpl.
   left.
   reflexivity.

   destruct H1.
   split.
   simpl.
   rewrite H.
   reflexivity.

   intro b.
   induction (R1_B a) as [| b'].
   intro H1.
   destruct H1.
   elim H0.

   intro H0.
   exists (Build_Y (BID b) (X' a')).
   split.
    unfold X'.
   simpl.
(* FALSE *)