-------------------------------------------------------------------------------------------------------------- [MGS 07 : Dependently typed programming (DTP)! !3rd lecture ! ! ! !Thorsten Altenkirch ] -------------------------------------------------------------------------------------------------------------- [Insert Nat, Bool] -------------------------------------------------------------------------------------------------------------- ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) -------------------------------------------------------------------------------------------------------------- let (-----------! ! one : Nat ) one => suc zero -------------------------------------------------------------------------------------------------------------- let (-----------! ! two : Nat ) two => suc one -------------------------------------------------------------------------------------------------------------- let (-------------! ! three : Nat ) three => suc two -------------------------------------------------------------------------------------------------------------- ( m, n : Nat ! let !---------------! ! add m n : Nat ) add m n <= rec m { add m n <= case m { add zero n => n add (suc m) n => suc (add m n) } } -------------------------------------------------------------------------------------------------------------- data (----------! where (-------------! ; (--------------! ! Bool : * ) ! true : Bool ) ! false : Bool ) -------------------------------------------------------------------------------------------------------------- [define propositional connectives ala BHK] -------------------------------------------------------------------------------------------------------------- ( A, B : * ! ( a : A ; b : B ! data !-------------! where !--------------------! ! And A B : * ) ! pair a b : And A B ) -------------------------------------------------------------------------------------------------------------- ( A, B : * ! ( a : A ! ( b : B ! data !------------! where !-----------------! ; !------------------! ! Or A B : * ) ! left a : Or A B ) ! right b : Or A B ) -------------------------------------------------------------------------------------------------------------- ( p : And A (Or B C) ! let !--------------------------------! ! lem p : Or (And A B) (And A C) ) lem p <= case p { lem (pair a b) <= case b { lem (pair a' (left a)) => left (pair a' a) lem (pair a (right b)) => right (pair a b) } } -------------------------------------------------------------------------------------------------------------- data (-----------! where ! False : * ) -------------------------------------------------------------------------------------------------------------- ( A : * ! let !-----------! ! Not A : * ) Not A => A -> False -------------------------------------------------------------------------------------------------------------- [What about de Morgan?] -------------------------------------------------------------------------------------------------------------- ( p : Not (Or A B) ! let !-----------------------------! ! dm1 p : And (Not A) (Not B) ) dm1 p => pair (lam a => p (left a)) (lam b => p (right b)) -------------------------------------------------------------------------------------------------------------- [Exercise: ! !There are for implications corresponding to the two de Morgan laws. One of them! !is unprovable constructively. Which one? Complete the other two. ] -------------------------------------------------------------------------------------------------------------- ( p : And (Not A) (Not B) ; q : Or A B ! let !---------------------------------------! ; dm2 p q [] ! dm2 p q : False ) -------------------------------------------------------------------------------------------------------------- ( p : Not (And A B) ! let !----------------------------! ! dm3 p : Or (Not A) (Not B) ) dm3 p [] -------------------------------------------------------------------------------------------------------------- ( p : Or (Not A) (Not B) ; q : And A B ! let !---------------------------------------! ; dm4 p q [] ! dm4 p q : False ) -------------------------------------------------------------------------------------------------------------- [Another constructively unprovable proposition: Excluded Middle] -------------------------------------------------------------------------------------------------------------- let (-------------------! ! EM : Or A (Not A) ) EM [] -------------------------------------------------------------------------------------------------------------- [However, we can define a "classical disjunction"] -------------------------------------------------------------------------------------------------------------- ( A, B : * ! let !-------------! ! COR A B : * ) COR A B => Not (And (Not A) (Not B)) -------------------------------------------------------------------------------------------------------------- [Exercise: Prove EM for classical disjunction.] -------------------------------------------------------------------------------------------------------------- let (---------------------! ; EMC [] ! EMC : COR A (Not A) ) -------------------------------------------------------------------------------------------------------------- [Using dependent types we can extend the BHK explanation to predicate logic with equality: ! !a proof of All a:A.P a is just a function assigning to any a:A a proof of P a. ! !We explain this by example: we prove that ! !All m,n:Nat . m+n = n+m ! !First we define equality ] -------------------------------------------------------------------------------------------------------------- ( a, b : A ! data !------------! where (---------------! ! Eq a b : * ) ! Refl : Eq a a ) -------------------------------------------------------------------------------------------------------------- [The constructor is the proof of reflexivity. To show that Eq is an equivalence relation! !we establish sym & trans ] -------------------------------------------------------------------------------------------------------------- ( p : Eq a b ! let !----------------! ! sym p : Eq b a ) sym p <= case p { sym Refl => Refl } -------------------------------------------------------------------------------------------------------------- ( p : Eq a b ; q : Eq b c ! let !--------------------------! ! trans p q : Eq a c ) trans p q <= case p { trans Refl q => q } -------------------------------------------------------------------------------------------------------------- [We can also show that a function respects equality] -------------------------------------------------------------------------------------------------------------- ( f : A -> B ; p : Eq _ A a b ! let !------------------------------! ! resp f p : Eq (f a) (f b) ) resp f p <= case p { resp f Refl => Refl } -------------------------------------------------------------------------------------------------------------- [Equality of equality proofs: there is only one] -------------------------------------------------------------------------------------------------------------- ( p, q : Eq a b ! let !-----------------------! ! eqUnique p q : Eq p q ) eqUnique p q <= case p { eqUnique Refl q <= case q { eqUnique Refl Refl => Refl } } -------------------------------------------------------------------------------------------------------------- [Now let's prove m+n=n+m] -------------------------------------------------------------------------------------------------------------- ( n : Nat ! let !----------------------------------! ! addComZero n : Eq n (add n zero) ) addComZero n <= rec n { addComZero n <= case n { addComZero zero => Refl addComZero (suc n) => resp suc (addComZero n) } } -------------------------------------------------------------------------------------------------------------- ( m, n : Nat ! let !-------------------------------------! ! addCom m n : Eq (add m n) (add n m) ) addCom m n <= rec m { addCom m n <= case m { addCom zero n => addComZero n addCom (suc m) n [] } } -------------------------------------------------------------------------------------------------------------- [Exercise: finish the proof] -------------------------------------------------------------------------------------------------------------- [Obs: addCom has no computational content, it will always return Refl] -------------------------------------------------------------------------------------------------------------- [Equality of natural numbers is decidable:] -------------------------------------------------------------------------------------------------------------- ( m, n : Nat ! let !---------------! ! eq m n : Bool ) eq m n <= rec m { eq m n <= case m { eq zero n <= case n { eq zero zero => true eq zero (suc n) => false } eq (suc m) n <= case n { eq (suc m) zero => false eq (suc m) (suc n) => eq m n } } } -------------------------------------------------------------------------------------------------------------- [the type of eq doesn't tell us much about the function,! !using dependent types we can do much better. ] -------------------------------------------------------------------------------------------------------------- ( p : Eq zero (suc n) ! let !---------------------! ! neqze p : False ) neqze p <= case p -------------------------------------------------------------------------------------------------------------- ( p : Eq (suc m) (suc n) ! let !------------------------! ! injSuc p : Eq m n ) injSuc p <= case p { injSuc Refl => Refl } -------------------------------------------------------------------------------------------------------------- ( p : Or (Eq m n) (Not (Eq m n)) ! let !--------------------------------------------------------------! ! eqSuc p : Or (Eq (suc m) (suc n)) (Not (Eq (suc m) (suc n))) ) eqSuc p <= case p { eqSuc (left a) <= case a { eqSuc (left Refl) => left Refl } eqSuc (right b) => right (lam q => b (injSuc [q])) } -------------------------------------------------------------------------------------------------------------- ( m, n : Nat ! let !--------------------------------------! ! eq' m n : Or (Eq m n) (Not (Eq m n)) ) eq' m n <= rec m { eq' m n <= case m { eq' zero n <= case n { eq' zero zero => left Refl eq' zero (suc n) => right neqze } eq' (suc m) n <= case n { eq' (suc m) zero => right (lam p => neqze (sym p)) eq' (suc m) (suc n) => eqSuc (eq' m n) } } } --------------------------------------------------------------------------------------------------------------