idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-03 20:42:13 +03:00
Code Issues Projects Releases Wiki Activity

Add proof that list reverse is involutory.

Browse Source
This commit is contained in:
Mathew Polzin 2020-12-28 17:30:24 -08:00
parent 0eef8e58f9
commit bc76809288
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/base/Data/List.idr
View File

@ -670,6 +670,14 @@ revAppend (v :: vs) ns
rewrite appendAssociative (reverse ns) (reverse vs) [v] in
Refl
||| List reverse applied twice yields the identity function.
export
reverseInvolutory : (xs : List a) -> reverse (reverse xs) = xs
reverseInvolutory [] = Refl
reverseInvolutory (x :: xs) = rewrite revOnto [x] xs in
rewrite sym (revAppend (reverse xs) [x]) in
cong (x ::) $ reverseInvolutory xs
export
dropFusion : (n, m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n+m) l
dropFusion Z m l = Refl