Allow reasoning level constraints in specifications

[chaudhuri]

It is often very useful to be able to refer to reasoning formulas from the specification logic. A common use case is not and = in the spec, which are supported by Teyjus but not by Abella. To preserve stratification, such "callbacks", which I am calling constraints, must not themselves use the seq or prog definitions, i.e., they cannot involve the spec level provability relation. Moreover, in order to support inst, it must be the case that these formulas contain no nominal constants or nabla.

The proposed syntax is $(metaterm) as an allowed element of the body of a clause (i.e., adding $ : prop -> o in specification formulas), where the metaterm is constrained to be constructed out of: conjunction, true, disjunction, false, implication, equality, forall, and exists. Disallowed are nabla and {}.

The interpretation adds the following cases to the seq predicate:

{ G |- $(F) }  :=  F ;
{ G, [$(F)] |- C } := F -> { G |- C }

It remains to be proved but seems plausible that cut will hold.

[agacek]

It seems like you would get into trouble with negation. Couldn't you prove something like pi x\ not (x = app M N) and then use instantiation to later have 'not (app M N = app M N)'?

[chaudhuri]

In my mental model, this would be disallowed because {pi x\ $(x = app M N -> false)} reduces to nabla n, {$(n = app M N -> false)} which does not further reduce because it violates the "no nominal constants inside constraints" rule. In other words, the rule is:

{ G |- $(F) } := F   if  supp(F) = {}.

Or, if the interpretation of {} cannot be made partial, then it amounts to:

{ G |- $(F) } := (supp(F) = {}) -> F.

I suppose this is not strictly OK since G doesn't provide a supp operator. An alternative would be to extend the "no nominal constants" condition to "no nominal constants or pi-bound variables".

The main use case of this is an if-then construct that looks like:

ifeq M N Then Else :- $(M = N), Then.
ifeq M N Then Else :- $(M = N -> false), Else.

This would continue to be possible under any of the restrictions.

[chaudhuri]

Just an addendum, the whole reason for this proposal is to avoid defining a eq and neq by hand. I should have said this earlier.

[lambdacalculator]

This is a very old but still open thread. I'm wondering whether another thought I've had a few times now might be relevant to the same aim. Often in a development, I have to put definitions in the theorem file, rather than the module file, because they use variables in a way that cannot be achieved in the specification language. A very simple example is the var predicate:

Define var : exp -> prop by
  nabla x, var x.

My idea is extending the specification language to include pis in the head, like so:

%% sig file
type var : exp -> o.

%% mod file
pi x\ var x.

I haven't looked at every case, but it seems that this could be achieved by an already existing case of the seq predicate:

{ G |- pi E }  :=  nabla x, { G |- E x };

In other words, it may just be a matter of changing the parser for specification files.

[lambdacalculator]

I'll add one more comment to this issue on the original suggestion, which I still think is good. One thing that I am often faced with in defining specification predicates over types with large numbers of constructors is the lack of a way to achieve a Prolog-like cut:

p(a) :- !, q(a).
p(X) :- r(X).

which, on a type with 20 constructors (and assuming I couldn't tolerate any overlap) would save me 19 clauses. With (in)equality, I could write

p(a) :- q(a).
p(X) :- $(X = a -> false), r(X).   % or better, $(X /= a)

In the same vein, the disjunction in the clause

p(X) :- q(X,Y), r(Y,Z), (s(Z) ; t(Z)).

would also have an easy translation to G, namely

exists Y Z, { G |- q X Y } /\ { G |- r Y Z } /\ ( { G |- s Z } \/ { G |- t Z } )

which is better than having to use the existing alternative:

p(X) :- q(X,Y), r(Y,Z), s(Z).
p(X) :- q(X,Y), r(Y,X), t(Z).

where I've purposefully inserted a typo to indicate one of many disadvantages of having to write delayed conjunctions this way!