fabian/veribase-idr2 - Change QJMKKLU2UF45IRLVJHSQQ6PHTLHHX34Z4ROJGQLBRQTMQ54D6G5AC

Split Data.Boolean

Created by fabian on June 19, 2021

QJMKKLU2UF45IRLVJHSQQ6PHTLHHX34Z4ROJGQLBRQTMQ54D6G5AC

Dependencies

In channels

main

Change contents

Insertion in veribase.ipkg at line 32 [3.6174]

[3.6269]

[4.1299]

	, Data.Boolean.Basic
	, Data.Boolean.Equivalence
	, Data.Boolean.Group
	, Data.Boolean.Lattice
	, Data.Boolean.Order

Deletion in src/Data/Boolean.idr at line 2 [3.117]

B:BD[3.138] → [3.138:139]

B:BD[3.139] → [5.667:682]

∅:D[5.782] → [6.138:139]

B:BD[7.190] → [6.138:139]

B:BD[6.139] → [5.783:810]

B:BD[5.838] → [5.838:869]

B:BD[5.869] → [2.2251:2279]

∅:D[5.869] → [6.140:141]

∅:D[2.2279] → [6.140:141]

B:BD[8.655] → [6.140:141]

B:BD[6.141] → [5.870:948]

∅:D[6.233] → [7.191:192]

∅:D[5.948] → [7.191:192]

B:BD[8.655] → [7.191:192]

B:BD[7.192] → [2.2280:2380]

∅:D[2.2380] → [7.192:211]

B:BD[7.192] → [7.192:211]

∅:D[9.86] → [3.154:171]

∅:D[7.211] → [3.154:171]

∅:D[10.235] → [3.154:171]

∅:D[8.655] → [3.154:171]

B:BD[3.154] → [3.154:171]

B:BD[3.171] → [9.87:104]

∅:D[9.104] → [3.171:213]

B:BD[3.171] → [3.171:213]

B:BD[3.213] → [9.105:124]

∅:D[9.124] → [10.236:687]

B:BD[3.213] → [10.236:687]

∅:D[10.687] → [3.213:214]

B:BD[3.213] → [3.213:214]

B:BD[3.214] → [11.1476:1625]

∅:D[11.1625] → [7.212:297]

B:BD[10.845] → [7.212:297]

B:BD[7.297] → [11.1626:1664]

∅:D[11.1664] → [7.334:562]

B:BD[7.334] → [7.334:562]

B:BD[7.562] → [11.1665:1699]

∅:D[11.1699] → [7.595:1264]

B:BD[7.595] → [7.595:1264]

B:BD[7.1264] → [11.1700:1733]

∅:D[11.1733] → [7.1296:1334]

B:BD[7.1296] → [7.1296:1334]

B:BD[7.1334] → [11.1734:1767]

∅:D[11.1767] → [7.1366:1544]

B:BD[7.1366] → [7.1366:1544]

∅:D[7.1544] → [10.845:846]

B:BD[10.845] → [10.845:846]

B:BD[10.846] → [7.1545:1745]

∅:D[7.1745] → [9.125:146]

B:BD[10.846] → [9.125:146]

∅:D[9.146] → [3.214:393]

∅:D[10.846] → [3.214:393]

B:BD[3.214] → [3.214:393]

B:BD[3.393] → [9.147:162]

B:BD[9.162] → [12.8:94]

∅:D[12.148] → [9.298:299]

B:BD[9.298] → [9.298:299]

B:BD[9.299] → [12.149:156]

∅:D[12.156] → [9.299:430]

B:BD[9.299] → [9.299:430]

B:BD[9.430] → [12.157:164]

∅:D[12.164] → [9.430:563]

B:BD[9.430] → [9.430:563]

∅:D[9.563] → [3.480:481]

B:BD[3.480] → [3.480:481]

B:BD[3.481] → [12.165:172]

∅:D[12.172] → [3.481:626]

B:BD[3.481] → [3.481:626]

B:BD[3.626] → [12.173:180]

∅:D[12.180] → [3.626:773]

B:BD[3.626] → [3.626:773]

