how to view backwards without crashing your program

[Sebastian Hanowski]

 Issues of replacing constrain-by-instantiation by constrain-by-equation
for   datatype   declarations    in   Sec.   5   of    the   OTT   paper
http://www.cs.nott.ac.uk/~txa/publ/ott-conf.pdf let me  revert to an old
vice of mine, that is to  constrain computations by equation in Epigram.
Where the first  is used to put focus on  unfocused families, the latter
let's the typechecker work even harder for you.

 For example,  subtraction on  the naturals requires  only less  then or
equal numbers to be substracted. You can assure this to the typechecker
by  passing an  argument which  is an  inductive proof  that the  second
number is less  then or equal to  the first. One can find  this in Edwin
Brady's thesis http://www.dcs.st-andrews.ac.uk/~eb/writings/thesis.pdf .
This also gives an additional possibility for recursion.

But one can also give this precondition by an equation:

------------------------------------------------------------------------------
                                       (  n : Nat   !
data (---------!  where (---------! ;  !------------!
     ! Nat : * )        ! O : Nat )    ! |+ n : Nat )
------------------------------------------------------------------------------
     (   m, n : Nat   !                
let  !----------------!                
     ! plus m n : Nat )                
                                       
     plus m n <= rec m                
     { plus m n <= case m              
       { plus O n => n                
         plus (|+ m) n => |+ (plus m n)
       }                              
     }                                
------------------------------------------------------------------------------
     ( m, n : Nat ;  p : m = plus n x !
let  !--------------------------------!
     !       minus m n p : Nat        )
                                       
     minus m n p <= case p            
     { minus (plus n m) n refl => m    
     }                                
------------------------------------------------------------------------------
inspect minus (|+ (|+ (|+ O))) (|+ (|+ O)) refl => |+ O : Nat
------------------------------------------------------------------------------


Alas this doesn't scale up to this obvious case:

------------------------------------------------------------------------------
     ( xs, ys : List X ;  y : X ;  p : xs = append ys (cons x nil) !
let  !-------------------------------------------------------------!
     !                        last xs p : X                        )
                                                                   
     last xs p <= case p                                            
     { last (append ys (cons xs nil)) refl => xs                    
     }                                                              
------------------------------------------------------------------------------
inspect last (cons O (cons (|+ O) (cons (|+ (|+ O)) nil))) refl => ? : Nat
------------------------------------------------------------------------------

(Note  that  ys  and  x  have   to  be  declared  because  of  Epigram's
heterogeneous inbuild equality.)

Thanks  to Epigram's  pattern analysis  being /programmable/  it's still
possible to decompose a list into a prefix and a one-element-tail on the
left (see below).

------------------------------------------------------------------------------
     (    xs : List X    !                  
let  !-------------------!                  
     ! last xs : Maybe X )                  
                                             
     last xs <= view (back xs)              
     { last nil => no                        
       last (append xs (cons x nil)) => yes x
     }                                      
------------------------------------------------------------------------------
inspect last l012 => yes (|+ (|+ O)) : Maybe Nat
------------------------------------------------------------------------------

I know  theses programs  don't lie  at the heart  of those  problems the
Epigram programming language  aims at making easy. It's just  that I had
liked  to give  more  interesting examples  of  preconditions than  some
condInfo : ∀P:*; b:Bool => (b=true -> P) -> (b=false -> P) -> P


Best regards,
Sebastian

Up to a tweak the view below is the same whose trail goes like this:
http://homepages.inf.ed.ac.uk/wadler/papers/view/view.ps.gz
http://www.cs.nott.ac.uk/~ctm/view-Dec6.ps.gz
http://sneezy.cs.nott.ac.uk/epigram/durham/examples/ctm/Back.epi

------------------------------------------------------------------------------
                                       (  n : Nat   !
data (---------!  where (---------! ;  !------------!
     ! Nat : * )        ! O : Nat )    ! |+ n : Nat )
------------------------------------------------------------------------------
     (   X : *    !                            ( x : X ;  xs : List X !
data !------------!  where (--------------! ;  !----------------------!
     ! List X : * )        ! nil : List X )    !  cons x xs : List X  )
------------------------------------------------------------------------------
let  l012 : List Nat                                    
                                                       
     l012 => cons O (cons (|+ O) (cons (|+ (|+ O)) nil))
------------------------------------------------------------------------------
     (    xs, ys : List X    !                        
let  !-----------------------!                        
     ! append xs ys : List X )                        
                                                       
     append xs ys <= rec xs                            
     { append xs ys <= case xs                        
       { append nil ys => ys                          
         append (cons x xs) ys => cons x (append xs ys)
       }                                              
     }                                                
------------------------------------------------------------------------------
     ( xs :   !                                                              
     !   List !                                                              
     !   % X  !                       ( x : X ;  xs : List X ;  b : Back xs !
data !--------!  where (---------! ;  !-------------------------------------!
     !  Back  !        ! bnil :  !    !   bcons x xs b :                    !
     !  % xs  !        !   Back  !    !     Back (append xs (cons x nil))   )
     !   : *  )        !   % nil )                                          
------------------------------------------------------------------------------
     ( x : X ;  xs : List X ;  b : Back xs !          
let  !-------------------------------------!          
     !    aux x xs b : Back (cons x xs)    )          
                                                       
     aux x xs b <= rec b                              
     { aux x bs b <= case b                            
       { aux x nil bnil => bcons x nil bnil            
         aux x (append bs (cons b nil)) (bcons b bs b')
           => bcons b (cons x bs) (aux x bs b')        
       }                                              
     }                                                
------------------------------------------------------------------------------
     (    xs : List X    !                    
let  !-------------------!                    
     ! back xs : Back xs )                    
                                               
     back xs <= rec xs                        
     { back xs <= case xs                      
       { back nil => bnil                      
         back (cons x xs) => aux x xs (back xs)
       }                                      
     }                                        
------------------------------------------------------------------------------
     (    X : *    !        (      x : X      !                    
data !-------------!  where !-----------------! ;  (--------------!
     ! Maybe X : * )        ! yes x : Maybe X )    ! no : Maybe X )
------------------------------------------------------------------------------
     (    xs : List X    !                  
let  !-------------------!                  
     ! last xs : Maybe X )                  
                                             
     last xs <= view (back xs)              
     { last nil => no                        
       last (append xs (cons x nil)) => yes x
     }                                      
------------------------------------------------------------------------------
inspect last l012 => yes (|+ (|+ O)) : Maybe Nat
------------------------------------------------------------------------------