Simple question COQ

Question

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$?

Answer 1

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.

Answer 2

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) *)
}.