Stream: math-comp users

Topic: Set preimage proof


view this post on Zulip Julin Shaji (Apr 08 2024 at 10:23):

I got a goal like this which says given a set {set A+B} in which all elements are value like inr _, the set given by inl @^-1 would be empty.

From mathcomp Require Import all_ssreflect.


Goal forall {A B: finType} (b: {set B}),
  (* inl @^-1: ((inr (A:=A)) @: b) = set0. *)
  inl @^-1: [set (inr (A:=A)) x | x in b] = set0.
Proof.
  move => A B b.
  (*
  1 subgoal

  A, B : finType
  b : {set B}

  ========================= (1 / 1)

  inl @^-1: [set inr x | x in b] = set0
  *)
  Search (_ @^-1: _).

How can we proceed from here?

Couldn't figure out a suitable lemma with the Search.

view this post on Zulip Reynald Affeldt (Apr 08 2024 at 10:33):

to show that two sets are equal, you can use apply/setP.

view this post on Zulip Julin Shaji (Apr 08 2024 at 10:45):

Thanks. Made some progress with it:

  Lemma foo1: forall {A B: finType} (b: {set B}),
    inl @^-1: ((inr (A:=A)) @: b) = set0.
    (* inl @^-1: [set (inr (A:=A)) x | x in b] = set0. *)
  Proof.
    move => A B b.
    apply/setP => //= x.
    rewrite !in_set.
(*
1 subgoal

A, B : finType
b : {set B}
x : A

========================= (1 / 1)

(inl x \in [set inr x | x in b]) = false
*)
  Search (_ \in _).

Rewriting with unfold_in reduces it to [set inr x | x in b] (inl x) = false but was not sure if that's the way to go..

view this post on Zulip Reynald Affeldt (Apr 08 2024 at 11:12):

apply/negbTE changes the goal with better notations

view this post on Zulip Reynald Affeldt (Apr 08 2024 at 11:13):

and then you want to look at imsetP because you are dealing with the image of a set

view this post on Zulip Julin Shaji (Apr 08 2024 at 11:26):

Could do it!
Not sure if I'm doing it in a proper way, though..

  Lemma bar: forall {A B: Type} (a: A) (b: B),
    inl (B:=B) a = inr (A:=A) b -> False.
  Proof.
    move => A B a b.
    move => H.
    inversion H.
  Qed.

  Lemma foo1: forall {A B: finType} (b: {set B}),
    inl @^-1: ((inr (A:=A)) @: b) = set0.
  Proof.
    move => A B b.
    apply/setP => //= x.
    rewrite !in_set.
    apply/negbTE/imsetP => [[eb]] => _.
    by apply: bar.
  Qed.

Is use of inversion more of a non-ssreflect style?

view this post on Zulip Reynald Affeldt (Apr 08 2024 at 11:30):

From mathcomp Require Import all_ssreflect.

Goal forall {A B: finType} (b: {set B}),
  (* inl @^-1: ((inr (A:=A)) @: b) = set0. *)
  inl @^-1: [set (inr (A:=A)) x | x in b] = set0.
Proof.
move => A B b.
apply/setP => x.
rewrite !inE.
apply/negbTE.
apply/imsetP.
by case.
Qed.

view this post on Zulip Reynald Affeldt (Apr 08 2024 at 11:31):

you don't need no inversion because the "inl = inr" hypo is already contradictory

view this post on Zulip Julin Shaji (Apr 08 2024 at 11:41):

Thanks!. Hadn't realized it can figure out the inl _ = inr _ being a contradiction by itself.
Did it separately because once I need to derive a=b from inl a = inl b. It didn't seem able to figure it out by itself then (or more likely, I didn't use some ssreflect feature).

view this post on Zulip Julin Shaji (Apr 08 2024 at 11:42):


I had also been trying to prove this:

  Lemma foo2: forall {A B: finType} (a: {set B}),
    (* a = inl @^-1: ((inl (B:=B)) @: a). *)
    a = inl @^-1: [set (inl (B:=B)) x | x in a].
  Proof.
    move => A B a.
    apply/setP => //= x.
    rewrite inE.
(*
1 subgoal

A, B : finType
a : {set B}
x : B

========================= (1 / 1)

(x \in a) = (inl x \in [set inl x0 | x0 in a])
*)

Is there some lemma that can help? I did a few Search-es, but couldn't spot any.

view this post on Zulip Quentin VERMANDE (Apr 08 2024 at 12:55):

Maybe mem_imset (found with Search imset mem, or more easily with Search (_ _ \in imset _ _) but that requires knowing what the notation hides).

view this post on Zulip Julin Shaji (Apr 08 2024 at 17:01):

mem_imset helped!

But I kind of ended up doing things a bit 'manually'..

  Lemma inl_inj {A B: Type}: injective (rT:=A+B) inl.
  Proof.  by rewrite /injective => ? ?; case.  Qed.

  Lemma foo2: forall {A B: finType} (a: {set A}),
    a = inl @^-1: [set (inl (B:=B)) x | x in a].
  Proof.
    move => A B a.
    apply/setP => //= x.
    rewrite finset.inE.
    symmetry.
    exact: (mem_imset (aT:=A) (rT:=A+B)%type inl a x inl_inj).
  Qed.

Could there be a better way to do this?

view this post on Zulip Quentin VERMANDE (Apr 08 2024 at 18:12):

You should not have to write finset., and you should be able to rewrite mem_imset just after inE.


Last updated: Jul 25 2024 at 15:02 UTC