From 0a68d57f804d376dd363a501cfd15affc242b153 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 3 Mar 2021 00:43:34 -0300 Subject: [PATCH] include proof of strong funext --- intro.tt | 57 +++++++++++++++++++++++++++++++------------- src/Elab.hs | 4 ++-- src/Elab/Monad.hs | 4 ++-- src/Elab/WiredIn.hs | 16 ++++++------- src/Main.hs | 17 ++++++------- src/Syntax/Pretty.hs | 56 +++++++++++++++++++++++++++++++++++++++++-- 6 files changed, 116 insertions(+), 38 deletions(-) diff --git a/intro.tt b/intro.tt index ca7b001..ea31fc7 100644 --- a/intro.tt +++ b/intro.tt @@ -138,10 +138,6 @@ funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} -> Path f g funext h i x = h x i -happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} - -> (p : Path f g) -> (x : A) -> Path (f x) (g x) -happly p x i = p i x - -- The proposition associated with an element of the interval ------------------------------------------------------------- @@ -520,42 +516,42 @@ IsoToEquiv {A} {B} iso = lemIso y x0 x1 p0 p1 = let rem0 : Path x0 (g y) - rem0 i = hcomp {A} (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i))) + rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i))) rem1 : Path x1 (g y) - rem1 i = hcomp {A} (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i))) + rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i))) p : Path x0 x1 - p i = hcomp {A} (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y)) + p i = comp (\i -> A) (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y)) fill0 : I -> I -> A - fill0 i j = hcomp {A} (\k [ (i = i0) -> t x0 (iand j k) - , (i = i1) -> g y - , (j = i0) -> g (p0 i) - ]) + fill0 i j = comp (\i -> A) (\k [ (i = i0) -> t x0 (iand j k) + , (i = i1) -> g y + , (j = i0) -> g (p0 i) + ]) (inS (g (p0 i))) fill1 : I -> I -> A - fill1 i j = hcomp {A} (\k [ (i = i0) -> t x1 (iand j k) + fill1 i j = comp (\i -> A) (\k [ (i = i0) -> t x1 (iand j k) , (i = i1) -> g y , (j = i0) -> g (p1 i) ]) (inS (g (p1 i))) fill2 : I -> I -> A - fill2 i j = hcomp {A} (\k [ (i = i0) -> rem0 (ior j (inot k)) + fill2 i j = comp (\i -> A) (\k [ (i = i0) -> rem0 (ior j (inot k)) , (i = i1) -> rem1 (ior j (inot k)) , (j = i1) -> g y ]) (inS (g y)) sq : I -> I -> A - sq i j = hcomp {A} (\k [ (i = i0) -> fill0 j (inot k) + sq i j = comp (\i -> A) (\k [ (i = i0) -> fill0 j (inot k) , (i = i1) -> fill1 j (inot k) , (j = i1) -> g y , (j = i0) -> t (p i) (inot k) ]) (inS (fill2 i j)) sq1 : I -> I -> B - sq1 i j = hcomp {B} (\k [ (i = i0) -> s (p0 j) k + sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 j) k , (i = i1) -> s (p1 j) k , (j = i0) -> s (f (p i)) k , (j = i1) -> s y k @@ -662,4 +658,33 @@ isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q -- of false as the point x is just from the endpoints of trueNotFalse. universeNotSet : isHSet Type -> bottom -universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false) \ No newline at end of file +universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false) + +-- Funext is an inverse of happly +--------------------------------- +-- +-- Above we proved function extensionality, namely, that functions +-- pointwise equal everywhere are themselves equal. +-- However, this formulation of the axiom is known as "weak" function +-- extensionality. The strong version is as follows: + +Hom : {A : Type} {B : A -> Type} (f : (x : A) -> B x) -> (g : (x : A) -> B x) -> Type +Hom {A} f g = (x : A) -> Path (f x) (g x) + +happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} + -> (p : Path f g) -> Hom f g +happly p x i = p i x + +-- Strong function extensionality: happly is an equivalence. + +happlyIsIso : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} + -> isIso {Path f g} {Hom f g} happly +happlyIsIso {A} {B} {f} {g} = (funext {A} {B} {f} {g}, \hom -> refl, \path -> refl) + +pathIsHom : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} + -> Path (Path f g) (Hom f g) +pathIsHom {A} {B} {f} {g} = + let + theIso : Iso (Path f g) (Hom f g) + theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g}) + in univalence (IsoToEquiv theIso) \ No newline at end of file diff --git a/src/Elab.hs b/src/Elab.hs index b9163cc..5f453a2 100644 --- a/src/Elab.hs +++ b/src/Elab.hs @@ -10,6 +10,8 @@ import Control.Exception import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Data.Traversable +import Data.Text (Text) +import Data.Map (Map) import Data.Typeable import Data.Foldable @@ -24,8 +26,6 @@ import Prettyprinter import Syntax.Pretty import Syntax -import Data.Map (Map) -import Data.Text (Text) infer :: P.Expr -> ElabM (Term, NFType) infer (P.Span ex a b) = withSpan a b $ infer ex diff --git a/src/Elab/Monad.hs b/src/Elab/Monad.hs index 69b635d..323fc7b 100644 --- a/src/Elab/Monad.hs +++ b/src/Elab/Monad.hs @@ -11,15 +11,15 @@ import Data.Text.Prettyprint.Doc.Render.Terminal (AnsiStyle) import qualified Data.Map.Strict as Map import Data.Text.Prettyprint.Doc import Data.Map.Strict (Map) +import Data.Sequence (Seq) import Data.Text (Text) import Data.Set (Set) import Data.Typeable +import Data.IORef import qualified Presyntax.Presyntax as P import Syntax -import Data.IORef -import Data.Sequence (Seq) data ElabEnv = ElabEnv { getEnv :: Map Name (NFType, Value) diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs index a625312..e69a9c2 100644 --- a/src/Elab/WiredIn.hs +++ b/src/Elab/WiredIn.hs @@ -209,7 +209,7 @@ ielim _line _left _right fn i = VI0 -> _left _ -> case x of VNe n sp -> VNe n (sp Seq.:|> PIElim _line _left _right i) - VSystem (Map.toList -> []) -> VSystem (Map.fromList []) + VSystem map -> VSystem (fmap (flip (ielim _line _left _right) i) map) _ -> error $ "can't ielim " ++ show fn outS :: NFSort -> NFEndp -> Value -> Value -> Value @@ -225,7 +225,7 @@ outS _ _ _ v = error $ "can't outS " ++ show v comp :: NFLine -> NFEndp -> Value -> Value -> Value comp _ VI1 u _ = u @@ VI1 @@ VItIsOne comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = - case force $ a @@ VVar (Bound (T.pack "neutral composition") 0) of + case force $ a @@ VVar (Bound (T.pack "i") 0) of VPi{} -> let plic i = let VPi p _ _ = force (a @@ i) in p @@ -235,7 +235,7 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i ybar i y = y' (inot i) y in VLam (plic VI1) . Closure (Bound "x" 0) $ \arg -> - comp (fun \i -> rng i (ybar i arg)) + comp (line \i -> rng i (ybar i arg)) phi (system \i isone -> vApp (plic i) (u @@ i @@ isone) (ybar i arg)) (VInc (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg))) @@ -257,7 +257,7 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = v' i = let VPath _ _ thev = force (a @@ i) in thev in VLine (a' VI1 @@ VI1) (u' VI1) (v' VI1) $ fun \j -> - comp (fun a') + comp (fun \x -> a' x @@ x) (phi `ior` j `ior` inot j) (system \i isone -> mkVSystem (Map.fromList [ (phi, ielim (a' VI0) (u' VI0) (v' VI0) (u @@ i @@ isone) j) , (j, v' i) @@ -321,7 +321,7 @@ system k = fun \i -> fun \isone -> k i isone fill :: NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value fill a phi u a0 j = - comp (fun \i -> a @@ (i `iand` j)) + comp (line \i -> a @@ (i `iand` j)) (phi `ior` inot j) (fun \i -> fun \isone -> mkVSystem (Map.fromList [ (phi, u @@ (i `iand` j) @@ isone) , (inot j, a0)])) @@ -372,8 +372,8 @@ equiv a b = exists' "f" (a ~> b) \f -> isEquiv a b f pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value) pres tyT tyA f phi t t0 = (VInc pathT phi (VLine (tyA VI1) c1 c2 (line path)), pathT, fun $ \u -> VLine (fun (const (tyA VI1))) c1 c2 (fun (const (f VI1 @@ (t VI1 @@ u))))) where pathT = VPath (fun (const (tyA VI1))) c1 c2 - c1 = comp (fun tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (tyA VI0) phi (f VI0 @@ t0)) - c2 = f VI1 @@ comp (fun tyT) phi (system \i u -> t i @@ u) t0 + c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (tyA VI0) phi (f VI0 @@ t0)) + c2 = f VI1 @@ comp (line tyT) phi (system \i u -> t i @@ u) t0 a0 = f VI0 @@ t0 v = fill (fun tyT) phi (system \i u -> t i @@ u) t0 @@ -411,4 +411,4 @@ elimBool prop x y bool = case force bool of VTt -> x VFf -> y - _ -> VIf prop x y bool \ No newline at end of file + _ -> VIf prop x y bool diff --git a/src/Main.hs b/src/Main.hs index f19a09b..9eec467 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -13,9 +13,15 @@ import qualified Data.ByteString.Lazy as Bsl import qualified Data.Text.Encoding as T import qualified Data.Map.Strict as Map import qualified Data.Text.IO as T +import qualified Data.Set as Set import qualified Data.Text as T +import Data.Sequence (Seq) import Data.Text ( Text ) import Data.Foldable +import Data.Maybe +import Data.IORef + +import Debug.Trace import Elab.Monad hiding (switch) import Elab.WiredIn @@ -26,6 +32,7 @@ import Options.Applicative import Presyntax.Presyntax (Posn(Posn)) import Presyntax.Parser +import Presyntax.Tokens import Presyntax.Lexer import Prettyprinter @@ -35,12 +42,6 @@ import Syntax import System.Console.Haskeline import System.Exit -import qualified Data.Set as Set -import Data.Maybe -import Presyntax.Tokens -import Debug.Trace -import Data.IORef -import Data.Sequence (Seq) main :: IO () main = do @@ -131,7 +132,7 @@ displayAndDie lines e = do exitFailure displayExceptions :: Text -> [Handler ()] -displayExceptions lines = +displayExceptions lines = [ Handler \(WhileChecking a b e) -> do T.putStrLn $ squiggleUnder a b lines displayExceptions' lines e @@ -177,7 +178,7 @@ reportUnsolved metas = do "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> prettyTm (quote (mvType m)) <+> "should satisfy:" for_ p \p -> T.putStrLn . render $ indent 2 $ prettyTm (quote (VNe (HMeta m) (fst p))) <+> pretty '≡' <+> prettyTm (quote (snd p)) - + displayExceptions' :: Exception e => Text -> e -> IO () displayExceptions' lines e = displayAndDie lines e `catch` \(_ :: ExitCode) -> pure () diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs index cbad306..9d44e9c 100644 --- a/src/Syntax/Pretty.hs +++ b/src/Syntax/Pretty.hs @@ -6,9 +6,11 @@ import Control.Arrow (Arrow(first)) import qualified Data.Map.Strict as Map import qualified Data.Text.Lazy as L +import qualified Data.Set as Set import qualified Data.Text as T import Data.Map.Strict (Map) import Data.Text (Text) +import Data.Set (Set) import Data.Generics import Presyntax.Presyntax (Plicity(..)) @@ -43,8 +45,14 @@ prettyTm = prettyTm . everywhere (mkT beautify) where (al, bod) = unwindLam l - prettyArgList (Ex, v) = pretty v - prettyArgList (Im, v) = braces (pretty v) + used = freeVars bod + + prettyArgList (Ex, v) + | v `Set.member` used = pretty v + | otherwise = pretty "_" + prettyArgList (Im, v) + | v `Set.member` used = braces $ pretty v + | otherwise = pretty "_" prettyTm (Meta x) = keyword $ pretty '?' <> pretty (mvName x) prettyTm Type{} = keyword $ pretty "Type" @@ -140,3 +148,47 @@ showValue = L.unpack . renderLazy . layoutSmart defaultLayoutOptions . prettyTm showFace :: Map Head Bool -> Doc AnsiStyle showFace = hsep . map go . Map.toList where go (h, b) = parens $ prettyTm (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0") + +freeVars :: Term -> Set Name +freeVars (Ref v) = Set.singleton v +freeVars (App _ f x) = Set.union (freeVars f) (freeVars x) +freeVars (Pi _ n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y) +freeVars (Lam _ n x) = n `Set.delete` freeVars x +freeVars (Let ns x) = Set.union (freeVars x `Set.difference` bound) freed where + bound = Set.fromList (map (\(x, _, _) -> x) ns) + freed = foldr (\(_, x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty ns +freeVars Meta{} = mempty +freeVars Type{} = mempty +freeVars Typeω{} = mempty +freeVars I{} = mempty +freeVars I0{} = mempty +freeVars I1{} = mempty +freeVars (Sigma n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y) +freeVars (Pair x y) = Set.unions $ map freeVars [x, y] +freeVars (Proj1 x) = Set.unions $ map freeVars [x] +freeVars (Proj2 x) = Set.unions $ map freeVars [x] +freeVars (IAnd x y) = Set.unions $ map freeVars [x, y] +freeVars (IOr x y) = Set.unions $ map freeVars [x, y] +freeVars (INot x) = Set.unions $ map freeVars [x] +freeVars (PathP x y z) = Set.unions $ map freeVars [x, y, z] +freeVars (IElim x y z a b) = Set.unions $ map freeVars [x, y, z, a, b] +freeVars (PathIntro x y z a) = Set.unions $ map freeVars [x, y, z, a] +freeVars (IsOne a) = Set.unions $ map freeVars [a] +freeVars (IsOne1 a) = Set.unions $ map freeVars [a] +freeVars (IsOne2 a) = Set.unions $ map freeVars [a] +freeVars ItIsOne{} = mempty +freeVars (Partial x y) = Set.unions $ map freeVars [x, y] +freeVars (PartialP x y) = Set.unions $ map freeVars [x, y] +freeVars (System fs) = foldr (\(x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty (Map.toList fs) + +freeVars (Sub x y z) = Set.unions $ map freeVars [x, y, z] +freeVars (Inc x y z) = Set.unions $ map freeVars [x, y, z] +freeVars (Ouc x y z a) = Set.unions $ map freeVars [x, y, z, a] +freeVars (Comp x y z a) = Set.unions $ map freeVars [x, y, z, a] +freeVars (GlueTy x y z a) = Set.unions $ map freeVars [x, y, z, a] +freeVars (Glue x y z a b c) = Set.unions $ map freeVars [x, y, z, a, b, c] +freeVars (Unglue x y z a c) = Set.unions $ map freeVars [x, y, z, a, c] +freeVars Bool{} = mempty +freeVars Tt{} = mempty +freeVars Ff{} = mempty +freeVars (If x y z a) = Set.unions $ map freeVars [x, y, z, a]