Last active
December 25, 2015 23:09
-
-
Save kik/7054648 to your computer and use it in GitHub Desktop.
おもちゃ証明器
僕の証明器はEckmann-Hiltonの定理が証明できる！2次のホモトピー群は可換群だ！
Proof term は全然読めなくなってきた。
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| *Main> initGlobal >>= mod_eq | |
| ... | |
| ---- Proof ---- | |
| fun A : Type UnivVar "eq" => fun a : A => fun alpha beta : eq_refl A a = eq_refl A a :> a = a :> A => $eq_trans (eq_refl A a = eq_refl A a :> a = a :> A) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha beta) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta)) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) beta alpha) (eq_ind (fun t t' : eq_refl A a = eq_refl A a :> a = a :> A => fun _ : t = t' :> eq_refl A a = eq_refl A a :> a = a :> A => $eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha t = $eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha t' :> eq_refl A a = eq_refl A a :> a = a :> A) (fun t : eq_refl A a = eq_refl A a :> a = a :> A => eq_refl (eq_refl A a = eq_refl A a :> a = a :> A) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha t)) beta ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) ($whisker_l_refl A a beta)) ($eq_trans (eq_refl A a = eq_refl A a :> a = a :> A) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta)) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta)) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) beta alpha) (eq_ind (fun t t' : eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A => fun _ : t = t' :> eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A => t ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) = t' ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) :> eq_refl A a = eq_refl A a :> a = a :> A) (fun t : eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A => eq_refl (eq_refl A a = eq_refl A a :> a = a :> A) (t ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta))) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha)) (eq_ind (fun t t' : eq_refl A a = eq_refl A a :> a = a :> A => fun _ : t = t' :> eq_refl A a = eq_refl A a :> a = a :> A => $eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) t = $eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) t' :> eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A) (fun t : eq_refl A a = eq_refl A a :> a = a :> A => eq_refl (eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) t)) alpha ($whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha) ($whisker_r_refl A a alpha))) ($eq_trans (eq_refl A a = eq_refl A a :> a = a :> A) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta)) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) ($whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha)) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) beta alpha) ($whisker_rl_lr A a a a (eq_refl A a) (eq_refl A a) alpha (eq_refl A a) (eq_refl A a) beta) ($eq_trans (eq_refl A a = eq_refl A a :> a = a :> A) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) ($whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha)) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) alpha) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) beta alpha) (eq_ind (fun t t' : $eq_trans A a a a (eq_refl A a) (eq_refl A a) = $eq_trans A a a a (eq_refl A a) (eq_refl A a) :> a = a :> A => fun _ : t = t' :> $eq_trans A a a a (eq_refl A a) (eq_refl A a) = $eq_trans A a a a (eq_refl A a) (eq_refl A a) :> a = a :> A => $eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) t = $eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) t' :> eq_refl A a = eq_refl A a :> a = a :> A) (fun t : $eq_trans A a a a (eq_refl A a) (eq_refl A a) = $eq_trans A a a a (eq_refl A a) (eq_refl A a) :> a = a :> A => eq_refl (eq_refl A a = eq_refl A a :> a = a :> A) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) t)) ($whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha) alpha ($eq_sym ($eq_trans A a a a (eq_refl A a) (eq_refl A a) = $eq_trans A a a a (eq_refl A a) (eq_refl A a) :> a = a :> A) alpha ($whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha) ($whisker_r_refl A a alpha))) (eq_ind (fun t t' : eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A => fun _ : t = t' :> eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A => t alpha = t' alpha :> eq_refl A a = eq_refl A a :> a = a :> A) (fun t : eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A => eq_refl (eq_refl A a = eq_refl A a :> a = a :> A) (t alpha)) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta)) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) (eq_ind (fun t t' : $eq_trans A a a a (eq_refl A a) (eq_refl A a) = $eq_trans A a a a (eq_refl A a) (eq_refl A a) :> a = a :> A => fun _ : t = t' :> $eq_trans A a a a (eq_refl A a) (eq_refl A a) = $eq_trans A a a a (eq_refl A a) (eq_refl A a) :> a = a :> A => $eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) t = $eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) t' :> eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A) (fun t : $eq_trans A a a a (eq_refl A a) (eq_refl A a) = $eq_trans A a a a (eq_refl A a) (eq_refl A a) :> a = a :> A => eq_refl (eq_refl A a = eq_refl A a :> a = a :> A -> eq_refl A a = eq_refl A a :> a = a :> A) ($eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) t)) ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) beta ($eq_sym ($eq_trans A a a a (eq_refl A a) (eq_refl A a) = $eq_trans A a a a (eq_refl A a) (eq_refl A a) :> a = a :> A) beta ($whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) ($whisker_l_refl A a beta))))))) | |
| Eckmann_Hilton is defined. | |
| *Main> |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE TupleSections #-} | |
| import Data.List | |
| import Data.Maybe | |
| import Data.IORef | |
| import Control.Applicative | |
| import Control.Exception hiding (try, assert) | |
| import Control.Monad.State | |
| import Control.Monad.Reader | |
| import Control.Monad.Error | |
| import Control.Monad.Writer | |
| import Text.Parsec hiding ((<|>)) | |
| data Univ = Univ0 | |
| | UnivLift Univ Int | |
| | UnivMax Univ Univ | |
| | UnivVar String | |
| deriving (Eq, Show) | |
| data Term = TmU Univ | |
| | TmVar Int | |
| | TmConst String | |
| | TmHole Int | |
| | TmProd (Maybe String) Type Term | |
| | TmAbs (Maybe String) Type Term | |
| | TmApp Term Term | |
| | TmEq Type Term Term | |
| | TmRefl Type Term | |
| | TmEqInd Type Term Term Term Term | |
| type TermParser a = Parsec String () a | |
| termParser :: [Maybe String] -> TermParser Term | |
| termParser env = do { t <- goExpr env; eof; return t } | |
| where | |
| ident = try $ do { spaces | |
| ; lookAhead $ letter <|> char '_' | |
| ; many1 $ alphaNum <|> oneOf "_'" | |
| } | |
| op s = try $ ops >>= \x -> if s == x then return () else mzero | |
| ops = do { spaces | |
| ; choice $ map (try . string) ["->", "=>", ":>", "(", ")", ",", ":", "="] | |
| } | |
| binder e body = binders [] e body <|> binder1 e body | |
| binder1 e body = do { names <- many1 ident | |
| ; op ":" | |
| ; ty <- goExpr e | |
| ; let bs = [(name, termShift i ty) | (i, name) <- zip [0..] names] | |
| e' = foldl (\x y -> Just y : x) e names | |
| ; body bs e' | |
| } | |
| binders bs e body = do { op "(" | |
| ; binder1 e $ \bs' e' -> do { op ")" | |
| ; binders (bs++bs') e' body | |
| <|> body (bs++bs') e' | |
| } | |
| } | |
| goExpr e = go10 | |
| where | |
| go10 = go4 | |
| go4 = go3 `chainr1` do { op "->"; return $ \x y -> TmProd Nothing x (termShift 1 y) } | |
| go3 = do { x <- go2 | |
| ; option x $ do { op "=" | |
| ; y <- go2 | |
| ; op ":>" | |
| ; a <- go3 | |
| ; return $ TmEq a x y | |
| } | |
| } | |
| go2 = many1 (try go1) >>= return . foldl1 TmApp | |
| go1 = do { v <- ident; goIdent v } | |
| <|> do { between (op "(") (op ")") go10 } | |
| goIdent "Type0" = return $ TmU Univ0 | |
| goIdent "Type" = do { name <- ident; return $ TmU (UnivVar name) } | |
| goIdent "forall" = binder e $ \bs e' -> do { op "," | |
| ; body <- goExpr e' | |
| ; return $ foldr (\(name, ty) b -> TmProd (Just name) ty b) body bs | |
| } | |
| goIdent "fun" = binder e $ \bs e' -> do { op "=>" | |
| ; body <- goExpr e' | |
| ; return $ foldr (\(name, ty) b -> TmAbs (Just name) ty b) body bs | |
| } | |
| goIdent "eq_refl" = TmRefl <$> go1 <*> go1 | |
| goIdent "eq_ind" = TmEqInd <$> go1 <*> go1 <*> go1 <*> go1 <*> go1 | |
| goIdent n = case elemIndex (Just n) e of | |
| Just i -> return $ TmVar i | |
| Nothing -> return $ TmConst n | |
| showsTerm :: Local -> Term -> ShowS | |
| showsTerm l = walk 10 $ env l | |
| where | |
| env l = foldr (\(n, _) e -> alpha e n:e) [] l | |
| alpha e n = newName e $ maybe "t" id n | |
| newName e n = if elem n e then newName e $ n ++ "'" else n | |
| walk pr e t = case t of | |
| TmU i -> showString "Type " . shows i | |
| TmVar i | i < length e -> showString $ e!!i | |
| | otherwise -> showString "_var_" . shows i | |
| TmConst n -> showString "$" . showString n | |
| TmHole i -> showString "_" . shows i | |
| TmProd n ty body | not (termUse 0 body) -> | |
| paren 4 $ walk 3 e ty . showString " -> " . walk 4 ("_":e) body | |
| TmProd _ _ _ -> | |
| paren 2 $ showString "forall " . prod e t | |
| where | |
| prod e (TmProd n ty t@(TmProd _ ty' body)) | |
| | termUse 0 body && termShift 1 ty == ty' = | |
| showString n' . showString " " . prod (n':e) t | |
| where n' = alpha e n | |
| prod e (TmProd n ty body) = | |
| showString n' . showString " : " . walk 10 e ty . showString ", " . walk 10 (n':e) body | |
| where n' = alpha e n | |
| prod _ _ = undefined | |
| TmAbs _ _ _ -> | |
| paren 2 $ showString "fun " . abs e t | |
| where | |
| abs e (TmAbs n ty t@(TmAbs _ ty' body)) | |
| | termShift 1 ty == ty' = | |
| showString n' . showString " " . abs (n':e) t | |
| where n' = if termUse 0 t then alpha e n else "_" | |
| abs e (TmAbs n ty body) = | |
| showString n' . showString " : " . walk 10 e ty . showString " => " . walk 10 (n':e) body | |
| where n' = if termUse 0 body then alpha e n else "_" | |
| TmApp t1 t2 -> paren 2 $ list [w 2 t1, w 1 t2] | |
| TmRefl a x -> paren 2 $ list [showString "eq_refl", w 1 a, w 1 x] | |
| TmEqInd ct c x y p -> paren 2 $ list $ showString "eq_ind" : map (w 1) [ct, c, x, y, p] | |
| TmEq a x y -> paren 3 $ list[w 2 x, showString "=", w 2 y, showString ":>", w 3 a] | |
| where | |
| w pr = walk pr e | |
| paren n s = showParen (pr < n) s | |
| list = foldr (.) id . intersperse (showChar ' ') | |
| instance Show Term where | |
| showsPrec _ t = showsTerm [] t | |
| instance Eq Term where | |
| TmU i == TmU j = i == j | |
| TmVar i == TmVar j = i == j | |
| TmConst i == TmConst j = i == j | |
| TmHole i == TmHole j = i == j | |
| TmProd _ t1 t2 == TmProd _ s1 s2 = t1 == s1 && t2 == s2 | |
| TmAbs _ t1 t2 == TmAbs _ s1 s2 = t1 == s1 && t2 == s2 | |
| TmApp t1 t2 == TmApp s1 s2 = t1 == s1 && t2 == s2 | |
| TmEq t1 t2 t3 == TmEq s1 s2 s3 = t1 == s1 && t2 == s2 && t3 == s3 | |
| TmRefl t1 t2 == TmRefl s1 s2 = t1 == s1 && t2 == s2 | |
| TmEqInd t1 t2 t3 t4 t5 == TmEqInd s1 s2 s3 s4 s5 = | |
| t1 == s1 && t2 == s2 && t3 == s3 && t4 == s4 && t5 == s5 | |
| _ == _ = False | |
| type Type = Term | |
| data Binding = Decl Type | |
| | Def Type Term | |
| deriving (Show, Eq) | |
| type UnivBindings = [(String, Univ)] | |
| type Local = [(Maybe String, Binding)] | |
| type GlobalBindings = [(String, Binding)] | |
| data Global = Global { gbindings :: GlobalBindings | |
| , ubindings :: UnivBindings | |
| } | |
| deriving (Show) | |
| data TermError = TypeError String | |
| deriving (Show) | |
| instance Error TermError where | |
| strMsg = TypeError | |
| type ReadGlobal a = Reader Global a | |
| type TermHandler a = ErrorT TermError (Reader Global) a | |
| typeError :: String -> TermHandler a | |
| typeError = throwError . TypeError | |
| lookupVar :: Local -> Int -> TermHandler (Maybe String, Binding) | |
| lookupVar env i = if null bs then err else return $ head bs | |
| where | |
| bs = drop i env | |
| err = typeError $ "unbound variable: " ++ show i | |
| lookupConst :: String -> TermHandler Binding | |
| lookupConst n = do | |
| g <- ask | |
| case lookup n (gbindings g) of | |
| Just b -> return b | |
| Nothing -> typeError $ "unbound constant: " ++ show n | |
| termShift :: Int -> Term -> Term | |
| termShift d = walk 0 | |
| where | |
| walk :: Int -> Term -> Term | |
| walk c t = case t of | |
| TmU _ -> t | |
| TmVar i | i >= c -> TmVar $ i + d | |
| | otherwise -> t | |
| TmConst _ -> t | |
| TmHole _ -> error "unable to shift hole" | |
| TmProd n ty body -> TmProd n (w id ty) (w (+1) body) | |
| TmAbs n ty body -> TmAbs n (w id ty) (w (+1) body) | |
| TmApp t1 t2 -> TmApp (w id t1) (w id t2) | |
| TmEq t1 t2 t3 -> TmEq (w id t1) (w id t2) (w id t3) | |
| TmRefl t1 t2 -> TmRefl (w id t1) (w id t2) | |
| TmEqInd ct a x y p -> | |
| TmEqInd (w id ct) (w id a) (w id x) (w id y) (w id p) | |
| where | |
| w f = walk $ f c | |
| termSubst :: Int -> Term -> Term -> Term | |
| termSubst j s = walk 0 | |
| where | |
| walk :: Int -> Term -> Term | |
| walk c t = case t of | |
| TmU _ -> t | |
| TmVar i | i == j + c -> termShift c s | |
| | otherwise -> t | |
| TmConst _ -> t | |
| TmHole _ -> error "unable to subst hole" | |
| TmProd n ty body -> TmProd n (w id ty) (w (+1) body) | |
| TmAbs n ty body -> TmAbs n (w id ty) (w (+1) body) | |
| TmApp t1 t2 -> TmApp (w id t1) (w id t2) | |
| TmEq t1 t2 t3 -> TmEq (w id t1) (w id t2) (w id t3) | |
| TmRefl t1 t2 -> TmRefl (w id t1) (w id t2) | |
| TmEqInd ct a x y p -> | |
| TmEqInd (w id ct) (w id a) (w id x) (w id y) (w id p) | |
| where | |
| w f = walk $ f c | |
| -- [s/0]t | |
| subst :: Term -> Term -> Term | |
| subst s t = termShift (-1) $ termSubst 0 (termShift 1 s) t | |
| termPattern :: Int -> Term -> Term -> Term | |
| termPattern i s = walk 0 s | |
| where | |
| walk c s t | s == t = TmVar $ i + c | |
| walk c s t = case t of | |
| TmProd n ty body -> TmProd n (w id ty) (w (+1) body) | |
| TmAbs n ty body -> TmAbs n (w id ty) (w (+1) body) | |
| TmApp t1 t2 -> TmApp (w id t1) (w id t2) | |
| TmEq t1 t2 t3 -> TmEq (w id t1) (w id t2) (w id t3) | |
| TmRefl t1 t2 -> TmRefl (w id t1) (w id t2) | |
| TmEqInd ct a x y p -> | |
| TmEqInd (w id ct) (w id a) (w id x) (w id y) (w id p) | |
| _ -> t | |
| where | |
| w f = walk (f c) (termShift (f 0) s) | |
| -- pattern s t = t' where [s/0]t' = t | |
| pattern :: Term -> Term -> Term | |
| pattern s t = termPattern 0 (termShift 1 s) (termShift 1 t) | |
| termUse :: Int -> Term -> Bool | |
| termUse j = walk 0 | |
| where | |
| walk c t = case t of | |
| TmVar i | i == j + c -> True | |
| | otherwise -> False | |
| TmProd n ty body -> w id ty || w (+1) body | |
| TmAbs n ty body -> w id ty || w (+1) body | |
| TmApp t1 t2 -> w id t1 || w id t2 | |
| TmEq t1 t2 t3 -> w id t1 || w id t2 || w id t3 | |
| TmRefl t1 t2 -> w id t1 || w id t2 | |
| TmEqInd ct a x y p -> or [w id ct, w id a, w id x, w id y, w id p] | |
| _ -> False | |
| where | |
| w f = walk (f c) | |
| reduceValue :: Local -> Term -> TermHandler Term | |
| reduceValue e = rd | |
| where | |
| rd t = case t of | |
| TmU _ -> return t | |
| TmVar v -> do (_, b) <- lookupVar e v | |
| case b of | |
| Def _ t' -> return $ termShift (v+1) t' | |
| _ -> return t | |
| TmConst n -> do b <- lookupConst n | |
| case b of | |
| Def _ t' -> return t' | |
| _ -> return t | |
| TmHole _ -> error "reducing Hole" | |
| TmProd n ty body -> TmProd n <$> rd ty <*> rd' ((n, Decl ty):) body | |
| TmAbs n ty body -> TmAbs n <$> rd ty <*> rd' ((n, Decl ty):) body | |
| TmApp t1 t2 -> do t1' <- rd t1 | |
| t2' <- rd t2 | |
| case t1' of | |
| TmAbs n ty body -> | |
| termShift (-1) <$> rd' ((n, Def ty t2'):) body | |
| _ -> return $ TmApp t1' t2' | |
| TmEq a x y -> TmEq <$> (rd a) <*> (rd x) <*> (rd y) | |
| TmRefl a x -> TmRefl <$> (rd a) <*> (rd x) | |
| TmEqInd ct c x y p -> do p' <- rd p | |
| case p' of | |
| TmRefl a z -> rd $ (TmApp c x) | |
| _ -> TmEqInd <$> rd ct <*> rd c <*> rd x <*> rd y <*> pure p' | |
| rd' f t = reduceValue (f e) t | |
| univLe :: Univ -> Univ -> TermHandler Bool | |
| univLe = go 0 | |
| where | |
| go n Univ0 Univ0 | n >= 0 = return True | |
| go n (UnivVar v1) (UnivVar v2) | n >= 0 && v1 == v2 = return True | |
| go n (UnivMax u v) w = | |
| (&&) <$> go n u w <*> go n v w | |
| go n (UnivLift u i) v = go (n - i) u v | |
| go n u (UnivLift v i) = go (n + i) u v | |
| go n u (UnivVar v) = do g <- ask | |
| case lookup v (ubindings g) of | |
| Nothing -> typeError $ "not declared universe: " ++ v | |
| Just w -> go n u w | |
| go n u (UnivMax v w) = | |
| (||) <$> go n u v <*> go n u w | |
| go _ _ _ = return False | |
| univEq :: Univ -> Univ -> TermHandler Bool | |
| univEq u1 u2 = (&&) <$> univLe u1 u2 <*> univLe u2 u1 | |
| -- e |- t1 <: t2 | |
| convertible :: Local -> Term -> Term -> TermHandler Bool | |
| convertible e t1 t2 = do t1' <- reduceValue e t1 | |
| t2' <- reduceValue e t2 | |
| go False t1' t2' | |
| where | |
| go _ s1 s2 | s1 == s2 = return True | |
| go True (TmU u1) (TmU u2) = univEq u1 u2 | |
| go False (TmU u1) (TmU u2) = univLe u1 u2 | |
| go e (TmProd _ ty1 body1) (TmProd _ ty2 body2) = | |
| ands [go True ty1 ty2, go e body1 body2] | |
| go e (TmAbs _ ty1 body1) (TmAbs _ ty2 body2) = | |
| ands [go True ty1 ty2, go e body1 body2] | |
| go e (TmApp f1 a1) (TmApp f2 a2) = | |
| ands [go e f1 f2, go True a1 a2] | |
| go _ (TmEq a1 x1 y1) (TmEq a2 x2 y2) = | |
| ands [go True a1 a2, go True x1 x2, go True y1 y2] | |
| go _ (TmRefl a1 x1) (TmRefl a2 x2) = | |
| ands [go True a1 a2, go True x1 x2] | |
| go _ (TmEqInd ct1 c1 x1 y1 p1) (TmEqInd ct2 c2 x2 y2 p2) = | |
| ands [go True ct1 ct2, go True c1 c2, go True x1 x2, go True y1 y2, go True p1 p2] | |
| go _ _ _ = return False | |
| ands = fmap and . sequence | |
| typeofBinding :: Binding -> Type | |
| typeofBinding (Decl ty) = ty | |
| typeofBinding (Def ty _) = ty | |
| reduceToUniverse :: Local -> Term -> TermHandler Univ | |
| reduceToUniverse e t = reduceValue e t >>= go | |
| where go (TmU i) = return i | |
| go t' = typeError $ "not universe: " ++ showsTerm e t' "" | |
| assertUniverse :: Local -> Term -> TermHandler () | |
| assertUniverse e t = void $ reduceToUniverse e t | |
| typeofType :: Local -> Term -> TermHandler Univ | |
| typeofType e t = reduceToUniverse e =<< typeof e t | |
| assertType :: Local -> Term -> TermHandler () | |
| assertType e t = void $ typeofType e t | |
| univOfProd :: Univ -> Univ -> TermHandler Univ | |
| univOfProd u1 u2 = return $ UnivMax u1 u2 | |
| univSucc :: Univ -> Univ | |
| univSucc (UnivLift u i) = UnivLift u (i + 1) | |
| univSucc (UnivMax u1 u2) = UnivMax (univSucc u1) (univSucc u2) | |
| univSucc u = UnivLift u 1 | |
| -- e |- t : ty | |
| typeCheck :: Local -> Term -> Term -> TermHandler () | |
| typeCheck e t ty = do tty <- typeof e t | |
| b <- convertible e tty ty | |
| unless b $ typeError $ "typecheck error: " ++ showsTerm e t "" ++ " : " ++ showsTerm e ty "" | |
| typeof :: Local -> Term -> TermHandler Type | |
| typeof e = to | |
| where | |
| to (TmU u) = return $ TmU $ univSucc u | |
| to (TmVar v) = do (_, b) <- lookupVar e v | |
| return $ termShift (v+1) $ typeofBinding b | |
| to (TmConst n) = do b <- lookupConst n | |
| return $ typeofBinding b | |
| to (TmHole _) = error "typeof Hole" | |
| to (TmProd n ty body) = do uty <- typeofType e ty | |
| ubody <- typeofType ((n, Decl ty):e) body | |
| TmU <$> (univOfProd uty ubody) | |
| to (TmAbs n ty body) = do assertType e ty | |
| tbody <- typeof ((n, Decl ty):e) body | |
| return $ TmProd n ty tbody | |
| to (TmApp t1 t2) = do tt1 <- to t1 | |
| case tt1 of | |
| TmProd _ ty body -> do | |
| typeCheck e t2 ty | |
| return $ subst t2 body | |
| _ -> error "not applicative" | |
| to (TmEq a x y) = do ta <- to a | |
| ua <- reduceToUniverse e ta | |
| typeCheck e x a | |
| typeCheck e y a | |
| return $ TmU ua | |
| to (TmRefl a x) = do assertType e a | |
| typeCheck e x a | |
| return $ TmEq a x x | |
| to (TmEqInd ct c x y p) = do | |
| a <- to x | |
| typeCheck e x a | |
| typeCheck e y a | |
| typeCheck e p $ TmEq a x y | |
| -- e, x:A, y:A, p:A |- ct x y p : U | |
| let e' = map (Nothing,) [Decl (TmEq (termShift 2 a) (TmVar 1) (TmVar 0)), Decl (termShift 1 a), Decl (termShift 0 a)] ++ e | |
| assertType e' (TmApp (TmApp (TmApp (termShift 3 ct) (TmVar 2)) (TmVar 1)) (TmVar 0)) | |
| -- e, z:A |- c z : ct z z (refl z) | |
| let e'' = (Nothing, Decl a):e | |
| let cz = TmApp (TmApp (TmApp (termShift 1 ct) (TmVar 0)) (TmVar 0)) (TmRefl (termShift 1 a) (TmVar 0)) | |
| typeCheck e'' (TmApp (termShift 1 c) (TmVar 0)) cz | |
| -- ct x y p | |
| return $ TmApp (TmApp (TmApp ct x) y) p | |
| data Goal = Goal Int Type Local | |
| deriving (Show) | |
| data ProofState = ProofState { goals :: [Goal] | |
| , proof :: Term | |
| , lemmaName :: String | |
| , mainGoal :: Term | |
| , nextHoleId :: Int | |
| } | |
| deriving (Show) | |
| data GlobalState = GlobalState Global (Maybe ProofState) | |
| --deriving (Show) | |
| printProofState :: ProofState -> IO () | |
| printProofState s = do mapM_ runGoal $ zip [1..] $ goals s | |
| --runProof $ proof s | |
| where | |
| runGoal (i, (Goal _ ty e)) = do | |
| putStrLn $ "---- Goal " ++ show i ++ " ----" | |
| mapM_ runBinding $ zip [0..] $ tails e | |
| putStrLn "====" | |
| putStrLn $ showsTerm e ty "" | |
| runProof p = do | |
| putStrLn $ "---- Proof ----" | |
| putStrLn $ showsTerm [] p "" | |
| runBinding (i, ((n, Decl ty):e)) = do | |
| putStrLn $ "[" ++ show i ++ "] " ++ name n ++ " : " ++ showsTerm e ty "" | |
| runBinding (i, ((n, Def t ty):e)) = do | |
| putStrLn $ "[" ++ show i ++ "] " ++ name n ++ " := " ++ showsTerm e t "" ++ " : " ++ showsTerm e ty "" | |
| runBinding (_, []) = return () | |
| name (Just n) = n | |
| name Nothing = "_" | |
| initGlobal :: IO (IORef GlobalState) | |
| initGlobal = newIORef $ GlobalState (Global { gbindings = [], ubindings = [] }) Nothing | |
| type ProverCommand a = ReaderT (IORef GlobalState) IO a | |
| type CommandImpl a = StateT GlobalState IO a | |
| runTermHandler :: TermHandler a -> CommandImpl a | |
| runTermHandler h = do GlobalState g _ <- get | |
| case runReader (runErrorT h) g of | |
| Right v -> return v | |
| Left e -> fail $ show e | |
| command :: CommandImpl () -> ProverCommand () | |
| command body = do | |
| gs <- ask | |
| lift $ catch (go gs) err | |
| where | |
| go s = readIORef s >>= execStateT body >>= writeIORef s | |
| err :: IOException -> IO () | |
| err e = do | |
| putStrLn $ "Error: " ++ show e | |
| return () | |
| parseTerm :: String -> CommandImpl Term | |
| parseTerm s = do GlobalState gs mps <- get | |
| let e = case mps of | |
| Just (ProofState { goals = Goal _ _ e :_ }) -> e | |
| _ -> [] | |
| case runParser (termParser (map fst e)) () "" s of | |
| Right t -> return t | |
| Left err -> fail $ show err | |
| uvar :: String -> Univ -> ProverCommand () | |
| uvar n u = command f | |
| where f = do GlobalState g mps <- get | |
| -- TODO: need check | |
| let g' = g { ubindings = (n, u):ubindings g } | |
| put $ GlobalState g' mps | |
| lemma :: String -> String -> ProverCommand () | |
| lemma n props = command f | |
| where f = do prop <- parseTerm props | |
| GlobalState g mps <- get | |
| unless (isNothing mps) $ fail "proof not complete" | |
| runTermHandler $ assertType [] prop | |
| liftIO $ printProofState (ps prop) | |
| put $ GlobalState g (Just (ps prop)) | |
| ps prop = ProofState { goals = [Goal 0 prop []] | |
| , proof = TmHole 0 | |
| , mainGoal = prop | |
| , lemmaName = n | |
| , nextHoleId = 1 | |
| } | |
| qed :: ProverCommand () | |
| qed = command f | |
| where f = do GlobalState g mps <- get | |
| case mps of | |
| Nothing -> fail "not in proof mode" | |
| Just ps -> do | |
| unless (null $ goals ps) $ fail "proof not complete" | |
| ty <- runTermHandler $ typeof [] (proof ps) | |
| b <- runTermHandler $ convertible [] ty (mainGoal ps) | |
| unless b $ fail "invalid proof" | |
| liftIO $ putStrLn $ lemmaName ps ++ " is defined." | |
| put $ GlobalState (g { gbindings = (lemmaName ps, Def (mainGoal ps) (proof ps)):gbindings g }) Nothing | |
| substHole :: Int -> Term -> Term -> Term | |
| substHole i = subst | |
| where | |
| subst s = go | |
| where | |
| go t@(TmU _) = t | |
| go t@(TmVar _) = t | |
| go t@(TmConst _) = t | |
| go t@(TmHole j) | i == j = s | |
| | otherwise = t | |
| go (TmProd n t1 t2) = TmProd n (go t1) (go t2) | |
| go (TmAbs n t1 t2) = TmAbs n (go t1) (go t2) | |
| go (TmApp t1 t2) = TmApp (go t1) (go t2) | |
| go (TmEq t1 t2 t3) = TmEq (go t1) (go t2) (go t3) | |
| go (TmRefl t1 t2) = TmRefl (go t1) (go t2) | |
| go (TmEqInd ct a x y p) = | |
| TmEqInd (go ct) (go a) (go x) (go y) (go p) | |
| type TacImpl a = CommandImpl a | |
| curGoal :: TacImpl Goal | |
| curGoal = do | |
| GlobalState _ s <- get | |
| case s of | |
| Just (ProofState { goals = g:_ }) -> return g | |
| _ -> fail "no more goal" | |
| updateGoal :: Int -> Term -> [Goal] -> TacImpl () | |
| updateGoal i pf ss = do | |
| GlobalState g ps <- get | |
| case ps of | |
| Just s@(ProofState { goals = _:gs }) -> | |
| put $ GlobalState g $ Just $ s { goals = ss ++ gs | |
| , proof = substHole i pf (proof s) | |
| } | |
| _ -> fail "no more goal" | |
| allocId :: TacImpl Int | |
| allocId = do | |
| GlobalState g ps <- get | |
| case ps of | |
| Just s -> do | |
| let i = nextHoleId s | |
| put $ GlobalState g $ Just $ s { nextHoleId = i + 1 } | |
| return i | |
| _ -> fail "not in proof mode" | |
| tac :: TacImpl () -> ProverCommand () | |
| tac f = command body | |
| where | |
| body = do | |
| f | |
| GlobalState g ps <- get | |
| case ps of | |
| Just s -> lift $ printProofState s | |
| Nothing -> return () | |
| exact :: String -> ProverCommand () | |
| exact ts = tac f | |
| where | |
| f = do | |
| t <- parseTerm ts | |
| Goal i g e <- curGoal | |
| ty <- runTermHandler $ typeof e t | |
| b <- runTermHandler $ convertible e ty g | |
| unless b $ fail "invalid proof" | |
| updateGoal i t [] | |
| assert :: String -> ProverCommand () | |
| assert ts = tac f | |
| where | |
| f = do | |
| t <- parseTerm ts | |
| Goal i g e <- curGoal | |
| holeId1 <- allocId | |
| holeId2 <- allocId | |
| let goal1 = Goal holeId1 (TmProd Nothing t (termShift 1 g)) e | |
| goal2 = Goal holeId2 t e | |
| updateGoal i (TmApp (TmHole holeId1) (TmHole holeId2)) [goal1, goal2] | |
| intros :: [String] -> ProverCommand () | |
| intros names = tac (f names) | |
| where | |
| f [] = return () | |
| f (name:ns) = do | |
| Goal i g e <- curGoal | |
| case g of | |
| TmProd _ ty body -> do | |
| holeId <- allocId | |
| updateGoal i (TmAbs (Just name) ty (TmHole holeId)) [Goal holeId body ((Just name, Decl ty):e)] | |
| f ns | |
| _ -> fail "not product type" | |
| introsw :: String -> ProverCommand () | |
| introsw names = intros $ words names | |
| intro :: String -> ProverCommand () | |
| intro name = intros [name] | |
| elim_eq :: String -> String -> ProverCommand () | |
| elim_eq name ts = tac f | |
| where | |
| f = do | |
| p <- parseTerm ts | |
| Goal i g e <- curGoal | |
| ty <- runTermHandler $ reduceValue e =<< typeof e p | |
| case ty of | |
| TmEq a x y -> do | |
| --liftIO $ putStrLn $ "eliminating: " ++ show p ++ " : " ++ show x ++ " = " ++ show y ++ " <: " ++ show a | |
| let ct = pattern (termShift 2 p) $ pattern (termShift 1 y) $ pattern x g | |
| --liftIO $ putStrLn $ "pattern: " ++ show ct | |
| let cz = pattern (TmVar 0) $ subst (TmVar 0) $ subst (TmVar 1) $ subst (TmRefl (termShift 2 a) (TmVar 2)) ct | |
| holeId <- allocId | |
| updateGoal i (TmEqInd (TmAbs Nothing a (TmAbs Nothing (termShift 1 a) (TmAbs Nothing (TmEq (termShift 2 a) (TmVar 1) (TmVar 0)) ct))) | |
| (TmAbs (Just name) a (TmHole holeId)) x y p) [Goal holeId cz ((Just name, Decl a):e)] | |
| _ -> | |
| fail "not eq type" | |
| trans :: String -> ProverCommand () | |
| trans s = tac f | |
| where | |
| f = do | |
| t <- parseTerm s | |
| Goal i g e <- curGoal | |
| case g of | |
| TmEq a x y -> do | |
| h1 <- allocId | |
| h2 <- allocId | |
| let g1 = TmEq a x t | |
| g2 = TmEq a t y | |
| updateGoal i (foldl1 TmApp [TmConst "eq_trans", a, x, t, y, TmHole h1, TmHole h2]) | |
| [Goal h1 g1 e, Goal h2 g2 e] | |
| _ -> fail "not identity type" | |
| sym :: ProverCommand () | |
| sym = do tac f | |
| where | |
| f = do | |
| Goal i g e <- curGoal | |
| case g of | |
| TmEq a x y -> do | |
| h1 <- allocId | |
| let g1 = TmEq a y x | |
| updateGoal i (foldl1 TmApp [TmConst "eq_sym", a, y, x, TmHole h1]) | |
| [Goal h1 g1 e] | |
| _ -> fail "not identity type" | |
| f_equal_1 :: ProverCommand () | |
| f_equal_1 = do tac f | |
| where | |
| f = do | |
| Goal i g e <- curGoal | |
| case g of | |
| TmEq a (TmApp f x) (TmApp g y) | x == y -> do | |
| h1 <- allocId | |
| a <- runTermHandler $ typeof e f | |
| b <- runTermHandler $ typeof e (TmApp f x) | |
| let g1 = TmEq a f g | |
| ct = TmAbs Nothing a (TmAbs Nothing (termShift 1 a) (TmAbs Nothing (TmEq (termShift 2 a) (TmVar 1) (TmVar 0)) | |
| (TmEq (termShift 3 b) | |
| (TmApp (TmVar 2) (termShift 3 x)) | |
| (TmApp (TmVar 1) (termShift 3 x))))) | |
| c = TmAbs Nothing a (TmRefl (termShift 1 b) (TmApp (TmVar 0) (termShift 1 x))) | |
| updateGoal i (TmEqInd ct c f g (TmHole h1)) [Goal h1 g1 e] | |
| _ -> fail "not identity type" | |
| f_equal_2 :: ProverCommand () | |
| f_equal_2 = do tac f | |
| where | |
| f = do | |
| Goal i g e <- curGoal | |
| case g of | |
| TmEq a (TmApp f x) (TmApp g y) | f == g -> do | |
| h1 <- allocId | |
| a <- runTermHandler $ typeof e x | |
| b <- runTermHandler $ typeof e (TmApp f x) | |
| let g1 = TmEq a x y | |
| ct = TmAbs Nothing a (TmAbs Nothing (termShift 1 a) (TmAbs Nothing (TmEq (termShift 2 a) (TmVar 1) (TmVar 0)) | |
| (TmEq (termShift 3 b) | |
| (TmApp (termShift 3 f) (TmVar 2)) | |
| (TmApp (termShift 3 f) (TmVar 1))))) | |
| c = TmAbs Nothing a (TmRefl (termShift 1 b) (TmApp (termShift 1 f) (TmVar 0))) | |
| updateGoal i (TmEqInd ct c x y (TmHole h1)) [Goal h1 g1 e] | |
| _ -> fail "not identity type" | |
| compute :: String -> ProverCommand () | |
| compute s = command f | |
| where | |
| f = do t <- parseTerm s | |
| GlobalState g mps <- get | |
| case mps of | |
| Nothing -> do | |
| v <- runTermHandler $ reduceValue [] t -- TODO: type check | |
| liftIO $ putStrLn $ "Value: " ++ show v | |
| Just (ProofState { goals = Goal _ _ e:_ }) -> do | |
| v <- runTermHandler $ reduceValue e t -- TODO: type check | |
| liftIO $ putStrLn $ "Value: " ++ show v | |
| mod_eq :: IORef GlobalState -> IO () | |
| mod_eq g = flip runReaderT g $ do | |
| uvar "eq" Univ0 | |
| lemma "eq_sym" "forall (A : Type eq) (x y : A), x = y :> A -> y = x :> A" | |
| introsw "A x y p" | |
| elim_eq "x'" "p" | |
| exact "eq_refl A x'" | |
| qed | |
| compute "fun A : Type eq => fun x : A => eq_sym A x x (eq_refl A x)" | |
| lemma "eq_trans" "forall (A : Type eq) (x y z : A), x = y :> A -> y = z :> A -> x = z :> A" | |
| introsw "A x y z p" | |
| elim_eq "x'" "p" | |
| intro "q" | |
| elim_eq "y'" "q" | |
| exact "eq_refl A y'" | |
| qed | |
| compute "fun A : Type eq => fun x : A => eq_trans A x x x (eq_refl A x) (eq_refl A x)" | |
| lemma "path_o_refl" "forall (A : Type eq) (x y : A) (p : x = y :> A), p = eq_trans A x y y p (eq_refl A y) :> (x = y :> A)" | |
| introsw "A x y p" | |
| elim_eq "x'" "p" | |
| exact "eq_refl (x' = x' :> A) (eq_refl A x')" | |
| qed | |
| lemma "refl_o_path" "forall (A : Type eq) (x y : A) (p : x = y :> A), p = eq_trans A x x y (eq_refl A x) p :> (x = y :> A)" | |
| introsw "A x y p" | |
| elim_eq "x'" "p" | |
| exact "eq_refl (x' = x' :> A) (eq_refl A x')" | |
| qed | |
| lemma "inv_o_path" "forall (A : Type eq) (x y : A) (p : x = y :> A), eq_trans A y x y (eq_sym A x y p) p = eq_refl A y :> (y = y :> A)" | |
| introsw "A x y p" | |
| elim_eq "x'" "p" | |
| exact "eq_refl (x' = x' :> A) (eq_refl A x')" | |
| qed | |
| lemma "path_o_inv" "forall (A : Type eq) (x y : A) (p : x = y :> A), eq_trans A x y x p (eq_sym A x y p) = eq_refl A x :> (x = x :> A)" | |
| introsw "A x y p" | |
| elim_eq "x'" "p" | |
| exact "eq_refl (x' = x' :> A) (eq_refl A x')" | |
| qed | |
| lemma "inv_inv" "forall (A : Type eq) (x y : A) (p : x = y :> A), eq_sym A y x (eq_sym A x y p) = p :> (x = y :> A)" | |
| introsw "A x y p" | |
| elim_eq "x'" "p" | |
| exact "eq_refl (x' = x' :> A) (eq_refl A x')" | |
| qed | |
| lemma "o_assoc" "forall (A : Type eq) (x y z w : A) (p : x = y :> A) (q : y = z :> A) (r : z = w :> A), eq_trans A x y w p (eq_trans A y z w q r) = eq_trans A x z w (eq_trans A x y z p q) r :> (x = w :> A)" | |
| introsw "A x y z w p" | |
| elim_eq "x'" "p" | |
| intro "q" | |
| elim_eq "y'" "q" | |
| intro "r" | |
| elim_eq "z'" "r" | |
| exact "eq_refl (z' = z' :> A) (eq_refl A z')" | |
| qed | |
| lemma | |
| "whisker_r" | |
| ("forall (A : Type eq) (a b c : A) (r : b = c :> A) (p q : a = b :> A) (alpha : p = q :> a = b :> A), " | |
| ++ "eq_trans A a b c p r = eq_trans A a b c q r :> a = c :> A") | |
| introsw "A a b c r" | |
| elim_eq "x" "r" | |
| introsw "p q alpha" | |
| trans "q" | |
| trans "p" | |
| sym | |
| exact "path_o_refl A a x p" | |
| exact "alpha" | |
| exact "path_o_refl A a x q" | |
| qed | |
| lemma | |
| "whisker_l" | |
| ("forall (A : Type eq) (a b c : A) (q : a = b :> A) (r s : b = c :> A) (beta : r = s :> b = c :> A), " | |
| ++ "eq_trans A a b c q r = eq_trans A a b c q s :> a = c :> A") | |
| introsw "A a b c q" | |
| elim_eq "x" "q" | |
| introsw "r s beta" | |
| trans "s" | |
| trans "r" | |
| sym | |
| exact "refl_o_path A x c r" | |
| exact "beta" | |
| exact "refl_o_path A x c s" | |
| qed | |
| lemma | |
| "whisker_r_refl" | |
| ("forall (A : Type eq) (a : A) (alpha : eq_refl A a = eq_refl A a :> a = a :> A), " | |
| ++ "alpha = whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha :> eq_refl A a = eq_refl A a :> a = a :> A") | |
| introsw "A a alpha" | |
| trans "eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) (eq_refl (a = a :> A) (eq_refl A a)) alpha" | |
| exact "refl_o_path (a = a :> A) (eq_refl A a) (eq_refl A a) alpha" | |
| exact "path_o_refl (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) (eq_refl (a = a :> A) (eq_refl A a)) alpha)" | |
| qed | |
| lemma | |
| "whisker_l_refl" | |
| ("forall (A : Type eq) (a : A) (beta : eq_refl A a = eq_refl A a :> a = a :> A), " | |
| ++ "beta = whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta :> eq_refl A a = eq_refl A a :> a = a :> A") | |
| introsw "A a beta" | |
| trans "eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) (eq_refl (a = a :> A) (eq_refl A a)) beta" | |
| exact "refl_o_path (a = a :> A) (eq_refl A a) (eq_refl A a) beta" | |
| exact "path_o_refl (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) (eq_refl (a = a :> A) (eq_refl A a)) beta)" | |
| qed | |
| lemma | |
| "whisker_rl_lr" | |
| ("forall (A : Type eq) (a b c : A) (p q : a = b :> A) (alpha : p = q :> a = b :> A) " | |
| ++ "(r s : b = c :> A) (beta : r = s :> b = c :> A), " | |
| ++ "eq_trans (a = c :> A) " | |
| ++ "(eq_trans A a b c p r) " | |
| ++ "(eq_trans A a b c q r) " | |
| ++ "(eq_trans A a b c q s) " | |
| ++ "(whisker_r A a b c r p q alpha) (whisker_l A a b c q r s beta) =" | |
| ++ "eq_trans (a = c :> A) " | |
| ++ "(eq_trans A a b c p r) " | |
| ++ "(eq_trans A a b c p s) " | |
| ++ "(eq_trans A a b c q s) " | |
| ++ "(whisker_l A a b c p r s beta) (whisker_r A a b c s p q alpha) " | |
| ++ ":> eq_trans A a b c p r = eq_trans A a b c q s :> a = c :> A") | |
| introsw "A a b c p q alpha" | |
| elim_eq "p'" "alpha" | |
| elim_eq "a'" "p'" | |
| introsw "r s beta" | |
| elim_eq "r'" "beta" | |
| elim_eq "b'" "r'" | |
| exact "eq_refl (eq_refl A b' = eq_refl A b' :> b' = b' :> A) (eq_refl (b' = b' :> A) (eq_refl A b'))" | |
| qed | |
| lemma "Eckmann_Hilton" | |
| ("forall (A : Type eq) (a : A) " | |
| ++ "(alpha : eq_refl A a = eq_refl A a :> a = a :> A)" | |
| ++ "(beta : eq_refl A a = eq_refl A a :> a = a :> A), " | |
| ++ "eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha beta = " | |
| ++ "eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) beta alpha :> eq_refl A a = eq_refl A a :> a = a :> A") | |
| introsw "A a alpha beta" | |
| trans ("eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha " | |
| ++ "(whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta)") | |
| f_equal_2 | |
| exact "whisker_l_refl A a beta" | |
| trans ("eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) " | |
| ++ "(whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha) " | |
| ++ "(whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta)") | |
| f_equal_1 | |
| f_equal_2 | |
| exact "whisker_r_refl A a alpha" | |
| trans ("eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) " | |
| ++ "(whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) " | |
| ++ "(whisker_r A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) alpha)") | |
| exact "whisker_rl_lr A a a a (eq_refl A a) (eq_refl A a) alpha (eq_refl A a) (eq_refl A a) beta" | |
| trans ("eq_trans (a = a :> A) (eq_refl A a) (eq_refl A a) (eq_refl A a) " | |
| ++ "(whisker_l A a a a (eq_refl A a) (eq_refl A a) (eq_refl A a) beta) " | |
| ++ "alpha") | |
| f_equal_2 | |
| sym | |
| exact "whisker_r_refl A a alpha" | |
| f_equal_1 | |
| f_equal_2 | |
| sym | |
| exact "whisker_l_refl A a beta" | |
| qed | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment