------------------------------------------------------------------------------ -- -- 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 !}