Not an inductive product

Using Coq
#1

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).
Admitted.

What is actually meant by an inductive product?

Thx.
Jerome.

#2

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.

#4

Hi silene. Thanks for your answer.

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.

#5

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.
#6

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 :slight_smile:

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.

Thanks for your help.
Jerome.

#7

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.