B:BD[3.773] → [13.0:263]


import Builtin
import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid
import Algebra.Lattice.JoinSemilattice
import Algebra.Lattice.MeetSemilattice
import Algebra.Relation.Equivalence
import Algebra.Relation.Preorder
import Algebra.Relation.Order
import Data.Either
%default total
--
-- Values
--
public export
data Boolean = False | True
--
-- Relation
--
data BooleanEquiv : (a, b : Boolean) -> Type where
  BothFalse : BooleanEquiv False False
  BothTrue  : BooleanEquiv True  True
public export
Uninhabited (BooleanEquiv False True) where
  uninhabited BothFalse impossible
  uninhabited BothTrue  impossible
public export
Uninhabited (BooleanEquiv True False) where
  uninhabited BothFalse impossible
  uninhabited BothTrue  impossible
public export
Equivalence Boolean where
  Equiv = BooleanEquiv
  decEquiv False False = Yes BothFalse
  decEquiv True  True  = Yes BothTrue
  decEquiv False True  = No  absurd
  decEquiv True  False = No  absurd
data BooleanLTE : (a, b : Boolean) -> Type where
  FalseLTEAny : BooleanLTE False b
  TrueLTETrue : BooleanLTE True  True
public export
Uninhabited (BooleanLTE True False) where
  uninhabited FalseLTEAny impossible
  uninhabited TrueLTETrue impossible
public export
Preorder Boolean where
  LTE = BooleanLTE
  decLTE False _     = Yes FalseLTEAny
  decLTE True  False = No  absurd
  decLTE True  True  = Yes TrueLTETrue
  proofReflexivity False = FalseLTEAny
  proofReflexivity True  = TrueLTETrue
  proofTransitivity False False _     FalseLTEAny FalseLTEAny = FalseLTEAny
  proofTransitivity False True  True  FalseLTEAny TrueLTETrue = FalseLTEAny
  proofTransitivity True  True  True  TrueLTETrue TrueLTETrue = TrueLTETrue
data BooleanLT : (a, b : Boolean) -> Type where
  FalseLTTrue : BooleanLT False True
public export
Uninhabited (BooleanLT False False) where
  uninhabited FalseLTTrue impossible
public export
Uninhabited (BooleanLT True _) where
  uninhabited FalseLTTrue impossible
public export
Order Boolean where
  LT = BooleanLT
  decLT False False = No  absurd
  decLT False True  = Yes FalseLTTrue
  decLT True  _     = No  absurd
  proofAntisymetry False False FalseLTEAny FalseLTEAny = BothFalse
  proofAntisymetry True  True  TrueLTETrue TrueLTETrue = BothTrue
  proofLTThenLTE FalseLTTrue = FalseLTEAny
  proofLTEThenLTOrEquiv False False FalseLTEAny = Right BothFalse
  proofLTEThenLTOrEquiv False True  FalseLTEAny = Left  FalseLTTrue
  proofLTEThenLTOrEquiv True  True  TrueLTETrue = Right BothTrue
--
-- Operations
--
not : Boolean -> Boolean
not False = True
not True  = False
proofNotInvolution : (a : Boolean) -> not (not a) = a
proofNotInvolution False = Refl
proofNotInvolution True  = Refl
public export
disj : Boolean -> Boolean -> Boolean
disj False False = False
disj _     _     = True
export
proofDisjLeftIdentity : (a : Boolean) -> False `disj` a = a
proofDisjLeftIdentity False = Refl
proofDisjLeftIdentity True  = Refl
export
proofDisjRightIdentity : (a : Boolean) -> a `disj` False = a
proofDisjRightIdentity False = Refl
proofDisjRightIdentity True  = Refl
export
proofDisjLeftAnnihilation : (a : Boolean) -> True `disj` a = True
proofDisjLeftAnnihilation False = Refl
proofDisjLeftAnnihilation True  = Refl
export
proofDisjRightAnnihilation : (a : Boolean) -> a `disj` True = True
proofDisjRightAnnihilation False = Refl
proofDisjRightAnnihilation True  = Refl
export
proofDisjCommutative : (a, b : Boolean) -> a `disj` b = b `disj` a
proofDisjCommutative False b =
  rewrite proofDisjLeftIdentity b in
  rewrite proofDisjRightIdentity b in
  Refl
