clean up letpair answer. revise Hw2

full/pi/Hw2.pi

@@ -1,11 +1,44 @@
 module Hw2 where
 
--- show that propositional equality is transitive 
+-- First: read section 7.2 of the lecture notes about how 
+-- propositional equality works in pi-forall. The key points are
+-- that `Refl` is a proof of the identity type `(a = b)` when 
+-- a is definitionally equal to b, and that `subst` is the elimination
+-- form.
+
+-- For example, we can show that equality is symmetric by 
+-- eliminating pf (of type `x = y`) when type checking 
+-- `Refl` against type `y = x`.  The `subst` adds the definition 
+-- `x = y` to the context, so both sides of `y = x` wh normalize to y. 
+
+sym : (A:Type) -> (x:A) -> (y:A) -> (x = y) -> y = x
+sym = \ A x y pf .
+  subst Refl by pf 
+
+-- Homework: show that propositional equality is transitive 
 
 trans : (A:Type) -> (x:A) -> (y:A) -> (z:A) -> (x = z) -> (z = y) -> (x = y)
 trans = \A x y z pf1 pf2 . 
   subst pf1 by pf2 
 
+-- Homework: show that it is congruent for (nondependent) application
+
+f_cong : (A:Type) -> (B : Type) -> (f : A -> B) -> (g : A -> B)
+       -> (x:A) -> (y:A) 
+       -> (f = g) -> (x = y) -> (f x = g y)
+f_cong = \ A B f g x y pf1 pf2 . 
+   subst (subst Refl by pf1) by pf2 
+
+-- Homework: what does congruence for dependent application look like?
+-- In other words, what if f and g above have a dependent type?
+
+f_cong_dep : (A:Type) -> (B : A -> Type) 
+       -> (f : (x:A) -> B x) -> (g : (x:A) -> B x)
+       -> (x:A) -> (y:A) 
+       -> (f = g) -> (p : x = y) -> (f x = subst g y by p)
+f_cong_dep =  \ A B f g x y pf1 pf2 . 
+   subst (subst Refl by pf1) by pf2 
+
 
 -- properties of booleans
 

full/src/TypeCheck.hs

@@ -36,6 +36,7 @@ checkType tm ty = do
   void $ tcTerm tm (Just nf)
 
 
+
 -- | Make sure that the term is a "type" (i.e. that it has type 'Type')
 tcType :: Term -> TcMonad ()
 tcType tm = void $ Env.withStage Irr $ checkType tm Type
@@ -289,18 +290,17 @@ tcTerm t@(Prod a b) (Just ty) = do
 
 
 tcTerm t@(LetPair p bnd) (Just ty) = do
+  ((x, y), body) <- Unbound.unbind bnd
   pty <- inferType p
   pty' <- Equal.whnf pty
   case pty' of
     Sigma tyA bnd' -> do
