path->neutral

doc/bool.ott

@@ -15,10 +15,10 @@ v :: 'v_' ::=
   | Bool                  ::   :: TyBool 
   | True                  ::   :: LitTrue
   | False                 ::   :: LitFalse
-  | if path then a else b ::   :: If
+  | if ne then a else b    ::   :: If
 
-path :: 'p_' ::=
-  | if path then a else b ::   :: If
+neutral , ne :: 'n_' ::=
+  | if ne then a else b    ::   :: If
 
 defns 
 Jwhnf :: '' ::= 
@@ -46,9 +46,9 @@ whnf True ~> True
 ------------------- :: false
 whnf False ~> False
 
-whnf a ~> path
+whnf a ~> ne
 ---------------------------------------------------- :: if_cong
-whnf if a then b1 else b2 ~> if path then b1 else b2
+whnf if a then b1 else b2 ~> if ne then b1 else b2
 
 
 defns

doc/data.ott

@@ -29,10 +29,10 @@ tm, a , b , A , B :: '' ::= {{ com terms and types }}
 v :: 'v_' ::= 
    | K args       ::     :: TCon
    | T args       ::     :: DCon 
-   | case p of { </ pati -> ai // i /> } ::     :: Case 
+   | case ne of { </ pati -> ai // i /> } ::     :: Case 
 
-path, p :: 'p_' ::=
-   | case p of { </ pati -> ai // i /> } ::     :: Case 
+neutral, ne :: 'n_' ::=
+   | case ne of { </ pati -> ai // i /> } ::     :: Case 
 
 
 args {{ tex \overline{a} }} , bs {{ tex \overline{b} }} :: '' ::= 
@@ -92,9 +92,9 @@ whnf b ~> v
 ---------------------------------------------------------------------- :: case
 whnf case (K args) of { </ pati -> ai // i /> } ~> v
 
-a ~> p
+a ~> ne
 ------------------------------------------------------------------------------- :: case_cong
-whnf case a of { </ pati -> ai // i /> } ~> case p of { </ pati -> ai // i /> }
+whnf case a of { </ pati -> ai // i /> } ~> case ne of { </ pati -> ai // i /> }
 
 
 defns

doc/equality.v

@@ -0,0 +1,95 @@
+
+Print bool_rect.
+
+(* 
+bool_rect = 
+fun (P : bool -> Type) (f : P true) (f0 : P false) (b : bool) => if b as b0 return (P b0) then f else f0
+     : forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+*)
+
+Section MyEq.
+
+Polymorphic Inductive myeq (A :Type)(a:A) : A -> Type :=
+  | myrefl : myeq A a a.
+
+Check myeq_rect.
+
+Lemma my_k : forall (A:Type) (x:A) (p : myeq A x x), myeq (myeq A x x) p (myrefl A x).
+Proof.
+  intros.
+  pose (h := myeq_rect).
+  specialize h with (y := x) (m := p).
+  specialize h with (P := fun a p0 => myeq (myeq A x a) p0 p0). simpl in h.
+
+Polymorphic Inductive myeq : forall (A :Type)(a:A), A -> Type :=
+  | myrefl : forall A a, myeq A a a.
+
+Check myeq_rect.
+
+(*
+myeq_rect
+     : forall (a : A) (P : forall a0 : A, myeq A a a0 -> Type), P a (myrefl A a) -> forall (y : A) (m : myeq A a y), P y m
+*)
+
+Lemma my_k : forall (A:Type) (x:A) (p : myeq A x x), myeq (myeq A x x) p (myrefl A x).
+Proof.
+  intros.
+  pose (h := myeq_rect).
+
+  specialize h with (m := p).
+  specialize (h (fun A x y p0 => myeq (myeq A x y) p0 (myrefl A x))).
+  (* goal is 
+
+    myeq (myeq A x x) p (myrefl A x) 
+
+    P (y : A) (m : myeq A x y)  will be instantiated by x and p
+
+    fun y m => myeq (myeq A x y) m m
+
+*)
+  specialize (h (fun y m => myeq (myeq A x y) m m)). simpl in h.
+  specialize (h (myrefl (myeq A x x) (myrefl A x))).
+  specialize (h x p).
+
+  specialize (h (fun a0 e => myeq (myeq A x x) p (myrefl A x))). simpl in h.
+  eapply h.
+  eapply myeq_rect with (P := fun (a0 : A) (p0 : myeq A a0 a0) => myeq _ p (myrefl A x)).
+
+k : [A:Type] -> [x:A] -> (p : x = x) -> (p = Refl)
+k = \ [A][x] p . 
+  subst Refl by p
+
+
+
+
+Check eq_rect.
+
+(* 
+eq_rect
+     : forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, x = y -> P y
+*)
+
+
+
+Definition sym : forall A (x y : A), x = y -> y = x :=
+
+   fun (A : Type) (x y : A) (H : x = y) => 
+     match H in (_ = y0) return (y0 = x) with
+     | eq_refl => eq_refl
+     end.
+
+Definition trans :=
+fun (A : Type) (x y z : A) (H : x = y) (H0 : y = z) => 
+  match H0 in (_ = y0) return (x = y0) with
+  | eq_refl => H
+  end.
+
+
+
+
+Definition uip : forall A (x y : A) (p : x = y) (q :x = y),  p = q.
+Proof.
+  intros.
+Search eq eq_refl.
+  match q in (_ = y0) return (p = q) with 
+  | eq_refl => 

doc/oplss.mng

@@ -1347,10 +1347,19 @@ The following judgment (shown in Figure~\ref{fig:whnf})
 %
 \[ \fbox{$[[whnf a ~> v]]$} \]
 %
-describes when a term $[[a]]$ reduces to some result $[[v]]$ in \emph{weak head normal form (whnf)}.
-For closed terms, these rules correspond to a big-step evaluation relation and produce
-a value. For open terms, the rules produce a term that is either headed by a variable
-or by some head form (i.e., $\lambda$ or $\Pi$).
+describes when a term $[[a]]$ reduces to some result $[[v]]$ in \emph{weak
+  head normal form (whnf)}.  For closed terms, these rules correspond to a
+big-step evaluation relation and produce a value (i.e. abstraction or type
+form).  For open terms, the rules could also produce terms that are some
+sequence of applications headed by a variable.  In this case, we call the term
+a \emph{neutral} term, and use the metavariable $[[ne]]$ to refer to it.
+
+\[ 
+\begin{array}{llcl}
+\textit{value}     & [[v]] & ::= & [[Type]]\ |\ [[\x.a]]\ |\ [[(x:A) -> B]]\ |\ [[()]]\ |\ [[Unit]]\ |\ [[ne]] \\
+\textit{neutral terms} & [[ne]] & ::= & [[x]]\ |\ [[ne a]] \\
+\end{array}
+\]
 
 For example, the term
 \begin{piforall}
@@ -1409,10 +1418,10 @@ In \texttt{version2} of the \href{version2/src/TypeCheck.hs}{implementation},
 these functions are called in a few places:
 \begin{itemize}
 \item \texttt{equate} is called at the end of \texttt{checkType} to make sure 
-that the annotate type matches the inferred type.
+that the annotated type matches the inferred type.
 \item \texttt{ensurePi} is called in the \texttt{App} case
 of \texttt{inferType}
-\item \texttt{whnf} is called in \texttt{checkType}
+\item \texttt{whnf} is called at the beginning of \texttt{checkType}
   to make sure that we are using the head form of the type in checking
   mode.
 \end{itemize}
@@ -1428,7 +1437,7 @@ $[[G |- a <=> b]]$?
 There are several ways to do so.
 
 The easiest one to explain is based on reduction---for \texttt{equate} to
-reduce the two arguments to some normal form and then compare those normal
+reduce the two arguments to a \emph{normal form} and then compare those normal
 forms for equivalence.
 
 One way to do this is with the following algorithm:
@@ -1440,9 +1449,9 @@ One way to do this is with the following algorithm:
     Unbound.aeq nf1 nf2
 \end{verbatim}
 
-However, we can do better.  Sometimes we can equate the terms without
-completely reducing them. Because reduction can be expensive (or even
-nonterminating) we would like to only reduce as much as necessary.
+However, we can do better.  Sometimes we can find out that terms are
+equivalent without fully reducing them. Because reduction can be expensive (or
+even nonterminating) we would like to only reduce as much as necessary.
 
 Therefore, the implementation of \cd{equate} has the following form.
 \begin{verbatim}

doc/pi-rules.tex

@@ -46,31 +46,31 @@
 \ottprodline{|}{\ottkw{Unit}}{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottsym{()}}{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottmv{x}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{ \ottnt{p}  \;  \ottnt{b} }{}{}{}{}\ottprodnewline
+\ottprodline{|}{ \ottnt{ne}  \;  \ottnt{b} }{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottsym{(}  \ottnt{v}  \ottsym{)}} {\textsf{S}}{}{}{}\ottprodnewline
 \ottprodline{|}{ \{  \ottmv{x} \!:\! \ottnt{A} \ |\  \ottnt{B}  \} }{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottsym{(}  \ottnt{a}  \ottsym{,}  \ottnt{b}  \ottsym{)}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottkw{let} \, \ottsym{(}  \ottmv{x}  \ottsym{,}  \ottmv{y}  \ottsym{)}  \ottsym{=}  \ottnt{p} \, \ottkw{in} \, \ottnt{a}}{}{}{}{}\ottprodnewline
+\ottprodline{|}{\ottkw{let} \, \ottsym{(}  \ottmv{x}  \ottsym{,}  \ottmv{y}  \ottsym{)}  \ottsym{=}  \ottnt{ne} \, \ottkw{in} \, \ottnt{a}}{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottkw{Bool}}{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottkw{True}}{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottkw{False}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottkw{if} \, \ottnt{path} \, \ottkw{then} \, \ottnt{a} \, \ottkw{else} \, \ottnt{b}}{}{}{}{}\ottprodnewline
+\ottprodline{|}{\ottkw{if} \, \ottnt{ne} \, \ottkw{then} \, \ottnt{a} \, \ottkw{else} \, \ottnt{b}}{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottnt{a}  \ottsym{=}  \ottnt{b}}{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottkw{refl}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{p}}{}{}{}{}\ottprodnewline
+\ottprodline{|}{\ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{ne}}{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottmv{K} \, \overline{a}}{}{}{}{}\ottprodnewline
 \ottprodline{|}{\ottmv{T} \, \overline{a}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottkw{case} \, \ottnt{p} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}}  \to  \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}}}{}{}{}{}}
+\ottprodline{|}{\ottkw{case} \, \ottnt{ne} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}}  \to  \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}}}{}{}{}{}}
 
