Agda-2.3.2.2: examples/AIM5/yoshiki/SET.agda
-------------------------------------------------------------------------------
--
-- 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;}
-}