@@ -460,6 +460,30 @@ instance Ord a => Ord (List a) where
460460-- Properties
461461--------------------------------------------------------------------------------
462462
463+-- append
464+appendNilRightNeutral : (l : List a) ->
465+ l ++ [] = l
466+appendNilRightNeutral [] = refl
467+appendNilRightNeutral (x::xs) =
468+ let inductiveHypothesis = appendNilRightNeutral xs in
469+ ?appendNilRightNeutralStepCase
470+
471+appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
472+ (l ++ c) ++ r = l ++ (c ++ r)
473+appendAssociative [] c r = refl
474+appendAssociative (x::xs) c r =
475+ let inductiveHypothesis = appendAssociative xs c r in
476+ ?appendAssociativeStepCase
477+
478+-- length
479+lengthAppend : (left : List a) -> (right : List a) ->
480+ length (left ++ right) = length left + length right
481+lengthAppend [] right = refl
482+lengthAppend (x::xs) right =
483+ let inductiveHypothesis = lengthAppend xs right in
484+ ?lengthAppendStepCase
485+
486+-- map
463487mapPreservesLength : (f : a -> b) -> (l : List a) ->
464488 length (map f l) = length l
465489mapPreservesLength f [] = refl
@@ -481,20 +505,7 @@ mapFusion f g (x::xs) =
481505 let inductiveHypothesis = mapFusion f g xs in
482506 ?mapFusionStepCase
483507
484−appendNilRightNeutral : (l : List a) ->
485− l ++ [] = l
486−appendNilRightNeutral [] = refl
487−appendNilRightNeutral (x::xs) =
488− let inductiveHypothesis = appendNilRightNeutral xs in
489− ?appendNilRightNeutralStepCase
490−
491−appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
492− (l ++ c) ++ r = l ++ (c ++ r)
493−appendAssociative [] c r = refl
494−appendAssociative (x::xs) c r =
495− let inductiveHypothesis = appendAssociative xs c r in
496− ?appendAssociativeStepCase
497−
508+-- hasAny
498509hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
499510 hasAnyBy p [] l = False
500511hasAnyByNilFalse p [] = refl
@@ -502,16 +513,9 @@ hasAnyByNilFalse p (x::xs) =
502513 let inductiveHypothesis = hasAnyByNilFalse p xs in
503514 ?hasAnyByNilFalseStepCase
504515
505−lengthAppend : (left : List a) -> (right : List a) ->
506− length (left ++ right) = length left + length right
507−lengthAppend [] right = refl
508−lengthAppend (x::xs) right =
509− let inductiveHypothesis = lengthAppend xs right in
510− ?lengthAppendStepCase
511−
512516hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
513517hasAnyNilFalse l = ?hasAnyNilFalseBody
514−
518+
515519--------------------------------------------------------------------------------
516520-- Proofs
517521--------------------------------------------------------------------------------
@@ -580,9 +584,6 @@ prelude.list.zipWithTailProof = proof {
580584 trivial;
581585}
582586
583−
584−---------- Proofs ----------
585−
586587prelude.list.zipWith3TailProof = proof {
587588 intros;
588589 rewrite (succInjective (length xs) (length ys) p);