-      (x, tyB) <- Unbound.unbind bnd'
-      ((x', y'), body) <- Unbound.unbind bnd
-      let tyB' = Unbound.subst x (Var x') tyB
-      decl <- def p (Prod (Var x') (Var y'))
-      Env.extendCtxs ([mkSig x' tyA, mkSig y' tyB'] ++ decl) $
+      let tyB = Unbound.instantiate bnd' [Var x]
+      decl <- def p (Prod (Var x) (Var y))
+      Env.extendCtxs ([mkSig x tyA, mkSig y tyB] ++ decl) $
           checkType body ty
       return ty
-    _ -> Env.err [DS "Scrutinee of pcase must have Sigma type"]
+    _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"]
 
 
 tcTerm PrintMe (Just ty) = do

main/pi/Hw2.pi

@@ -1,11 +1,45 @@
 module Hw2 where
 
--- show that propositional equality is transitive 
+-- First: read section 7.2 of the lecture notes about how 
+-- propositional equality works in pi-forall. The key points are
+-- that `Refl` is a proof of the identity type `(a = b)` when 
+-- a is definitionally equal to b, and that `subst` is the elimination
+-- form.
+
+-- For example, we can show that equality is symmetric by 
+-- eliminating pf (of type `x = y`) when type checking 
+-- `Refl` against type `y = x`.  The `subst` adds the definition 
+-- `x = y` to the context, so both sides of `y = x` wh normalize to y. 
+
+sym : (A:Type) -> (x:A) -> (y:A) -> (x = y) -> y = x
+sym = \ A x y pf .
+  subst Refl by pf 
+
+-- Homework: show that propositional equality is transitive 
 
 trans : (A:Type) -> (x:A) -> (y:A) -> (z:A) -> (x = z) -> (z = y) -> (x = y)
 trans = {- SOLN DATA -} \A x y z pf1 pf2 . 
   subst pf1 by pf2 {- STUBWITH TRUSTME -}
 
+-- Homework: show that it is congruent for (nondependent) application
+
+f_cong : (A:Type) -> (B : Type) -> (f : A -> B) -> (g : A -> B)
+       -> (x:A) -> (y:A) 
+       -> (f = g) -> (x = y) -> (f x = g y)
+f_cong = {- SOLN DATA -} \ A B f g x y pf1 pf2 . 
+   subst (subst Refl by pf1) by pf2 {- STUBWITH TRUSTME -}
+
+-- Homework: what does congruence for dependent application look like?
+-- In other words, what if f and g above have a dependent type?
+
+{- SOLN DATA -}
+f_cong_dep : (A:Type) -> (B : A -> Type) 
+       -> (f : (x:A) -> B x) -> (g : (x:A) -> B x)
+       -> (x:A) -> (y:A) 
+       -> (f = g) -> (p : x = y) -> (f x = subst g y by p)
+f_cong_dep =  \ A B f g x y pf1 pf2 . 
+   subst (subst Refl by pf1) by pf2 {- STUBWITH -}
+
 
 -- properties of booleans
 

main/src/TypeCheck.hs

@@ -38,6 +38,7 @@ checkType tm ty = {- SOLN EQUAL -} do
   void $ tcTerm tm (Just nf)
 {- STUBWITH void $ tcTerm tm (Just ty) -}
 
+
 -- | Make sure that the term is a "type" (i.e. that it has type 'Type')
 tcType :: Term -> TcMonad ()
 tcType tm = void $ {- SOLN EP -} Env.withStage Irr $ {- STUBWITH -}checkType tm Type
@@ -309,18 +310,17 @@ tcTerm t@(Prod a b) (Just ty) = {- SOLN EQUAL -} do
 {- STUBWITH Env.err [DS "unimplemented"] -}
 
 tcTerm t@(LetPair p bnd) (Just ty) = {- SOLN EQUAL -} do
+  ((x, y), body) <- Unbound.unbind bnd
   pty <- inferType p
   pty' <- Equal.whnf pty
   case pty' of
     Sigma tyA bnd' -> do
-      (x, tyB) <- Unbound.unbind bnd'
-      ((x', y'), body) <- Unbound.unbind bnd
-      let tyB' = Unbound.subst x (Var x') tyB
-      decl <- def p (Prod (Var x') (Var y'))
-      Env.extendCtxs ([mkSig x' tyA, mkSig y' tyB'] ++ decl) $
+      let tyB = Unbound.instantiate bnd' [Var x]
+      decl <- def p (Prod (Var x) (Var y))
+      Env.extendCtxs ([mkSig x tyA, mkSig y tyB] ++ decl) $
           checkType body ty
       return ty
-    _ -> Env.err [DS "Scrutinee of pcase must have Sigma type"]
+    _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"]
 {- STUBWITH Env.err [DS "unimplemented"] -}
 
 tcTerm PrintMe (Just ty) = do

version2/pi/Hw2.pi

@@ -1,10 +1,37 @@
 module Hw2 where
 
--- show that propositional equality is transitive 
+-- First: read section 7.2 of the lecture notes about how 
+-- propositional equality works in pi-forall. The key points are
+-- that `Refl` is a proof of the identity type `(a = b)` when 
+-- a is definitionally equal to b, and that `subst` is the elimination
+-- form.
+
+-- For example, we can show that equality is symmetric by 
+-- eliminating pf (of type `x = y`) when type checking 
+-- `Refl` against type `y = x`.  The `subst` adds the definition 
+-- `x = y` to the context, so both sides of `y = x` wh normalize to y. 
+
+sym : (A:Type) -> (x:A) -> (y:A) -> (x = y) -> y = x
+sym = \ A x y pf .
+  subst Refl by pf 
+
+-- Homework: show that propositional equality is transitive 
 
 trans : (A:Type) -> (x:A) -> (y:A) -> (z:A) -> (x = z) -> (z = y) -> (x = y)
 trans = TRUSTME
 
+-- Homework: show that it is congruent for (nondependent) application
+
+f_cong : (A:Type) -> (B : Type) -> (f : A -> B) -> (g : A -> B)
+       -> (x:A) -> (y:A) 
+       -> (f = g) -> (x = y) -> (f x = g y)
+f_cong = TRUSTME
+
+-- Homework: what does congruence for dependent application look like?
+-- In other words, what if f and g above have a dependent type?
+
+
+
 
 -- properties of booleans
 

version2/src/TypeCheck.hs

@@ -34,6 +34,7 @@ checkType tm ty = do
   void $ tcTerm tm (Just nf)
 
 
+
 -- | Make sure that the term is a "type" (i.e. that it has type 'Type')
 tcType :: Term -> TcMonad ()
 tcType tm = void $ checkType tm Type
@@ -186,18 +187,17 @@ tcTerm t@(Prod a b) (Just ty) = do
 
 
 tcTerm t@(LetPair p bnd) (Just ty) = do
+  ((x, y), body) <- Unbound.unbind bnd
   pty <- inferType p
   pty' <- Equal.whnf pty
   case pty' of
     Sigma tyA bnd' -> do
-      (x, tyB) <- Unbound.unbind bnd'
-      ((x', y'), body) <- Unbound.unbind bnd
-      let tyB' = Unbound.subst x (Var x') tyB
-      decl <- def p (Prod (Var x') (Var y'))
-      Env.extendCtxs ([mkSig x' tyA, mkSig y' tyB'] ++ decl) $
+      let tyB = Unbound.instantiate bnd' [Var x]
+      decl <- def p (Prod (Var x) (Var y))
+      Env.extendCtxs ([mkSig x tyA, mkSig y tyB] ++ decl) $
           checkType body ty
       return ty
-    _ -> Env.err [DS "Scrutinee of pcase must have Sigma type"]
+    _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"]
 
 
 tcTerm PrintMe (Just ty) = do

version3/pi/Hw2.pi

@@ -1,10 +1,37 @@
 module Hw2 where
 
--- show that propositional equality is transitive 
+-- First: read section 7.2 of the lecture notes about how 
+-- propositional equality works in pi-forall. The key points are
+-- that `Refl` is a proof of the identity type `(a = b)` when 
+-- a is definitionally equal to b, and that `subst` is the elimination
+-- form.
+
+-- For example, we can show that equality is symmetric by 
+-- eliminating pf (of type `x = y`) when type checking 
+-- `Refl` against type `y = x`.  The `subst` adds the definition 
+-- `x = y` to the context, so both sides of `y = x` wh normalize to y. 
+
+sym : (A:Type) -> (x:A) -> (y:A) -> (x = y) -> y = x
+sym = \ A x y pf .
+  subst Refl by pf 
+
+-- Homework: show that propositional equality is transitive 
 
 trans : (A:Type) -> (x:A) -> (y:A) -> (z:A) -> (x = z) -> (z = y) -> (x = y)
 trans = TRUSTME
 
+-- Homework: show that it is congruent for (nondependent) application
+
+f_cong : (A:Type) -> (B : Type) -> (f : A -> B) -> (g : A -> B)
+       -> (x:A) -> (y:A) 
+       -> (f = g) -> (x = y) -> (f x = g y)
+f_cong = TRUSTME
+
+-- Homework: what does congruence for dependent application look like?
+-- In other words, what if f and g above have a dependent type?
+
+
+
 
 -- properties of booleans
 

version3/src/TypeCheck.hs

@@ -34,6 +34,7 @@ checkType tm ty = do
   void $ tcTerm tm (Just nf)
 
 
+
 -- | Make sure that the term is a "type" (i.e. that it has type 'Type')
 tcType :: Term -> TcMonad ()
 tcType tm = void $ Env.withStage Irr $ checkType tm Type
@@ -195,18 +196,17 @@ tcTerm t@(Prod a b) (Just ty) = do
 
 
 tcTerm t@(LetPair p bnd) (Just ty) = do
+  ((x, y), body) <- Unbound.unbind bnd
   pty <- inferType p
   pty' <- Equal.whnf pty
   case pty' of
     Sigma tyA bnd' -> do
-      (x, tyB) <- Unbound.unbind bnd'
-      ((x', y'), body) <- Unbound.unbind bnd
-      let tyB' = Unbound.subst x (Var x') tyB
-      decl <- def p (Prod (Var x') (Var y'))
-      Env.extendCtxs ([mkSig x' tyA, mkSig y' tyB'] ++ decl) $
+      let tyB = Unbound.instantiate bnd' [Var x]
+      decl <- def p (Prod (Var x) (Var y))
+      Env.extendCtxs ([mkSig x tyA, mkSig y tyB] ++ decl) $
           checkType body ty
       return ty
-    _ -> Env.err [DS "Scrutinee of pcase must have Sigma type"]
+    _ -> Env.err [DS "Scrutinee of LetPair must have Sigma type"]
 
 
 tcTerm PrintMe (Just ty) = do