I'm playing around with the `Sets`

sublibrary of the stdlib. I'm at the beginning of the journey, the `Ensembles.v`

file. The behaviour of the `Union`

inductive is not clear to me.

This inductive is:

```
Inductive Union (B C:Ensemble) : Ensemble :=
| Union_introl : forall x:U, In B x -> In (Union B C) x
| Union_intror : forall x:U, In C x -> In (Union B C) x.
```

Then this is harder than it should be:

```
From Coq.Sets Require Import Ensembles.
Lemma In_Union_iff (B C : Ensemble) (x : U) :
In (Union B C) x <-> (In B x) \/ (In C x).
Proof.
split.
- intros H; inversion H as [y H' E | y H' E]; [left | right]; exact H'.
- intros [H | H]; [apply Union_introl | apply Union_intror]; exact H.
Qed.
```

- I didn't manage to intro-pattern
`In (Union B C x`

effectively. - Then, I tried
`destruct H`

which is strange as soon as one wants to name things. - Then I ended with this
`inversion`

where`y`

and`E`

are both useless, but cannot be discarded.

So there might be things I don't understand. Do you have a better solution?

Then, I tried destruct H which is strange as soon as one wants to name things.

I don't know what you mean. In any case isn't inversion the global worst for naming things?

This:

```
Lemma In_Union_iff (B C : Ensemble) (x : U) :
In (Union B C) x <-> (In B x) \/ (In C x).
Proof.
split.
- intros H42; destruct H42.
```

does exactly what is needed but generates a fresh name automatically, which I do not want.

```
U : Type
B, C : Ensemble
x : U
H : In B x
========================= (1 / 2)
In B x \/ In C x
```

Now this:

```
Lemma In_Union_iff (B C : Ensemble) (x : U) :
In (Union B C) x <-> (In B x) \/ (In C x).
Proof.
split.
- intros H42; destruct H42 as [H | H].
```

produces the unexpected:

```
U : Type
B, C : Ensemble
H : U
H0 : In B H
========================= (1 / 2)
In B H \/ In C H
```

destruct as wants 1 name for each argument of the constructor

```
| Union_introl : forall x:U, In B x -> In (Union B C) x
```

arguments are `x:U`

and `_:In B x`

update:

```
Lemma In_Union_iff (B C : Ensemble) (x : U) :
In (Union B C) x <-> (In B x) \/ (In C x).
Proof.
split.
- intros H42; destruct H42 as [x H | x H].
```

gives the best result, but I have no idea why I can introduce the name `x`

while it was already there.

the `x`

which is introduced is not the `x`

which was in the context

this may be more visible if you do

```
Lemma In_Union_iff (B C : Ensemble) (y : U) :
In (Union B C) y <-> (In B y) \/ (In C y).
Proof.
split.
- intros H. destruct H.
(* x : U instead of y : U which disappeared *)
```

ah, it's because of what Gaëtan said and because `Union`

's last argument is an index

Paolo Giarrusso said:

ah, it's because of what Gaëtan said and because

`Union`

's last argument is an index

Hmm, I think I don't understand this sentence well enough. Do you have some pointers?

in `Inductive foo (bar:Bar) : forall baz : Baz, Prop := ...`

, `bar`

is a parameter and `baz`

an index

Gaëtan Gilbert said:

in

`Inductive foo (bar:Bar) : forall baz : Baz, Prop := ...`

,`bar`

is a parameter and`baz`

an index

I get it, but I still don't really understand why it's important to make this distinction :p

because this index indeed could be a parameter. Here's a datatype with an index that can't:

```
Inductive Forall (A : Type) (P : A → Prop) : list A → Prop :=
| Forall_nil : Forall P nil
| Forall_cons : ∀ (x : A) (l : list A), P x → Forall P l → Forall P (x :: l).
```

now when you do `destruct thing`

with `thing : foo bli blu`

, `destruct`

will generalize the goal over `blu`

(so the goal can be seen as `(fun var => stuff) blu`

) and produce a proof term `match thing in foo _ var return stuff with ... end`

To keep on with this:

This:

```
Lemma In_Union_iff (B C : Ensemble) (x : U) :
In (Union B C) x <-> (In B x) \/ (In C x).
Proof.
split.
- intros [x H | x H].
```

gives `x is already used.`

somehow breaking my dream that `intros H; destruct H as intro_pattern`

is the same as `intros intro_pattern`

.

this generalization means that destruct will forget about the value of `blu`

there are also some heuristics to `clear`

variables which are not any more useful from the context, typically `thing`

and `blu`

when they happen to be hypotheses

`intros`

does not do the same clearing I guess

(also `intros`

will not generalize hypotheses over `blu`

, only the goal conclusion)

Thank you both for being so patient and helpful. I'm seriously considering https://inutile.club/estatis/brain-transplant/ to keep on.

tldr matching and `destruct`

leave parameters untouched but not indices

this means when declaring an inductive you should prefer using parameters when possible (ie if all constructors look like `forall x, ... -> Ind x ...`

then `x`

should be a parameter instead)

and Union breaks this rule so that it can say `Inductive Union _ _ : Ensemble`

instead of `Inductive Union _ _ _ : Prop`

Thank you very much. This is a very clear explanation of Union. Are there places where I can have more information on this parameter versus indices thing?

you can look around https://coq.inria.fr/doc/master/refman/language/core/inductive.html#the-match-with-end-construction

On it, thanks, there's also a paragraph about indices in the mathcomp-book, subsection 5.2.1.

Gaëtan Gilbert said:

you can look around https://coq.inria.fr/doc/master/refman/language/core/inductive.html#the-match-with-end-construction

That is **not** an easy Saturday evening read!

This problem is rather delicate.

Last updated: Jun 23 2024 at 05:02 UTC