Stream: math-comp analysis

Topic: boolp and contra


view this post on Zulip vlj (Sep 28 2020 at 18:05):

I'm having some troubles doing contra like tactic for classical_sets.
I'm trying to prove Y <> X /\ X `<=` Y -> X `<=` Y /\ (exists2 a : T, Y a & ~ X a)
So far I can prove that the goal can be rewritten as Y `\` X != set0. I'd like to use setD_eq0 by doing contraposition reasonning. Unfortunatly I don't know how to do : apparently contraPN is not available in classical_sets.v ("The reference contraPN was not found in the current environment.") despite all_ssreflect being imported.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2020 at 18:13):

@vlj contraPN was added recently, maybe your math-comp version is too old

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2020 at 18:13):

if so just copy to an aux library that you can remove when upgrading

view this post on Zulip vlj (Sep 28 2020 at 18:18):

ho ok didn't know

view this post on Zulip vlj (Sep 28 2020 at 20:02):

is there a double negation in boolp ?

view this post on Zulip vlj (Sep 28 2020 at 20:03):

err contrapT

view this post on Zulip Cyril Cohen (Sep 29 2020 at 13:12):

vlj said:

is there a double negation in boolp ?

notK ?

view this post on Zulip Cyril Cohen (Sep 29 2020 at 13:12):

(double negation elimination)

view this post on Zulip vlj (Sep 30 2020 at 12:26):

thanks ! will try to see if it simplify the proof

view this post on Zulip vlj (Sep 30 2020 at 12:34):

actually contra_not_neq is actually better fitter.


Last updated: Aug 11 2022 at 02:03 UTC