not p versus p implies false

Stream: new members

[Michael Beeson]

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]

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]

Can you post a #mwe?

[Kevin Buzzard]

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]

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]

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

[Michael Beeson]

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]

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.

[Michael Beeson]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

I don't think lean does it by default

[Kenny Lau]

or as I say, never unfold definitions

[Kevin Buzzard]

Right

[Kevin Buzzard]

If you're unfolding definitions you could be writing API

[Michael Beeson]

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]

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]

@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]

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]

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]

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

[Mario Carneiro]

@Michael Beeson

[Kevin Buzzard]

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

[Mike Shulman]

Kevin Buzzard said:

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

I don't understand what you mean by that. Most dependent type theories like MLTT and CIC have decidable and transitive definitional equality.

[Jeremy Avigad]

In his MS thesis (https://github.com/digama0/lean-type-theory/releases/tag/v1.0), Mario showed that the combination of singleton elimination and definitional proof irrelevance has bad theoretical properties. Roughly, you can repeatedly replace a well-foundness prop by an equivalent one and unroll a computation another step, so that deciding whether you can get to 0 that way is equivalent to deciding the halting problem. You can decide where to lay the blame, but if you want Lean's definitional equality to have the properties above and be transitive, then it is undecidable.

Thierry Coquand and Andreas Abel went a step further, and showed that you get a failure of normalization: https://arxiv.org/abs/1911.08174. To type theory purists, these features are pretty damning (though maybe less shocking than Agda's type in type). But most Lean users aren't bothered by it. The type system works really well, and definitional proof irrelevance is a nice feature to have when you are formalizing mathematics.

[Mike Shulman]

What do you mean by "Agda's type in type"? Agda and Coq both have an optional type-in-type feature, but it's not part of the core theory.

[Jeremy Avigad]

I meant only that the normalization issue does not affect soundness. In theory, it can have bad effects for type checking, but in practice, it's not a problem.

[Mike Shulman]

Ok, I see, thanks.

Am I right that this problem is solved by the "SProp" now available in Coq and Agda by having only a restricted form of singleton elimination?

[Mario Carneiro]

@Mike Shulman Last I checked, I believe SProp is also susceptible to the Coquand-Abel counterexample. It is a really general result

[Mike Shulman]

The end of the Coquand-Abel paper you linked to says

The type-theoretic proof assistants Agda and Coq have recently [GCST19] been equipped with a proof-irrelevant universe of propositions (“strict Prop”). In this universe, propositional equality can be defined, but cannot be eliminated into types that are not strict propositions themselves. Under this restriction, Gilbert [Gil19, 4.3] formally proved normalization and decidability of type checking for the predicative case.

[Mario Carneiro]

"For the predicative case" seems like a bit of an ask

[Mario Carneiro]

That's probably fine for Agda but not for Coq

[Mike Shulman]

The next paragraph says the impredicative case is an open question. So it's at least not obvious that their counterexample applies.

[Mario Carneiro]

I guess the restriction under consideration here is that cast : A = B -> A -> B only works when A and B are SProp? That seems restricted to the point of uselessness

[Mario Carneiro]

I don't use Coq so I don't know how much this SProp thing actually gets used or what the community norms around it are

[Mike Shulman]

I haven't used Coq much myself since SProp was introduced, and we don't use it in the HoTT library anyway, so I couldn't tell you. Although one of the points of SProp is to be compatible with univalence, which definitely rules out a cast along a proof-irrelevant equality for types that aren't propositions.

I can see that that isn't what you want, but I just wanted to clarify the situation. It sounds like you can pick two out of the three of complete and decidable type- and equality-checking, definitional proof irrelevance, and singleton elimination. SProp pushes on that a little by giving you the first two plus some singleton elimination.

[Mario Carneiro]

Ah, I suppose that's true. Definitional proof irrelevance is not very important for lean in practice - I think propositional would be fine - but it has a great simplifying effect on the mental model of how these types work, by restricting them to "sets" in your parlance. A set theoretic universe is a well understood construct

[Mike Shulman]

I'm happy to hear that definitional proof irrelevance isn't that important in practice. Personally, I think the right approach is to construct a mental model around propositional equality, not definitional equality. Not every type may be a set, but those that are -- propositionally so -- should form an equally familiar set-theoretic universe from that point of view. However, this is the lean zulip, not the HoTT zulip, so I'll shut up now. (-:O

[Jeremy Avigad]

Definitional proof irrelevance is not very important for lean in practice

@Mario Carneiro are you sure that is true? When we use e.g. fin n, you do calculations and apply hypotheses as long as the values match. I was under the impression that it would be a real mess if we had to do extra work to make the proofs of i < n match.

[Floris van Doorn]

I imagine that Mario was talking about the case where we only had propositional proof irrelevance instead of definitional proof irrelevance. Without propositional proof irrelevance, I think life would be a lot harder in many places, but with it, you can do most of the same things as we currently can in Lean. For things like fin you can just call an extensionality lemma first (and specifically in the case of fin things will also be fine in without any proof irrelevance - since you can prove that < and ≤ on ℕ are subsingletons without proof irrelevance).