Stream: new members
Topic: How to "unpack" notation?
Abhimanyu Pallavi Sudhir (Oct 14 2018 at 16:31):
How can I "unpack" notation like
∩, etc.? I want to convert a proposition of the form
x ∉ S to
x ∈ S → false. Is this possible just definitionally or do I need to apply some lemma?
Abhimanyu Pallavi Sudhir (Oct 14 2018 at 16:33):
You'd think just
change should work, but it doesn't seem to do anything.
Bryan Gin-ge Chen (Oct 14 2018 at 16:37):
This doesn't directly answer your question (which I think might be more a matter of how to get lean to avoid printing certain notation), but given
h : x ∉ S and
H : x ∈ S, the term
h H is
false. For this reason I don't think I've ever needed to change things like you're describing.
Abhimanyu Pallavi Sudhir (Oct 14 2018 at 16:38):
But in that case, shouldn't
not_forall_not work on something of the form
¬∀ (x : S), x ∉ T? It gives me an error
invalid rewrite tactic, failed to synthesize type class instance.
Rob Lewis (Oct 14 2018 at 16:41):
not_forall_not requires the predicate to be decidable. Try putting
local attribute [instance] classical.prop_decidable somewhere above your proof.
Abhimanyu Pallavi Sudhir (Oct 14 2018 at 16:42):
That works, thanks. But what exactly does it do? Does it just tell Lean that all propositions are decidable or is there something more? (If so, is it really any different from classical.em?)
Rob Lewis (Oct 14 2018 at 16:53):
Yes, it adds a (local) type class instance that tells Lean all propositions are decidable. It's derived from classical.em.
Rob Lewis (Oct 14 2018 at 16:55):
A lot of things are written using decidability instances, like the
if p then _ else _ notation. If you're working classically and don't care about decidability, you need that line at the top of your file.
Abhimanyu Pallavi Sudhir (Oct 14 2018 at 16:56):
Ah ok -- so both em and prop-decidable follow from the same mathematical law, but have different types.
Rob Lewis (Oct 14 2018 at 16:59):
em produces a proof,
prop_decidable produces data.
Kevin Buzzard (Oct 14 2018 at 17:39):
Abhi -- whenever you see a
failed to synthesize type class instance error this means that the type class inference machine (the square bracket machine) has failed. The error often shows exactly what it has failed to construct (it was trying to fill in a variable you did not give it explicitly because it was in square brackets, and the goal in the error is the type of the term it failed to construct).
import logic.basic #check @not_forall_not
shows you that for this function to run in the usual way (i.e. without any messing around with
@) Lean needs to get the type class machine to produce a proof of
decidable (∃ (x : α), p x). If
p is random then Lean can't do this (because there are examples in computer science where this sort of this really is not decidable). But note that
(∃ (x : α), p x) is a proposition, so if you decide to be a mathematician and work in our wonderful world where every proposition is decidable (indeed, in classical mathematics there is no notion of decidability), then you can tell the type class inference machine that this is what you want to do by feeding the relevant definition into the machine.
Now if you were making the definition "all propositions are decidable" from scratch you could just use the
instance keyword instead of the
definition one, but in this case the relevant claim that all propositions are decidable is already a definition (
classical.prop_decidable) and it's in core Lean. The issue is hence that this definition is not something which the machine knows about. Rob's trick
local attribute [instance] classical.prop_decidable (and actually from experience I would recommend instead
local attribute [instance, priority 0] classical.prop_decidable) tags the definition with the "instance" tag, which is exactly what you need to do to make the type class inference machine notice it.
You can learn more about type class inference in chapter 10 of Theorem Proving In Lean
Kevin Buzzard (Oct 14 2018 at 17:46):
But back to the original question -- I remember well wanting to know exactly the same as what you want to know now. Here are some tips.
1) Before the statement of whatever you are working on, you can switch notation off completely, by writing
set_option pp.notation false. Example:
set_option pp.notation false #check 1 ∈ (@set.univ ℕ) -- has_mem.mem 1 set.univ : Prop
If you want to unfold even further, there is a command for that: the
set_option pp.notation false example : 1 ∈ (@set.univ ℕ) → false := begin unfold has_mem.mem, unfold set.mem, unfold set.univ, sorry end
When I was trying to figure out what the hell was going on, I wrote a lot of code which looked like this. You can write each line after you've seen the goal at the end of the line before. The
unfolds do not change the goal at all (I think), they just change the way it is displayed. So once you've unfolded enough to figure out what's going on you can actually just delete all the
unfolds. Also you can write them all in one line (
unfold X Y Z ...) (no commas).
Abhimanyu Pallavi Sudhir (Oct 14 2018 at 17:57):
@Kevin Buzzard "The unfolds do not change the goal at all" -- the same applies to
change, doesn't it? Except you need to actually supply what you want to change things to. I've been using that to clarify things so far.
unfold is nice, but with
change I can actually figure out the answer without Lean telling me.
Patrick Massot (Oct 14 2018 at 18:08):
unfold does change the goal, there are proofs where you cannot remove an
Kevin Buzzard (Oct 14 2018 at 19:44):
For goals you use
show, for hypotheses you use
change. I have no idea why different words are used for these.
Abhimanyu Pallavi Sudhir (Oct 14 2018 at 19:45):
change works on goals too -- just don't put an
Patrick Massot (Oct 14 2018 at 19:46):
Patrick Massot (Oct 14 2018 at 19:46):
I never understood the difference between this use of
change. I always use
change since it's more descriptive
Kevin Buzzard (Oct 14 2018 at 20:03):
changeworks on goals too -- just don't put an
Mario Carneiro (Oct 14 2018 at 20:07):
show are almost exactly the same. One difference is that
show will also switch to another goal if it matches what you say when the first goal doesn't
Mario Carneiro (Oct 14 2018 at 20:08):
change also has
change with which is like definitional
Last updated: May 12 2021 at 04:19 UTC