# luqui/dana

Proved the application theorem on function types.

`In desperate need of more automation, the plumbing is getting out of hand.`
luqui committed Jun 19, 2009
1 parent 558100d commit ab06f38962ab3a3a861db0185d021db088b0b43b
Showing with 76 additions and 11 deletions.
1. +4 −1 ixi/IXi/Helpers.hs
2. +54 −8 ixi/IXi/Prelude.hs
3. +5 −1 ixi/IXi/Proof.hs
4. +13 −1 ixi/IXi/Term.hs
 @@ -1,5 +1,5 @@ module IXi.Helpers - ( convNF, convInverseNF, convEquiv, convInverseBeta + ( convNF, convInverseNF, convEquiv, convInverseBeta, convAbstract , unfoldn, foldn ) where @@ -91,3 +91,6 @@ foldn n = mconcat . zipWith (\$) appLs . reverse . bodies n bodies 0 _ = [] bodies n t@(Lambda t') = t : bodies (n-1) t' bodies n _ = error "foldn not given n nested lambdas" + +convAbstract :: Name -> Term -> Conversion +convAbstract name = convInverseBeta . Lambda . abstract name
 @@ -33,10 +33,10 @@ unfold_Impl = unfoldn 2 -- |- Q -- |- KQI --- |- Ξ(KP)(KQ) --- |- P ==> Q -- |- KPI -- |- P +-- |- Ξ(KP)(KQ) +-- |- P ==> Q modusPonens :: Exp -> Tactic -> Tactic -> Tactic modusPonens p pqPf pPf = conversion (fold_K _I) \$ @@ -108,8 +108,8 @@ unfold_Compose = unfoldn 3 _Arrow = fun (\a -> fun (\b -> fun (\f -> _Xi % a % (b ° f)))) a --> b = _Arrow % a % b -fold_arrow = foldn 3 (hoas _Arrow) -unfold_arrow = unfoldn 3 +fold_Arrow = foldn 3 (hoas _Arrow) +unfold_Arrow = unfoldn 3 _L = _U --> _H @@ -122,7 +122,7 @@ _L = _U --> _H la_hax la = conversion fold_Compose \$ implRule (hoas _U) u_everything \$ - conversion fold_arrow la + conversion fold_Arrow la -- |- LA -- |- (U-->H)A @@ -132,7 +132,7 @@ la_hax la = -- Ux |- (H°A)x -- Ux |- H(Ax) hax_la x hax = - conversion unfold_arrow \$ + conversion unfold_Arrow \$ xiRule x (conversion (convInAppR unfold_K) (theorem thm_h_true)) \$ (\_ -> conversion unfold_Compose hax) @@ -161,7 +161,7 @@ thm_lu = prove (hoas (_L % _U)) \$ arrowTypeHelper la lb = newName \$ \x -> hax_la x \$ - conversion (convInAppR unfold_arrow) \$ + conversion (convInAppR unfold_Arrow) \$ newName \$ \y -> hxiRule y (la_hax la) (\_ -> conversion (convInAppR unfold_Compose) (la_hax lb)) @@ -170,7 +170,8 @@ arrowTypeHelper la lb = -- |- L(U --> H) -- |- LU -- |- LH -thm_ll = prove (hoas (_L % _L)) \$ arrowTypeHelper (theorem thm_lu) (theorem thm_lh) +thm_ll = prove (hoas (_L % _L)) \$ + arrowTypeHelper (theorem thm_lu) (theorem thm_lh) -- |- ΞL(\A. ΞL(\B. L(A --> B))) -- |- H(LA) @@ -187,3 +188,48 @@ thm_arrow_type = prove (hoas (_Xi % _L % fun (\a -> _Xi % _L % fun (\b -> _L % ( newName \$ \b -> lambdaXiRule b (la_hax (theorem thm_ll)) \$ \lb -> arrowTypeHelper la lb + + +-- (A-->B)f, Ax |- B(fx) +-- (A-->B)f, Ax |- (B°f)x +-- (A-->B)f, Ax |- Ax +-- (A-->B)f, Ax |- ΞA(B°f) +-- (A-->B)f, Ax |- (A-->B)f +arrowApplyHelper a pfABf pfAx = + conversion fold_Compose \$ + implRule (hoas a) pfAx (conversion fold_Arrow pfABf) + +pullName name rest = inspect (\seq -> conversion (convAbstract name (Sequent.goal seq)) rest) + +-- |- ΞL(\A. ΞL(\B. Ξ(A-->B)(\f. ΞA(\x. B(fx))))) +-- |- LL +-- LA |- ΞL(\B. Ξ(A-->B)(\f. ΞA(\x. B(fx)))) +-- LA |- LL +-- LA, LB |- Ξ(A-->B)(\f. ΞA(\x. B(fx))) +-- LA, LB |- L(A-->B) +-- LA, LB |- (\B. L(A-->B))B +-- LA, LB |- LB +-- LA, LB |- ΞL(\B. L(A --> B)) +-- LA, LB |- (\A. ΞL(\B. L(A --> B))A +-- LA, LB |- LA +-- LA, LB |- ΞL(\A. ΞL(\B. L(A --> B))) +-- LA, LB, (A-->B)f |- ΞA(\x. B(fx)) +-- LA, LB, (A-->B)f |- LA +-- LA, LB, (A-->B)f, Ax |- B(fx) +-- {arrowApplyHelper} +thm_arrow_apply = prove (hoas \$ + _Xi % _L % fun (\a -> _Xi % _L % fun (\b -> + _Xi % (a --> b) % fun (\f -> _Xi % a % fun (\x -> + b % (f % x)))))) \$ + newName \$ \a -> + lambdaXiRule a (la_hax (theorem thm_ll)) \$ \la -> + newName \$ \b -> + lambdaXiRule b (la_hax (theorem thm_ll)) \$ \lb -> + newName \$ \f -> + lambdaXiRule f (la_hax \$ + pullName b \$ implRule (hoas _L) lb \$ + pullName a \$ implRule (hoas _L) la \$ + theorem thm_arrow_type) \$ \abf -> + newName \$ \x -> + lambdaXiRule x (la_hax la) \$ \ax -> + arrowApplyHelper (name a) abf ax
 @@ -3,7 +3,7 @@ module IXi.Proof , hypothesis, conversion , implRule, xiRule, hxiRule, hhRule, xihRule , theorem - , Theorem, thmStatement, prove + , Theorem, thmStatement, thmProof, prove ) where @@ -22,6 +22,7 @@ data Proof | HHRule | XIHRule Proof | Theorem Theorem + deriving (Show) hypothesis = Hypothesis conversion = Conversion @@ -72,6 +73,9 @@ instance Show Theorem where thmStatement :: Theorem -> Term thmStatement (MkTheorem t _) = t +thmProof :: Theorem -> Proof +thmProof (MkTheorem _ pf) = pf + prove :: Term -> Proof -> Either String Theorem prove stmt proof =
 @@ -3,7 +3,7 @@ module IXi.Term , showTermWith, showTerm , quote, subst, substNamed , unfree, free, freeNames, nameFree - , swapVars + , swapVars, abstract , Name, safeName, safeName' ) @@ -118,3 +118,15 @@ nameFree n t = n `Set.member` freeNames t -- swaps indices 0 and 1 swapVars :: Term -> Term swapVars = subst 0 (Var 1) . quote 2 + +abstract :: Name -> Term -> Term +abstract name = go 0 + where + go n (Lambda t) = Lambda (go (n+1) t) + go n (t :% u) = go n t :% go n u + go n (Var z) | z < n = Var z + | otherwise = Var (z+1) + go n (NameVar nm) | nm == name = Var n + | otherwise = NameVar nm + go n Xi = Xi + go n H = H