Hello all
I don't use Epigram very often, but I like to have a bit of fun now
and then.
I thought I'd start with something pointless, a unit type...
-----------------------------------------------------------------
data (---------! where (-----------!
! Run : * ) ! run : Run )
-----------------------------------------------------------------
...and continue with something even more pointless...
-----------------------------------------------------------------
( ran : Run ; t : T !
let !--------------------!
! also ran t : Run )
also ran t <= case ran
{ also run t => run
}
-----------------------------------------------------------------
...so I could prove this utterly pointless theorem:
-----------------------------------------------------------------
( t : T !
! ran : Run !
! P : Run -> * !
! m : all ran : Run ; x : T => P (also ran x) !
let !----------------------------------------------!
! with t ran P m : P ran )
with t ran P m <= case ran
{ with t run P m => m run t
}
-----------------------------------------------------------------
What am I up to? Well, let's have Nat, Pair, Vec, and...
--------------------------------------------------------------------
( ran : Run ; xys : Vec n (Pair S T) !
let !------------------------------------------!
! unzip ran xys : Pair (Vec n S) (Vec n T) )
unzip ran xys <= rec xys
{ unzip ran xys <= case xys
{ unzip ran vnil => pair vnil vnil
unzip ran (vcons xy xys) <= with (unzip run xys) ran
{ unzip (also ran x) (vcons xy xys) <= case x
{ unzip (also ran (pair s t)) (vcons xy xys) <= case xy
{ unzip (also ran (pair s' t')) (vcons (pair s t) xys)
=> pair (vcons s s') (vcons t t')
}
}
}
}
}
--------------------------------------------------------------------
What? No auxiliary functions? Who'd'a' thought it?
Note that this is *not* the with rule which James and I gave in VfL.
The intermediate value is not abstracted from types, hence you can't
use this to do nifty rewriting, or any of the tricky dependent
examples. But for run of the mill stuff, it's not so bad.
The point is that the pattern (also ran x) certainly covers the
Run type, and it's in normal form so it doesn't get computed away.
So just nominate which thing x is, and you get another ran, so you
can do it again...
Well I thought it was funny anyway. Why ever did it take this long?
Cheers
Conor
PS The attached file shows a more interesting example (decidability of
equality for Nat, in the style of the brothers Gershwin). To elaborate it,
you'll need the bug fixes I just committed, which should start propagating
round about 4am.
--
http://www.cs.rhul.ac.uk/~conor tick tick tick tick tick tick tick
-----------------------------------------------------------------------------
data (---------! where (-----------!
! Run : * ) ! run : Run )
-----------------------------------------------------------------------------
( ran : Run ; t : T !
let !--------------------!
! also ran t : Run )
also ran t <= case ran
{ also run t => run
}
-----------------------------------------------------------------------------
( t : T !
! !
! ran : Run !
! !
! P : Run -> * ; m : all ran : Run ; x : T => P (also ran x) !
let !--------------------------------------------------------------!
! with t ran P m : P ran )
with t ran P m <= case ran
{ with t run P m => m run t
}
-----------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
-----------------------------------------------------------------------------
( P : * ! ( p : P ! ( np : P -> Zero !
data !-----------! where !--------------------! ; !----------------------!
! Dec P : * ) ! 'strue P p : Dec P ) ! 'sfalse P np : Dec P )
-----------------------------------------------------------------------------
( x, y : Nat !
let !----------------!
! NoConf x y : * )
NoConf x y <= case x
{ NoConf zero y <= case y
{ NoConf zero zero => One
NoConf zero (suc y) => Zero
}
NoConf (suc x) y <= case y
{ NoConf (suc x) zero => Zero
NoConf (suc x) (suc y) => x = y
}
}
-----------------------------------------------------------------------------
( x, y : Nat ; q : x = y !
let !-----------------------------!
! noConf _x _y q : NoConf x y )
noConf _ x _ y q <= case q
{ noConf _ x _ x refl <= case x
{ noConf _ zero _ zero refl => ()
noConf _ (suc x) _ (suc x) refl => refl
}
}
-----------------------------------------------------------------------------
( f : S -> T ; g : R -> S ; r : R !
let !-----------------------------------!
! comp f g r : T )
comp f g r => f (g r)
-----------------------------------------------------------------------------
( ran : Run ; i, j : Nat !
let !-----------------------------!
! natEq ran i j : Dec (i = j) )
natEq ran i j <= rec i
{ natEq ran i j <= case i
{ natEq ran zero j <= case j
{ natEq ran zero zero => 'strue ? refl
natEq ran zero (suc j) => 'sfalse ? noConf
}
natEq ran (suc i) j <= case j
{ natEq ran (suc i) zero => 'sfalse ? noConf
natEq ran (suc i) (suc j) <= with (natEq run i j) ran
{ natEq (also ran x) (suc i) (suc j) <= case x
{ natEq (also ran ('strue (i = i) refl)) (suc i) (suc i)
=> 'strue ? refl
natEq (also ran ('sfalse (i = j) np)) (suc i) (suc j)
=> 'sfalse ? (comp np noConf)
}
}
}
}
}
-----------------------------------------------------------------------------
inspect natEq run (suc (suc zero)) (suc (suc zero))
=>
'strue (suc (suc zero) = suc (suc zero)) refl
: Dec (suc (suc zero) = suc (suc zero))
-----------------------------------------------------------------------------
inspect natEq run (suc (suc zero)) (suc zero)
=>
'sfalse (suc (suc zero) = suc zero)
% (lam r => !
! noConf _ (suc zero) _ zero !
! % (noConf _ (suc (suc zero)) _ (suc zero) r))
: Dec (suc (suc zero) = suc zero)
-----------------------------------------------------------------------------
( S, T : * ! ( s : S ; t : T !
data !--------------! where !---------------------!
! Pair S T : * ) ! pair s t : Pair S T )
-----------------------------------------------------------------------------
( n : Nat ; X : * ! ( x : X ; xs : Vec n X !
data !------------------! where (------------! ; !-----------------------!
! Vec n X : * ) ! vnil : ! ! vcons x xs : !
! Vec zero ! ! Vec (suc n) X )
! % X )
-----------------------------------------------------------------------------
( ran : Run ; xys : Vec n (Pair S T) !
let !------------------------------------------!
! unzip ran xys : Pair (Vec n S) (Vec n T) )
unzip ran xys <= rec xys
{ unzip ran xys <= case xys
{ unzip ran vnil => pair vnil vnil
unzip ran (vcons xy xys) <= with (unzip run xys) ran
{ unzip (also ran x) (vcons xy xys) <= case x
{ unzip (also ran (pair s t)) (vcons xy xys) <= case xy
{ unzip (also ran (pair s' t')) (vcons (pair s t) xys)
=> pair (vcons s s') (vcons t t')
}
}
}
}
}
-----------------------------------------------------------------------------
