CODEWITHSUNDEEP
recordcoq
verifying
verifying

Reputation: 39

Coq - Passing parameters to a record

I'm having trouble in comparing elements of sets belonging to two distinct instances of the same record type. Consider the following record. 

Record ToyRec := {
    X:Set;
    Labels:Set;
    r:X->Labels
}

Say that two objects T1 and T2 of type ToyRec form a good pair if for every element in T1.(X) there exists an element in T2.(X) with the same label. 

Definition GoodPair(T1 T2:ToyRec):Prop := 
forall x1:T1.(X), exists x2:T2.(X), T1.(r) x1 = T2.(r) x2.

The problem is that I get an error saying that T1.(r) x1 is of type X1.(Labels), and T2.(r) x2 is of type X2.(Labels).

I understand the problem, and I imagine it could be solved if I could somehow declare the set Labels outside the record, and then pass it as a parameter. Is there a way to do this in Coq? Or what would be the most elegant way of defining the records I want and the property GoodPair?

Upvotes: 1

Views: 173

Answers (1)

Vinz
Vinz

Reputation: 6047

The closest thing I got from your code his the following:

Record ToyRec {Labels : Set} := {
  X:Set;
  r:X->Labels
}.

Definition GoodPair {Labels:Set} (T1 T2 : @ToyRec Labels) : Prop :=
  forall x1: X T1, exists x2: X T2, r T1 x1 = r T2 x2.

By having Labels as a dependency for ToyRec you can be sure that both records are using the same type.

PS: I used {Labels : Set} instead of (Labels : Set) to specify that this argument is implicit and should be inferred whenever possible.

Upvotes: 2

Related Questions