-\newcommand{\ottpath}{
-\ottrulehead{\ottnt{path}  ,\ \ottnt{p}}{::=}{\ottcom{paths (neutral terms)}}\ottprodnewline
+\newcommand{\ottneutral}{
+\ottrulehead{\ottnt{neutral}  ,\ \ottnt{ne}}{::=}{\ottcom{neutral terms}}\ottprodnewline
 \ottfirstprodline{|}{\ottmv{x}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{ \ottnt{p}  \;  \ottnt{b} }{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottsym{(}  \ottnt{p}  \ottsym{)}} {\textsf{S}}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottkw{let} \, \ottsym{(}  \ottmv{x}  \ottsym{,}  \ottmv{y}  \ottsym{)}  \ottsym{=}  \ottnt{p} \, \ottkw{in} \, \ottnt{a}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottkw{if} \, \ottnt{path} \, \ottkw{then} \, \ottnt{a} \, \ottkw{else} \, \ottnt{b}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{p}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottkw{case} \, \ottnt{p} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}}  \to  \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}}}{}{}{}{}}
+\ottprodline{|}{ \ottnt{ne}  \;  \ottnt{a} }{}{}{}{}\ottprodnewline
+\ottprodline{|}{\ottsym{(}  \ottnt{ne}  \ottsym{)}} {\textsf{S}}{}{}{}\ottprodnewline
+\ottprodline{|}{\ottkw{let} \, \ottsym{(}  \ottmv{x}  \ottsym{,}  \ottmv{y}  \ottsym{)}  \ottsym{=}  \ottnt{ne} \, \ottkw{in} \, \ottnt{a}}{}{}{}{}\ottprodnewline
+\ottprodline{|}{\ottkw{if} \, \ottnt{ne} \, \ottkw{then} \, \ottnt{a} \, \ottkw{else} \, \ottnt{b}}{}{}{}{}\ottprodnewline
+\ottprodline{|}{\ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{ne}}{}{}{}{}\ottprodnewline
+\ottprodline{|}{\ottkw{case} \, \ottnt{ne} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}}  \to  \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}}}{}{}{}{}}
 
 \newcommand{\ottargs}{
 \ottrulehead{\overline{a}  ,\ \overline{b}}{::=}{}\ottprodnewline
@@ -158,7 +158,7 @@
 \newcommand{\ottgrammar}{\ottgrammartabular{
 \ottep\ottinterrule
 \ottv\ottinterrule
-\ottpath\ottinterrule
+\ottneutral\ottinterrule
 \ottargs\ottinterrule
 \ottpat\ottinterrule
 \ottms\ottinterrule
@@ -209,9 +209,9 @@
 
 
 \newcommand{\ottdrulewhnfXXapp}[1]{\ottdrule[#1]{%
-\ottpremise{ \ottkw{whnf} \  \ottnt{a}  \leadsto  \ottnt{path} }%
+\ottpremise{ \ottkw{whnf} \  \ottnt{a}  \leadsto  \ottnt{ne} }%
 }{
- \ottkw{whnf} \   \ottnt{a}  \;  \ottnt{b}   \leadsto   \ottnt{path}  \;  \ottnt{b}  }{%
+ \ottkw{whnf} \   \ottnt{a}  \;  \ottnt{b}   \leadsto   \ottnt{ne}  \;  \ottnt{b}  }{%
 {\ottdrulename{whnf\_app}}{}%
 }}
 
@@ -234,9 +234,9 @@
 
 
 \newcommand{\ottdrulewhnfXXprodcong}[1]{\ottdrule[#1]{%
-\ottpremise{ \ottkw{whnf} \  \ottnt{a}  \leadsto  \ottnt{p} }%
+\ottpremise{ \ottkw{whnf} \  \ottnt{a}  \leadsto  \ottnt{ne} }%
 }{
- \ottkw{whnf} \  \ottkw{let} \, \ottsym{(}  \ottmv{x}  \ottsym{,}  \ottmv{y}  \ottsym{)}  \ottsym{=}  \ottnt{a} \, \ottkw{in} \, \ottnt{b}  \leadsto  \ottkw{let} \, \ottsym{(}  \ottmv{x}  \ottsym{,}  \ottmv{y}  \ottsym{)}  \ottsym{=}  \ottnt{p} \, \ottkw{in} \, \ottnt{b} }{%
+ \ottkw{whnf} \  \ottkw{let} \, \ottsym{(}  \ottmv{x}  \ottsym{,}  \ottmv{y}  \ottsym{)}  \ottsym{=}  \ottnt{a} \, \ottkw{in} \, \ottnt{b}  \leadsto  \ottkw{let} \, \ottsym{(}  \ottmv{x}  \ottsym{,}  \ottmv{y}  \ottsym{)}  \ottsym{=}  \ottnt{ne} \, \ottkw{in} \, \ottnt{b} }{%
 {\ottdrulename{whnf\_prodcong}}{}%
 }}
 
@@ -281,9 +281,9 @@
 
 
 \newcommand{\ottdrulewhnfXXifXXcong}[1]{\ottdrule[#1]{%
-\ottpremise{ \ottkw{whnf} \  \ottnt{a}  \leadsto  \ottnt{path} }%
+\ottpremise{ \ottkw{whnf} \  \ottnt{a}  \leadsto  \ottnt{ne} }%
 }{
- \ottkw{whnf} \  \ottkw{if} \, \ottnt{a} \, \ottkw{then} \, \ottnt{b_{{\mathrm{1}}}} \, \ottkw{else} \, \ottnt{b_{{\mathrm{2}}}}  \leadsto  \ottkw{if} \, \ottnt{path} \, \ottkw{then} \, \ottnt{b_{{\mathrm{1}}}} \, \ottkw{else} \, \ottnt{b_{{\mathrm{2}}}} }{%
+ \ottkw{whnf} \  \ottkw{if} \, \ottnt{a} \, \ottkw{then} \, \ottnt{b_{{\mathrm{1}}}} \, \ottkw{else} \, \ottnt{b_{{\mathrm{2}}}}  \leadsto  \ottkw{if} \, \ottnt{ne} \, \ottkw{then} \, \ottnt{b_{{\mathrm{1}}}} \, \ottkw{else} \, \ottnt{b_{{\mathrm{2}}}} }{%
 {\ottdrulename{whnf\_if\_cong}}{}%
 }}
 
@@ -312,9 +312,9 @@
 
 
 \newcommand{\ottdrulewhnfXXsubstXXcong}[1]{\ottdrule[#1]{%
-\ottpremise{ \ottkw{whnf} \  \ottnt{b}  \leadsto  \ottnt{p} }%
+\ottpremise{ \ottkw{whnf} \  \ottnt{b}  \leadsto  \ottnt{ne} }%
 }{
- \ottkw{whnf} \  \ottsym{(}  \ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{p}  \ottsym{)}  \leadsto  \ottsym{(}  \ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{p}  \ottsym{)} }{%
+ \ottkw{whnf} \  \ottsym{(}  \ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{ne}  \ottsym{)}  \leadsto  \ottsym{(}  \ottkw{subst} \, \ottnt{a} \, \ottkw{by} \, \ottnt{ne}  \ottsym{)} }{%
 {\ottdrulename{whnf\_subst\_cong}}{}%
 }}
 
@@ -343,9 +343,9 @@
 
 
 \newcommand{\ottdrulewhnfXXcaseXXcong}[1]{\ottdrule[#1]{%
-\ottpremise{\ottnt{a}  \leadsto  \ottnt{p}}%
+\ottpremise{\ottnt{a}  \leadsto  \ottnt{ne}}%
 }{
- \ottkw{whnf} \  \ottkw{case} \, \ottnt{a} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}}  \to  \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}}  \leadsto  \ottkw{case} \, \ottnt{p} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}}  \to  \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}} }{%
+ \ottkw{whnf} \  \ottkw{case} \, \ottnt{a} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}}  \to  \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}}  \leadsto  \ottkw{case} \, \ottnt{ne} \, \ottkw{of} \, \ottsym{\{} \, \ottcomp{\ottnt{pat_{\ottmv{i}}}  \to  \ottnt{a_{\ottmv{i}}}}{\ottmv{i}} \, \ottsym{\}} }{%
 {\ottdrulename{whnf\_case\_cong}}{}%
 }}
 

