Stream: math-comp users

Topic: Proof involving set equality


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

view this post on Zulip Quentin VERMANDE (Apr 08 2024 at 07:20):

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

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

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

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

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

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

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

Thanks.


Last updated: Jul 15 2024 at 19:01 UTC