Stream: new members

Topic: not p versus p implies false

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.)

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

Bryan Gin-ge Chen (Sep 10 2020 at 04:45):

Can you post a #mwe?

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

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.

Kevin Buzzard (Sep 10 2020 at 06:15):

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

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.

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.

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

Kevin Buzzard (Sep 10 2020 at 06:26):

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

Kevin Buzzard (Sep 10 2020 at 06:26):

I don't think lean does it by default

Kenny Lau (Sep 10 2020 at 06:26):

or as I say, never unfold definitions

Right

Kevin Buzzard (Sep 10 2020 at 06:26):

If you're unfolding definitions you could be writing API

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.

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.)

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

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).

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

Mario Carneiro (Sep 10 2020 at 08:06):

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

@Michael Beeson

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