proofDisjCommutative True b = rewrite proofDisjRightAnnihilation b in Refl

Replacement in src/Data/Boolean.idr at line 3 [3.117]

B:BD[13.264] → [13.264:331]

∅:D[13.331] → [3.773:774]

B:BD[3.773] → [3.773:774]

B:BD[3.774] → [9.564:578]

B:BD[9.578] → [13.332:416]

B:BD[13.416] → [2.2381:2423]

∅:D[2.2423] → [13.460:476]

B:BD[13.460] → [13.460:476]

∅:D[13.476] → [9.578:648]

B:BD[9.578] → [9.578:648]

B:BD[9.648] → [2.2424:2455]

∅:D[2.2455] → [9.681:779]

B:BD[9.681] → [9.681:779]

B:BD[9.779] → [2.2456:2491]

∅:D[2.2491] → [13.477:616]

B:BD[9.816] → [13.477:616]

∅:D[13.616] → [3.904:905]

∅:D[9.816] → [3.904:905]

B:BD[3.904] → [3.904:905]

B:BD[3.905] → [9.817:912]

B:BD[9.912] → [12.181:182]

B:BD[12.182] → [11.1768:1813]

∅:D[11.1813] → [9.956:1002]

B:BD[9.956] → [9.956:1002]

∅:D[9.1002] → [3.1038:1039]

B:BD[3.1038] → [3.1038:1039]

B:BD[3.1039] → [13.617:750]

∅:D[13.750] → [3.1294:1295]

B:BD[3.1294] → [3.1294:1295]

B:BD[3.1295] → [9.1003:1017]

B:BD[9.1017] → [12.191:273]

∅:D[12.327] → [9.1134:1135]

B:BD[9.1134] → [9.1134:1135]

B:BD[9.1135] → [12.328:335]

∅:D[12.335] → [9.1135:1265]

B:BD[9.1135] → [9.1135:1265]

B:BD[9.1265] → [12.336:343]

∅:D[12.343] → [9.1265:1397]

B:BD[9.1265] → [9.1265:1397]

∅:D[9.1397] → [3.1632:1633]

B:BD[3.1632] → [3.1632:1633]

B:BD[3.1633] → [12.344:351]

∅:D[12.351] → [3.1633:1780]

B:BD[3.1633] → [3.1633:1780]

B:BD[3.1780] → [12.352:359]

∅:D[12.359] → [3.1780:1929]

B:BD[3.1780] → [3.1780:1929]

B:BD[3.1929] → [13.751:1181]

B:BD[13.1181] → [2.2492:2534]

∅:D[13.1225] → [3.1929:1930]

∅:D[2.2534] → [3.1929:1930]

B:BD[3.1929] → [3.1929:1930]

B:BD[3.1930] → [9.1398:1482]

B:BD[9.1482] → [2.2535:2602]

∅:D[11.1847] → [9.1552:1650]

∅:D[2.2602] → [9.1552:1650]

B:BD[9.1552] → [9.1552:1650]

∅:D[9.1650] → [3.2059:2060]

B:BD[3.2059] → [3.2059:2060]

B:BD[3.2060] → [9.1651:1745]

B:BD[9.1745] → [12.360:361]

∅:D[12.361] → [9.1745:1836]

B:BD[9.1745] → [9.1745:1836]

∅:D[9.1836] → [3.2192:2193]

B:BD[3.2192] → [3.2192:2193]

B:BD[6.250] → [6.250:267]

∅:D[6.267] → [10.847:862]

B:BD[3.2703] → [10.847:862]

B:BD[10.862] → [6.268:377]

B:BD[6.377] → [12.370:371]

B:BD[12.371] → [2.2603:2665]

∅:D[2.2665] → [6.441:721]

B:BD[6.441] → [6.441:721]

B:BD[6.721] → [11.1848:1930]

∅:D[11.1930] → [6.1049:1255]

B:BD[6.1049] → [6.1049:1255]

