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:

How would you prove it with pen and paper?

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

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

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