------------------------------------------------------------------------------- -- -- SET (in Hedberg library) for agda2 -- as of 2006.9.29 morning -- Yoshiki. -- module SET where ---------------------------------------------------------------------------- -- Auxiliary. ---------------------------------------------------------------------------- -- no : (x : A) -> B : Set if A : Set B : Set -- yes : (x : A) -> B type if A type B type -- El M type if M : Set data Unop (A : Set) : Set1 where unopI : (A -> A) -> Unop A data Pred (A : Set) : Set1 where PredI : (A -> Set) -> Pred A data Rel (A : Set) : Set1 where RelI : (A -> A -> Set) -> Rel A data Reflexive {A : Set} (R : A -> A -> Set) : Set where reflexiveI : ((a : A) -> R a a) -> Reflexive R data Symmetrical {A : Set} (R : A -> A -> Set) : Set where symmetricalI : ({a b : A} -> R a b -> R a b) -> Symmetrical R data Transitive {A : Set} (R : A -> A -> Set) : Set where transitiveI : ({a b c : A} -> R a b -> R b c -> R a c) -> Transitive R compositionalI : {A : Set} -> (R : A -> A -> Set) -> ({a b c : A} -> R b c -> R a b -> R a c) -> Transitive R compositionalI {A} R f = transitiveI (\{a b c : A} -> \(x : R a b) -> \(y : R b c) -> f y x) data Substitutive {A : Set} (R : A -> A -> Set) : Set1 where substitutiveI : ((P : A -> Set) -> {a b : A} -> R a b -> P a -> P b) -> Substitutive R data Collapsed (A : Set) : Set1 where collapsedI : ((P : A -> Set) -> {a b : A} -> P a -> P b) -> Collapsed A cmp : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C cmp f g a = f (g a) seq : {A B C : Set} -> (A -> B) -> (B -> C) -> A -> C seq f g = cmp g f S : {A B C : Set} -> (C -> B -> A) -> (C -> B) -> C -> A S x y z = x z (y z) K : {A B : Set} -> A -> B -> A K x y = x I : {A : Set} -> A -> A I a = a -- of course I = S K K id = \{A : Set} -> I {A} const = \{A B : Set} -> K {A}{B} -- Set version pS : {P Q R : Set} -> (R -> Q -> P) -> (R -> Q) -> R -> P pS x y z = x z (y z) pK : {P Q : Set} -> P -> Q -> P pK x y = x pI : {P : Set} -> P -> P pI a = a proj : {A : Set} -> (B : A -> Set) -> (a : A) -> (f : (aa : A) -> B aa) -> B a proj B a f = f a flip : {A B C : Set} (f : A -> B -> C) (b : B) (a : A) -> C flip f b a = f a b -- separate definition of FlipRel is necessary because it is not the case -- that Set : Set. FlipRel : {A : Set} -> (R : A -> A -> Set) -> (a b : A) -> Set FlipRel R a b = R b a ---------------------------------------------------------------------------- -- Product sets. ---------------------------------------------------------------------------- -- Prod : (A : Set) -> (A -> Set) -> Set -- Prod A B = (a : A) -> B a -- The above is not type-correct since (a : A) -> B a is not well-formed -- but the following works. data Prod (A : Set) (B : A -> Set) : Set where prodI : ((a : A) -> B a) -> Prod A B mapProd : {A : Set} -> {B C : A -> Set} -> ((a : A) -> B a -> C a) -> Prod A B -> Prod A C mapProd {A} f (prodI g) = prodI (\(a : A) -> f a (g a)) -- data Fun (A B : Set) : Set1 where -- funI : (A -> B) -> Fun A B Fun : Set -> Set -> Set Fun A B = Prod A (\(_ : A) -> B) mapFun : {A B C D : Set} -> (B -> A) -> (C -> D) -> (A -> C) -> B -> D mapFun {A} {B} {C} {D} f g h x = g (h (f x)) -- mapFun (|X1 |X2 |Y1 |Y2 :: Set) -- :: (X2 -> X1) -> (Y1 -> Y2) -> (X1 -> Y1) -> X2 -> Y2 -- = \f -> \g -> \h -> \x -> -- g (h (f x)) --------------------------------------------------------------------------- -- Identity proof sets. --------------------------------------------------------------------------- -- to accept the following definition more general scheme of -- inductive definition is required -- data Id (A : Set) (a b : A) : Set1 where -- ref : (a : A) -> Id A a a -- -- elimId (|X :: Set) -- (C :: (x1 x2 :: X) |-> Id x1 x2 -> Set) -- (refC :: (x :: X) -> C (refId x)) -- (|x1 |x2 :: X) -- (u :: Id x1 x2) :: -- C u -- = case u of { (ref x) -> refC x;} -- -- abstract whenId (|X :: Set)(C :: Rel X)(c :: (x :: X) -> C x x) -- :: (x1 x2 :: X) |-> Id x1 x2 -> C x1 x2 -- = elimId (\x1 x2 |-> \(u :: Id x1 x2) -> C x1 x2) c -- -- abstract substId (|X :: Set) :: Substitutive Id -- = \(C :: Pred X) -> -- whenId (\x1 x2 -> C x1 -> C x2) (\x -> id) -- -- abstract mapId (|X :: Set)(|Y :: Set)(f :: X -> Y) -- :: (x1 x2 :: X) |-> Id x1 x2 -> Id (f x1) (f x2) -- = whenId (\x1 x2 -> Id (f x1) (f x2)) (\(x :: X) -> refId (f x)) -- -- abstract symId (|X :: Set) :: Symmetrical Id -- = whenId (\(x1 x2 :: X) -> Id x2 x1) refId -- -- abstract cmpId (|X :: Set) :: Compositional Id -- = let lem :: (x y :: X) |-> Id x y -> (z :: X) |-> Id z x -> Id z y -- = whenId ( \(x y :: _) -> (z :: X) |-> Id z x -> Id z y) -- ( \x -> \z |-> id) -- in \(x1 x2 x3 :: _) |-> -- \(u :: Id x2 x3) -> -- \(v :: Id x1 x2) -> -- lem u v -- -- abstract tranId (|X :: Set) :: Transitive Id -- = \(x1 x2 x3 :: X) |-> -- \(u :: Id x1 x2) -> -- \(v :: Id x2 x3) -> -- cmpId v u ---------------------------------------------------------------------------- -- The empty set. ---------------------------------------------------------------------------- data Zero : Set where -- --abstract whenZero (X :: Set)(z :: Zero) :: X -- -- = case z of { } -- do not know how to encode whenZero; the following does not work. -- whenZero : (X : Set) -> (z : Zero) -> X -- whenZero X z = -- --elimZero (C :: Zero -> Set)(z :: Zero) :: C z -- -- = case z of { } -- elimZero either! -- elimZero : (C : Zero -> Set) -> (z : Zero) -> C z -- elimZero C z = -- -- abstract collZero :: Collapsed Zero -- = \(C :: Zero -> Set) -> -- \(z1 z2 :: Zero) |-> -- \(c :: C z1) -> -- case z1 of { } -- ---------------------------------------------------------------------------- -- The singleton set. ---------------------------------------------------------------------------- data Unit : Set where uu : Unit elUnit = uu elimUnit : (C : Unit -> Set) -> C uu -> (u : Unit) -> C u elimUnit C c uu = c -- Do not know of the exact use of Collapse! -- collUnit : (C : Unit -> Set) -> {u1 u2 : Unit} -> C u1 -> Collapsed Unit -- collUnit C {uu} {uu} A = collapsedI (\(P : Unit -> Set) -> \{a b : Unit} -> \(y : P a) -> A) -- abstract collUnit :: Collapsed Unit -- = \(C :: Unit -> Set) -> -- \(u1 u2 :: Unit) |-> -- \(c :: C u1) -> -- case u1 of { (tt) -> case u2 of { (tt) -> c;};} --------------------------------------------------------------------------- -- The successor set adds a new element. --------------------------------------------------------------------------- data Succ (A : Set) : Set where zerS : Succ A sucS : A -> Succ A zerSucc = \{A : Set} -> zerS {A} sucSucc = \{A : Set} -> sucS {A} elimSucc : {X : Set} -> (C : Succ X -> Set) -> C zerS -> ((x : X) -> C (sucS x)) -> (xx : Succ X) -> (C xx) elimSucc C c_z c_s zerS = c_z elimSucc C c_z c_s (sucS x) = c_s x whenSucc : {X Y : Set} -> Y -> (X -> Y) -> (Succ X) -> Y whenSucc y_z y_s zerS = y_z whenSucc y_z y_s (sucS x) = y_s x mapSucc : {X Y : Set} -> (X -> Y) -> Succ X -> Succ Y mapSucc {X} {_} f = whenSucc zerS (\(x : X) -> sucS (f x)) --------------------------------------------------------------------------- -- The (binary) disjoint union. --------------------------------------------------------------------------- data Plus (A B : Set) : Set where inl : A -> Plus A B inr : B -> Plus A B elimPlus : {X Y : Set} -> (C : Plus X Y -> Set) -> ((x : X) -> C (inl x)) -> ((y : Y) -> C (inr y)) -> (z : Plus X Y) -> C z elimPlus {X} {Y} C c_lft c_rgt (inl x) = c_lft x elimPlus {X} {Y} C c_lft c_rgt (inr x) = c_rgt x when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> Plus X Y -> Z when {X} {Y} {Z} f g (inl x) = f x when {X} {Y} {Z} f g (inr y) = g y whenplus : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> Plus X Y -> Z whenplus = when mapPlus : {X1 X2 Y1 Y2 : Set} -> (X1 -> X2) -> (Y1 -> Y2) -> Plus X1 Y1 -> Plus X2 Y2 mapPlus f g = when (\x1 -> inl (f x1)) (\y1 -> inr (g y1)) swapPlus : {X Y : Set} -> Plus X Y -> Plus Y X swapPlus = when inr inl ---------------------------------------------------------------------------- -- Dependent pairs. ---------------------------------------------------------------------------- data Sum (A : Set) (B : A -> Set) : Set where sumI : (fst : A) -> B fst -> Sum A B depPair : {A : Set} -> {B : A -> Set} -> (a : A) -> B a -> Sum A B depPair a b = sumI a b depFst : {A : Set} -> {B : A -> Set} -> (c : Sum A B) -> A depFst (sumI fst snd) = fst depSnd : {A : Set} -> {B : A -> Set} -> (c : Sum A B) -> B (depFst c) depSnd (sumI fst snd) = snd depCur : {A : Set} -> {B : A -> Set} -> {C : Set} -> (f : Sum A B -> C) -> (a : A) -> B a -> C depCur f = \a -> \b -> f (depPair a b) -- the above works but the below does not---why? -- depCur : {X : Set} -> {Y : X -> Set} -> {Z : Set} -> (f : Sum X Y -> Z) -- -> {x : X} -> Y x -> Z -- depCur {X} {Y} {Z} f = \{x} -> \y -> f (depPair x y) -- Error message : -- When checking that the expression \{x} -> \y -> f (depPair x y) -- has type Y _x -> Z -- found an implicit lambda where an explicit lambda was expected depUncur : {A : Set} -> {B : A -> Set} -> {C : Set} -> ((a : A) -> B a -> C) -> Sum A B -> C depUncur f ab = f (depFst ab) (depSnd ab) depCurry : {A : Set} -> {B : A -> Set} -> {C : Sum A B -> Set} -> (f : (ab : Sum A B) -> C ab) -> (a : A) -> (b : B a) -> C (depPair a b) depCurry f a b = f (depPair a b) depUncurry : {A : Set} -> {B : A -> Set} -> {C : Sum A B -> Set} -> (f : (a : A) -> (b : B a) -> C (depPair a b)) -> (ab : Sum A B) -> C ab depUncurry f (sumI fst snd) = f fst snd mapSum : {A : Set} -> {B1 : A -> Set} -> {B2 : A -> Set} -> (f : (a : A) -> B1 a -> B2 a) -> Sum A B1 -> Sum A B2 mapSum f (sumI fst snd) = depPair fst (f fst snd) elimSum = \{A : Set}{B : A -> Set}{C : Sum A B -> Set} -> depUncurry{A}{B}{C} --------------------------------------------------------------------------- -- Nondependent pairs (binary) cartesian product. --------------------------------------------------------------------------- Times : Set -> Set -> Set Times A B = Sum A (\(_ : A) -> B) pair : {A : Set} -> {B : Set} -> A -> B -> Times A B pair a b = sumI a b fst : {A : Set} -> {B : Set} -> Times A B -> A fst (sumI a _) = a snd : {A : Set} -> {B : Set} -> Times A B -> B snd (sumI _ b) = b pairfun : {C : Set} -> {A : Set} -> {B : Set} -> (C -> A) -> (C -> B) -> C -> Times A B pairfun f g c = pair (f c) (g c) mapTimes : {A1 : Set} -> {A2 : Set} -> {B1 : Set} -> {B2 : Set} -> (A1 -> A2) -> (B1 -> B2) -> Times A1 B1 -> Times A2 B2 mapTimes f g (sumI a b) = pair (f a) (g b) swapTimes : {A : Set} -> {B : Set} -> Times A B -> Times B A swapTimes (sumI a b) = sumI b a cur : {A : Set} -> {B : Set} -> {C : Set} -> (f : Times A B -> C) -> A -> B -> C cur f a b = f (pair a b) uncur : {A : Set} -> {B : Set} -> {C : Set} -> (A -> B -> C) -> Times A B -> C uncur f (sumI a b) = f a b curry : {A : Set} -> {B : Set} -> {C : Times A B -> Set} -> ((p : Times A B) -> C p) -> (a : A) ->(b : B) -> C (pair a b) curry f a b = f (pair a b) uncurry : {A : Set} -> {B : Set} -> {C : Times A B -> Set} -> ((a : A) -> (b : B) -> C (pair a b)) -> (p : Times A B) -> C p uncurry f (sumI a b) = f a b elimTimes = \{A B : Set}{C : Times A B -> Set} -> uncurry{A}{B}{C} --------------------------------------------------------------------------- -- Natural numbers. --------------------------------------------------------------------------- data Nat : Set where zero : Nat succ : Nat -> Nat elimNat : (C : Nat -> Set) -> (C zero) -> ((m : Nat) -> C m -> C (succ m)) -> (n : Nat) -> C n elimNat C c_z c_s zero = c_z elimNat C c_z c_s (succ m') = c_s m' (elimNat C c_z c_s m') ---------------------------------------------------------------------------- -- Linear universe of finite sets. ---------------------------------------------------------------------------- Fin : (m : Nat) -> Set Fin zero = Zero Fin (succ n) = Succ (Fin n) {- Fin 0 = {} Fin 1 = { zerS } Fin 2 = { zerS (sucS zerS) } Fin 3 = { zerS (sucS zerS) (sucS (sucS zerS)) } -} valFin : (n' : Nat) -> Fin n' -> Nat valFin zero () valFin (succ n) zerS = zero valFin (succ n) (sucS x) = succ (valFin n x) zeroFin : (n : Nat) -> Fin (succ n) zeroFin n = zerS succFin : (n : Nat) -> Fin n -> Fin (succ n) succFin n N = sucS N ---------------------------------------------------------------------------- -- Do these really belong here? ---------------------------------------------------------------------------- HEAD : {A : Set} -> (n : Nat) -> (Fin (succ n) -> A) -> A HEAD n f = f (zeroFin n) TAIL : {A : Set} -> (n : Nat) -> (Fin (succ n) -> A) -> Fin n -> A TAIL n f N = f (succFin n N) ---------------------------------------------------------------------------- -- Lists. ---------------------------------------------------------------------------- data List (A : Set) : Set where nil : List A con : A -> List A -> List A elimList : {A : Set} -> (C : List A -> Set) -> (C nil) -> ((a : A) -> (as : List A) -> C as -> C (con a as)) -> (as : List A) -> C as elimList _ c_nil _ nil = c_nil elimList C c_nil c_con (con a as) = c_con a as (elimList C c_nil c_con as) ---------------------------------------------------------------------------- -- Tuples are "dependently typed vectors". ---------------------------------------------------------------------------- data Nill : Set where nill : Nill data Cons (A B : Set) : Set where cons : A -> B -> Cons A B Tuple : (n : Nat) -> (C : Fin n -> Set) -> Set Tuple zero = \ C -> Nill Tuple (succ n) = \ C -> Cons (C zerS) (Tuple n (\(N : Fin n) -> C (sucS N))) ---------------------------------------------------------------------------- -- Vectors homogeneously typed tuples. ---------------------------------------------------------------------------- Vec : Set -> Nat -> Set Vec A m = Tuple m (\(n : Fin m) -> A) ---------------------------------------------------------------------------- -- Monoidal expressions. ---------------------------------------------------------------------------- data Mon (A : Set) : Set where unit : Mon A at : A -> Mon A mul : Mon A -> Mon A -> Mon A {- -} ---------------------------------------------------------------------------- -- Propositions. ---------------------------------------------------------------------------- data Implies (A B : Set) : Set where impliesI : (A -> B) -> Implies A B data Absurd : Set where data Taut : Set where tt : Taut data Not (P : Set) : Set where notI : (P -> Absurd) -> Not P -- encoding of Exists is unsatisfactory! Its type should be Set. data Exists (A : Set) (P : A -> Set) : Set where existsI : (evidence : A) -> P evidence -> Exists A P data Forall (A : Set) (P : A -> Set) : Set where forallI : ((a : A) -> P a) -> Forall A P data And (A B : Set) : Set where andI : A -> B -> And A B Iff : Set -> Set -> Set Iff A B = And (Implies A B) (Implies B A) data Or (A B : Set) : Set where orIl : (a : A) -> Or A B orIr : (b : B) -> Or A B Decidable : Set -> Set Decidable P = Or P (Implies P Absurd) data DecidablePred {A : Set} (P : A -> Set) : Set where decidablepredIl : (a : A) -> (P a) -> DecidablePred P decidablepredIr : (a : A) -> (Implies (P a) Absurd) -> DecidablePred P data DecidableRel {A : Set} (R : A -> A -> Set) : Set where decidablerelIl : (a b : A) -> (R a b) -> DecidableRel R decidablerelIr : (a b : A) -> (Implies (R a b) Absurd) -> DecidableRel R data Least {A : Set} (_<=_ : A -> A -> Set) (P : A -> Set) (a : A) : Set where leastI : (P a) -> ((aa : A) -> P aa -> (a <= aa)) -> Least _<=_ P a data Greatest {A : Set} (_<=_ : A -> A -> Set) (P : A -> Set) (a : A) : Set where greatestI : (P a) -> ((aa : A) -> P aa -> (aa <= a)) -> Greatest _<=_ P a ---------------------------------------------------------------------------- -- Booleans. ---------------------------------------------------------------------------- data Bool : Set where true : Bool false : Bool elimBool : (C : Bool -> Set) -> C true -> C false -> (b : Bool) -> C b elimBool C c_t c_f true = c_t elimBool C c_t c_f false = c_f whenBool : (C : Set) -> C -> C -> Bool -> C whenBool C c_t c_f b = elimBool (\(_ : Bool) -> C) c_t c_f b data pred (A : Set) : Set where predI : (A -> Bool) -> pred A data rel (A : Set) : Set where relI : (A -> A -> Bool) -> rel A True : Bool -> Set True true = Taut True false = Absurd bool2set = True pred2Pred : {A : Set} -> pred A -> Pred A pred2Pred (predI p) = PredI (\a -> True (p a)) rel2Rel : {A : Set} -> rel A -> Rel A rel2Rel (relI r) = RelI (\a -> \b -> True (r a b)) -- decTrue : (p : Bool) -> Decidable (True p) -- decTrue true = orIl tt -- decTrue false = orIr (impliesI pI) -- decTrue false = orIr (impliesI (\(p : (True false)) -> p)) -- dec_lem : {P : Set} -> (decP : Decidable P) -- -> Exists A {- abstract dec_lem (|P :: Set)(decP :: Decidable P) :: Exist |_ (\(b :: Bool) -> Iff (True b) P) = case decP of { (inl trueP) -> struct { fst = true@_; snd = struct { fst = const |_ |_ trueP; -- (True true@_) snd = const |_ |_ tt;};}; (inr notP) -> struct { fst = false@_; snd = struct { fst = whenZero P; snd = notP;};};} dec2bool :: (P :: Set) |-> (decP :: Decidable P) -> Bool = \(P :: Set) |-> \(decP :: Decidable P) -> (dec_lem |_ decP).fst dec2bool_spec (|P :: Set)(decP :: Decidable P) :: Iff (True (dec2bool |_ decP)) P = (dec_lem |_ decP).snd abstract collTrue :: (b :: Bool) -> Collapsed (True b) = let aux (X :: Set)(C :: X -> Set) :: (b :: Bool) -> (f :: True b -> X) -> (t1 :: True b) |-> (t2 :: True b) |-> C (f t1) -> C (f t2) = \(b :: Bool) -> case b of { (true) -> \(f :: (x :: True true@_) -> X) -> \(t1 t2 :: True true@_) |-> \(c :: C (f t1)) -> case t1 of { (tt) -> case t2 of { (tt) -> c;};}; (false) -> \(f :: (x :: True false@_) -> X) -> \(t1 t2 :: True false@_) |-> \(c :: C (f t1)) -> case t1 of { };} in \(b :: Bool) -> \(P :: True b -> Set) -> aux (True b) P b id bool2nat (p :: Bool) :: Nat = case p of { (true) -> succ zero; (false) -> zero;} -}