B:BD[6.1255] → [12.372:373]

B:BD[12.373] → [2.2666:2728]

∅:D[2.2728] → [6.1319:2024]

B:BD[6.1319] → [6.1319:2024]

∅:D[6.2024] → [10.862:951]

B:BD[10.862] → [10.862:951]

public export
[BooleanDisjMagma] Magma Boolean where
  (<>) = disj
public export
[BooleanDisjCommutativeMagma] CommutativeMagma Boolean using BooleanDisjMagma where
  proofCommutative = proofDisjCommutative
public export
[BooleanDisjSemigroup] Semigroup Boolean using BooleanDisjMagma where
  proofAssociative False b c =
    rewrite proofDisjLeftIdentity b in
    rewrite proofDisjLeftIdentity (b `disj` c) in
    Refl
  proofAssociative True b c = Refl
public export
[BooleanDisjCommutativeSemigroup] CommutativeSemigroup Boolean using BooleanDisjCommutativeMagma BooleanDisjSemigroup where
public export
[BooleanDisjMonoid] Monoid Boolean using BooleanDisjSemigroup where
  id = False
  proofLeftIdentity  = proofDisjLeftIdentity
  proofRightIdentity = proofDisjRightIdentity
public export
[BooleanDisjCommutativeMonoid] CommutativeMonoid Boolean using BooleanDisjCommutativeSemigroup BooleanDisjMonoid where
public export
conj : Boolean -> Boolean -> Boolean
conj True True = True
conj _    _    = False
export
proofConjLeftIdentity : (a : Boolean) -> True `conj` a = a
proofConjLeftIdentity False = Refl
proofConjLeftIdentity True  = Refl
export
proofConjRightIdentity : (a : Boolean) -> a `conj` True = a
proofConjRightIdentity False = Refl
proofConjRightIdentity True  = Refl
export
proofConjLeftAnnihilation : (a : Boolean) -> False `conj` a = False
proofConjLeftAnnihilation False = Refl
proofConjLeftAnnihilation True  = Refl
export
proofConjRightAnnihilation : (a : Boolean) -> a `conj` False = False
proofConjRightAnnihilation False = Refl
proofConjRightAnnihilation True  = Refl
export
proofConjCommutative : (a, b : Boolean) -> a `conj` b = b `conj` a
proofConjCommutative False b = rewrite proofConjRightAnnihilation b in Refl
proofConjCommutative True b =
  rewrite proofConjLeftIdentity b in
  rewrite proofConjRightIdentity b in
  Refl
public export
[BooleanConjMagma] Magma Boolean where
  (<>) = conj
public export
[BooleanConjCommutativeMagma] CommutativeMagma Boolean using BooleanConjMagma where
  proofCommutative = proofConjCommutative
public export
[BooleanConjSemigroup] Semigroup Boolean using BooleanConjMagma where
  proofAssociative False b c = Refl
  proofAssociative True  b c =
    rewrite proofConjLeftIdentity b in
    rewrite proofConjLeftIdentity (b `conj` c) in
    Refl
public export
[BooleanConjMonoid] Monoid Boolean using BooleanConjSemigroup where
  id = True
  proofLeftIdentity  = proofConjLeftIdentity
  proofRightIdentity = proofConjRightIdentity
--
-- Lattice
--
public export
MeetSemilattice Boolean where
  (/\) = conj
  proofIdempotence False = Refl
  proofIdempotence True  = Refl
  proofAssociative = proofAssociative @{BooleanConjSemigroup}
  proofCommutative = proofConjCommutative
  proofLowerBound False False = (FalseLTEAny, FalseLTEAny)
  proofLowerBound False True  = (FalseLTEAny, FalseLTEAny)
  proofLowerBound True  False = (FalseLTEAny, FalseLTEAny)
  proofLowerBound True  True  = (TrueLTETrue, TrueLTETrue)
  proofGreatestLowerBound False y     z     FalseLTEAny FalseLTEAny = FalseLTEAny
  proofGreatestLowerBound True  True  True  TrueLTETrue TrueLTETrue = TrueLTETrue
