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.


Last updated: Jan 29 2023 at 19:02 UTC