Permalink
Browse files

A bunch more proofs.

  • Loading branch information...
1 parent 2a145c1 commit df3a1da1c060c2db3f49fc2a8368ebe90008abf7 @luqui committed Jun 15, 2009
Showing with 71 additions and 8 deletions.
  1. +0 −8 ixi/IXi/Helpers.hs
  2. +71 −0 ixi/IXi/Prelude.hs
View
@@ -48,11 +48,3 @@ convEquiv t t' =
(nf2, conv2) = convInverseNF t'
in
if nf1 == nf2 then Just (conv1 `mappend` conv2) else Nothing
-
--- X -> (\x. x) X -> (\y. (\x. x) X) Y -> (\x. \y. x) X Y
-convExpandK y = mconcat [
- convExpandId,
- convExpandConst y,
- convInAppL convExpandLambda ]
-
-convReduceK = mconcat [convInAppL convBetaReduce, convBetaReduce]
View
@@ -5,10 +5,19 @@ import IXi.HOAS
import IXi.Term
import IXi.Helpers
import IXi.Conversion
+import Data.Monoid (mconcat)
_K = fun (\x -> fun (\y -> x))
_I = fun (\x -> x)
+-- X -> (\x. x) X -> (\y. (\x. x) X) Y -> (\x. \y. x) X Y
+convExpandK y = mconcat [
+ convExpandId,
+ convExpandConst y,
+ convInAppL convExpandLambda ]
+
+convReduceK = mconcat [convInAppL convBetaReduce, convBetaReduce]
+
p ==> q = _Xi % (_K % p) % (_K % q)
-- |- Q
@@ -52,3 +61,65 @@ impl_refl = prove (hoas (_Xi % _H % fun (\p -> p ==> p))) $
newName $ \pvar ->
lambdaXiRule pvar hhRule $ \hp ->
implAbstract hp (\p -> p)
+
+_True = _Xi % _H % _H
+
+-- |- ΞHH
+-- |- H(Hx)
+-- Hx |- Hx
+true_true = prove (hoas (_Xi % _H % _H)) $
+ newName $ \x ->
+ xiRule x hhRule id
+
+-- |- H True
+-- |- H(ΞHH)
+-- |- H(Hx)
+-- Hx |- H(Hx)
+h_true = prove (hoas (_H % _True)) $
+ newName $ \x ->
+ hxiRule x hhRule (\_ -> hhRule)
+
+_U = _K % _True
+
+-- |- U x
+-- |- K True x
+-- |- True
+u_everything x = conversion convReduceK (theorem true_true)
+
+f ° g = fun (\x -> f % (g % x))
+
+-- A(Bx) -> A(B((\x.x)x)) -> A((\x. Bx)x) -> (\x. A(Bx))x
+convExpandCompose = mconcat [
+ convInAppR (convInAppR convExpandId),
+ convInAppR (convExpandRight),
+ convExpandRight ]
+
+a --> b = fun (\f -> _Xi % a % (b ° f))
+
+_L = _U --> _H
+
+-- |- ΞAB
+-- |- H(Ax)
+-- |- (H°A)x
+-- |- Ux
+-- |- ΞU(H°A)
+-- |- LA
+-- Ax |- Bx
+xiLRule x lPf abPf =
+ xiRule x
+ (conversion convExpandCompose
+ (implRule (hoas _U) (u_everything (name x)) lPf))
+ abPf
+
+-- |- LH
+-- |- (U --> H)H
+-- |- ΞU(H°H)
+-- |- H(Ux)
+-- |- H True
+-- Ux |- (H°H)x
+-- Ux |- H(Hx)
+lh = prove (hoas (_L % _H)) $
+ conversion convBetaReduce $
+ newName $ \x ->
+ xiRule x (conversion (convInAppR convReduceK) (theorem h_true))
+ (\h -> conversion convBetaReduce hhRule)

0 comments on commit df3a1da

Please sign in to comment.