------------------------------------------------------------------------------
--
-- Agda demonstration code for
-- JAIST/TRUST - AIST/CVS joint workshop on verification technology (VERITE)
-- 2005-09-22, Kanazawa Bunka Hall
--   Peter Dybjer    (Chalmers University of Techonology)
--   Makoto Takeyama (AIST/CVS)
--
------------------------------------------------------------------------------

identity :: (X::Set)-> X -> X
identity = \(X::Set)-> \(x::X)-> x

-- A fragment of predicate logic.   Shallow embedding
data Absurd =                    -- Absurdity proposition is
                                 -- the inductive type with
                                 -- no constructor

Not :: Set -> Set                -- Intuitionistic negation
Not A = A -> Absurd

data Or(P,Q::Set) = inl(p::P) | inr(q::Q)
                                 -- read "in left",  "in right"

data Exists(A::Set)(P::A -> Set)
   = introEx(wit::A)(prf::P wit)      -- "witness" and "proof"

witness(A::Set)(P::A -> Set)::Exists A P -> A
   = \ex -> case ex of (introEx wit prf)-> wit 

ex_prf(A::Set)(P::A -> Set)
   ::(ex :: Exists A P) -> P (witness ex)
   = \ex -> case ex of (introEx wit prf)-> prf

----------------

lem(A::Set)(P::A -> Set):: Exists A P -> Not((x::A)-> Not(P x))
  = \asm -> \asm'-> asm' (witness asm) (ex_prf asm)
----------------


-- Type theoretic axiom of choice
ac(A,B::Set)(R::A -> B -> Set)

  :: ((x::A)-> Exists B (\y -> R x y)) ->
      Exists (A -> B) (\f -> (x::A)-> R x (f x))
  = \h -> introEx (\x -> witness (h x) )
                  (\x -> ex_prf (h x) )

------------------

data Nat = zer | suc(n::Nat)

elimNat::(P    :: Nat -> Set)->
         (base :: P zer)->
         (step :: (n'::Nat)-> P n' -> P (suc n'))->

         (n :: Nat) -> P n

elimNat P base step n =
    case n of (zer   )-> base
              (suc n')-> step n' (elimNat P base step n')

eqNat :: Nat -> Nat -> Bool
eqNat m n = case m of
            (zer   )-> case n of (zer   )-> True
                                 (suc n')-> False
            (suc m')-> case n of (zer   )-> False
                                 (suc n')-> eqNat m' n'

data Ty = X(nam::String) | (=>)(A,B::Ty)
data Tm = K | S | ($)(a,b::Tm)

idata  In :: Tm -> Ty -> Set where
  axK(A,B::Ty)   :: In K (A => (B => A))
  axS(A,B,C::Ty) :: In S ((A =>(B => C)) =>
                         ((A => B) =>
                          (A => C)))

  axAp(A,B::Ty)(f,a::Tm)
      (d1::In f (A => B))(d2::In a A)
      --------------------------------
                 :: In (f $ a) B

Typable :: Tm -> Set
Typable a = Exists Ty (\A -> In a A)

dec_type :: (a::Tm)-> Typable a `Or` Not (Typable a)
dec_type a0 =  
  case a0 of
  (K     )-> inl (introEx (X "A" => (X "B" => (X "A")))
                  (axK (X "A") (X "B")))

  (S     )-> inl (introEx (X "A" => (X "B" => (X "C")) =>
                           ((X "A" => (X "B")) => (X "A" => (X "C"))))
                  (axS (X "A") (X "B") (X "C")))

  (f $ a)-> {! some clever stuff here !}