Hi,
had just liked to flip over a predicate transformer that I tinkered
with today.
------------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
------------------------------------------------------------------------------
( n : Nat ! ( i : Fin n !
data !-----------! where (------------------! ; !--------------------!
! Fin n : * ) ! fz : Fin (suc n) ) ! fs i : Fin (suc n) )
------------------------------------------------------------------------------
( A, B : * ! ( a : A ! ( b : B !
data !------------! where !----------------! ; !----------------!
! Or A B : * ) ! inl a : Or A B ) ! inr b : Or A B )
------------------------------------------------------------------------------
( n : Nat ; P : Fin n -> * !
let !---------------------------!
! Any n P : * )
Any n P <= rec n
{ Any n P <= case n
{ Any zero P => Fin zero
Any (suc n) P => Or (Any n (lam i => P (fs i))) (P fz)
}
}
------------------------------------------------------------------------------
( n : Nat ; P : Fin n -> * ; p : Any n P !
let !------------------------------------------!
! findex n P p : Fin n )
findex n P p <= rec n
{ findex n P p <= case n
{ findex zero P p <= case p
findex (suc n) P p <= case p
{ findex (suc n) P (inl a) => fs (findex n (lam i => P (fs i)) a)
findex (suc n) P (inr b) => fz
}
}
}
------------------------------------------------------------------------------
( n : Nat ; P : Fin n -> * ; p : Any n P !
let !------------------------------------------!
! find n P p : P (findex n P p) )
find n P p <= rec n
{ find n P p <= case n
{ find zero P p <= case p
find (suc n) P p <= case p
{ find (suc n) P (inl a) => find n (lam i => P (fs i)) a
find (suc n) P (inr b) => b
}
}
}
------------------------------------------------------------------------------
( A : * ; B : A -> * ! ( a : A ; b : B a !
data !---------------------! where !---------------------!
! Sigma A B : * ) ! tup a b : Sigma A B )
------------------------------------------------------------------------------
( n : Nat ; P : (Fin n) -> * ; p : Any n P !
let !--------------------------------------------!
! chexist n P p : Sigma (Fin n) P )
chexist n P p => tup (findex n P p) (find n P p)
------------------------------------------------------------------------------
I was hoping it could be useful for formulating the pigoeon hole
principle.
------------------------------------------------------------------------------
( i : Fin (suc n) ; j : Fin n !
let !------------------------------!
! thin i j : Fin (suc n) )
thin i j <= rec i
{ thin i j <= case i
{ thin fz j => fs j
thin (fs i) j <= case j
{ thin (fs i) fz => fz
thin (fs i) (fs j) => fs (thin i j)
}
}
}
------------------------------------------------------------------------------
( A, B : * ! ( a : A ; b : B !
data !-------------! where !--------------------!
! And A B : * ) ! pair a b : And A B )
------------------------------------------------------------------------------
( n : Nat ; P : Fin n -> * !
let !---------------------------!
! All n P : * )
All n P <= rec n
{ All n P <= case n
{ All zero P => Fin (suc zero)
All (suc n) P => And (All n (lam i => P (fs i))) (P fz)
}
}
------------------------------------------------------------------------------
( i ; j !
data !-----------! where (-------------!
! H i j : * ) ! occ : H i j )
------------------------------------------------------------------------------
[ ( n : Nat ; p : All (suc n) (lam i => Any n (lam j => H i j)) !!
!let !--------------------------------------------------------------!!
! ! PHP n p : Any n (lam j => Any (suc! (lam i => !! !!
! ! ! !% n) ! And (H i j) !! !!
! ! ! ! % (H (thin i j) j))) )]
------------------------------------------------------------------------------
Cheers,
Sebastian
