Stream: math-comp users

Topic: ✔ stuck at finding good relation between \in and \notin


view this post on Zulip walker (Oct 26 2022 at 14:25):

From mathcomp Require Import all_ssreflect zify .

Lemma foo {A: eqType}: forall (x: A) (l: list A), (x \in l -> False) -> x \notin l.
Proof.
move => x l x_not_in_l.
apply: negbT. (* x \in l = false*)
(* stuck here*)

I am not even sure if negbT is the right approach , I searched for \notin and ctrl+fed for reflect but didn't find anything useful.

view this post on Zulip Pierre Roux (Oct 26 2022 at 14:31):

Locate "\notin".

gives

Notation "x \notin A" := (negb (in_mem x (mem A))) : bool_scope (default interpretation)

and

Locate "\in"

gives

Notation "x \in A" := (in_mem x (mem A)) : bool_scope (default interpretation)

so \notin is just the boolean negation (negb) of \in and anything on negation (like negP for instance) should work.

view this post on Zulip walker (Oct 26 2022 at 15:13):

negP was the thing i was struggling to find, thanks!

view this post on Zulip Notification Bot (Oct 26 2022 at 15:13):

walker has marked this topic as resolved.


Last updated: Oct 13 2024 at 01:02 UTC