Stream: Coq users

Topic: About inversion and `Union`


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 *)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 04 2023 at 16:16):

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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 04 2023 at 16:20):

intros does not do the same clearing I guess

view this post on Zulip Gaëtan Gilbert (Nov 04 2023 at 16:20):

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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 04 2023 at 16:22):

tldr matching and destruct leave parameters untouched but not indices

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Nov 04 2023 at 16:48):

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

view this post on Zulip 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.

view this post on Zulip Pierre Rousselin (Nov 04 2023 at 17:33):

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!

view this post on Zulip Pierre Rousselin (Nov 04 2023 at 17:41):

This problem is rather delicate.


Last updated: Jun 23 2024 at 05:02 UTC