# Simple question COQ

I'm a beginner in the coq proof assistant, so sorry if my question is silly. I would like to prove properties of a mathematical object. For clarity I will describe an over-simplified version of my object. Intuitively, the object has three sets A, B, C. The list A is of the form $$A= \{(0,x_1) (0,x_2), ... ,(0,x_n)\}$$ i.e, all pairs consist of the number zero and an arbitrary number. Analogously, the set B is of the form $$B = \{(1,y_1)(1,y_2)...(1,y_m)\}$$. And the set $C$ is such that C = A U B. For concreteness the sets $A,B,C$ can be defined as lists, if for some reason it is not inconvenient in Coq

So the simplified object would be of the following form:

Object

A : Set of elements of the form (0,x) where x is some number

B : Set of elements of the form (1,y) where x is some number

C : Set such that C = A U B

The Condition that the structure must satisfy is:

If (0,a) belongs to A then (1,a) belongs to B.

Questions:

1) How do I define a type consisting of pairs in which the first element is 0 and the second an arbitrary natural number? (Obs: This was answered by @KonstantinWeitz but his answer received a minus. Why wouldn't Konstantin's answer be satisfactory in Coq?)

2)How do I define the object above in coq? I tried to do it with records. But the problem is that I have no idea of how to define a type of question 1.

3) How to I impose the condition that this object is valid only if for each (0,x_n) in A there is a (1,y_n) in B with y_n=x_n? And the condition that $C = A \cup B$?

• I think this is on-topic. Yes, Coq proofs are very similar to programming but I guarantee that this question would not be answered on Stack Overflow. Indeed, if it were posted there, they'd punt it straight back here. – David Richerby Nov 5 '14 at 8:12
• You do not want to do 1). What are registers in Coq? – Andrej Bauer Nov 5 '14 at 10:18
• Please restrict yourself to one question per post. Also, note that this is close to "tech support" for Coq; maybe a mailing list or board dedicated to Coq is the better address? Computer Science is mostly about implementation-agnostic principles; there may be such in your question which you should then point out. – Raphael Nov 5 '14 at 16:58
• @Raphael, if you insist, I believe that the point here is how to map very simple set theoretic constructions to the calculus of inductive constructions... – formalizer Nov 5 '14 at 22:53
• Because you should use sum types in Coq to "tag" things, not numbers like 0 and 1. – Andrej Bauer Nov 5 '14 at 23:50

Set-theoretic thinking is creating trouble, as you are trying to do things in non-Coq ways. Let me show you a solution which works better, and then you can explain what your actual non-simplified problem is -- we can probably optimize that one to.

If we have two lists A and B then we do not have to tag the elements of the first list with 0 and the second one with 1. That is, rather than having

A = [(0,x_1), ..., (n,x_n)] and B = [(1,y_1), ..., (m, y_m)]

we can equivalently have just

A = [x_1, ..., x_n] and B = [y_1, ..., y_m].

So, we are really trying to define:

A pair of lists such that the elements of the first one are contained in the second one.

We are going to use the standard library for lists (by the way if you are simulating sets by using lists, you shouldn't).

Require Import List.

(* We define what it means for the elements of list X to be
contained in list Y. *)
Definition contained_in {T} (X : list T) (Y : list T) :=
forall x, In x X -> In x Y.

(* Now we define our data structure. It is a Record with three fields. *)
Record MyLists := {
A : list nat;
B : list nat;
valid : contained_in A B
}.

(** For example, suppose we want to construct A = [1,2,3] and B = [2,3,3,1,5]. *)
Definition example : MyLists.
Proof.
(* We give Coq the fields we know about. *)
refine {| A := 1::2::3::nil ; B := 2::3::3::1::5::nil |}.
(* Coq tells us we also have to provide the 'valid' field. *)
(* We tell Coq to do it itself. *)
firstorder.
Defined.

• I don't think (Coq) code has any business being here, but the rest of the answer seems strong to me. So, if you must.... *theatrical sigh* – Raphael Nov 5 '14 at 17:03
• @AndrejBauer Thank you for your answer. The structure I have in mind is application specific, so I will skip its precise definition. The idea is that I would like it to be as concrete as possible. For this reason, I would like to have a list A (regarded as a set) such that A=[(0,x_1),...,(0,x_n)] and another list B = [(1,y_1),...,(1,y_m)]. For instance, In the same structure I would need to have a third set C = A U B. I will edit the question to be a bit more precise. – formalizer Nov 5 '14 at 23:08
• Are you ever going to mix the lists $A$ and $B$? Is that why you are tagging them, so they don't get confused? Well, in that case you should use a sum type instead of set-theoretic tags. – Andrej Bauer Nov 5 '14 at 23:51
• @Raphael: You can look at this as a lesson in how not to do set theory in type theory. – Andrej Bauer Nov 5 '14 at 23:52
• This is a meta-discussion, but I think that Coq code has much reason to be here on CS, even if it has no reason being here in the answer to this question. If giving a proof is a good answer, giving a machine-checkable proof is a GREAT answer. – Pseudonym Nov 6 '14 at 22:29

Here you go:

Require Import List.

Definition Singleton (n:nat) := {n':nat | n' = n}.   (* 1) *)

Definition zero : Singleton 0. compute. eauto. Defined.
Definition one : Singleton 1. compute. eauto. Defined.

Record MyLists := {   (* 2) *)
A : list ((Singleton 0) * nat);
B : list ((Singleton 1) * nat);
valid : forall n, In (zero,n) A -> In (one,n) B   (* 3) *)
}.