Zulip Chat Archive

Stream: new members

Topic: not p versus p implies false


view this post on Zulip Michael Beeson (Sep 10 2020 at 04:40):

I thought not p and p-> false were the same. But:
If I do
have h30: ¬ (c ∈ p):= λ h, (h3 (h29 h)), I get h30: ¬ (c ∈ p)
but if I do
have h30 := λ h, (h3 (h29 h), I get h30: p -> false.
What's up with that?
(This is not meant to be a working example. And my proof is working, so it's just a question about
what is going on, nothing needs to be fixed.)

view this post on Zulip Johan Commelin (Sep 10 2020 at 04:43):

They are defeq. I don't know what c \in p in your example means, but it looks like it is the same as p

view this post on Zulip Bryan Gin-ge Chen (Sep 10 2020 at 04:45):

Can you post a #mwe?

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

They are not syntactically equal but they are definitionally equal. You can move between them with change and in term mode but tactics like rw are sensitive to the difference

view this post on Zulip Michael Beeson (Sep 10 2020 at 06:14):

Here's a MWE:

variables (p r s:Prop)

example:(¬ r  (s  r)  ¬ s):=

   begin
     intro h2,
     intro h3,
     have h4:= λ h, (h2 (h3 h)),
     have h5:¬ s:= λ h, (h2 (h3 h)),
     exact h4,   -- or exact h5, both work
   end

So put your cursor before the exact h4 step and note the difference between h4 and h5.

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 06:15):

exact sees through definitional equality. I don't understand the question.

view this post on Zulip Michael Beeson (Sep 10 2020 at 06:21):

The observation is that h4 gets type s-> false rather than ¬ s:
The question, if there is one here, is why that is? Those two types are "definitionally equal", which I think (but am not sure)
means "have the same normal form after beta, eta, and delta reduction." So which one IS the normal form, s->false or ¬ s ?
I guess it is s -> false and then ¬ s reduces to s-> false, since that's the type you get from h4. But when in h5, you specify the
type, then it prints the type I specified (¬ s) since they have a common reduct.

So the Lean type system is rather complex and with all those legal reductions it's problematic whether it really has
strong normalization. How do we know that it does? Well, that is a question that goes far beyond the original curiosity so please feel free to ignore it. I don't want to get distracted into theoretical stuff, I'm trying to check a proof.

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 06:24):

I am not a logician, I'm not sure I understand your question. Lean does not unfold definitions by default, but will do so if you ask it to.

view this post on Zulip Michael Beeson (Sep 10 2020 at 06:25):

OK let's forget about this, it's not interfering with my proof at all.

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 06:25):

I deal with super-complex terms in eg commutative algebra and some terms might not even have a normal form, or if they do I don't want to see it

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 06:26):

Deciding whether to proceed by unfolding a definition or not is very situation-dependent

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 06:26):

I don't think lean does it by default

view this post on Zulip Kenny Lau (Sep 10 2020 at 06:26):

or as I say, never unfold definitions

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 06:26):

Right

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 06:26):

If you're unfolding definitions you could be writing API

view this post on Zulip Michael Beeson (Sep 10 2020 at 06:27):

I read in the manual that you can tag your definitions with certain tags (attributes) to control when they will be unfolded during rewriting. But so far I'm doing fine controlling it manually. And I'm unfolding definitions all the time, usefully.

view this post on Zulip Kyle Miller (Sep 10 2020 at 06:30):

In case it's helpful, in core.lean the definition of logical negation is

def not (a : Prop) := a  false
prefix `¬` := not

(I think definitional equality in Lean works by trying to unify two lambda expressions, unfolding definitions as needed. It's on a best-effort basis, and I think the only guarantees are (1) it notices when things are obviously the same and (2) it won't say two things are definitionally equal if they aren't.)

view this post on Zulip Kenny Lau (Sep 10 2020 at 06:32):

@Michael Beeson I can tell you a list of rules, which you won't remember, or you can just learn it by osmosis the way everyone did

view this post on Zulip Mario Carneiro (Sep 10 2020 at 08:04):

So which one IS the normal form, s->false or ¬ s ?
I guess it is s -> false and then ¬ s reduces to s-> false, since that's the type you get from h4. But when in h5, you specify the
type, then it prints the type I specified (¬ s) since they have a common reduct.

The normal form is s -> false. You can test this with #reduce. But, and this is important, when lean tests for definitional equality it does not reduce both sides to a normal form and test the result for equality. Semantically it's equivalent to that, but that would be far too expensive in most cases (and #reduce is pretty unusable for reasonable sized terms for this reason). Instead, it selectively unfolds definitions on both sides, and uses heuristics to try to luck out and find that two things are syntactically equal and hence defeq, or that they have different head constructors and cannot be defeq, with some edge cases that involve doing lots of unfolding, potentially as far as the normal form (which is the worst case scenario).

view this post on Zulip Mario Carneiro (Sep 10 2020 at 08:05):

So the Lean type system is rather complex and with all those legal reductions it's problematic whether it really has
strong normalization.

It doesn't

view this post on Zulip Mario Carneiro (Sep 10 2020 at 08:06):

Lean's consistency is based on a model theoretic argument, not a syntactic one

view this post on Zulip Mario Carneiro (Sep 10 2020 at 08:06):

@Michael Beeson

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 10:54):

Lean's refl isn't transitive (because it's decidable).


Last updated: May 14 2021 at 04:22 UTC