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