Stream: math-comp users

Topic: A proof with {set unit}


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

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

How would you prove it with pen and paper?

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

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

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