---

Comment: sqequal_com
Here are the essentials:
    1. For any two terms a and b, we intend 'a ~ b' to be a type (in U{1})
    2. For any term a, 'a ~ a'
    3. For two terms a and b, 'a ~ b' if b computes to a (normal
       direct computation)
    4. For any of the following types T, and two terms a, b in T, we
           have 'a = b in T => a ~ b'
       a. int
       b. Atom
       c. any equality type (such as Unit)
    5. Two terms 'opid1{params1}(a1, ..., an)' and 'opid2{params2}(b1, ..., bn)'
       are squiggle equal if opid1 and opid2 are the same,
       params1 and params2 are the same, the arity of the terms is
       the same, and 'a1 ~ b1', ..., 'an ~ bn'
       -- This rule is not strictly necessary, given the substitution
       rule, and the reflexive rule, but it is pretty useful in any case.
    6. Substitution: if 'T[a]' is a hypothesis or conclusion in a
       sequent, and 'a ~ b', then 'T[a]' can be replaced by 'T[b]'
       (and there is no need to prove functionality).

We don't have a rule for proving when two squiggle types are equal, so
we can't use the squiggle type as a hypothesis.  If we had one, the
rule would be something like this:
    'a ~ b = c ~ d in U1'
if 'a ~ b <=> c ~ d' and all free variables in a, b, c, and d belong to
"canonical" types (T is a canonical type if
'all a, b: T. a = b in T => a ~ b').

Note added May 2010:
  There are, in fact, rules for proving when two squiggle types are equal. They are
sqequalExtensionalEquality and sqequalIntensionalEquality.
Neither of these allows one to prove that H |- (a ~ b) \in ℙ unless
 the free varaibles in a and b are bound in H to "squiggle" types, T, that satisfy
SQType(T).  
This is crucial, as demonstrated by the following example:

Base is the type of all closed term with ~ as its equality relation, so Base is a sqiggle type.
The rule Error :equalityEqualityBase lets us prove that (x = y \in T) is a type provided
that T is a type and x and y are in Base.
If we simply define ⌜a ~ b⌝ to be a = b \in ⌜Base⌝, then we can prove 0 = 1 \in ℤ as follows:
Substitute the easily proved equation 0 = 1 \in Top, to get two subgoals, 1 = 1 in ℤ (which is
trivial) and  x:Top |- (x = 1 \in ℤ) \in ℙ. On the second subgoal use Error :equalityEqualityBase
to reduce to proving ⌜ℤ ∈ ℙ⌝, ⌜x ∈ Base⌝, and ⌜1 ∈ Base⌝. The second of these is not true
because (x:Top |- x \in Base) implies that ⌜Top ⊆r Base⌝ which is false.
But if ⌜x ∈ Base⌝ can simply "fold" to ⌜x ~ x⌝ then it can be proved
using the rule sqequalReflexivity, and we have proved False!!
 


⋅

Comment: sq_type_com
There are other types in Nuprl that we can consider first order types.
Each of these types has canonical members.  For example, ⌜𝔹⌝ is a type with
canonical memebers because there is only one representativ for ⌜tt⌝ and
one representative for ⌜ff⌝.  We package this concept in the ⌜SQType(T)⌝
predicate, which states that equal terms in T are also sqequal.  This
is used by MemCD, so that these types sre treated as first-order types.

Definition: sq_type
SQType(T) ==  ∀x,y:T.  ((x = y ∈ T) ⇒ {x ~ y})

Lemma: base_sq
SQType(Base)

Lemma: sqequal-wf-base
∀[x,y:Base].  (x ~ y ∈ ℙ)

Lemma: istype-sqequal
∀[x,y:Base].  istype(x ~ y)

Lemma: baseof_sq
∀[T:Type]. SQType(baseof(T))

Lemma: subtype_base_sq
∀[A:Type]. SQType(A) supposing A ⊆r Base

Comment: case_ite_com
In the reset of this library, we develop tactics to break apart
⌜if test then truecase else falsecase fi ⌝ terms.  Since we have sqequality,
on test, it is possible to break apart these terms without generating
well-formedness subgoals on the ⌜truecase⌝ and ⌜falsecase⌝ subterms, even if
term is a hypothesis.

Lemma: ycomb_wf_trivial
Y ∈ Void ⟶ Void

Lemma: ycomb-unroll
∀[f:Top]. (Y f ~ f (Y f))

Comment: vr-list-of-added-rules
⌜sqequalnIntensionalEquality⌝
⌜sqlenIntensionalEquality⌝
⌜sqlenSubtypeRel⌝
⌜sqequalnSqlen⌝
⌜sqlenSqequaln⌝
⌜sqequalnSymm⌝
⋅

Lemma: sqle-wf
∀[x,y:Base].  (x ≤ y ∈ Type)

Lemma: sqequal_zero
∀[x,y:Top].  (x ~0 y)

Lemma: sqle_trans
∀a,b,c:Base.  ((a ≤ b) ⇒ (b ≤ c) ⇒ (a ≤ c))

Lemma: pair-eta
∀[p:Top × Top]. (p ~ <fst(p), snd(p)>)

Lemma: sq_stable__sqequal
∀x,y:Base.  SqStable(x ~ y)

Lemma: not_zero_sqequal_one
(0 ~ 1) ⇒ False

Lemma: not_all_sqequal
(∀[a,b:Base].  (a ~ b)) ⇒ False

Lemma: false-sqequal
∀[a,b:Base].  ((¬(a ~ b)) ⇒ ((a ~ b) = (0 ~ 1) ∈ Type))

Lemma: decidable__less_than'
∀i,j:ℤ.  Dec(less_than'(i;j))

Lemma: decidable__lt
∀i,j:ℤ.  Dec(i < j)

Lemma: decidable__le
∀i,j:ℤ.  Dec(i ≤ j)

Lemma: less-trichotomy
∀a,b:ℤ.  (a < b ∨ b < a ∨ (a = b ∈ ℤ))

Lemma: add-comm
∀x,y:ℤ.  ((x + y) = (y + x) ∈ ℤ)

Lemma: add-monotonic
∀a,b,c,d:ℤ.  (a < b ⇒ ((c = d ∈ ℤ) ∨ c < d) ⇒ a + c < b + d)



Home Index