45 lines
1.1 KiB
Idris
45 lines
1.1 KiB
Idris
module HomeworkFifteen
|
|
%default total
|
|
|
|
data Term = Tru | Fls | Not Term | Cond Term Term Term
|
|
|
|
data Et : Term -> Type where
|
|
ETru : Et Tru
|
|
EFls : Et (Not Fls)
|
|
ENot : Et t -> Et (Not (Not t))
|
|
ECondT : Et tc -> Et tt -> Et (Cond tc tt te)
|
|
ECondF : Et (Not tc) -> Et te -> Et (Cond tc tt te)
|
|
|
|
ex1 : Et (Not (Not (Not Fls)))
|
|
ex1 = ENot EFls
|
|
|
|
ex2 : Et (Cond Tru (Not Fls) Tru)
|
|
ex2 = ECondT ETru EFls
|
|
|
|
ex3 : Et (Cond Fls Fls Tru)
|
|
ex3 = ECondF EFls ETru
|
|
|
|
infixl 5 !!
|
|
|
|
data (!!) : Term -> Term -> Type where
|
|
STru : Tru !! Tru
|
|
SFls : Fls !! Fls
|
|
SNotT : t !! Tru -> Not t !! Fls
|
|
SNotF : t !! Fls -> Not t !! Tru
|
|
SCondT : tc !! Tru -> tt !! v -> (Cond tc tt te) !! v
|
|
SCondF : tc !! Fls -> te !! v -> (Cond tc tt te) !! v
|
|
|
|
lemma : Et t -> t !! Tru
|
|
lemma ETru = STru
|
|
lemma EFls = SNotF SFls
|
|
lemma (ENot e) = SNotF $ SNotT $ lemma e
|
|
lemma (ECondT c t) = SCondT (lemma c) (lemma t)
|
|
lemma (ECondF c e) with (lemma c)
|
|
| SNotF pc = SCondF pc (lemma e)
|
|
|
|
lemma' : t !! Tru -> Et t
|
|
lemma' STru = ETru
|
|
lemma' (SNotF f) = ?stuckHere
|
|
lemma' (SCondT tc tt) = ECondT (lemma' tc) (lemma' tt)
|
|
lemma' (SCondF tc te) = ECondF (lemma' $ SNotF tc) (lemma' te)
|