Something like fun x y z => e with e an inductive value, that is, an object whose type is an inductive type. Here, Union U _ _ is the inductive type itself. So, you would be able to destruct a value of type Union U _ _, but not the type itself.
Ensemble is a function that associates to any type or sort the type “U->Prop”. Ensemble itself has type “Type->Type”.
Section s1.
Variable U:Type.
Check Ensemble U.
Check Union U (Empty_set U) (Empty_set U).
End s1.
Gives:
Ensemble U
: Type
Union U (Empty_set U) (Empty_set U)
: Ensemble U
“Ensemble U” has type “Type” and is actually the type “U->Prop”, whereas “Union U _ _” has type “U->Prop”, so this is an actual function. Maybe after all “destruct (Union U _ _)” fails for a different reason than “destruct nat”?
I was also wondering whether “product” in “not an inductive product” means “the produce of” rather than being a synonymous of multiplication? What do you think?
No. It is the one from multiplication, or rather, it is the one found in expressions such as “Cartesian product” (i.e., tuple). Anyway, that does not change the meaning, you can only destruct something with an inductive type.
An object S of type U -> Prop should be seen as a predicate over U, or equivalently, as the characteristic function of a subset of U. Then, an element x is part of S, if the property S x holds. Suppose T is another object of type U -> Prop. The element x is part of both S and T if it satisfies S x /\ T x. In other words, you can define the predicate characterizing the intersection of S and T as fun x => S x /\ T x (which still has type U -> Prop). More generally, you can define an intersection operator as fun S T x => S x /\ T x, and if you want to make it implicitly generic with respect to U, you get fun {U} (S T: U -> Prop) x => S x /\ T x. The exact same thing can be done to define the union, except that you would replace the conjunction by a disjunction.
The Ensembles library provides all these definitions, but I would recommend against using it, especially if you are a beginner with Coq. (And if you are not a beginner, you do not need it anyway.) I think it would be much more instructive for you to directly manipulate predicates by hand:
Definition union {U} (S T : U -> Prop) (x : U) := S x \/ T x.
Definition inter {U} (S T : U -> Prop) (x : U) := S x /\ T x.
Definition empty {U} (x : U) := False.
Definition subset {U} (S T : U -> Prop) := forall x, S x -> T x.
Goal forall U (S T : U -> Prop), subset (union S T) (union T S).
Proof. intros U S T x. unfold union. tauto. Qed.
Inductive contains0 : list nat → Prop :=
| in_hd : forall l, contains0 (0 :: l)
| in_tl : forall l b, contains0 l → contains0 (b :: l).
To me it looks like an inductively defined predicate. It does not behave like a type:
Fail Variable x : contains0.
Union’s definition is similar to that. It is not possible to define a variable of type (Union U A B).
So I more and more think the message “Not an inductive product” means: the term is not the product of an inductive definition. And indeed: it is the definition itself! Both in the case of “nat”, which is a type, and the case of “Union” and “contains0” which, to me, are predicates.
I hope I am not going completely off-charts with that interpretation
As for your definitions for sets: they look great and quite natural. I would not have dared going that way and that’s why I preferred using the library. I also had expected the library to provide a greater number of basic lemmas. There are at least a couple of proofs I would like to complete with the library definitions though.
This is indeed a predicate over list nat, which means that, once applied, it becomes a type:
Variable x : contains0 nil.
Same thing for Union.
I do not see what an “inductive product” would have in common with a cartesian product or a tuple.
Tuples are inductive values (and conversely).
The following inductive type has a unique constructor whose type is a (non-dependent) product. More precisely, the type foo is isomorphic to the type of pairs of natural numbers.
Inductive foo := Foo : nat -> nat -> foo.
As for the type family contains0, it has two constructors, and both of them have types that are (dependent) products.
A constructor of type A -> B -> C -> qux is conceptually not different from a tuple of type A*B*C. In fact, Coq even allows you to use a tuple syntax to destruct inductive values, e.g.,
Definition bar (x : foo) :=
let (a,b) := x in a + b.
