# Not an inductive product

Hello,

I am experimenting a bit with the Ensembles library (Coq.Sets.Ensembles) trying to prove various trivial things.

When I try to use “destruct” tactic on an Union, I get the error “Not an inductive product”, whereas “apply Union_ind” works fine.

Small self contained example:

Require Import Coq.Sets.Ensembles.
Lemma union_empty_inc: forall U:Type, forall A:Ensemble U,
Included U A (Union U (Empty_set U) A).
Proof.
intros **.
unfold Included.
intros **.
Fail destruct (Union U).
Fail destruct (Union U (Empty_set U) A).
apply (Union_ind U (Empty_set U) A).

What is actually meant by an inductive product?

Thx.
Jerome.

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.

Maybe it is as if I would have written “destruct nat.”, which BTW gives the same error (Not an inductive product).

I am not sure I completely understand Ensembles in the Coq library. Here is how I would put it.

Require Import Coq.Sets.Ensembles.
Print Ensemble.

Gives:

Ensemble = fun U : Type => U → Prop
: Type → Type

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?

I hope I did not say too many stupid things.

BR,
Jerome.

Yes.

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.
``````

Hi silene,

I am not a complete beginner in Coq, but that’s the first time I venture beyond exercises.

I do not see what an “inductive product” would have in common with a cartesian product or a tuple. In Coq documentation at Tactics — Coq 8.13.1 documentation there is the following definition:

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.

Jerome.

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.
``````