[Agda] 2 questions
Danko Ilik
danko at student.chalmers.se
Fri Dec 30 19:25:32 CET 2005
Hello,
I'm trying to use Agda, the Types 2005 summer school version.
1. I get the following error when I check-load: "error in process
filter: Stack overflow in regexp matcher". Do you have any suggestion on
how to avoid this?
2. How can I define an axiom of a type which is not Set? In agdalight
you just leave out the proof term, but here it doesn't work...
I attach the problematic file ExtAC.agda. The axiom which I want to have
is ExtAC.
Thanks and happy holidays,
Danko
-------------- next part --------------
--#include "Framework.agda"
-- The extensional axiom of choice
ExtAC :: ((A,B::Set) |-> (R::A->B->Set) ->
(eqA::Rel A) -> (eqB::Rel B) ->
EquivRel eqA -> EquivRel eqB ->
((x,y::A) -> x `eqA` y -> (z::B) -> R x z -> R y z) ->
((x,y::B) -> x `eqB` y -> (z::A) -> R z x -> R z y) ->
((x::A) -> Exists (\y -> R x y)) ->
Exists (\(f::A->B) ->
((x::A) -> R x (f x)) /\
((x,y::A) -> x `eqA` y -> (f x) `eqB` (f y))))
ExtAC = ?
LEM :: (P::Set) -> P \/ Not P
LEM P = let -- an equivalence relation on Bool
eqb :: Rel Bool
eqb = \a b -> case a of
(False)-> case b of
(False)-> Unit
(True)-> Empty
(True)-> case b of
(False)-> Empty
(True)-> Unit
Equiv_eqb :: EquivRel eqb
Equiv_eqb = struct
isRefl:: Reflexive eqb
isRefl = \(x::Bool)->
case x of
(False)-> unit
(True)-> unit
isSymm:: Symmetrical eqb
isSymm = \(x1,x2::Bool) |-> \(h::eqb x1 x2)->
case x1 of
(False)-> case x2 of
(False)-> unit
(True)-> h
(True)-> case x2 of
(False)-> h
(True)-> unit
isTrans:: Transitive eqb
isTrans = \(x1,x2,x3::Bool) |->
\(h1::eqb x1 x2)->
\(h2::eqb x2 x3)->
case x1 of
(False)-> case x2 of
(False)-> case x3 of
(False)-> unit
(True)-> h2
(True) -> case x3 of
(False) -> unit
(True) -> h1
(True) -> case x2 of
(False)-> case x3 of
(False)-> h1
(True)-> unit
(True) -> case x3 of
(False) -> h2
(True) -> unit
-- eqb is decidable
Decid_eqb :: (x,y::Bool) -> eqb x y \/ Not (eqb x y)
Decid_eqb x y = case x of
(False)-> case y of
(False)-> orI1 unit
(True)-> orI2 (\ff -> ff )
(True)-> case y of
(False)-> orI2 (\ff -> ff )
(True)-> orI1 unit
-- the relation R
R :: Rel Bool
R a b = eqb a b \/ P
-- which is an equivalence
EquivR :: EquivRel R
EquivR = struct --ova moze mnogu poednostavno samo orI1 i Equiv_eq
isRefl :: Reflexive R
isRefl = \(x::Bool)->
case x of
(False)-> orI1 unit
(True)-> orI1 unit
isSymm:: Symmetrical R
isSymm = \(x1,x2::Bool) |-> \(h::R x1 x2)->
case x1 of
(False)-> case x2 of
(False)-> orI1 unit
(True)-> h
(True)-> case x2 of
(False)-> h
(True)-> orI1 unit
isTrans:: Transitive R
isTrans = \(x1,x2,x3::Bool) |->
\(h1::Plus (eqb x1 x2) P)->
\(h2::Plus (eqb x2 x3) P)->
case x1 of
(False)-> case x2 of
(False)-> case x3 of
(False)-> orI1 unit
(True)-> h2
(True) -> case x3 of
(False) -> orI1 unit
(True) -> h1
(True) -> case x2 of
(False)-> case x3 of
(False)-> h1
(True)-> orI1 unit
(True) -> case x3 of
(False) -> h2
(True) -> orI1 unit
-- R is left-extensional
LExtR :: (x,y::Bool) -> R x y -> (z::Bool) -> R x z -> R y z
LExtR x y h1 z h2 = EquivR.isTrans (EquivR.isSymm h1) h2
-- R is right-extensional
RExtR :: (x,y::Bool) -> eqb x y -> (z::Bool) -> R z x -> R z y
RExtR x y h1 z h2 = EquivR.isTrans h2 (orI1 h1)
-- use ExtAC to get the choice function
choicef :: Exists (\(f::Bool->Bool) ->
((x::Bool) -> R x (f x)) /\
((x,y::Bool) -> x `R` y -> (f x) `eqb` (f y)))
choicef = let lemma :: (x::Bool) -> Exists (\y -> R x y)
lemma = \(x::Bool)-> pair x (EquivR.isRefl x )
in ExtAC R R eqb EquivR Equiv_eqb LExtR RExtR lemma
-- extract the function only
cf :: Bool->Bool
cf = fst choicef
-- decidability, direction 1
decid1 :: eqb (cf False) (cf True) -> P
decid1 =
let
lemma7 :: R False True -> P
lemma7 h = orE h
(\ff -> whenEmpty P ff )
(\p -> p )
lemma5 :: (x,y::Bool) -> eqb (cf x) (cf y) -> R x y
lemma5 x y h =
let
step1 :: R x (cf x)
step1 = snd choicef
step2 :: R x (cf y)
step2 = RExtR (cf x )
(cf y )
h
x
(fst (snd choicef))
step3 :: R y (cf y)
step3 = snd choicef
step4 :: R (cf y) y
step4 = EquivR.isSymm step3
in EquivR.isTrans step2 step4
in \h -> lemma7 (lemma5 False True h)
-- decidability, direction 2
decid2 :: P -> eqb (cf False) (cf True)
decid2 =
let lemma8 :: P -> R False True
lemma8 = orI2
lemma6 :: (x,y::Bool) -> R x y -> eqb (cf x) (cf y)
lemma6 = snd (snd choicef )
in \h -> lemma6 False True (lemma8 h)
-- a logical tautology we need
taut (A,B,C,D::Set) :: A \/ B -> (A->C) -> (B->D) -> C \/ D
taut = \(h::Plus A B)->
\(h1::A -> C)->
\(h2::B -> D)->
orE h
(\(a::A)->
orI1 (h1 a ))
(\(b::B)->
orI2 (h2 b ))
-- and an other one, constraposition
contrap (A,B::Set) :: (A->B) -> Not B -> Not A
contrap h1 h2 = \a -> h2 (h1 a)
in taut (Decid_eqb (cf False) (cf True))
decid1
(contrap decid2)
-------------- next part --------------
---------------------------------------------------------------------------
--- The empty set --------------------------------------------------------
---------------------------------------------------------------------------
-- The empty set corresponds to absurdity ---------------------------------
data Empty :: Set =
elimEmpty :: (C::Empty -> Set) -> (z::Empty) -> C z
elimEmpty C z = case z of { }
whenEmpty :: (X::Set) -> Empty -> X
whenEmpty X z = case z of { }
Not :: Set -> Set
Not X = X -> Empty
absurdElim (A::Set) :: A -> Not A -> (X::Set) -> X
absurdElim h h' X = whenEmpty X (h' h)
---------------------------------------------------------------------------
--- The unit set ---------------------------------------------------------
---------------------------------------------------------------------------
-- The unit set corresponds to truth --------------------------------------
data Unit :: Set = unit
elimUnit :: (C::Unit -> Set) -> (c_unit::C unit) -> (u::Unit) -> C u
elimUnit C c_unit u = case u of
(unit) -> c_unit
---------------------------------------------------------------------------
-- The (binary) disjoint union. -------------------------------------------
---------------------------------------------------------------------------
-- Corresponds to or ------------------------------------------------------
data Plus (X,Y::Set) = inl (x::X) | inr (y::Y)
elimPlus (X,Y::Set) ::
(C::Plus X Y -> Set) ->
(c_lft::(x::X) -> C (inl x)) ->
(c_rgt::(y::Y) -> C (inr y)) ->
(xy::Plus X Y) ->
C xy
elimPlus C c_lft c_rgt xy = case xy of
(inl x) -> c_lft x
(inr y) -> c_rgt y
whenPlus (X,Y,Z::Set) :: (f::X -> Z) -> (g::Y -> Z) -> (Plus X Y -> Z)
whenPlus f g = \xy ->
case xy of
(inl x) -> f x
(inr y) -> g y
mapPlus (X1,X2,Y1,Y2::Set) ::
(f::X1 -> X2) -> (g::Y1 -> Y2) -> (Plus X1 Y1 -> Plus X2 Y2)
mapPlus f g = whenPlus (\x1 -> inl (f x1)) (\y1 -> inr (g y1))
---------------------------------------------------------------------------
-- Dependent pairs. -------------------------------------------------------
---------------------------------------------------------------------------
-- Corresponds to existential ---------------------------------------------
data Sigma (|X::Set) (Y::X -> Set) =
pair (x::X)(y::Y x)
fst (X::Set)(Y::(X -> Set)) :: Sigma Y -> X
fst xy = case xy of
(pair x y) -> x
snd (X::Set)(Y::(X -> Set)) :: (xy::Sigma Y) -> Y (fst xy)
snd xy = case xy of
(pair x y) -> y
curry (X::Set)(Y::(X -> Set))(Z::Set) ::
(f::Sigma (\x -> Y x) -> Z) -> (x::X) |-> (Y x -> Z)
curry f = \x |-> \y -> f (pair x y)
uncurry (X::Set)(Y::(X -> Set))(Z::Set) ::
((x::X) -> (Y x -> Z)) -> Sigma (\x -> Y x) -> Z
uncurry f xy = f (fst xy) (snd xy)
curryS (X::Set)(Y::(X -> Set)) ::
(Z::Sigma (\x -> Y x) -> Set) ->
(f::(xy::Sigma (\x -> Y x)) -> Z xy) ->
(x::X) ->
(y::Y x) ->
Z (pair x y)
curryS Z f = \(x::X) -> \(y::Y x) -> f (pair x y)
uncurryS (X::Set)(Y::(X -> Set)) ::
(Z::Sigma (\x -> Y x) -> Set) ->
(f::(x::X) -> (y::Y x) -> Z (pair x y)) ->
(xy::Sigma (\x -> Y x)) ->
Z xy
uncurryS Z f xy = case xy of
(pair x y) -> f x y
mapSigma (X::Set)(Y1,Y2::X -> Set) ::
(f::(x::X) -> (Y1 x -> Y2 x)) -> Sigma (\x -> Y1 x) -> Sigma (\x -> Y2 x)
mapSigma f p = case p of
(pair x y) -> pair x (f x y)
Pred :: Set -> Type
Pred X = X -> Set
Rel :: Set -> Type
Rel X = X -> X -> Set
(/\) :: Set -> Set -> Set
P /\ Q = Sigma (\(p::P) -> Q)
(<->) :: Set -> Set -> Set
P <-> Q = (P->Q) /\ (Q->P)
Exists (X::Set) :: (P::Pred X) -> Set
Exists P = Sigma P
witness (X::Set)(P::Pred X) :: Exists P -> X
witness h = fst h
--proof (X::Set)(P::Pred X) :: Exists P -> P
--proof h = snd h
(\/) :: Set -> Set -> Set
P \/ Q = Plus P Q
orI1 (P,Q::Set) :: P -> P \/ Q
orI1 p = inl p
orI2 (P,Q::Set) :: Q -> P \/ Q
orI2 q = inr q
orE (P,Q,R::Set) :: P \/ Q -> (P->R) -> (Q->R) -> R
orE pq pr qr = case pq of
(inl p)-> pr p
(inr q)-> qr q
-- data Bool = False | True
-- is pre-defined
elimBool :: (C :: Bool -> Type) ->
(c_t :: C True) ->
(c_f :: C False) ->
(b :: Bool) ->
C b
elimBool C c_t c_f b = case b of
(False) -> c_f
(True) -> c_t
liftBool :: Bool -> Set
liftBool b = if b then Unit else Empty
T :: Bool -> Set
T b = if b then Unit else Empty
not :: Bool -> Bool
not b = if b then False else True
(&&) :: Bool -> Bool -> Bool
b1 && b2 = if b1 then b2 else False
(||) :: Bool -> Bool -> Bool
b1 || b2 = if b1 then True else b2
imp :: (x,y::Bool) -> Bool
imp x y = (not x) || y
iff :: (x,y::Bool) -> Bool
iff x y = x `imp` y && y `imp` x
pred :: (X::Set) -> Set
pred X = X -> Bool
rel :: (X::Set) -> Set
rel X = X -> X -> Bool
Reflexive (X::Set) :: (R::Rel X) -> Set
Reflexive R = (x::X) -> x `R` x
Symmetrical (X::Set) :: (R::Rel X) -> Set
Symmetrical R = (x1,x2::X) |-> (x1 `R` x2 -> x2 `R` x1)
Transitive (X::Set) :: (R::Rel X) -> Set
Transitive R = (x1,x2,x3::X) |-> (x1 `R` x2 -> x2 `R` x3 -> x1 `R` x3)
Substitutive (X::Set) :: (R::Rel X) -> Type
Substitutive R = (P::X -> Set) ->
(x1,x2::X) |->
x1 `R` x2 -> P x1 -> P x2
EquivRel(X::Set) :: (R::Rel X) -> Set
EquivRel R = sig
isRefl :: Reflexive R
isSymm :: Symmetrical R
isTrans :: Transitive R
DRel :: Set -> Set
DRel X = X -> X -> Bool
dRel (X::Set) :: DRel X -> Rel X
dRel R = \x y -> liftBool (R x y)
More information about the Agda
mailing list