public export
JoinSemilattice Boolean where
  (\/) = disj
  proofIdempotence False = Refl
  proofIdempotence True  = Refl
  proofAssociative = proofAssociative @{BooleanDisjSemigroup}
  proofCommutative = proofDisjCommutative
  proofUpperBound False False = (FalseLTEAny, FalseLTEAny)
  proofUpperBound False True  = (FalseLTEAny, TrueLTETrue)
  proofUpperBound True  False = (TrueLTETrue, FalseLTEAny)
  proofUpperBound True  True  = (TrueLTETrue, TrueLTETrue)
  proofLeastUpperBound False False False FalseLTEAny FalseLTEAny = FalseLTEAny
  proofLeastUpperBound True  False False FalseLTEAny FalseLTEAny = FalseLTEAny
  proofLeastUpperBound True  False True  FalseLTEAny TrueLTETrue = TrueLTETrue
  proofLeastUpperBound True  True  False TrueLTETrue FalseLTEAny = TrueLTETrue
  proofLeastUpperBound True  True  True  TrueLTETrue TrueLTETrue = TrueLTETrue
--
-- Util
--
public export
decToBoolean : Dec t -> Boolean
decToBoolean (Yes _) = True
decToBoolean (No  _) = False

[13.264]

import public Data.Boolean.Basic
import public Data.Boolean.Equivalence
import public Data.Boolean.Order
import public Data.Boolean.Group
import public Data.Boolean.Lattice

File addition: Boolean (d--x------)
[3.14]

File addition: Order.idr (----------)

[0.303]

module Data.Boolean.Order
import Builtin
import Algebra.Relation.Equivalence
import Algebra.Relation.Preorder
import Algebra.Relation.Order
import public Data.Boolean.Basic
import public Data.Boolean.Equivalence
%default total
public export
data BooleanLTE : (a, b : Boolean) -> Type where
  FalseLTEAny : BooleanLTE False b
  TrueLTETrue : BooleanLTE True  True
public export
Uninhabited (BooleanLTE True False) where
  uninhabited FalseLTEAny impossible
  uninhabited TrueLTETrue impossible
public export
Preorder Boolean where
  LTE = BooleanLTE
  decLTE False _     = Yes FalseLTEAny
  decLTE True  False = No  absurd
  decLTE True  True  = Yes TrueLTETrue
  proofReflexivity False = FalseLTEAny
  proofReflexivity True  = TrueLTETrue
  proofTransitivity False False _     FalseLTEAny FalseLTEAny = FalseLTEAny
  proofTransitivity False True  True  FalseLTEAny TrueLTETrue = FalseLTEAny
  proofTransitivity True  True  True  TrueLTETrue TrueLTETrue = TrueLTETrue
data BooleanLT : (a, b : Boolean) -> Type where
  FalseLTTrue : BooleanLT False True
public export
Uninhabited (BooleanLT False False) where
  uninhabited FalseLTTrue impossible
public export
Uninhabited (BooleanLT True _) where
  uninhabited FalseLTTrue impossible
public export
Order Boolean where
  LT = BooleanLT
  decLT False False = No  absurd
  decLT False True  = Yes FalseLTTrue
  decLT True  _     = No  absurd
  proofAntisymetry False False FalseLTEAny FalseLTEAny = BothFalse
  proofAntisymetry True  True  TrueLTETrue TrueLTETrue = BothTrue
  proofLTThenLTE FalseLTTrue = FalseLTEAny
  proofLTEThenLTOrEquiv False False FalseLTEAny = Right BothFalse
  proofLTEThenLTOrEquiv False True  FalseLTEAny = Left  FalseLTTrue
  proofLTEThenLTOrEquiv True  True  TrueLTETrue = Right BothTrue

File addition: Lattice.idr (----------)

[0.303]

