---

Comment: core_1_summary
Display forms for primitive terms of type-theory. Abstractions for 
propositions-as-types correspondence. Parenthesization control. 

Comment: core_1_intro
Defines display forms for primitive terms of Nuprl's type
theory, and introduces abstractions for propositions-as-types
correspondence. Also contains precedence objects that control
parenthesization of displays.  

Comment: graphic chars A0-AF
These are all the current nuprl graphic characters,
sorted by icode.

0x80 (128): ℙ|ℝ|ℕ|ℂ|ℚ|ℤ|𝕌|⇐|=|⇒|⌜|⌝|⊢|∫|⋅|↓
0x90 (144): α|β|∧|¬|∈|π|λ|γ|δ|↑|±|⊕|∞|∂|⊂|⊃
0xa0 (160): ⋂|⋃|∀|∃|⊗|↔|←|& #x2192|≠|∼|≤|≥|≡|∨|←|─
0xb0 (176): →|Σ|Δ|Π|×|÷|+|-|o|⊆|⊇|0|1|2|3| 
0xc0 (192): 𝔹|ρ|a|q|b|z|c

Comment: EndExtendedTermDForms
 
⋅

Comment: prec_com
Suggested uses for generic precedences are:
(examples given in ()'s)

In main_prec:
  preop     1 arg term with prefix text    (not, minus, squash)
  postop   1 arg term with postfix text   (pi1, pi2)
  inop      2 arg term with infix text     (compose, append)
  wk_preop  term with prefix and maybe infix text (mon_reduce) 
  wk_postop term with postfix and maybe infix text 
  bd_preop  term with prefix and maybe infix text (exists, for, lambda)
  bd_postop term with postfix and maybe infix text 

  The bd_*op are intended for terms that bind 1 or more variables in their
  rightmost argument. Having these weak precedences corresponds with 
  the convention that common binding terms have maximal scope.

  The exposed slot of pre and postop terms (including wk_* and bd_*) should 
  have E paren control so that ops can be stacked without adding 
  parenthesization.

  terms that use inop should use the infix_df_gen display form generator from
  the boot theory. This uses iteration control to suppress parenthesization of
  right associated term rather than E paren control, since then multiple
  dfs can use inop and will always be parenthesized when nested inside 
  one another.

In logic_prec:

  atomrel: atomic relations with infix and maybe postfix text (equal, member, lt)


A good place to add pointers to new auxiliary precedence objects is
in parallel with *arith_prec*.



Comment: PRIM_DISPS
display forms for primitive terms
⋅

Definition: computed_display def
=d ==
  if b is a pair then let x,y = b 
                      in if x="display-as"
                         then if y is a pair then let u,v = y 
                                                  in if u="decimal-rational" then fst(v) else b fi  otherwise b
                         else b
                         fi  otherwise b

Definition: axiom def
Ax ==  PRIMITIVE

Definition: equal def
s = t ∈ T ==  PRIMITIVE

Definition: sqequal def
This is Doug Howe's computational bi-simulation relation on terms.
We call if "squiggle" equality or `sqequal`.
It is equivalent to the conjunction of the comutational simulation
relations ⌜s ≤ t⌝ and ⌜t ≤ s⌝. (see: sqequalSqle)

The simulation ⌜s ≤ t⌝ is a coinductive relation 
on terms that says (essentially) that for any canonical form X, 
if s computes to ⌜X[a1;
                    a2;
                    ...]⌝ 
then there exist terms b1, b2,... such that 
t computes to ⌜X[b1;
                 b2;
                 ...]⌝
and ⌜a1 ≤ b1⌝,⌜a2 ≤ b2⌝,...

Using "Howe's trick" this relation is extended to open terms 
(i.e. terms with free variables) 
and proved to be a "contexual congruence relation".

It is an invariant of the Nuprl type system that all types are closed under
⌜s ~ t⌝. This justifies the rules for sqequal substitution
sqequalSubstitution
sqequalHypSubstitution 
 ⋅

s ~ t ==  PRIMITIVE

Definition: sqequal_n def
s ~n t ==  PRIMITIVE

Definition: sqle def
This is Doug Howe's computational simulation relation on terms.
We call if "squiggle" less-or-equal or `sqle`.

The simulation ⌜s ≤ t⌝ is a coinductive relation 
on terms that says (essentially) that for any canonical form X, 
if s computes to ⌜X[a1;
                    a2;
                    ...]⌝ 
then there exist terms b1, b2,... such that 
t computes to ⌜X[b1;
                 b2;
                 ...]⌝
and ⌜a1 ≤ b1⌝,⌜a2 ≤ b2⌝,...

See also the documentation for ⌜s ~ t⌝.⋅

s ≤ t ==  PRIMITIVE

Definition: sqle_n def
s ≤n t ==  PRIMITIVE

Definition: universe def
Type ==  PRIMITIVE

Definition: void def
Void ==  PRIMITIVE

Definition: atom def
Atom ==  PRIMITIVE

Definition: base def
Base ==  PRIMITIVE

Definition: token def
"$token" ==  PRIMITIVE

Definition: int def
ℤ ==  PRIMITIVE

Definition: object def
Object ==  PRIMITIVE

Definition: natural_number def
$n ==  PRIMITIVE

Definition: minus def
-n ==  PRIMITIVE

Definition: add def
n + m ==  PRIMITIVE

Definition: subtract
n - m ==  n + (-m)

Definition: multiply
n * m ==  PRIMITIVE

Definition: divrem def
divrem(n; m) ==  PRIMITIVE

Definition: divide def
n ÷ m ==  let q,r = divrem(n; m) in q

Definition: remainder def
n rem m ==  let q,r = divrem(n; m) in r

Definition: ind def
I(v) where I(α) = 
  when x = α < 0,  y = I(α+1).  d[x; y]
  when α = 0.  b
  when  w = α > 0,  z = I(α-1).  u[w; z]
end where  ==
  PRIMITIVE

Definition: union def
left + right ==  PRIMITIVE

Definition: inl def
inl x ==  PRIMITIVE

Definition: inr def
inr x  ==  PRIMITIVE

Definition: decide def
case b of inl(x) => s[x] | inr(y) => t[y] ==  PRIMITIVE

Definition: product def
x:A × B[x] ==  PRIMITIVE

Definition: pair def
<a, b> ==  PRIMITIVE

Definition: spread def
let x,y = A in B[x; y] ==  PRIMITIVE

Definition: function def
x:A ⟶ B[x] ==  PRIMITIVE

Definition: isect def
The intersection of a family of types is a new primitive type.
Its partial equivalence relation is the intersection of all the
partial equivalence relations in the family.

Thus,  u = v in ⋂x:A. B[x] just when  u = v in B[x] for every ⌜x ∈ A⌝.

Viewed a proposition, the intersection type can be seen as
"uniform" universal quantification, ⌜∀[x:A]. B[x]⌝⋅

⋂x:A. B[x] ==  PRIMITIVE

Definition: lambda def
λx.A[x] ==  PRIMITIVE

Definition: fix def
fix(F) ==  PRIMITIVE

Definition: apply def
f a ==  PRIMITIVE

Definition: set def
This primitive Nuprl type is essentially the same as ⌜Image((x:A × B[x]),(λp.(fst(p))))⌝
So its members are the members of A for which B[x] is true, but the evidence
for B[x] is not kept.

The elimination rule for this type is setElimination
From hypothesis u:{x:A| B[x]}  we get u:A and a "hidden" B[u] that becomes
unhidden when we are proving a subgoal of the form equality or member. ⋅

{x:A| B[x]}  ==  PRIMITIVE

Definition: atom_eq def
if a=b then c else d fi  ==  PRIMITIVE

Definition: int_eq def
In Nuprl the integers are primitive (rather than constructed inductively).
Therefore the basic arithmetic operations are implemented in the computation
system (using LISP bignum package) and axiomatized in the rules.

The operation
   if a=b then c else d 
is the primitive equality test on integers a and b,
returning c when a=b and d otherwise.

The only rules we need for this are:
int_eqReduceTrueSq  which says:
H  ⊢ if a=b then s else t ~ u

  BY int_eqReduceTrueSq ()
  
  H  ⊢ s ~ u
  H  ⊢ a = b

and 
int_eqReduceFalseSq which says:
H  ⊢ if a=b then s else t ~ u

  BY int_eqReduceFalseSq ()
  
  H  ⊢ t ~ u
  H  ⊢ (a = b) ⟶ Void⋅

if a=b then c else d ==  PRIMITIVE

Definition: less def
if (a) < (b)  then c  else d ==  PRIMITIVE

Definition: rec_ind def
letrec x(y) = B[x; y] in x(A) ==  fix((λx,y. B[x; y])) A

Definition: rec def
rec(x.A[x]) ==  PRIMITIVE

Comment: LOGIC_ABS1
Basic Logic Abstractions
⋅

Definition: member
t ∈ T ==  t = t ∈ T

Definition: unit
Unit ==  0 ∈ ℤ

Definition: true
True ==  0 ∈ ℤ

Definition: false
False ==  Void

Definition: and
P ∧ Q ==  P × Q

Definition: or
P ∨ Q ==  P + Q

Definition: implies
P ⇒ Q ==  P ⟶ Q

Definition: rev_implies
P ⇐ Q ==  Q ⇒ P

Definition: squash
↓T ==  Image(T,(λx.Ax))

Definition: oldsquash
oldsquash(T) ==  {True| T} 

Definition: not
¬A ==  A ⇒ False

Definition: nequal
a ≠ b ∈ T  ==  ¬(a = b ∈ T)

Definition: iff
P ⇐⇒ Q ==  (P ⇒ Q) ∧ (P ⇐ Q)

Definition: exists
∃x:A. B[x] ==  x:A × B[x]

Definition: sq_exists
∃x:A [B[x]] ==  {x:A| B[x]} 

Definition: all
∀x:A. B[x] ==  x:A ⟶ B[x]

Comment: INT_ABS1

⋅

Definition: le
A ≤ B ==  (¬less_than'(B;A)) ∧ (A ∈ ℤ) ∧ (B ∈ ℤ)

Definition: ge
i ≥ j  ==  j ≤ i

Definition: gt
i > j ==  j < i

Comment: subtype_com
Basic primitive for subtyping. Intended meaning is:

S subtype T iff
  1. Every element of S is also an element of T
  2. If x,y are equal elements of S, they are also equal
     elements of t.

Definition: image-type_def
There are four rules about this primitive type.
imageEquality
    which implies that Image(A,f) is a type if A ∈ Type and f ∈ Base; 
imageMemberEquality
    which implies that the terms ⌜f a⌝, a ∈ A are members of Image(A,f);
imageElimination  says that these are the only members of Image(A,f)
    so ⌜x ∈ Image(A,f)⌝ can be replaced by ⌜f a⌝ for a "hiddden" a ∈ A;
imageEqInduction
   If forall a,b ∈ Base. (f a ∈ T  and a=b ∈ A  implies f(a)=f(b) ∈ T) then
   the equivalence class of f t1 in Image(A,f) contains  
   the equivalence class of f t1 in T⋅

Image(T,f) ==  PRIMITIVE

Comment: about directed_Auto_additions
A "directed" auto addition is a tactic, tac,  together with
  1) an opid (token) that says the tactic should only be tried when the
     concl has that opid.
  2) another token, that is its "key" that we can print out for debugging and
     use to update the table with a different tactic.
  3) a boolean that (when true) says that any subgoals left by the tactic
     that have the label `must complete`
     must complete using a weakened Auto
  We organize the directed auto additions into a lookup table using the 
  opid as the first key, and then the other token as the second key. 
⋅⋅

Comment: about labeled_Auto_additions
Some additions to Auto are controlled by the proof label
 (the label like `wf` or `aux` that tactics can add to subgoals
  with AddHiddenLabel `xxx`).
Such an addition is a pair `xxx` , tac and the intent is that
Auto should try tactic tac on (and only on) goals with label `xxx`.

If we keep these additions on a list that is not Auto_additions
or directed_Auto_additiions, then we can avoid trying (`xxx`, tac)
at all (even to just Fail if the label is not `xxx`) on goals
with label not equal to `xxx`.

We also assume that at most one tactic is triggered by each label
because we use this method for special purposes where the controlling
tactic (such as the congruence closure procedure) can choose unique
labels for steps that it wants Auto to handle with these additions.

Thus, the labeled_Auto_additions are a simple (tok # tactic) list,
 (an alist).

 
⋅⋅



Home Index