Unprovable statement

[sacerdot]

Theorem foo: forall P Q, nabla (x : o), { [ P ] |- Q x} -> nabla y, Q x = Q y.

seems unprovable (to me). It is provable for all rigid Ps and I expect it to be provable in the general case. I don't want an enumeration of the formulas of P and I know that stating the equality between P and Q x is unsound. However, I have the impression that restricting Q over x (i.e. forcing the set of visible names to be the same) should be sound. I don't have a formal proof though.

The consequence is that certain predicates over contexts must restrict the possible shapes of the contexts in situations where more loose specification would suffice. For example, I needed a predicate closed : olist -> term -> prop defined by recursion over the term that stated that every free name in the term had a declaration in olist (i.e. mem decl gamma). This should be sufficient, but it does not completely defines the shapes of entries in gamma. Therefore at a certain point I am faced with the unprovable goal above and the only solution seems to be to artificially restrict gamma (using another predicate) to describe all its possible entries.

[chaudhuri]

This is an interesting case. I gave it a bit of thought and I don't see an obvious way to relax our no-flexible-heads restriction to admit this case while avoiding the bug that made that restriction necessary.

I'll discuss this with Dale and others.

[chaudhuri]

I think there is no way to do something like this without risking unsoundness. I'm closing this, but feel free to reopen if anyone has any bright ideas.

(Please also see your email, Claudio. I gave a counterexample there.)

[lambdacalculator]

Can we have that example, or references to examples, in this ticket? I've also wondered about these rigidity restrictions and, as a catalyst for possible bright ideas, would like to have some examples to think about. Thanks.

[sacerdot]

I cannot edit the closed ticket anymore, but you can find in attachment the code. It is part of an exercise I gave to a student. It define the untyped lambda-calculus, a variant where all functions are binary and a compilation of the second calculus into the first. There is just one skip in the .thm file and that's the unprovable statement.

As Kaustuv pointed out, the statement only makes sense when P is a predicate. Otherwise it can later be instantiated with (forall x, P x) leading to an inconsistency.

The way to complete the development without skipping anything is to declare a new predicate over contexts that states the exact shape of everything in Gamma so that the skipped theorem becomes provable. We did that, but it is something quite annoying to do.

Cheers, C.S.C.

On Tue, 2018-04-03 at 18:26 +0000, lambdacalculator wrote:

Can we have that example, or references to examples, in this ticket? I've also wondered about these rigidity restrictions and, as a catalyst for possible bright ideas, would like to have some examples to think about. Thanks. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread. -- Prof. Claudio Sacerdoti Coen Department of Computer Science and Engineering University of Bologna

[chaudhuri]

@lambdacalculator: sorry, I should have put that here as well. Here's a relevant excerpt from the email discussion.

Theorem foo: forall P Q, nabla (x : o),

{ [ P ] |- Q x} -> nabla y, Q x = Q y.

seems unprovable (to me). It is provable for all rigid Ps and I expect it to be provable in the general case.

This can't be provable in the general case because the support of an assumption---anything to the left of the |- in object sequents---can always grow. For instance, imagine we had this situation:

{ [ pi x\ p x ] |- p n1 }

This sequent is provable, but it doesn't imply that p n1 = p n2.