Squash Stability and Hidden Hypotheses

A hidden hypothesis P in a sequent can be unhidden if one of two conditions are met:

1. The proposition P is squash stable.
2. The conclusion of is squash stable.

A proposition is squash stable  if it is possible to figure out what its computational content is, given that you know that some computational content  exists (in the classical sense). The computational content of a proposition is some term that inhabits the proposition when it is considered as a type.

The squash stable predicate is defined in the core_2 theory as follows:

The proposition   (read `squash P  ') is considered true exactly when P is true. However, P's computational content when true can be arbitrary whereas 's computational content when true can only be the trivial constant term that inhabits the unit type. ( is defined as where x does not occur free in P).

As with decidability, it turns out that the property   can be inferred for many P from knowing that for the immediate subterms Q of P. It is also true that for any P. The tactic ProveSqStable takes advantage of these facts and attempts to prove goals of the form

by backchaining with any lemmas in the Nuprl library that have names with the prefixes sq_stable__ or decidable__ (note the two underscores in each case). There are many examples of such lemmas in the core_2 theory.

Since ProveSqStable  can be rather slow, it isn't called by the D tactic when D is applied to a set type hypothesis . However, D does check the sequent conclusion for trivial ways in which it might be squash stable.

The D tactic does recognise property lemmas  for abstractions that are wrapped  around set types. Property lemmas state that particular set type predicates are squash stable. If D is applied to an abstraction wrapped around a set type and there is a property lemma for the abstraction, then the predicate of the set type is always added unhidden to the hypothesis list.

Consider some abstraction where the are variables that have been slotted in for the immediate subterms of A. Say that unfolds to . Then the property lemma for A should have form

and should be named opid _properties  where opid is the opid of A. Examples of properties lemmas can be found in the theory int_1. Property lemmas can often be completely proven using the tactic ProvePropertiesLemma  .

Tactics related to unhiding are as follows:

UnhideSqStableHyp i

Hypothesis i should be a hidden hypothesis. This tactic tries to prove the hidden hypothesis squash stable using ProveSqStable.

This tactic tries to prove the conclusion squash stable using ProveSqStable. If it succeeds in this, all hidden hypotheses are unhidden.

Tries to unhide hidden hypotheses, first by checking whether the conclusion is squash stable and then, if this fails, by checking whether each hidden hypothesis is squash stable.

Hypothesis i should be declaration of form A or a proposition of form or where in either case A is an abstraction with a properties lemma. AddProperties adds the predicate part of the set type underlying A as a new hypothesis immediately after i. It does not change hypothesis i.