Zulip Chat Archive

Stream: new members

Topic: push_neg takes non-intuitionistic step

view this post on Zulip Michael Beeson (Nov 25 2020 at 19:49):

h6: ¬¬(Nc M (Φ M (𝕋 M m)) = two  Nc M (Φ M (𝕋 M m)) = three)

Then push_neg at h6 removes the double negation, instead of just pushing one negation. Up until now, I have never seen
push_neg take an intuitionistically incorrect step. Now I need to be triple-vigilant to check the axioms used in my proofs.
Too bad about this as offhand I do not know how to push just the one negation.

view this post on Zulip Ruben Van de Velde (Nov 25 2020 at 20:18):

Perhaps the documentation should be clearer on that

view this post on Zulip Johan Commelin (Nov 25 2020 at 20:24):

@Michael Beeson I am afraid that you are fighting uphill, because mathlib is very decidably classical. Supporting intuitionistism is not on one of our priorities, and hence we also don't point out every occurence of classical or intuitionistic arguments.

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 20:25):

Maybe use the lemmas that do the rewriting instead of push_neg?

Last updated: May 15 2021 at 00:39 UTC