wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

starting progress on (non-dependent) products

Browse source
This commit is contained in:
William Ball 2025-01-24 00:57:13 -08:00
parent 52ce107a04
commit 2c1f193d77
Signed by: wball
GPG key ID: B8682D8137B70765
8 changed files with 123 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
examples/logic.pg
View file

@ -35,20 +35,17 @@ def double_neg_intro (A : ★) (a : A) : not (not A) :=
-- Conjunction
def ∧ (A B : ★) : ★ := forall (C : ★), (A → B → C) → C;
def ∧ (A B : ★) : ★ := {A × B};
infixl 10 ∧;
-- introduction rule
def and_intro (A B : ★) (a : A) (b : B) : A ∧ B :=
fun (C : ★) (H : A → B → C) => H a b;
def and_intro (A B : ★) (a : A) (b : B) : A ∧ B := <a, b>;
-- left elimination rule
def and_elim_l (A B : ★) (ab : A ∧ B) : A :=
ab A (fun (a : A) (b : B) => a);
def and_elim_l (A B : ★) (ab : A ∧ B) : A := π₁ ab;
-- right elimination rule
def and_elim_r (A B : ★) (ab : A ∧ B) : B :=
ab B (fun (a : A) (b : B) => b);
def and_elim_r (A B : ★) (ab : A ∧ B) : B := π₂ ab;
-- --------------------------------------------------------------------------------------------------------------
@ -149,31 +146,25 @@ section Theorems
-- ~(A ∨ B) => ~A ∧ ~B
def de_morgan1 (h : not (A ∨ B)) : not A ∧ not B :=
and_intro (not A) (not B)
([a : A] h (or_intro_l A B a))
([b : B] h (or_intro_r A B b));
<[a : A] h (or_intro_l A B a)
,[b : B] h (or_intro_r A B b)>;
-- ~A ∧ ~B => ~(A ∨ B)
def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) :=
fun (contra : A ∨ B) =>
or_elim A B false contra
(and_elim_l (not A) (not B) h)
(and_elim_r (not A) (not B) h);
or_elim A B false contra (π₁ h) (π₂ h);
-- ~A ∨ ~B => ~(A ∧ B)
def de_morgan3 (h : not A ∨ not B) : not (A ∧ B) :=
fun (contra : A ∧ B) =>
or_elim (not A) (not B) false h
(fun (na : not A) => na (and_elim_l A B contra))
(fun (nb : not B) => nb (and_elim_r A B contra));
(fun (na : not A) => na (π₁ contra))
(fun (nb : not B) => nb (π₂ contra));
-- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
-- A ∧ B => B ∧ A
def and_comm (h : A ∧ B) : B ∧ A :=
and_intro B A
(and_elim_r A B h)
(and_elim_l A B h);
def and_comm (h : A ∧ B) : B ∧ A := <π₂ h, π₁ h>;
-- A ∨ B => B ∨ A
def or_comm (h : A ∨ B) : B ∨ A :=
@ -183,23 +174,11 @@ section Theorems
-- A ∧ (B ∧ C) => (A ∧ B) ∧ C
def and_assoc_l (h : A ∧ (B ∧ C)) : (A ∧ B) ∧ C :=
let (a := (and_elim_l A (B ∧ C) h))
(bc := (and_elim_r A (B ∧ C) h))
(b := (and_elim_l B C bc))
(c := (and_elim_r B C bc))
in
and_intro (A ∧ B) C (and_intro A B a b) c
end;
<<π₁ h, π₁ (π₂ h)>, π₂ (π₂ h)>;
-- (A ∧ B) ∧ C => A ∧ (B ∧ C)
def and_assoc_r (h : (A ∧ B) ∧ C) : A ∧ (B ∧ C) :=
let (ab := and_elim_l (A ∧ B) C h)
(a := and_elim_l A B ab)
(b := and_elim_r A B ab)
(c := and_elim_r (A ∧ B) C h)
in
and_intro A (B ∧ C) a (and_intro B C b c)
end;
<π₁ (π₁ h), <π₂ (π₁ h), π₂ h>>;
-- A ∨ (B ∨ C) => (A ∨ B) ∨ C
def or_assoc_l (h : A ∨ (B ∨ C)) : (A ∨ B) ∨ C :=
@ -221,21 +200,15 @@ section Theorems
-- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
def and_distrib_l_or (h : A ∧ (B ∨ C)) : A ∧ B ∨ A ∧ C :=
or_elim B C (A ∧ B ∨ A ∧ C) (and_elim_r A (B ∨ C) h)
(fun (b : B) => or_intro_l (A ∧ B) (A ∧ C)
(and_intro A B (and_elim_l A (B ∨ C) h) b))
(fun (c : C) => or_intro_r (A ∧ B) (A ∧ C)
(and_intro A C (and_elim_l A (B ∨ C) h) c));
or_elim B C (A ∧ B ∨ A ∧ C) (π₂ h)
(fun (b : B) => or_intro_l (A ∧ B) (A ∧ C) <π₁ h, b>)
(fun (c : C) => or_intro_r (A ∧ B) (A ∧ C) <π₁ h, c>);
-- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
def and_factor_l_or (h : A ∧ B ∨ A ∧ C) : A ∧ (B ∨ C) :=
or_elim (A ∧ B) (A ∧ C) (A ∧ (B ∨ C)) h
(fun (ab : A ∧ B) => and_intro A (B ∨ C)
(and_elim_l A B ab)
(or_intro_l B C (and_elim_r A B ab)))
(fun (ac : A ∧ C) => and_intro A (B ∨ C)
(and_elim_l A C ac)
(or_intro_r B C (and_elim_r A C ac)));
(fun (ab : A ∧ B) => <π₁ ab, or_intro_l B C (π₂ ab)>)
(fun (ac : A ∧ C) => <π₁ ac, or_intro_r B C (π₂ ac)>);
-- Thanks Quinn!
-- A ∨ B => ~B => A

