b87be34 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some minor shuffling of proofs to make it easier to see what has been proved.

b87be34Dominic Mulligan15 years ago

lib/prelude/list.idr+26−25

compare with master

unifiedsplit

@@ -460,6 +460,30 @@ instance Ord a => Ord (List a) where

460-- Properties

461--------------------------------------------------------------------------------

462

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

463mapPreservesLength : (f : a -> b) -> (l : List a) ->

487mapPreservesLength : (f : a -> b) -> (l : List a) ->

464 length (map f l) = length l

488 length (map f l) = length l

465mapPreservesLength f [] = refl

489mapPreservesLength f [] = refl

@@ -481,20 +505,7 @@ mapFusion f g (x::xs) =

481 let inductiveHypothesis = mapFusion f g xs in

505 let inductiveHypothesis = mapFusion f g xs in

482 ?mapFusionStepCase

506 ?mapFusionStepCase

483

507

484−appendNilRightNeutral : (l : List a) ->

508+-- hasAny

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−

498hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->

509hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->

499 hasAnyBy p [] l = False

510 hasAnyBy p [] l = False

500hasAnyByNilFalse p [] = refl

511hasAnyByNilFalse p [] = refl

@@ -502,16 +513,9 @@ hasAnyByNilFalse p (x::xs) =

502 let inductiveHypothesis = hasAnyByNilFalse p xs in

513 let inductiveHypothesis = hasAnyByNilFalse p xs in

503 ?hasAnyByNilFalseStepCase

514 ?hasAnyByNilFalseStepCase

504

515

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−

512hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False

516hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False

513hasAnyNilFalse l = ?hasAnyNilFalseBody

517hasAnyNilFalse l = ?hasAnyNilFalseBody

514−

518+

515--------------------------------------------------------------------------------

519--------------------------------------------------------------------------------

516-- Proofs

520-- Proofs

517--------------------------------------------------------------------------------

521--------------------------------------------------------------------------------

@@ -580,9 +584,6 @@ prelude.list.zipWithTailProof = proof {

580 trivial;

584 trivial;

581}

585}

582

586

583−

584−---------- Proofs ----------

585−

586prelude.list.zipWith3TailProof = proof {

587prelude.list.zipWith3TailProof = proof {

587 intros;

588 intros;

588 rewrite (succInjective (length xs) (length ys) p);

589 rewrite (succInjective (length xs) (length ys) p);