module Data.Boolean.Lattice
import Builtin
import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Lattice.MeetSemilattice
import Algebra.Lattice.JoinSemilattice
import Algebra.Relation.Preorder
import Algebra.Relation.Order
import public Data.Boolean.Basic
import public Data.Boolean.Order
import public Data.Boolean.Group
%default total
public export
JoinSemilattice Boolean where
  (\/) = disj
  proofIdempotence False = Refl
  proofIdempotence True  = Refl
  proofAssociative = proofAssociative @{BooleanDisjSemigroup}
  proofCommutative = proofDisjCommutative
  proofUpperBound False False = (FalseLTEAny, FalseLTEAny)
  proofUpperBound False True  = (FalseLTEAny, TrueLTETrue)
  proofUpperBound True  False = (TrueLTETrue, FalseLTEAny)
  proofUpperBound True  True  = (TrueLTETrue, TrueLTETrue)
  proofLeastUpperBound False False False FalseLTEAny FalseLTEAny = FalseLTEAny
  proofLeastUpperBound True  False False FalseLTEAny FalseLTEAny = FalseLTEAny
  proofLeastUpperBound True  False True  FalseLTEAny TrueLTETrue = TrueLTETrue
  proofLeastUpperBound True  True  False TrueLTETrue FalseLTEAny = TrueLTETrue
  proofLeastUpperBound True  True  True  TrueLTETrue TrueLTETrue = TrueLTETrue
public export
MeetSemilattice Boolean where
  (/\) = conj
  proofIdempotence False = Refl
  proofIdempotence True  = Refl
  proofAssociative = proofAssociative @{BooleanConjSemigroup}
  proofCommutative = proofConjCommutative
  proofLowerBound False False = (FalseLTEAny, FalseLTEAny)
  proofLowerBound False True  = (FalseLTEAny, FalseLTEAny)
  proofLowerBound True  False = (FalseLTEAny, FalseLTEAny)
  proofLowerBound True  True  = (TrueLTETrue, TrueLTETrue)
  proofGreatestLowerBound False y     z     FalseLTEAny FalseLTEAny = FalseLTEAny
  proofGreatestLowerBound True  True  True  TrueLTETrue TrueLTETrue = TrueLTETrue

File addition: Group.idr (----------)

[0.303]

module Data.Boolean.Group
import Builtin
import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid
import public Data.Boolean.Basic
%default total
public export
[BooleanDisjMagma] Magma Boolean where
  (<>) = disj
public export
[BooleanDisjCommutativeMagma] CommutativeMagma Boolean using BooleanDisjMagma where
  proofCommutative = proofDisjCommutative
public export
[BooleanDisjSemigroup] Semigroup Boolean using BooleanDisjMagma where
  proofAssociative False b c =
    rewrite proofDisjLeftIdentity b in
    rewrite proofDisjLeftIdentity (b `disj` c) in
    Refl
  proofAssociative True b c = Refl
public export
[BooleanDisjCommutativeSemigroup] CommutativeSemigroup Boolean using BooleanDisjCommutativeMagma BooleanDisjSemigroup where
public export
[BooleanDisjMonoid] Monoid Boolean using BooleanDisjSemigroup where
  id = False
  proofLeftIdentity  = proofDisjLeftIdentity
  proofRightIdentity = proofDisjRightIdentity
public export
[BooleanDisjCommutativeMonoid] CommutativeMonoid Boolean using BooleanDisjCommutativeSemigroup BooleanDisjMonoid where
public export
[BooleanConjMagma] Magma Boolean where
  (<>) = conj
public export
[BooleanConjCommutativeMagma] CommutativeMagma Boolean using BooleanConjMagma where
  proofCommutative = proofConjCommutative
public export
[BooleanConjSemigroup] Semigroup Boolean using BooleanConjMagma where
  proofAssociative False b c = Refl
  proofAssociative True  b c =
    rewrite proofConjLeftIdentity b in
    rewrite proofConjLeftIdentity (b `conj` c) in
    Refl
public export
[BooleanConjMonoid] Monoid Boolean using BooleanConjSemigroup where
  id = True
  proofLeftIdentity  = proofConjLeftIdentity
  proofRightIdentity = proofConjRightIdentity

File addition: Equivalence.idr (----------)

[0.303]

