## Stream: new members

### Topic: not equals

#### Michael Beeson (Sep 05 2020 at 16:07):

 h3: ∀ a b:M, (a ≠ b ↔ ¬ (a = b)) := begin ifinish, end 
This fails, specifically "solve1 tactic failed, focused goal has not been solved".
I got here because something that should rewrite a certain equality did not rewrite when I had \neq instead of = .
So apparently \neq is not just an abbreviation for not equal ??

#backticks

#### Kenny Lau (Sep 05 2020 at 16:09):

\ne is just an abbreviation for not equals, but some tactics cannot see through abbreviations

#### Rob Lewis (Sep 05 2020 at 16:12):

What you've posted isn't a #mwe and it's missing something relevant, because this works fine:

import tactic.finish

example {M : Type} : ∀ a b : M, a ≠ b ↔ ¬ a = b :=
by ifinish


#### Michael Beeson (Sep 05 2020 at 16:14):

Yes, something trivial was wrong with the posted syntax, and I guess Kenny Lau's answer explains the original problem.
So the moral is, I should just use neg (a=b) and never use a \neq b.

#### Rob Lewis (Sep 05 2020 at 16:14):

But also note that ifinish and ifriends aren't advertised for a reason.

import tactic.finish

example (p : Prop) : ¬ ¬ p → p :=
by ifinish


#### Michael Beeson (Sep 05 2020 at 16:16):

Ouch! I've been using ifinish under the assumption that it is intuitionistic. That's what it says in the file where it's defined.

#### Michael Beeson (Sep 05 2020 at 16:18):

Someone told me once about a command to see what axioms have been used in a file. What was that again?
I've used ifinish many times to polish off the last few steps. Now my whole development might not be intuitionistically correct??

#### Rob Lewis (Sep 05 2020 at 16:18):

See the top of that file.

The variants ifinish, iclarify, and isafe try to restrict to intuitionistic logic. But the
done tactic leaks classical logic:

lean
example {P : Prop} : ¬¬P → P :=
by using_smt (do smt_tactic.intros, smt_tactic.close)


They also do not work well with the current heuristic instantiation method used by ematch.
So they are left here mainly for reference.


#### Johan Commelin (Sep 05 2020 at 16:18):

#print my_lemma

#### Michael Beeson (Sep 05 2020 at 16:20):

So "try to" means "do not".

#### Alex J. Best (Sep 05 2020 at 16:23):

It means "does not always", you can always #print axioms my_classical_lemma_name to check if it did anything non-classical though.

#### Reid Barton (Sep 05 2020 at 16:24):

There has to be a joke involving "do or do not" and classical logic in here somewhere

#### Michael Beeson (Sep 05 2020 at 16:24):

How can I use #print axioms on my whole file at once to check if it is really intuitionistically correct?

(deleted)

#### Michael Beeson (Sep 05 2020 at 16:26):

And why should I (not to mention the referee of my journal article) believe that #print axioms is telling the truth about that?

#### Rob Lewis (Sep 05 2020 at 16:26):

AFAIK there's no per-file way to check, just per-declaration.

#### Michael Beeson (Sep 05 2020 at 16:28):

So after every lemma that uses ifinish, I have to put #print axioms <lemma_name> and check manually that
it doesn't list anything classical. I thought I was using a computer proof-checker.

#### Reid Barton (Sep 05 2020 at 16:28):

Is there a tactic interface to #print axioms?

#### Alex J. Best (Sep 05 2020 at 16:29):

Of course the ifinish situation is a bit unfortunate, and it is not intended to work in this way, but nobody has had the time+need+energy to fix it. As far as I know there is no obstacle to making a version of ifinish that really is intuitionistic.

#### Reid Barton (Sep 05 2020 at 16:42):

Here is a super hacky way to print all the axioms used by everything in the current file. Import it and invoke it with #axioms_all. You could grep the output for choice.

import tactic.core

section

open lean lean.parser

@[user_command] meta def axioms_all (_ : interactive.parse \$ tk "#axioms_all") : parser unit :=
do e ← get_env,
e.fold (return ()) (λ d rest, do
when (e.in_current_file d.to_name)
(do emit_command_here ("#check " ++ d.to_name.to_string),
emit_command_here ("#print axioms " ++ d.to_name.to_string),
return ()),
rest),
return ()

end


#### Michael Beeson (Sep 06 2020 at 17:05):

Reid, your code for #axioms_all works, and (happily) there's no "choice" in the output, so I'm good to go.
But, your code did produce a message I thought you should see:

invalid 'Model.no_confusion' application, elaborator has special support for no_confusion but the expected type must be known

#### Kevin Buzzard (Sep 06 2020 at 17:07):

Throw in some type annotations

#### Rob Lewis (Sep 06 2020 at 17:10):

This is almost certainly from the line #check Model.no_confusion that it generates. Simplest solution: in Reid's code, change "#check " to "#check @"

#### Reid Barton (Sep 06 2020 at 17:12):

This is a good idea anyway if you want to see the full types.

Last updated: May 08 2021 at 05:14 UTC