WIP: define semantics in Idris.semantics-with-proof

1 files changed, 52 insertions, 8 deletions

diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
index 11bb894..b8eec99 100644
--- a/src/Encoded/Bool.idr
+++ b/src/Encoded/Bool.idr
@@ -3,18 +3,13 @@ module Encoded.Bool
 import Term.Semantics
 import Term.Syntax
 
+-- Type ------------------------------------------------------------------------
+
 export
 B : Ty
 B = N
 
-export
-Show (TypeOf B) where
-  show 0 = "true"
-  show (S k) = "false"
-
-export
-toBool : TypeOf B -> Bool
-toBool = (== 0)
+-- Universal Properties --------------------------------------------------------
 
 export
 True : Term B ctx
@@ -31,6 +26,8 @@ if' = Abs' (\b =>
     (Abs $ Const $ Var Here)
     (Const $ Const $ Abs $ Var Here))
 
+-- Utilities -------------------------------------------------------------------
+
 export
 and : Term (B ~> B ~> B) ctx
 and = Abs' (\b => App if' [<b, Id, Const False])
@@ -46,3 +43,50 @@ not = Abs' (\b => App if' [<b, False, True])
 export
 isZero : Term (N ~> B) ctx
 isZero = Id
+
+-- Semantics -------------------------------------------------------------------
+
+-- Conversion to Idris
+
+export
+toBool : TypeOf B -> Bool
+toBool = (== 0)
+
+export
+fromBool : Bool -> TypeOf B
+fromBool b = if b then 0 else 1
+
+export
+toFromId : (b : Bool) -> toBool (fromBool b) = b
+toFromId False = Refl
+toFromId True = Refl
+
+-- Redefinition in Idris
+
+namespace Sem
+  public export
+  True : TypeOf B
+  True = 0
+
+  public export
+  False : TypeOf B
+  False = 1
+
+  public export
+  if' : TypeOf B -> a -> a -> a
+  if' b = rec b (\t, _ => t) (\_, _, f => f)
+
+-- Homomorphism
+
+export
+trueHomo : toBool True = True
+trueHomo = Refl
+
+export
+falseHomo : toBool False = False
+falseHomo = Refl
+
+export
+ifHomo : (b : Bool) -> (0 x, y : a) -> if' (fromBool b) x y = if b then x else y
+ifHomo True x y = Refl
+ifHomo False x y = Refl