@@ -284,7 +284,7 @@ zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
284284zipWith f [] (y::ys) Refl impossible
285285zipWith f (x::xs) [] Refl impossible
286286zipWith f [] [] p = []
287−zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
287+zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys (succInjective _ _ p))
288288
289289||| Combine three lists of the same length elementwise using some function.
290290||| @ f the function to combine elements with
@@ -301,7 +301,7 @@ zipWith3 f [] (y::ys) _ Refl q impossible
301301zipWith3 f (x::xs) [] _ Refl q impossible
302302zipWith3 f [] [] [] p q = []
303303zipWith3 f (x::xs) (y::ys) (z::zs) p q =
304− f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
304+ f x y z :: (zipWith3 f xs ys zs (succInjective _ _ p) (succInjective _ _ q))
305305
306306||| Combine two lists elementwise into pairs
307307zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
@@ -785,7 +785,7 @@ appendNilRightNeutral : (l : List a) ->
785785appendNilRightNeutral [] = Refl
786786appendNilRightNeutral (x::xs) =
787787 let inductiveHypothesis = appendNilRightNeutral xs in
788− ?appendNilRightNeutralStepCase
788+ rewrite inductiveHypothesis in Refl
789789
790790||| Appending lists is associative.
791791appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
@@ -793,7 +793,7 @@ appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
793793appendAssociative [] c r = Refl
794794appendAssociative (x::xs) c r =
795795 let inductiveHypothesis = appendAssociative xs c r in
796− ?appendAssociativeStepCase
796+ rewrite inductiveHypothesis in Refl
797797
798798||| The length of two lists that are appended is the sum of the lengths
799799||| of the input lists.
@@ -802,7 +802,7 @@ lengthAppend : (left : List a) -> (right : List a) ->
802802lengthAppend [] right = Refl
803803lengthAppend (x::xs) right =
804804 let inductiveHypothesis = lengthAppend xs right in
805− ?lengthAppendStepCase
805+ rewrite inductiveHypothesis in Refl
806806
807807||| Mapping a function over a list doesn't change its length.
808808mapPreservesLength : (f : a -> b) -> (l : List a) ->
@@ -810,7 +810,7 @@ mapPreservesLength : (f : a -> b) -> (l : List a) ->
810810mapPreservesLength f [] = Refl
811811mapPreservesLength f (x::xs) =
812812 let inductiveHypothesis = mapPreservesLength f xs in
813− ?mapPreservesLengthStepCase
813+ rewrite inductiveHypothesis in Refl
814814
815815||| Mapping a function over two lists and appending them is equivalent
816816||| to appending them and then mapping the function.
@@ -819,7 +819,7 @@ mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
819819mapDistributesOverAppend f [] r = Refl
820820mapDistributesOverAppend f (x::xs) r =
821821 let inductiveHypothesis = mapDistributesOverAppend f xs r in
822− ?mapDistributesOverAppendStepCase
822+ rewrite inductiveHypothesis in Refl
823823
824824||| Mapping two functions is the same as mapping their composition.
825825mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
@@ -827,7 +827,7 @@ mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
827827mapFusion f g [] = Refl
828828mapFusion f g (x::xs) =
829829 let inductiveHypothesis = mapFusion f g xs in
830− ?mapFusionStepCase
830+ rewrite inductiveHypothesis in Refl
831831
832832||| No list contains an element of the empty list by any predicate.
833833hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
@@ -835,11 +835,11 @@ hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
835835hasAnyByNilFalse p [] = Refl
836836hasAnyByNilFalse p (x::xs) =
837837 let inductiveHypothesis = hasAnyByNilFalse p xs in
838− ?hasAnyByNilFalseStepCase
838+ rewrite inductiveHypothesis in Refl
839839
840840||| No list contains an element of the empty list.
841841hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
842−hasAnyNilFalse l = ?hasAnyNilFalseBody
842+hasAnyNilFalse l = rewrite (hasAnyByNilFalse (==) l) in Refl
843843
844844foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
845845foldlAsFoldr f z t = foldr (flip (.) . flip f) id t z
@@ -850,74 +850,3 @@ foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q x
850850foldlMatchesFoldr f q [] = Refl
851851foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
852852
853−
854−--------------------------------------------------------------------------------
855−-- Proofs
856−--------------------------------------------------------------------------------
857−
858−lengthAppendStepCase = proof {
859− intros;
860− rewrite inductiveHypothesis;
861− trivial;
862−}
863−
864−hasAnyNilFalseBody = proof {
865− intros;
866− rewrite (hasAnyByNilFalse (==) l);
867− trivial;
868−}
869−
870−hasAnyByNilFalseStepCase = proof {
871− intros;
872− rewrite inductiveHypothesis;
873− trivial;
874−}
875−
876−appendNilRightNeutralStepCase = proof {
877− intros;
878− rewrite inductiveHypothesis;
879− trivial;
880−}
881−
882−appendAssociativeStepCase = proof {
883− intros;
884− rewrite inductiveHypothesis;
885− trivial;
886−}
887−
888−mapFusionStepCase = proof {
889− intros;
890− rewrite inductiveHypothesis;
891− trivial;
892−}
893−
894−mapDistributesOverAppendStepCase = proof {
895− intros;
896− rewrite inductiveHypothesis;
897− trivial;
898−}
899−
900−mapPreservesLengthStepCase = proof {
901− intros;
902− rewrite inductiveHypothesis;
903− trivial;
904−}
905−
906−zipWithTailProof = proof {
907− intros;
908− rewrite (succInjective (length xs) (length ys) p);
909− trivial;
910−}
911−
912−zipWith3TailProof = proof {
913− intros;
914− rewrite (succInjective (length xs) (length ys) p);
915− trivial;
916−}
917−
918−zipWith3TailProof' = proof {
919− intros;
920− rewrite (succInjective (length ys) (length zs) q);
921− trivial;
922−}
923−