doc/pi.ott

@@ -73,21 +73,21 @@ v :: 'v_' ::= {{ com values and weak head normal forms }}
 
   | x               ::   :: Var
 
-  | p b             ::   :: App
+  | ne b            ::   :: App
 
   | ( v )           :: S :: Paren
 
 
-path, p :: 'p_' ::= {{ com paths (neutral terms) }}
+neutral, ne :: 'n_' ::= {{ com neutral terms }}
 
   | x               ::   :: Var 
 
-  | p b             ::   :: App 
+  | ne a             ::   :: App 
 
-  | ( p )           :: S :: Paren
+  | ( ne )           :: S :: Paren
 
 subrules 
-  p <:: v
+  ne <:: v
   v <:: a
 
 substitutions
@@ -200,9 +200,9 @@ whnf (x:A) -> B ~> (x:A) -> B
 whnf x ~> x
 
 
-whnf a ~> path
+whnf a ~> ne
 ---------------------- :: app
-whnf a b ~> path b
+whnf a b ~> ne b
 
 % remove type annotations when normalizing
 %

doc/sigma.ott

@@ -19,10 +19,10 @@ tm, a , b , A , B :: '' ::= {{ com terms and types }}
 v :: 'v_' ::= 
   | { x : A | B }    ::   :: Sigma
   | ( a , b )        ::   :: Prod 
-  | let ( x , y ) = p in a ::  :: LetPair
+  | let ( x , y ) = ne in a ::  :: LetPair
 
-path, p :: 'p_' ::= 
-  | let ( x , y ) = p in a ::  :: LetPair
+neutral, ne :: 'n_' ::= 
+  | let ( x , y ) = ne in a ::  :: LetPair
 
 defns 
 Jwhnf :: '' ::= 
@@ -36,9 +36,9 @@ whnf (b [a1/x] [a2/y]) ~> v
 ------------------------------- :: letpair
 whnf let (x,y) = a in b ~> v
 
-whnf a ~> p
+whnf a ~> ne
 --------------------------------------------- :: prodcong
-whnf let (x,y) = a in b ~> let (x,y) = p in b
+whnf let (x,y) = a in b ~> let (x,y) = ne in b
 
 
 defns