17
lib/Check.hs
View file

@ -16,6 +16,12 @@ matchPi x mt =
(Pi _ a b) -> pure (a, b)
t -> throwError $ ExpectedPiType x t
matchProd :: Expr -> Expr -> ReaderT Env Result (Expr, Expr)
matchProd x mt =
whnf mt >>= \case
(Prod a b) -> pure (a, b)
t -> throwError $ ExpectedProdType x t
findLevel :: Context -> Expr -> ReaderT Env Result Integer
findLevel g a = do
s <- findType g a
@ -72,6 +78,17 @@ findType g e@(Let _ (Just t) v b) = do
_ <- findType g t
betaEquiv' e t res
pure t
findType g (Prod a b) = do
aSort <- findType g a
bSort <- findType g b
liftEither $ compSort a b aSort bSort
findType g (Pair a b) = do
aType <- findType g a
bType <- findType g b
validateType g $ Prod aType bType
pure $ Prod aType bType
findType g (Pi1 x) = fst <$> (findType g x >>= matchProd x)
findType g (Pi2 x) = snd <$> (findType g x >>= matchProd x)
checkType :: Env -> Expr -> Result Expr
checkType env t = runReaderT (findType [] t) env

12
lib/Elaborator.hs
View file

@ -116,6 +116,10 @@ usedVars (I.Let name ascr value body) = saveState $ do
ascr' <- traverse usedVars ascr
removeName name
S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
usedVars (I.Prod m n) = S.union <$> usedVars m <*> usedVars n
usedVars (I.Pair m n) = S.union <$> usedVars m <*> usedVars n
usedVars (I.Pi1 x) = usedVars x
usedVars (I.Pi2 x) = usedVars x
-- traverse the body of a definition, adding the necessary section arguments to
-- any definitions made within the section
@ -142,6 +146,10 @@ traverseBody (I.Let name ascr value body) = saveState $ do
value' <- traverseBody value
removeName name
I.Let name ascr' value' <$> traverseBody body
traverseBody (I.Prod m n) = I.Prod <$> traverseBody m <*> traverseBody n
traverseBody (I.Pair m n) = I.Pair <$> traverseBody m <*> traverseBody n
traverseBody (I.Pi1 x) = I.Pi1 <$> traverseBody x
traverseBody (I.Pi2 x) = I.Pi2 <$> traverseBody x
mkPi :: (Text, IRExpr) -> IRExpr -> IRExpr
mkPi (param, typ) = I.Pi param typ
@ -206,3 +214,7 @@ elaborate ir = evalState (elaborate' ir) []
ty' <- elaborate' ty
modify (name :)
E.Let name (Just ty') val' <$> elaborate' body
elaborate' (I.Prod m n) = E.Prod <$> elaborate' m <*> elaborate' n
elaborate' (I.Pair m n) = E.Pair <$> elaborate' m <*> elaborate' n
elaborate' (I.Pi1 x) = E.Pi1 <$> elaborate' x
elaborate' (I.Pi2 x) = E.Pi2 <$> elaborate' x

2
lib/Errors.hs
View file

@ -9,6 +9,7 @@ data Error
= UnboundVariable Text
| NotASort Expr
| ExpectedPiType Expr Expr
| ExpectedProdType Expr Expr
| NotEquivalent Expr Expr Expr
| PNMissingType Text
| DuplicateDefinition Text
@ -18,6 +19,7 @@ instance Pretty Error where
pretty (UnboundVariable x) = "Unbound variable: '" <> pretty x <> "'"
pretty (NotASort x) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> "is not a type"
pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a function, instead is type" <> line <> pretty t)
pretty (ExpectedProdType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a pair, instead is type" <> line <> pretty t)
pretty (NotEquivalent a a' e) =
group $
hang 4 ("Cannot unify" <> line <> pretty a)

26
lib/Eval.hs
View file

@ -45,6 +45,10 @@ subst k s (App m n) = App (subst k s m) (subst k s n)
subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices s) n)
subst k s (Let x t v b) = Let x t (subst k s v) (subst (k + 1) (incIndices s) b)
subst k s (Prod m n) = Prod (subst k s m) (subst k s n)
subst k s (Pair m n) = Pair (subst k s m) (subst k s n)
subst k s (Pi1 x) = Pi1 (subst k s x)
subst k s (Pi2 x) = Pi2 (subst k s x)
envLookupVal :: Text -> ReaderT Env Result Expr
envLookupVal n = asks ((_val <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
@ -59,6 +63,12 @@ reduce (Abs x t v) = Abs x <$> reduce t <*> reduce v
reduce (Pi x t v) = Pi x <$> reduce t <*> reduce v
reduce (Free n) = envLookupVal n
reduce (Let _ _ v b) = pure $ subst 0 v b
reduce (Prod a b) = Prod <$> reduce a <*> reduce b
reduce (Pair a b) = Pair <$> reduce a <*> reduce b
reduce (Pi1 (Pair a _)) = pure a
reduce (Pi2 (Pair _ b)) = pure b
reduce (Pi1 x) = Pi1 <$> reduce x
reduce (Pi2 x) = Pi2 <$> reduce x
reduce e = pure e
normalize :: Expr -> ReaderT Env Result Expr
@ -78,6 +88,18 @@ whnf (App m n) = do
else whnf $ App m' n
whnf (Free n) = envLookupVal n >>= whnf
whnf (Let _ _ v b) = whnf $ subst 0 v b
whnf (Pi1 (Pair a _)) = pure a
whnf (Pi2 (Pair _ b)) = pure b
whnf (Pi1 x) = do
x' <- whnf x
if x == x'
then pure $ Pi1 x
else whnf $ Pi1 x'
whnf (Pi2 x) = do
x' <- whnf x
if x == x'
then pure $ Pi2 x
else whnf $ Pi2 x'
whnf e = pure e
betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
@ -99,6 +121,10 @@ betaEquiv e1 e2
(Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
(Let _ _ v b, e) -> betaEquiv (subst 0 v b) e
(e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
(Prod a b, Prod a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b'
(Pair a b, Pair a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b'
(Pi1 x, Pi1 x') -> betaEquiv x x'
(Pi2 x, Pi2 x') -> betaEquiv x x'
_ -> pure False -- remaining cases impossible, false, or redundant
betaEquiv' :: Expr -> Expr -> Expr -> ReaderT Env Result ()

20
lib/Expr.hs
View file

@ -15,6 +15,10 @@ data Expr where
Abs :: Text -> Expr -> Expr -> Expr
Pi :: Text -> Expr -> Expr -> Expr
Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr
Prod :: Expr -> Expr -> Expr
Pair :: Expr -> Expr -> Expr
Pi1 :: Expr -> Expr
Pi2 :: Expr -> Expr
deriving (Show, Ord)
instance Pretty Expr where
@ -30,6 +34,10 @@ instance Eq Expr where
(Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2
(Pi _ t1 b1) == (Pi _ t2 b2) = t1 == t2 && b1 == b2
(Let _ _ v1 b1) == (Let _ _ v2 b2) = v1 == v2 && b1 == b2
(Prod x1 y1) == (Prod x2 y2) = x1 == x2 && y1 == y2
(Pair x1 y1) == (Pair x2 y2) = x1 == x2 && y1 == y2
(Pi1 x) == (Pi1 y) = x == y
(Pi2 x) == (Pi2 y) = x == y
_ == _ = False
occursFree :: Integer -> Expr -> Bool
@ -42,6 +50,10 @@ occursFree n (App a b) = on (||) (occursFree n) a b
occursFree n (Abs _ a b) = occursFree n a || occursFree (n + 1) b
occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b
occursFree n (Let _ _ v b) = occursFree n v || occursFree (n + 1) b
occursFree n (Prod x y) = occursFree n x || occursFree n y
occursFree n (Pair x y) = occursFree n x || occursFree n y
occursFree n (Pi1 x) = occursFree n x
occursFree n (Pi2 x) = occursFree n x
shiftIndices :: Integer -> Integer -> Expr -> Expr
shiftIndices d c (Var x k)
@ -55,6 +67,10 @@ shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
shiftIndices d c (Abs x m n) = Abs x (shiftIndices d c m) (shiftIndices d (c + 1) n)
shiftIndices d c (Pi x m n) = Pi x (shiftIndices d c m) (shiftIndices d (c + 1) n)
shiftIndices d c (Let x t v b) = Let x t (shiftIndices d c v) (shiftIndices d (c + 1) b)
shiftIndices d c (Prod m n) = Prod (shiftIndices d c m) (shiftIndices d c n)
shiftIndices d c (Pair m n) = Pair (shiftIndices d c m) (shiftIndices d c n)
shiftIndices d c (Pi1 x) = Pi1 (shiftIndices d c x)
shiftIndices d c (Pi2 x) = Pi2 (shiftIndices d c x)
incIndices :: Expr -> Expr
incIndices = shiftIndices 1 0
@ -206,6 +222,10 @@ prettyExpr k expr = case expr of
where
(binds, body) = collectLets expr
bindings = sep $ map pretty binds
(Prod x y) -> parens $ parens (pretty x) <+> "×" <+> parens (pretty y)
(Pair x y) -> parens $ pretty x <> "," <+> pretty y
(Pi1 x) -> parens $ "π₁" <+> parens (pretty x)
(Pi2 x) -> parens $ "π₂" <+> parens (pretty x)
prettyT :: Expr -> Text
prettyT = renderStrict . layoutSmart defaultLayoutOptions . pretty

10
lib/IR.hs
View file

@ -27,6 +27,16 @@ data IRExpr
, letValue :: IRExpr
, letBody :: IRExpr
}
| Prod
{ prodLeft :: IRExpr
, prodRight :: IRExpr
}
| Pair
{ pairLeft :: IRExpr
, pairRight :: IRExpr
}
| Pi1 IRExpr
| Pi2 IRExpr
deriving (Show, Eq, Ord)
data IRSectionDef

20
lib/Parser.hs
View file

@ -174,8 +174,26 @@ pSort = lexeme $ pStar <|> pSquare
pOpSection :: Parser IRExpr
pOpSection = lexeme $ parens $ Var <$> pSymbol
pProd :: Parser IRExpr
pProd = lexeme $ between (char '{') (char '}') $ do
left <- pIRExpr
_ <- symbol "×"
Prod left <$> pIRExpr
pPair :: Parser IRExpr
pPair = lexeme $ between (char '<') (char '>') $ do
left <- pIRExpr
_ <- symbol ","
Pair left <$> pIRExpr
pPi1 :: Parser IRExpr
pPi1 = lexeme $ symbol "π₁" >> Pi1 <$> pIRExpr
pPi2 :: Parser IRExpr
pPi2 = lexeme $ symbol "π₂" >> Pi2 <$> pIRExpr
pTerm :: Parser IRExpr
pTerm = lexeme $ label "term" $ choice [pSort, pPureVar, pVar, try pOpSection, parens pIRExpr]
pTerm = lexeme $ label "term" $ choice [pSort, pPi1, pPi2, pPureVar, pVar, pProd, pPair, try pOpSection, parens pIRExpr]
pInfix :: Parser IRExpr
pInfix = parseWithPrec 0