Zulip Chat Archive

Stream: new members

Topic: not equals


view this post on Zulip 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 ??

view this post on Zulip Kenny Lau (Sep 05 2020 at 16:08):

#backticks

view this post on Zulip Kenny Lau (Sep 05 2020 at 16:09):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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??

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 05 2020 at 16:18):

#print my_lemma

view this post on Zulip Michael Beeson (Sep 05 2020 at 16:20):

So "try to" means "do not".

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Alex J. Best (Sep 05 2020 at 16:25):

(deleted)

view this post on Zulip 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?

view this post on Zulip Rob Lewis (Sep 05 2020 at 16:26):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 05 2020 at 16:28):

Is there a tactic interface to #print axioms?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 17:07):

Throw in some type annotations

view this post on Zulip 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 @"

view this post on Zulip 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