40 lines
930 B
Idris
40 lines
930 B
Idris
module HomeworkFour
|
|
%default total
|
|
%access public export
|
|
|
|
even : Nat -> Bool
|
|
even Z = True
|
|
even (S Z) = False
|
|
even (S (S n)) = even n
|
|
|
|
evenSuc : even n = True -> even (S n) = False
|
|
evenSuc {n=Z} Refl = Refl
|
|
evenSuc {n=S Z} Refl impossible
|
|
evenSuc {n=S (S m)} p = evenSuc {n=m} p
|
|
|
|
oddSuc : even n = False -> even (S n) = True
|
|
oddSuc {n=Z} Refl impossible
|
|
oddSuc {n=S Z} Refl = Refl
|
|
oddSuc {n=S (S m)} p = oddSuc {n=m} p
|
|
|
|
evenFlip : even n = b -> even (S n) = not b
|
|
evenFlip {n=Z} Refl = Refl
|
|
evenFlip {n=S Z} Refl = Refl
|
|
evenFlip {n=S (S m)} p = evenFlip {n=m} p
|
|
|
|
evenFlip' : even n = b -> even (S n) = not b
|
|
evenFlip' {b=True} p = evenSuc p
|
|
evenFlip' {b=False} p = oddSuc p
|
|
|
|
evenSucSuc : even n = True -> even (S (S n)) = True
|
|
evenSucSuc p = p
|
|
|
|
oddSucSuc : even n = False -> even (S (S n)) = False
|
|
oddSucSuc p = p
|
|
|
|
evenStay : even n = b -> even (S (S n)) = b
|
|
evenStay p = p
|
|
|
|
evenStayEq : even n = even (S (S n))
|
|
evenStayEq = Refl
|