Zulip Chat Archive

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 ??

Kenny Lau (Sep 05 2020 at 16:08):

#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?

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

(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: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib