## Stream: Coq users

### Topic: About inversion and `Union`

#### Pierre Rousselin (Nov 04 2023 at 15:58):

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.
``````
1. I didn't manage to intro-pattern `In (Union B C x` effectively.
2. Then, I tried `destruct H` which is strange as soon as one wants to name things.
3. 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?

#### Gaëtan Gilbert (Nov 04 2023 at 16:00):

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?

#### Pierre Rousselin (Nov 04 2023 at 16:06):

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

#### Pierre Rousselin (Nov 04 2023 at 16:07):

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

#### Gaëtan Gilbert (Nov 04 2023 at 16:08):

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`

#### Pierre Rousselin (Nov 04 2023 at 16:09):

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.

#### Gaëtan Gilbert (Nov 04 2023 at 16:11):

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 *)
``````

#### Paolo Giarrusso (Nov 04 2023 at 16:11):

ah, it's because of what Gaëtan said and because `Union`'s last argument is an index

#### Pierre Rousselin (Nov 04 2023 at 16:12):

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?

#### Gaëtan Gilbert (Nov 04 2023 at 16:13):

in `Inductive foo (bar:Bar) : forall baz : Baz, Prop := ...`, `bar` is a parameter and `baz` an index

#### Pierre Rousselin (Nov 04 2023 at 16:14):

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

#### Paolo Giarrusso (Nov 04 2023 at 16:15):

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

#### Gaëtan Gilbert (Nov 04 2023 at 16:16):

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`

#### Pierre Rousselin (Nov 04 2023 at 16:16):

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

#### Gaëtan Gilbert (Nov 04 2023 at 16:16):

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

#### Gaëtan Gilbert (Nov 04 2023 at 16:18):

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

#### Gaëtan Gilbert (Nov 04 2023 at 16:20):

`intros` does not do the same clearing I guess

#### Gaëtan Gilbert (Nov 04 2023 at 16:20):

(also `intros` will not generalize hypotheses over `blu`, only the goal conclusion)

#### Pierre Rousselin (Nov 04 2023 at 16:20):

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

#### Gaëtan Gilbert (Nov 04 2023 at 16:22):

tldr matching and `destruct` leave parameters untouched but not indices

#### Gaëtan Gilbert (Nov 04 2023 at 16:24):

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`

#### Pierre Rousselin (Nov 04 2023 at 16:36):

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?

#### Pierre Rousselin (Nov 04 2023 at 16:50):

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

#### Pierre Rousselin (Nov 04 2023 at 17:33):

Gaëtan Gilbert said:

That is not an easy Saturday evening read!

#### Pierre Rousselin (Nov 04 2023 at 17:41):

This problem is rather delicate.

Last updated: Jun 23 2024 at 05:02 UTC