## Stream: math-comp users

### Topic: A proof with {set unit}

#### Julin Shaji (Apr 08 2024 at 18:12):

How can one proceed for a goal like:

 Goal forall a:{set unit},
(tt \in (if if tt \in a then true else false then [set tt] else set0)) =
(tt \in a).
Proof.
move => a.


I'm having trouble figuring out ways to look for suitable lemmas again.. :grimacing:

#### Quentin VERMANDE (Apr 08 2024 at 18:14):

How would you prove it with pen and paper?

#### Julin Shaji (Apr 08 2024 at 18:28):

In the paper proof, we could say that there are only 2 possible values that a can have, right?

So, I was thinking like this:

a is a set of unit values.
Since unit has only one possible value (tt), a is either set0 or [set tt].
If we could do case analysis on a, we would've had two cases.

case 1: a = set0.

(tt \in (if if tt \in set0 then true else false then [set tt] else set0)) =
(tt \in set0).

↓

(tt \in (if false then [set tt] else set0)) =
(tt \in set0).

↓

(tt \in set0) =
(tt \in set0).


case 2: a = [set tt].

(tt \in (if if tt \in [set tt] then true else false then [set tt] else [set tt])) =
(tt \in [set tt]).

↓

(tt \in (if true then [set tt] else [set tt])) =
(tt \in [set tt]).

↓

(tt \in [set tt]) =
(tt \in [set tt]).


#### Julin Shaji (Apr 08 2024 at 18:55):

I think I got something:

  Goal forall a:{set unit},
(tt \in (if if tt \in a then true else false then [set tt] else set0)) =
(tt \in a).
Proof.
move => a.
(* rewrite !unfold_in. *)
apply: set1_inj.
apply/setP; case.
- rewrite !inE.
by case (tt \in a) eqn:Hatt; rewrite inE.
- rewrite inE /=.
by case (tt \in a) eqn:Hatt; rewrite Hatt !inE.
Qed.


#### Quentin VERMANDE (Apr 08 2024 at 19:17):

Your informal proof is correct, but it is hard to do a case distinction on a. In the formal proof, you do the easier case analysis on tt \in a. Note that after the first case, the goal is basically the same as at the start of the proof, so you could directly do your case analysis on tt \in a and get a one-line proof.

Last updated: Jul 23 2024 at 20:01 UTC