Stream: math-comp users

Topic: Proof involving set equality

Julin Shaji (Apr 08 2024 at 05:09):

I got a function like:

``````From mathcomp Require Import all_ssreflect.

Definition foo: {set unit} -> bool :=
fun s => if s == set0 then false else true.
``````

Now, I'm trying to prove this:

``````Goal
foo set0 = false.
Proof.
rewrite /foo.
case (set0 == set0) eqn:H.
(*
2 subgoals

H : (set0 == set0) = true

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

false = false

========================= (2 / 2)

true = false
*)
``````

But we can't pattern match in the usual sense for set, right?
Is it still possible to do this proof?

Quentin VERMANDE (Apr 08 2024 at 07:20):

Did you `Search` for lemmas using things that appear in your goal?

Julin Shaji (Apr 08 2024 at 07:40):

I had tried `Search set0.` but didn't spot anything that seemed usable here.
Also tried `Search set0 (_ == _).` but didn't find any there either..

Julin Shaji (Apr 08 2024 at 07:42):

And it's not a good idea to attempt to use the `ffun` underlying a set directly, right?

Julin Shaji (Apr 08 2024 at 09:28):

Could prove a similar thing after rephrasing `foo`:

``````Definition foo': {set unit} -> bool :=
fun s => if (mem s) tt then true else false.

Goal
foo' set0 = false.
Proof.
by rewrite /foo' /= inE.
Qed.
``````

Reynald Affeldt (Apr 08 2024 at 09:59):

you can maybe write `foo` as `fun s => s != set0.` and rewrite with the lemma `eqxx` to prove your goal.

Quentin VERMANDE (Apr 08 2024 at 10:05):

You needed to `Search (_ == _)` which would have shown `eq_refl` as the first result (of which `eqxx` is a notation). Now, `by rewrite /foo eqxx.` solves the goal.

Julin Shaji (Apr 08 2024 at 10:09):

Thanks.

Last updated: Jul 15 2024 at 19:01 UTC