module Data.Boolean.Equivalence
import Builtin
import Algebra.Relation.Equivalence
import public Data.Boolean.Basic
%default total
public export
data BooleanEquiv : (a, b : Boolean) -> Type where
  BothFalse : BooleanEquiv False False
  BothTrue  : BooleanEquiv True  True
public export
Uninhabited (BooleanEquiv False True) where
  uninhabited BothFalse impossible
  uninhabited BothTrue  impossible
public export
Uninhabited (BooleanEquiv True False) where
  uninhabited BothFalse impossible
  uninhabited BothTrue  impossible
public export
Equivalence Boolean where
  Equiv = BooleanEquiv
  decEquiv False False = Yes BothFalse
  decEquiv True  True  = Yes BothTrue
  decEquiv False True  = No  absurd
  decEquiv True  False = No  absurd

File addition: Basic.idr (----------)

[0.303]

module Data.Boolean.Basic
import Builtin
%default total
public export
data Boolean = False | True
--
-- Negation / Complement
--
public export
not : Boolean -> Boolean
not False = True
not True  = False
export
proofNotInvolution : (a : Boolean) -> not (not a) = a
proofNotInvolution False = Refl
proofNotInvolution True  = Refl
--
-- Disjunction / Inclusive OR
--
public export
disj : Boolean -> Boolean -> Boolean
disj False False = False
disj _     _     = True
export
proofDisjLeftIdentity : (a : Boolean) -> False `disj` a = a
proofDisjLeftIdentity False = Refl
proofDisjLeftIdentity True  = Refl
export
proofDisjRightIdentity : (a : Boolean) -> a `disj` False = a
proofDisjRightIdentity False = Refl
proofDisjRightIdentity True  = Refl
export
proofDisjLeftAnnihilation : (a : Boolean) -> True `disj` a = True
proofDisjLeftAnnihilation False = Refl
proofDisjLeftAnnihilation True  = Refl
export
proofDisjRightAnnihilation : (a : Boolean) -> a `disj` True = True
proofDisjRightAnnihilation False = Refl
proofDisjRightAnnihilation True  = Refl
export
proofDisjCommutative : (a, b : Boolean) -> a `disj` b = b `disj` a
proofDisjCommutative False b =
  rewrite proofDisjLeftIdentity b in
  rewrite proofDisjRightIdentity b in
  Refl
proofDisjCommutative True b = rewrite proofDisjRightAnnihilation b in Refl
--
-- Conjunction / AND
--
public export
conj : Boolean -> Boolean -> Boolean
conj True True = True
conj _    _    = False
export
proofConjLeftIdentity : (a : Boolean) -> True `conj` a = a
proofConjLeftIdentity False = Refl
proofConjLeftIdentity True  = Refl
export
proofConjRightIdentity : (a : Boolean) -> a `conj` True = a
proofConjRightIdentity False = Refl
proofConjRightIdentity True  = Refl
export
proofConjLeftAnnihilation : (a : Boolean) -> False `conj` a = False
proofConjLeftAnnihilation False = Refl
proofConjLeftAnnihilation True  = Refl
export
proofConjRightAnnihilation : (a : Boolean) -> a `conj` False = False
proofConjRightAnnihilation False = Refl
proofConjRightAnnihilation True  = Refl
export
proofConjCommutative : (a, b : Boolean) -> a `conj` b = b `conj` a
proofConjCommutative False b = rewrite proofConjRightAnnihilation b in Refl
proofConjCommutative True b =
  rewrite proofConjLeftIdentity b in
  rewrite proofConjRightIdentity b in
  Refl
--
-- Util
--
public export
decToBoolean : Dec t -> Boolean
decToBoolean (Yes _) = True
decToBoolean (No  _) = False

Split Data.Boolean

Dependencies

In channels

Change contents

Insertion in veribase.ipkg at line 32 [3.6174]

Deletion in src/Data/Boolean.idr at line 2 [3.117]

Replacement in src/Data/Boolean.idr at line 3 [3.117]

File addition: Boolean (d--x------)

File addition: Order.idr (----------)

File addition: Lattice.idr (----------)

File addition: Group.idr (----------)

File addition: Equivalence.idr (----------)

File addition: Basic.idr (----------)